:: Article ARYTM_2, MML version 4.124.1059
:: ARYTM_2:funcnot 1
definition
  func DEDEKIND_CUTS -> Element of bool bool RAT+ equals
    {b<sub>1</sub> where b<sub>1</sub> is Element of bool RAT+: for b<sub>2</sub> being Element of RAT+ st b<sub>2</sub> in b<sub>1</sub>
       holds (for b<sub>3</sub> being Element of RAT+ st b<sub>3</sub> <=' b<sub>2</sub>
          holds b<sub>3</sub> in b<sub>1</sub>) & (ex b<sub>3</sub> being Element of RAT+ st b<sub>3</sub> in b<sub>1</sub> & <!--ANTONYM-->b<sub>2</sub> < b<sub>3</sub>)} \ {RAT+};
end;

:: ARYTM_2:def 1
theorem
DEDEKIND_CUTS = {B1 where B1 is Element of bool RAT+: for B2 being Element of RAT+
      st B2 in B1
   holds (for B3 being Element of RAT+
         st B3 <=' B2
      holds B3 in B1 & ex B3 being Element of RAT+ st
      (B3 in B1 & not (B3 <=' B2)))} \ {RAT+};

:: ARYTM_2:funcreg 1
registration
  cluster DEDEKIND_CUTS ->  non empty;
end;

:: ARYTM_2:funcnot 2
definition
  func REAL+ -> set equals
    (RAT+ \/ DEDEKIND_CUTS) \ {{b<sub>2</sub> where b<sub>2</sub> is Element of RAT+: <!--ANTONYM-->b<sub>2</sub> < b<sub>1</sub>} where b<sub>1</sub> is Element of RAT+: <!--ANTONYM-->b<sub>1</sub> <> {}};
end;

:: ARYTM_2:def 2
theorem
REAL+ = (RAT+ \/ DEDEKIND_CUTS) \ {{B2 where B2 is Element of RAT+: not (B1 <=' B2)} where B1 is Element of RAT+: not (B1 = {})};

:: ARYTM_2:th 1
theorem
RAT+ c= REAL+;

:: ARYTM_2:th 2
theorem
omega c= REAL+;

:: ARYTM_2:funcreg 2
registration
  cluster REAL+ ->  non empty;
end;

:: ARYTM_2:funcnot 3
definition
  let a<sub>1</sub> be Element of REAL+;
  func DEDEKIND_CUT A1 -> Element of DEDEKIND_CUTS means
    ex b<sub>1</sub> being Element of RAT+ st a<sub>1</sub> = b<sub>1</sub> & it = {b<sub>2</sub> where b<sub>2</sub> is Element of RAT+: <!--ANTONYM-->b<sub>2</sub> < b<sub>1</sub>}
    if a<sub>1</sub> in RAT+
    otherwise it = a<sub>1</sub>;
end;

:: ARYTM_2:def 3
theorem
for B1 being Element of REAL+
for B2 being Element of DEDEKIND_CUTS holds
   ((B1 in RAT+ implies    B2 = DEDEKIND_CUT B1
   iff
      ex B3 being Element of RAT+ st
         (B1 = B3 & B2 = {B4 where B4 is Element of RAT+: not (B3 <=' B4)})) & B1 in RAT+ or    B2 = DEDEKIND_CUT B1
   iff
      B2 = B1);

:: ARYTM_2:th 3
theorem
for B1 being set holds
   not ([{},B1] in REAL+);

:: ARYTM_2:funcnot 4
definition
  let a<sub>1</sub> be Element of DEDEKIND_CUTS;
  func GLUED A1 -> Element of REAL+ means
    ex b<sub>1</sub> being Element of RAT+ st it = b<sub>1</sub> & (for b<sub>2</sub> being Element of RAT+ holds
          b<sub>2</sub> in a<sub>1</sub> iff <!--ANTONYM-->b<sub>2</sub> < b<sub>1</sub>)
    if ex b<sub>1</sub> being Element of RAT+ st for b<sub>2</sub> being Element of RAT+ holds
          b<sub>2</sub> in a<sub>1</sub> iff <!--ANTONYM-->b<sub>2</sub> < b<sub>1</sub>
    otherwise it = a<sub>1</sub>;
end;

:: ARYTM_2:def 4
theorem
for B1 being Element of DEDEKIND_CUTS
for B2 being Element of REAL+ holds
   (for B3 being Element of RAT+ holds
      ex B4 being Element of RAT+ st
         (B4 in B1 & B3 <=' B4) or (not (B3 <=' B4) & not (B4 in B1)) or    B2 = GLUED B1
   iff
      ex B3 being Element of RAT+ st
         (B2 = B3 & for B4 being Element of RAT+ holds
               B4 in B1
            iff
               not (B3 <=' B4)) & (for B3 being Element of RAT+ holds
      ex B4 being Element of RAT+ st
         (B4 in B1 & B3 <=' B4) or (not (B3 <=' B4) & not (B4 in B1)) implies    B2 = GLUED B1
   iff
      B2 = B1));

:: ARYTM_2:prednot 1
definition
  let a<sub>1</sub>, a<sub>2</sub> be Element of REAL+;
  pred A1 <=' A2 means
    ex b<sub>1</sub>, b<sub>2</sub> being Element of RAT+ st a<sub>1</sub> = b<sub>1</sub> & a<sub>2</sub> = b<sub>2</sub> & b<sub>1</sub> <=' b<sub>2</sub>
    if a<sub>1</sub> in RAT+ & a<sub>2</sub> in RAT+,
a<sub>1</sub> in a<sub>2</sub>
    if a<sub>1</sub> in RAT+ & not a<sub>2</sub> in RAT+,
not a<sub>2</sub> in a<sub>1</sub>
    if not a<sub>1</sub> in RAT+ & a<sub>2</sub> in RAT+
    otherwise a<sub>1</sub> c= a<sub>2</sub>;
  connectedness;
    for a<sub>1</sub>, a<sub>2</sub> being Element of REAL+  holds
       a<sub>1</sub> <=' a<sub>2</sub> or a<sub>2</sub> <=' a<sub>1</sub>;
end;

:: ARYTM_2:dfs 5
definiens
  let A1 be Element of REAL+;
  let A2 be Element of REAL+;
To prove
     A1 <=' A2
it is sufficient to prove
  per cases;
  case (A1 in RAT+ & A2 in RAT+);
    thus ex B1 being Element of RAT+ st
       ex B2 being Element of RAT+ st
          (A1 = B1 & A2 = B2 & B1 <=' B2);
  end;
  case (A1 in RAT+ & not (A2 in RAT+));
    thus A1 in A2;
  end;
  case (not (A1 in RAT+) & A2 in RAT+);
    thus not (A2 in A1);
  end;
  case ((A1 in RAT+ implies not (A2 in RAT+)) & (A1 in RAT+ implies A2 in RAT+) & (not (A1 in RAT+) implies not (A2 in RAT+)));
    thus A1 c= A2;;
  end;

:: ARYTM_2:def 5
theorem
for B1, B2 being Element of REAL+ holds
(((B1 in RAT+ & B2 in RAT+) implies    B1 <=' B2
iff
   ex B3 being Element of RAT+ st
      ex B4 being Element of RAT+ st
         (B1 = B3 & B2 = B4 & B3 <=' B4)) & ((B1 in RAT+ & not (B2 in RAT+)) implies    B1 <=' B2
iff
   B1 in B2) & ((not (B1 in RAT+) & B2 in RAT+) implies    B1 <=' B2
iff
   not (B2 in B1)) & (((B1 in RAT+ implies not (B2 in RAT+)) & (B1 in RAT+ implies B2 in RAT+) & (not (B1 in RAT+) implies not (B2 in RAT+))) implies    B1 <=' B2
iff
   B1 c= B2));

:: ARYTM_2:prednot 2
notation
  let a<sub>1</sub>, a<sub>2</sub> be Element of REAL+;
  antonym a<sub>2</sub> < a<sub>1</sub> for a<sub>1</sub> <=' a<sub>2</sub>;
end;

:: ARYTM_2:funcnot 5
definition
  let a<sub>1</sub>, a<sub>2</sub> be Element of DEDEKIND_CUTS;
  func A1 + A2 -> Element of DEDEKIND_CUTS equals
    {b<sub>1</sub> + b<sub>2</sub> where b<sub>1</sub> is Element of RAT+, b<sub>2</sub> is Element of RAT+: b<sub>1</sub> in a<sub>1</sub> & b<sub>2</sub> in a<sub>2</sub>};
  commutativity;
    for a<sub>1</sub>, a<sub>2</sub> being Element of DEDEKIND_CUTS holds
    a<sub>1</sub> + a<sub>2</sub> = a<sub>2</sub> + a<sub>1</sub>;
end;

:: ARYTM_2:def 6
theorem
for B1, B2 being Element of DEDEKIND_CUTS holds
B1 + B2 = {B3 + B4 where B3 is Element of RAT+, B4 is Element of RAT+: (B3 in B1 & B4 in B2)};

:: ARYTM_2:funcnot 6
definition
  let a<sub>1</sub>, a<sub>2</sub> be Element of DEDEKIND_CUTS;
  func A1 *' A2 -> Element of DEDEKIND_CUTS equals
    {b<sub>1</sub> *' b<sub>2</sub> where b<sub>1</sub> is Element of RAT+, b<sub>2</sub> is Element of RAT+: b<sub>1</sub> in a<sub>1</sub> & b<sub>2</sub> in a<sub>2</sub>};
  commutativity;
    for a<sub>1</sub>, a<sub>2</sub> being Element of DEDEKIND_CUTS holds
    a<sub>1</sub> *' a<sub>2</sub> = a<sub>2</sub> *' a<sub>1</sub>;
end;

:: ARYTM_2:def 7
theorem
for B1, B2 being Element of DEDEKIND_CUTS holds
B1 *' B2 = {B3 *' B4 where B3 is Element of RAT+, B4 is Element of RAT+: (B3 in B1 & B4 in B2)};

:: ARYTM_2:funcnot 7
definition
  let a<sub>1</sub>, a<sub>2</sub> be Element of REAL+;
  func A1 + A2 -> Element of REAL+ equals
    a<sub>1</sub>
    if a<sub>2</sub> = {},
a<sub>2</sub>
    if a<sub>1</sub> = {}
    otherwise GLUED ((DEDEKIND_CUT a<sub>1</sub>) + DEDEKIND_CUT a<sub>2</sub>);
  commutativity;
    for a<sub>1</sub>, a<sub>2</sub> being Element of REAL+ holds
    a<sub>1</sub> + a<sub>2</sub> = a<sub>2</sub> + a<sub>1</sub>;
end;

:: ARYTM_2:def 8
theorem
for B1, B2 being Element of REAL+ holds
((B2 = {} implies B1 + B2 = B1) & (B1 = {} implies B1 + B2 = B2) & ((not (B2 = {}) & not (B1 = {})) implies B1 + B2 = GLUED ((DEDEKIND_CUT B1) + DEDEKIND_CUT B2)));

:: ARYTM_2:funcnot 8
definition
  let a<sub>1</sub>, a<sub>2</sub> be Element of REAL+;
  func A1 *' A2 -> Element of REAL+ equals
    GLUED ((DEDEKIND_CUT a<sub>1</sub>) *' DEDEKIND_CUT a<sub>2</sub>);
  commutativity;
    for a<sub>1</sub>, a<sub>2</sub> being Element of REAL+ holds
    a<sub>1</sub> *' a<sub>2</sub> = a<sub>2</sub> *' a<sub>1</sub>;
end;

:: ARYTM_2:def 9
theorem
for B1, B2 being Element of REAL+ holds
B1 *' B2 = GLUED ((DEDEKIND_CUT B1) *' DEDEKIND_CUT B2);

:: ARYTM_2:th 4
theorem
for B1, B2 being Element of REAL+ holds
(B1 = {} implies B1 *' B2 = {});

:: ARYTM_2:th 5
canceled;

:: ARYTM_2:th 6
theorem
for B1, B2 being Element of REAL+ holds
(B1 + B2 = {} implies B1 = {});

:: ARYTM_2:th 7
theorem
for B1, B2, B3 being Element of REAL+ holds
B1 + (B2 + B3) = (B1 + B2) + B3;

:: ARYTM_2:th 8
theorem
{B1 where B1 is Element of bool RAT+: for B2 being Element of RAT+
      st B2 in B1
   holds (for B3 being Element of RAT+
         st B3 <=' B2
      holds B3 in B1 & ex B3 being Element of RAT+ st
      (B3 in B1 & not (B3 <=' B2)))} is c=-linear;

:: ARYTM_2:th 9
theorem
for B1, B2 being Element of bool REAL+ holds
((ex B3 being Element of REAL+ st
   B3 in B1 & ex B3 being Element of REAL+ st
   B3 in B2 & for B3, B4 being Element of REAL+ holds
((B3 in B1 & B4 in B2) implies B3 <=' B4)) implies ex B3 being Element of REAL+ st
   for B4, B5 being Element of REAL+ holds
   ((B4 in B1 & B5 in B2) implies (B4 <=' B3 & B3 <=' B5)));

:: ARYTM_2:th 10
theorem
for B1, B2 being Element of REAL+ holds
(B1 <=' B2 implies ex B3 being Element of REAL+ st
   B1 + B3 = B2);

:: ARYTM_2:th 11
theorem
for B1, B2 being Element of REAL+ holds
ex B3 being Element of REAL+ st
   B1 + B3 = B2 or B2 + B3 = B1;

:: ARYTM_2:th 12
theorem
for B1, B2, B3 being Element of REAL+ holds
(B1 + B2 = B1 + B3 implies B2 = B3);

:: ARYTM_2:th 13
theorem
for B1, B2, B3 being Element of REAL+ holds
B1 *' (B2 *' B3) = (B1 *' B2) *' B3;

:: ARYTM_2:th 14
theorem
for B1, B2, B3 being Element of REAL+ holds
B1 *' (B2 + B3) = (B1 *' B2) + (B1 *' B3);

:: ARYTM_2:th 15
theorem
for B1 being Element of REAL+
      st not (B1 = {})
   holds ex B2 being Element of REAL+ st
      B1 *' B2 = one;

:: ARYTM_2:th 16
theorem
for B1, B2 being Element of REAL+ holds
(B1 = one implies B1 *' B2 = B2);

:: ARYTM_2:th 17
theorem
for B1, B2 being Element of REAL+ holds
((B1 in omega & B2 in omega) implies B2 + B1 in omega);

:: ARYTM_2:th 18
theorem
for B1 being Element of bool REAL+
      st ({} in B1 & for B2, B3 being Element of REAL+ holds
        ((B2 in B1 & B3 = one) implies B2 + B3 in B1))
   holds omega c= B1;

:: ARYTM_2:th 19
theorem
for B1 being Element of REAL+
   st B1 in omega
for B2 being Element of REAL+ holds
      B2 in B1
   iff
      (B2 in omega & not (B2 = B1) & B2 <=' B1);

:: ARYTM_2:th 20
theorem
for B1, B2, B3 being Element of REAL+ holds
(B1 = B2 + B3 implies B3 <=' B1);

:: ARYTM_2:th 21
theorem
({} in REAL+ & one in REAL+);

:: ARYTM_2:th 22
theorem
for B1, B2 being Element of REAL+ holds
((B1 in RAT+ & B2 in RAT+) implies ex B3 being Element of RAT+ st
   ex B4 being Element of RAT+ st
      (B1 = B3 & B2 = B4 & B1 *' B2 = B3 *' B4));