:: Arithmetic of Non Negative Rational Numbers :: by Grzegorz Bancerek :: :: Received March 7, 1998 :: Copyright (c) 1998-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDINAL1, XBOOLE_0, ORDINAL2, TARSKI, SUBSET_1, ORDINAL3, ARYTM_3, CARD_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3; constructors SUBSET_1, ORDINAL3; registrations XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, ORDINAL3; requirements BOOLE, SUBSET, NUMERALS; definitions TARSKI, ORDINAL1; equalities TARSKI, ORDINAL1; expansions TARSKI; theorems TARSKI, XBOOLE_0, ORDINAL1, ORDINAL2, ORDINAL3, XBOOLE_1, XTUPLE_0; schemes ORDINAL1; begin :: Natural ordinals reserve A,B,C for Ordinal; Lm1: {} in omega by ORDINAL1:def 11; Lm2: 1 in omega; definition func one -> set equals 1; correctness; end; begin :: Relative prime numbers and divisibility definition let a,b be Ordinal; pred a,b are_coprime means for c,d1,d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds c = 1; symmetry; end; theorem not {},{} are_coprime proof take {}, {}, {}; thus thesis by ORDINAL2:35; end; theorem Th2: 1,A are_coprime by ORDINAL3:37; theorem Th3: {},A are_coprime implies A = 1 proof A1: {} = A*^{} & A = A*^1 by ORDINAL2:38,39; assume {},A are_coprime & A <> 1; hence contradiction by A1; end; reserve a,b,c,d for natural Ordinal; defpred PP[set] means ex B st B c= \$1 & \$1 in omega & \$1 <> {} & not ex c,d1, d2 being natural Ordinal st d1,d2 are_coprime & \$1 = c *^ d1 & B = c *^ d2; theorem a <> {} or b <> {} implies ex c,d1,d2 being natural Ordinal st d1,d2 are_coprime & a = c *^ d1 & b = c *^ d2 proof assume that A1: a <> {} or b <> {} and A2: not ex c,d1,d2 being natural Ordinal st d1,d2 are_coprime & a = c *^ d1 & b = c *^ d2; A3: ex A st PP[A] proof per cases; suppose A4: a c= b; take A = b, B = a; thus B c= A & A in omega & A <> {} by A1,A4,ORDINAL1:def 12; thus thesis by A2; end; suppose A5: b c= a; take A = a, B = b; thus B c= A & A in omega & A <> {} by A1,A5,ORDINAL1:def 12; thus thesis by A2; end; end; consider A such that A6: PP[A] and A7: for C st PP[C] holds A c= C from ORDINAL1:sch 1(A3); consider B such that A8: B c= A and A9: A in omega and A10: A <> {} and A11: not ex c,d1,d2 being natural Ordinal st d1,d2 are_coprime & A = c *^ d1 & B = c *^ d2 by A6; reconsider A,B as Element of omega by A8,A9,ORDINAL1:12; A = 1 *^ A & B = 1 *^ B by ORDINAL2:39; then not A,B are_coprime by A11; then consider c,d1,d2 being Ordinal such that A12: A = c *^ d1 and A13: B = c *^ d2 and A14: c <> 1; A15: c <> {} by A10,A12,ORDINAL2:35; then A16: d1 c= A & d2 c= B by A12,A13,ORDINAL3:36; A17: d1 <> {} by A10,A12,ORDINAL2:38; then c c= A by A12,ORDINAL3:36; then reconsider c,d1,d2 as Element of omega by A16,ORDINAL1:12; 1 in c or c in 1 by A14,ORDINAL1:14; then 1*^d1 in A by A12,A17,A15,ORDINAL3:14,19; then A18: d1 in A by ORDINAL2:39; A19: now let c9,d19,d29 be natural Ordinal; assume that A20: d19,d29 are_coprime and A21: d1 = c9 *^ d19 & d2 = c9 *^ d29; A = c*^c9*^d19 & B = c*^c9*^d29 by A12,A13,A21,ORDINAL3:50; hence contradiction by A11,A20; end; A = d1*^c & B = d2*^c by A12,A13; then d2 c= d1 by A8,A15,ORDINAL3:35; hence contradiction by A7,A17,A19,A18,ORDINAL1:5; end; reserve l,m,n for natural Ordinal; registration let m,n; cluster m div^ n -> natural; coherence proof A1: n = {} implies m div^ n = {} & {}*^1 = {} by ORDINAL2:35,ORDINAL3:def 6; n in 1 or 1 c= n by ORDINAL1:16; then (m div^ n)*^1 c= (m div^ n)*^n by A1,ORDINAL3:14,20; then A2: m div^ n c= (m div^ n)*^n by ORDINAL2:39; (m div^ n)*^n c= m & m in omega by ORDINAL1:def 12,ORDINAL3:64; hence m div^ n in omega by A2,ORDINAL1:12,XBOOLE_1:1; end; cluster m mod^ n -> natural; coherence proof (m div^ n)*^n+^(m mod^ n) = m by ORDINAL3:65; then A3: m mod^ n c= m by ORDINAL3:24; m in omega by ORDINAL1:def 12; hence m mod^ n in omega by A3,ORDINAL1:12; end; end; definition let k,n be Ordinal; pred k divides n means ex a being Ordinal st n = k*^a; reflexivity proof let n be Ordinal; take 1; thus thesis by ORDINAL2:39; end; end; theorem Th5: a divides b iff ex c st b = a*^c proof thus a divides b implies ex c st b = a*^c proof given c being Ordinal such that A1: b = a*^c; per cases; suppose b = {}; then b = a*^{} by ORDINAL2:38; hence thesis; end; suppose b <> {}; then c is Element of omega by A1,ORDINAL3:75; hence thesis by A1; end; end; thus thesis; end; theorem Th6: for m,n st {} in m holds n mod^ m in m proof let m,n; assume {} in m; then A1: ex C st n = (n div^ m)*^m+^C & C in m by ORDINAL3:def 6; n mod^ m = n-^(n div^ m)*^m by ORDINAL3:def 7; hence thesis by A1,ORDINAL3:52; end; theorem Th7: for n,m holds m divides n iff n = m *^ (n div^ m) proof let n,m; assume A1: not thesis; then consider a such that A2: n = m*^a by Th5; {}*^a = {} by ORDINAL2:35; then {} <> m by A1,A2,ORDINAL2:35; then A3: {} in m by ORDINAL3:8; n = a*^m+^{} by A2,ORDINAL2:27; hence thesis by A1,A2,A3,ORDINAL3:def 6; end; theorem Th8: for n,m st n divides m & m divides n holds n = m proof let n,m; assume that A1: n divides m and A2: m divides n; A3: m = n *^ (m div^ n) by A1,Th7; A4: (m div^ n) *^ (n div^ m) = 1 implies n = m proof assume (m div^ n) *^ (n div^ m) = 1; then m div^ n = 1 by ORDINAL3:37; hence thesis by A3,ORDINAL2:39; end; n = m *^ (n div^ m) by A2,Th7; then A5: n *^ 1 = n & n = n *^ ((m div^ n) *^ (n div^ m)) by A3,ORDINAL2:39 ,ORDINAL3:50; n = {} implies n = m by A3,ORDINAL2:35; hence thesis by A5,A4,ORDINAL3:33; end; theorem Th9: n divides {} & 1 divides n proof {} = n *^ {} by ORDINAL2:35; hence n divides {}; n = 1 *^ n by ORDINAL2:39; hence thesis; end; theorem Th10: for n,m st {} in m & n divides m holds n c= m proof let n,m such that A1: {} in m; given a being Ordinal such that A2: m = n*^a; a <> {} by A1,A2,ORDINAL2:38; hence thesis by A2,ORDINAL3:36; end; theorem Th11: for n,m,l st n divides m & n divides m +^ l holds n divides l proof let n,m,l; assume n divides m; then consider a such that A1: m = n*^a by Th5; assume n divides m +^ l; then consider b such that A2: m +^ l = n*^b by Th5; assume A3: not n divides l; l = n*^b -^ n*^a by A1,A2,ORDINAL3:52 .= (b-^a)*^n by ORDINAL3:63; hence thesis by A3; end; Lm3: 1 = succ 0; definition let k,n be natural Ordinal; func k lcm n -> Element of omega means : Def4: k divides it & n divides it & for m st k divides m & n divides m holds it divides m; existence proof per cases; suppose A1: k = {} or n = {}; reconsider w = {} as Element of omega by ORDINAL1:def 12; take w; thus k divides w & n divides w by Th9; let m; assume k divides m & n divides m; hence thesis by A1; end; suppose A2: k <> {} & n <> {}; {} c= k; then {} c< k by A2,XBOOLE_0:def 8; then A3: {} in k by ORDINAL1:11; {} c= n; then {} c< n by A2,XBOOLE_0:def 8; then {} in n by ORDINAL1:11; then A4: 1 c= n by Lm3,ORDINAL1:21; defpred P[Ordinal] means ex m st \$1 = m & k divides m & n divides m & k c= m; A5: k*^1 = k by ORDINAL2:39; k divides k *^ n & n divides k *^ n; then A6: ex A st P[A] by A4,A5,ORDINAL2:41; consider A such that A7: P[A] and A8: for B st P[B] holds A c= B from ORDINAL1:sch 1(A6); consider l such that A9: A = l and A10: k divides l and A11: n divides l and A12: k c= l by A7; reconsider l as Element of omega by ORDINAL1:def 12; take l; thus k divides l & n divides l by A10,A11; let m such that A13: k divides m and A14: n divides m; A15: m = l*^(m div^ l)+^(m mod^ l) by ORDINAL3:65; l = k*^(l div^ k) by A10,Th7; then l*^(m div^ l) = k*^((l div^ k)*^(m div^ l)) by ORDINAL3:50; then k divides l*^(m div^ l); then A16: k divides m mod^ l by A13,A15,Th11; l = n*^(l div^ n) by A11,Th7; then l*^(m div^ l) = n*^((l div^ n)*^(m div^ l)) by ORDINAL3:50; then n divides l*^(m div^ l); then A17: n divides m mod^ l by A14,A15,Th11; now A18: {} c= m mod^ l; assume m mod^ l <> {}; then {} c< m mod^ l by A18,XBOOLE_0:def 8; then k c= m mod^ l by A16,Th10,ORDINAL1:11; then l c= m mod^ l by A8,A9,A16,A17; hence contradiction by A12,A3,Th6,ORDINAL1:5; end; then m = l*^(m div^ l) by A15,ORDINAL2:27; hence thesis; end; end; uniqueness proof let m1,m2 be Element of omega; assume k divides m1 & n divides m1 & ( for m st k divides m & n divides m holds m1 divides m)& k divides m2 &( n divides m2 & for m st k divides m & n divides m holds m2 divides m ); then m1 divides m2 & m2 divides m1; hence thesis by Th8; end; commutativity; end; theorem Th12: m lcm n divides m*^n proof m divides m*^n & n divides m*^n; hence thesis by Def4; end; theorem Th13: n <> {} implies (m*^n) div^ (m lcm n) divides m proof assume A1: n <> {}; take ((m lcm n) div^ n); n divides m lcm n by Def4; then A2: m lcm n = n*^((m lcm n) div^ n) by Th7; m lcm n divides m*^n by Th12; then m*^n = (m lcm n)*^ ((m*^n) div^ (m lcm n)) by Th7; then n*^m = n*^(((m lcm n) div^ n)*^ ((m*^n) div^ (m lcm n))) by A2, ORDINAL3:50; hence m = ((m*^n) div^ (m lcm n))*^((m lcm n) div^ n) by A1,ORDINAL3:33; end; definition let k,n be natural Ordinal; func k hcf n -> Element of omega means : Def5: it divides k & it divides n & for m st m divides k & m divides n holds m divides it; existence proof per cases; suppose A1: k = {} or n = {}; then reconsider m = k \/ n as Element of omega by ORDINAL1:def 12; take m; thus m divides k & m divides n by A1,Th9; thus thesis by A1; end; suppose A2: k <> {} & n <> {}; reconsider l = (k*^n) div^ (k lcm n) as Element of omega by ORDINAL1:def 12; take l; thus l divides k & l divides n by A2,Th13; let m; assume that A3: m divides k and A4: m divides n; A5: n = m*^(n div^ m) by A4,Th7; then A6: n div^ m <> {} by A2,ORDINAL2:35; m*^(k div^ m)*^(n div^ m) = n*^(k div^ m) by A5,ORDINAL3:50; then A7: n divides m*^(k div^ m)*^(n div^ m); set mm = m*^((k div^ m)*^(n div^ m)); A8: mm = m*^(k div^ m)*^(n div^ m) by ORDINAL3:50; A9: k = m*^(k div^ m) by A3,Th7; then k div^ m <> {} by A2,ORDINAL2:35; then A10: (k div^ m)*^(n div^ m) <> {} by A6,ORDINAL3:31; k divides m*^(k div^ m)*^(n div^ m) by A9; then k lcm n divides m*^(k div^ m)*^(n div^ m) by A7,Def4; then A11: mm = (k lcm n)*^(mm div^ (k lcm n)) by A8,Th7; m <> {} by A2,A9,ORDINAL2:35; then k lcm n <> {} by A11,A10,ORDINAL2:35,ORDINAL3:31; then A12: k*^n = k*^n+^{} & {} in k lcm n by ORDINAL2:27,ORDINAL3:8; mm*^m = (k lcm n)*^(m*^(mm div^ (k lcm n))) by A11,ORDINAL3:50; then k*^n = (k lcm n)*^(m*^(mm div^ (k lcm n))) by A9,A5,A8,ORDINAL3:50; then l = m*^(mm div^ (k lcm n)) by A12,ORDINAL3:66; hence thesis; end; end; uniqueness proof let m1,m2 be Element of omega; assume m1 divides k & m1 divides n & ( for m st m divides k & m divides n holds m divides m1)& m2 divides k &( m2 divides n & for m st m divides k & m divides n holds m divides m2 ); then m1 divides m2 & m2 divides m1; hence thesis by Th8; end; commutativity; end; theorem Th14: a hcf {} = a & a lcm {} = {} proof reconsider e = a, c = {} as Element of omega by ORDINAL1:def 12; A1: for b st a divides b & {} divides b holds c divides b; ( for n st n divides a & n divides {} holds n divides e)& a divides c by Th9; hence thesis by A1,Def4,Def5; end; theorem Th15: a hcf b = {} implies a = {} proof a hcf b divides a by Def5; then a = (a hcf b)*^(a div^ (a hcf b)) by Th7; hence thesis by ORDINAL2:35; end; theorem Th16: a hcf a = a & a lcm a = a proof reconsider c = a as Element of omega by ORDINAL1:def 12; for b st b divides a & b divides a holds b divides c; hence a hcf a = a by Def5; for b st a divides b & a divides b holds c divides b; hence thesis by Def4; end; theorem Th17: (a*^c) hcf (b*^c) = (a hcf b)*^c proof per cases; suppose A1: c = {}; then A2: (a hcf b)*^c = {} by ORDINAL2:35; a*^c = {} & b*^c = {} by A1,ORDINAL2:35; hence thesis by A2,Th16; end; suppose A3: c <> {} & a <> {}; reconsider d = (a hcf b)*^c as Element of omega by ORDINAL1:def 12; set e = ((a*^c) hcf (b*^c)) div^ d; a hcf b divides b by Def5; then b = (a hcf b)*^(b div^ (a hcf b)) by Th7; then b*^c = d*^(b div^ (a hcf b)) by ORDINAL3:50; then A4: d divides b*^c; a hcf b divides a by Def5; then a = (a hcf b)*^(a div^ (a hcf b)) by Th7; then a*^c = d*^(a div^ (a hcf b)) by ORDINAL3:50; then d divides a*^c; then d divides (a*^c) hcf (b*^c) by A4,Def5; then A5: (a*^c) hcf (b*^c) = d*^e by Th7 .= (a hcf b)*^e*^c by ORDINAL3:50; then (a hcf b)*^e*^c divides b*^c by Def5; then (a hcf b)*^e*^c*^((b*^c)div^((a hcf b)*^e*^c)) = b*^c by Th7; then (a hcf b)*^e*^((b*^c)div^((a hcf b)*^e*^c))*^c = b*^c by ORDINAL3:50; then (a hcf b)*^e*^((b*^c)div^((a hcf b)*^e*^c)) = b by A3,ORDINAL3:33; then A6: (a hcf b)*^e divides b; (a hcf b)*^e*^c divides a*^c by A5,Def5; then (a hcf b)*^e*^c*^((a*^c)div^((a hcf b)*^e*^c)) = a*^c by Th7; then (a hcf b)*^e*^((a*^c)div^((a hcf b)*^e*^c))*^c = a*^c by ORDINAL3:50; then (a hcf b)*^e*^((a*^c)div^((a hcf b)*^e*^c)) = a by A3,ORDINAL3:33; then (a hcf b)*^e divides a; then (a hcf b)*^e divides a hcf b by A6,Def5; then (a hcf b)*^e*^((a hcf b) div^ ((a hcf b)*^e)) = a hcf b by Th7; then (a hcf b)*^(e*^((a hcf b) div^ ((a hcf b)*^e))) = a hcf b by ORDINAL3:50 .= (a hcf b)*^1 by ORDINAL2:39; then a hcf b = {} or e*^((a hcf b) div^ ((a hcf b)*^e)) = 1 by ORDINAL3:33; then e = 1 by A3,Th15,ORDINAL3:37; hence thesis by A5,ORDINAL2:39; end; suppose a = {}; then a hcf b = b & a*^c = {} by Th14,ORDINAL2:35; hence thesis by Th14; end; end; theorem Th18: b <> {} implies a hcf b <> {} & b div^ (a hcf b) <> {} proof a hcf b divides b by Def5; then b = (a hcf b)*^(b div^ (a hcf b)) by Th7; hence thesis by ORDINAL2:35; end; theorem Th19: a <> {} or b <> {} implies a div^ (a hcf b), b div^ (a hcf b) are_coprime proof assume A1: a <> {} or b <> {}; set ab = a hcf b; A2: 1*^a = a & 1*^b = b by ORDINAL2:39; per cases; suppose a = {} or b = {}; then ab = b & b div^ b = 1 or ab = a & a div^ a = 1 by A1,A2,Th14, ORDINAL3:68; hence thesis by Th2; end; suppose A3: a <> {} & b <> {}; ab divides b by Def5; then A4: b = ab*^(b div^ ab) by Th7; then A5: b div^ ab <> {} by A3,ORDINAL2:35; let c,d1,d2 be Ordinal such that A6: a div^ (a hcf b) = c *^ d1 and A7: b div^ (a hcf b) = c *^ d2; ab divides a by Def5; then A8: a = ab*^(a div^ ab) by Th7; then a div^ ab <> {} by A3,ORDINAL2:35; then reconsider c,d1,d2 as Element of omega by A6,A7,A5,ORDINAL3:75; b = ab*^c*^d2 by A4,A7,ORDINAL3:50; then A9: ab*^c divides b; a = ab*^c*^d1 by A8,A6,ORDINAL3:50; then ab*^c divides a; then ab*^c divides ab by A9,Def5; then ab = (ab*^c)*^(ab div^ (ab*^c)) by Th7; then ab = ab*^(c*^(ab div^ (ab*^c))) by ORDINAL3:50; then A10: ab*^1 = ab*^(c*^(ab div^ (ab*^c))) by ORDINAL2:39; ab <> {} by A3,A8,ORDINAL2:35; then 1 = c*^(ab div^ (ab*^c)) by A10,ORDINAL3:33; hence thesis by ORDINAL3:37; end; end; Lm4: 0 = {}; theorem Th20: a,b are_coprime iff a hcf b = 1 proof a hcf b divides b by Def5; then A1: b = (a hcf b)*^(b div^ (a hcf b)) by Th7; a hcf b divides a by Def5; then a = (a hcf b)*^(a div^ (a hcf b)) by Th7; hence a,b are_coprime implies a hcf b = 1 by A1; assume A2: a hcf b = 1; let c,d1,d2 be Ordinal such that A3: a = c*^d1 & b = c*^d2; a <> {} or b <> {} by A2,Th14,Lm4; then reconsider c as Element of omega by A3,ORDINAL3:75; c divides a & c divides b by A3; then c divides 1 by A2,Def5; then ex d st 1 = c*^d by Th5; hence thesis by ORDINAL3:37; end; definition let a,b be natural Ordinal; func RED(a,b) -> Element of omega equals a div^ (a hcf b); coherence by ORDINAL1:def 12; end; theorem Th21: RED(a,b)*^(a hcf b) = a proof a hcf b divides a by Def5; hence thesis by Th7; end; theorem a <> {} or b <> {} implies RED(a,b), RED(b,a) are_coprime by Th19; theorem Th23: a,b are_coprime implies RED(a,b) = a proof assume a,b are_coprime; then a hcf b = 1 by Th20; hence thesis by ORDINAL3:71; end; theorem Th24: RED(a,1) = a & RED(1,a) = 1 proof a,1 are_coprime by Th2; then a hcf 1 = 1 by Th20; hence thesis by ORDINAL3:71; end; theorem b <> {} implies RED(b,a) <> {} by Th18; theorem Th26: RED({},a) = {} & (a <> {} implies RED(a,{}) = 1) proof thus RED({},a) = {} by ORDINAL3:70; assume A1: a <> {}; thus RED(a,{}) = a div^ a by Th14 .= a*^1 div^ a by ORDINAL2:39 .= 1 by A1,ORDINAL3:68; end; theorem Th27: a <> {} implies RED(a,a) = 1 proof assume A1: a <> {}; thus RED(a,a) = a div^ a by Th16 .= a*^1 div^ a by ORDINAL2:39 .= 1 by A1,ORDINAL3:68; end; theorem Th28: c <> {} implies RED(a*^c, b*^c) = RED(a, b) proof assume A1: c <> {}; a <> {} implies a hcf b <> {} by Th18; then A2: a <> {} implies (a hcf b)*^c <> {} by A1,ORDINAL3:31; A3: RED({},b) = {} & {}*^((a hcf b)*^c) = {} by ORDINAL2:35,ORDINAL3:70; A4: a hcf b divides a by Def5; thus RED(a*^c, b*^c) = (a*^c)div^((a hcf b)*^c) by Th17 .= (((a div^(a hcf b))*^(a hcf b))*^c)div^((a hcf b)*^c) by A4,Th7 .= (RED(a,b)*^((a hcf b)*^c))div^((a hcf b)*^c) by ORDINAL3:50 .= RED(a, b) by A2,A3,ORDINAL3:68,70; end; set RATplus = {[a,b] where a,b is Element of omega: a,b are_coprime & b <> {}}; 1,1 are_coprime by Th2; then [1,1] in RATplus by Lm4; then reconsider RATplus as non empty set; Lm5: [a,b] in RATplus implies a,b are_coprime & b <> {} proof assume [a,b] in RATplus; then consider c,d being Element of omega such that A1: [a,b] = [c,d] and A2: c,d are_coprime & d <> {}; a = c by A1,XTUPLE_0:1; hence thesis by A1,A2,XTUPLE_0:1; end; begin :: Non negative rationals reserve i,j,k for Element of omega; definition func RAT+ -> set equals ({[i,j]: i,j are_coprime & j <> {}} \ the set of all [k,1]) \/ omega; correctness; end; Lm6: omega c= RAT+ by XBOOLE_1:7; reserve x,y,z for Element of RAT+; registration cluster RAT+ -> non empty; coherence; end; registration cluster non empty ordinal for Element of RAT+; existence by Lm2,Lm6,Lm4; end; theorem Th29: x in omega or ex i,j st x = [i,j] & i,j are_coprime & j <> {} & j <> 1 proof assume not x in omega; then A1: x in RATplus \ the set of all [k,1] by XBOOLE_0:def 3; then A2: not x in the set of all [k,1] by XBOOLE_0:def 5; x in RATplus by A1; then consider a,b being Element of omega such that A3: x = [a,b] & a,b are_coprime & b <> {}; [a,1] in the set of all [k,1]; hence thesis by A2,A3; end; theorem Th30: not ex i,j being set st [i,j] is Ordinal proof given i,j being set such that A1: [i,j] is Ordinal; {} in {{i},{i,j}} by A1,ORDINAL3:8; hence thesis by TARSKI:def 2; end; theorem Th31: A in RAT+ implies A in omega proof assume A in RAT+ & not A in omega; then ex i,j st A = [i,j] & i,j are_coprime & j <> {} & j <> 1 by Th29; hence thesis by Th30; end; registration cluster -> natural for ordinal Element of RAT+; coherence proof let x be ordinal Element of RAT+; assume not x in omega; then A1: ex i,j st x = [i,j] & i,j are_coprime & j <> {} & j <> 1 by Th29; then {} in x by ORDINAL3:8; hence thesis by A1,TARSKI:def 2; end; end; theorem Th32: not ex i,j being object st [i,j] in omega proof given i,j being object such that A1: [i,j] in omega; reconsider a = [i,j] as Element of omega by A1; {} in a by ORDINAL3:8; hence thesis by TARSKI:def 2; end; theorem Th33: [i,j] in RAT+ iff i,j are_coprime & j <> {} & j <> 1 proof A1: not [i,j] in omega by Th32; hereby assume [i,j] in RAT+; then A2: [i,j] in RATplus \ the set of all [k,1] by A1,XBOOLE_0:def 3; hence i,j are_coprime & j <> {} by Lm5; not [i,j] in the set of all [k,1] by A2,XBOOLE_0:def 5; hence j <> 1; end; assume i,j are_coprime & j <> {}; then A3: [i,j] in RATplus; assume j <> 1; then not ex k st [i,j] = [k,1] by XTUPLE_0:1; then not [i,j] in the set of all [k,1]; then [i,j] in RATplus \ the set of all [k,1] by A3,XBOOLE_0:def 5; hence thesis by XBOOLE_0:def 3; end; definition let x be Element of RAT+; func numerator x -> Element of omega means :Def8: it = x if x in omega otherwise ex a st x = [it,a]; existence proof thus x in omega implies ex a being Element of omega st a = x; assume not x in omega; then x in RATplus \ the set of all [k,1] by XBOOLE_0:def 3; then x in RATplus; then consider a,b being Element of omega such that A1: x = [a,b] and a,b are_coprime and b <> {}; take a,b; thus thesis by A1; end; correctness by XTUPLE_0:1; func denominator x -> Element of omega means : Def9: it = 1 if x in omega otherwise ex a st x = [a,it]; existence proof thus x in omega implies ex a being Element of omega st a = 1; assume not x in omega; then x in RATplus \ the set of all [k,1] by XBOOLE_0:def 3; then x in RATplus; then consider a,b being Element of omega such that A2: x = [a,b] and a,b are_coprime and b <> {}; take b,a; thus thesis by A2; end; correctness by XTUPLE_0:1; end; theorem Th34: numerator x, denominator x are_coprime proof per cases; suppose x in omega; then denominator x = 1 by Def9; hence thesis by Th2; end; suppose A1: not x in omega; then consider i,j such that A2: x = [i,j] and A3: i,j are_coprime and j <> {} and j <> 1 by Th29; i = numerator x by A1,A2,Def8; hence thesis by A1,A2,A3,Def9; end; end; theorem Th35: denominator x <> {} proof per cases; suppose x in omega; hence thesis by Def9,Lm4; end; suppose A1: not x in omega; then ex i,j st x = [i,j] & i,j are_coprime & j <> {} & j <> 1 by Th29; hence thesis by A1,Def9; end; end; theorem Th36: not x in omega implies x = [numerator x, denominator x] & denominator x <> 1 proof assume A1: not x in omega; then consider i,j such that A2: x = [i,j] and i,j are_coprime and j <> {} and A3: j <> 1 by Th29; i = numerator x by A1,A2,Def8; hence thesis by A1,A2,A3,Def9; end; theorem Th37: x <> {} iff numerator x <> {} proof hereby assume that A1: x <> {} and A2: numerator x = {}; A3: not x in omega by A1,A2,Def8; then consider i,j such that A4: x = [i,j] and A5: i,j are_coprime and j <> {} and A6: j <> 1 by Th29; i = {} by A2,A3,A4,Def8; hence contradiction by A5,A6,Th3; end; {} in omega by ORDINAL1:def 11; hence thesis by Def8; end; theorem x in omega iff denominator x = 1 by Def9,Th36; definition let i,j be natural Ordinal; func i/j -> Element of RAT+ equals :Def10: {} if j = {}, RED(i,j) if RED(j,i ) = 1 otherwise [RED(i,j), RED(j,i)]; coherence proof A1: now assume j <> {}; then RED(i,j), RED(j,i) are_coprime & RED(j,i) <> {} by Th18,Th19; hence RED(j,i) <> 1 implies [RED(i,j), RED(j,i)] in RAT+ by Th33; end; thus thesis by A1,Lm1,Lm6; end; consistency by Th26,Lm4; end; notation let i,j be natural Ordinal; synonym quotient(i,j) for i/j; end; theorem Th39: (numerator x)/(denominator x) = x proof A1: denominator x <> {} by Th35; A2: RED(numerator x, denominator x) = numerator x by Th23,Th34; numerator x, denominator x are_coprime by Th34; then A3: RED(denominator x, numerator x) = denominator x by Th23; per cases; suppose A4: denominator x = 1; then x in omega by Th36; then numerator x = x by Def8; hence thesis by A2,A3,A4,Def10; end; suppose A5: denominator x <> 1; then not x in omega by Def9; then x = [numerator x, denominator x] by Th36; hence thesis by A1,A2,A3,A5,Def10; end; end; theorem Th40: {}/b = {} & a/1 = a proof A1: b <> {} implies RED(b,{}) = 1 by Th26; RED({},b) = {} by Th26; hence {}/b = {} by A1,Def10; RED(1,a) = 1 & RED(a,1) = a by Th24; hence thesis by Def10; end; theorem Th41: a <> {} implies a/a = 1 proof assume a <> {}; then RED(a,a) = 1 by Th27; hence thesis by Def10; end; theorem Th42: b <> {} implies numerator (a/b) = RED(a,b) & denominator (a/b) = RED(b,a) proof assume A1: b <> {}; per cases; suppose A2: RED(b,a) = 1; then a/b = RED(a,b) by Def10; hence thesis by A2,Def8,Def9; end; suppose A3: RED(b,a) <> 1; A4: not [RED(a,b), RED(b,a)] in omega by Th32; a/b = [RED(a,b), RED(b,a)] by A1,A3,Def10; hence thesis by A4,Def8,Def9; end; end; theorem Th43: i,j are_coprime & j <> {} implies numerator (i/j) = i & denominator (i/j) = j proof assume i,j are_coprime; then RED(i,j) = i & RED(j,i) = j by Th23; hence thesis by Th42; end; theorem Th44: c <> {} implies (a*^c)/(b*^c) = a/b proof assume A1: c <> {}; per cases; suppose b = {}; then a/b = {} & b*^c = {} by Def10,ORDINAL2:35; hence thesis by Def10; end; suppose A2: b <> {}; then A3: b*^c <> {} by A1,ORDINAL3:31; then A4: denominator ((a*^c)/(b*^c)) = RED(b*^c,a*^c) by Th42 .= RED(b,a) by A1,Th28 .= denominator (a/b) by A2,Th42; numerator ((a*^c)/(b*^c)) = RED(a*^c,b*^c) by A3,Th42 .= RED(a,b) by A1,Th28 .= numerator (a/b) by A2,Th42; hence (a*^c)/(b*^c) = (numerator (a/b))/denominator (a/b) by A4,Th39 .= a/b by Th39; end; end; reserve i,j,k for natural Ordinal; theorem Th45: j <> {} & l <> {} implies (i/j = k/l iff i*^l = j*^k) proof assume that A1: j <> {} and A2: l <> {}; set x = i/j, y = k/l; set ny = numerator y, dy = denominator y; A3: ny = RED(k,l) by A2,Th42; set nx = numerator x, dx = denominator x; A4: dx = RED(j,i) by A1,Th42; A5: dy = RED(l,k) by A2,Th42; A6: nx = RED(i,j) by A1,Th42; hereby assume i/j = k/l; then i = ny*^(i hcf j) & l = dx*^(l hcf k) by A6,A5,Th21; hence i*^l = ny*^(i hcf j)*^dx*^(l hcf k) by ORDINAL3:50 .= ny*^((i hcf j)*^dx)*^(l hcf k) by ORDINAL3:50 .= ny*^j*^(l hcf k) by A4,Th21 .= j*^(ny*^(l hcf k)) by ORDINAL3:50 .= j*^k by A3,Th21; end; assume A7: i*^l = j*^k; then dx = RED(j*^l,j*^k) by A2,A4,Th28; then A8: dx = dy by A1,A5,Th28; nx = RED(j*^k,j*^l) by A2,A6,A7,Th28; then nx = ny by A1,A3,Th28; then x = ny/dy by A8,Th39; hence thesis by Th39; end; definition let x,y be Element of RAT+; func x+y -> Element of RAT+ equals ((numerator x)*^(denominator y)+^( numerator y)*^(denominator x)) / ((denominator x)*^(denominator y)); coherence; commutativity; func x*'y -> Element of RAT+ equals ((numerator x)*^(numerator y)) / (( denominator x)*^(denominator y)); coherence; commutativity; end; theorem Th46: j <> {} & l <> {} implies (i/j)+(k/l) = (i*^l+^j*^k)/(j*^l) proof assume that A1: j <> {} and A2: l <> {}; A3: denominator (k/l) = RED(l,k) & denominator (i/j) = RED(j,i) by A1,A2,Th42; numerator (k/l) = RED(k,l) & numerator (i/j) = RED(i,j) by A1,A2,Th42; hence (i/j)+(k/l) = (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j) /(RED (j,i)*^RED(l,k)*^(i hcf j)) by A1,A3,Th15,Th44 .= (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j) /(RED(l,k)*^(RED( j,i)*^(i hcf j))) by ORDINAL3:50 .= (RED(i,j)*^RED(l,k)+^RED(j,i)*^RED(k,l))*^(i hcf j)/(RED(l,k)*^j) by Th21 .= (RED(i,j)*^RED(l,k)*^(i hcf j)+^RED(j,i)*^RED(k,l)*^(i hcf j)) /(RED( l,k)*^j) by ORDINAL3:46 .= (RED(l,k)*^(RED(i,j)*^(i hcf j))+^RED(j,i)*^RED(k,l)*^(i hcf j)) /( RED(l,k)*^j) by ORDINAL3:50 .= (RED(l,k)*^i+^RED(j,i)*^RED(k,l)*^(i hcf j))/(RED(l,k)*^j) by Th21 .= (RED(l,k)*^i+^RED(k,l)*^(RED(j,i)*^(i hcf j)))/(RED(l,k)*^j) by ORDINAL3:50 .= (RED(l,k)*^i+^RED(k,l)*^j)/(RED(l,k)*^j) by Th21 .= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(RED(l,k)*^j*^(k hcf l)) by A2 ,Th15,Th44 .= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(j*^(RED(l,k)*^(k hcf l))) by ORDINAL3:50 .= ((RED(l,k)*^i+^RED(k,l)*^j)*^(k hcf l))/(j*^l) by Th21 .= (RED(l,k)*^i*^(k hcf l)+^RED(k,l)*^j*^(k hcf l))/(j*^l) by ORDINAL3:46 .= (i*^(RED(l,k)*^(k hcf l))+^RED(k,l)*^j*^(k hcf l))/(j*^l) by ORDINAL3:50 .= (i*^l+^RED(k,l)*^j*^(k hcf l))/(j*^l) by Th21 .= (i*^l+^j*^(RED(k,l)*^(k hcf l)))/(j*^l) by ORDINAL3:50 .= (i*^l+^j*^k)/(j*^l) by Th21; end; theorem Th47: k <> {} implies (i/k)+(j/k) = (i+^j)/k proof assume A1: k <> {}; hence (i/k)+(j/k) = (i*^k+^j*^k)/(k*^k) by Th46 .= ((i+^j)*^k)/(k*^k) by ORDINAL3:46 .= (i+^j)/k by A1,Th44; end; registration cluster empty for Element of RAT+; existence by Lm1,Lm6; end; definition redefine func {} -> Element of RAT+; coherence by Lm1,Lm6; redefine func one -> non empty ordinal Element of RAT+; coherence by Lm6,Lm4; end; theorem Th48: x*'{} = {} proof numerator {} = {} & (numerator x)*^{} = {} by Def8,Lm1,ORDINAL2:35; hence thesis by Th40; end; theorem Th49: (i/j)*'(k/l) = (i*^k)/(j*^l) proof per cases; suppose A1: j <> {} & l <> {}; then A2: denominator (k/l) = RED(l,k) & denominator (i/j) = RED(j,i) by Th42; numerator (k/l) = RED(k,l) & numerator (i/j) = RED(i,j) by A1,Th42; hence (i/j)*'(k/l) = (RED(i,j)*^RED(k,l)*^(i hcf j))/(RED(j,i)*^RED(l,k)*^( i hcf j)) by A1,A2,Th15,Th44 .= (RED(k,l)*^(RED(i,j)*^(i hcf j)))/(RED(j,i)*^RED(l,k)*^(i hcf j)) by ORDINAL3:50 .= (RED(k,l)*^i)/(RED(j,i)*^RED(l,k)*^(i hcf j)) by Th21 .= (RED(k,l)*^i)/(RED(l,k)*^(RED(j,i)*^(i hcf j))) by ORDINAL3:50 .= (RED(k,l)*^i)/(RED(l,k)*^j) by Th21 .= (RED(k,l)*^i*^(l hcf k))/(RED(l,k)*^j*^(l hcf k)) by A1,Th15,Th44 .= (i*^(RED(k,l)*^(l hcf k)))/(RED(l,k)*^j*^(l hcf k)) by ORDINAL3:50 .= (i*^k)/(RED(l,k)*^j*^(l hcf k)) by Th21 .= (i*^k)/(j*^(RED(l,k)*^(l hcf k))) by ORDINAL3:50 .= (i*^k)/(j*^l) by Th21; end; suppose A3: j = {} or l = {}; then i/j = {} or k/l = {} by Def10; then A4: (i/j)*'(k/l) = {} by Th48; j*^l = {} by A3,ORDINAL2:35; hence thesis by A4,Def10; end; end; theorem Th50: x+{} = x proof A1: (numerator x)*^1 = numerator x & {}*^(denominator x) = {} by ORDINAL2:35,39 ; A2: (denominator x)*^1 = denominator x & (numerator x)+^{} = numerator x by ORDINAL2:27,39; denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1; hence thesis by A1,A2,Th39; end; theorem Th51: (x+y)+z = x+(y+z) proof set nx = numerator x, ny = numerator y, nz = numerator z; set dx = denominator x, dy = denominator y, dz = denominator z; A1: dy <> {} by Th35; A2: dz <> {} by Th35; then A3: dy*^dz <> {} by A1,ORDINAL3:31; A4: dx <> {} by Th35; then A5: dx*^dy <> {} by A1,ORDINAL3:31; thus x+y+z = (nx*^dy+^dx*^ny)/(dx*^dy)+nz/dz by Th39 .= ((nx*^dy+^dx*^ny)*^dz+^(dx*^dy)*^nz)/(dx*^dy*^dz) by A2,A5,Th46 .= (nx*^dy*^dz+^dx*^ny*^dz+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:46 .= (nx*^(dy*^dz)+^dx*^ny*^dz+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:50 .= (nx*^(dy*^dz)+^dx*^(ny*^dz)+^dx*^dy*^nz)/(dx*^dy*^dz) by ORDINAL3:50 .= (nx*^(dy*^dz)+^dx*^(ny*^dz)+^dx*^(dy*^nz))/(dx*^dy*^dz) by ORDINAL3:50 .= (nx*^(dy*^dz)+^(dx*^(ny*^dz)+^dx*^(dy*^nz)))/(dx*^dy*^dz) by ORDINAL3:30 .= (nx*^(dy*^dz)+^dx*^(ny*^dz+^dy*^nz))/(dx*^dy*^dz) by ORDINAL3:46 .= (nx*^(dy*^dz)+^dx*^(ny*^dz+^dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50 .= (ny*^dz+^dy*^nz)/(dy*^dz)+nx/dx by A4,A3,Th46 .= x+(y+z) by Th39; end; theorem Th52: (x*'y)*'z = x*'(y*'z) proof set nx = numerator x, ny = numerator y, nz = numerator z; set dx = denominator x, dy = denominator y, dz = denominator z; A1: x = nx/dx by Th39; z = nz/dz by Th39; hence (x*'y)*'z = (nx*^ny*^nz)/(dx*^dy*^dz) by Th49 .= (nx*^(ny*^nz))/(dx*^dy*^dz) by ORDINAL3:50 .= (nx*^(ny*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50 .= x*'(y*'z) by A1,Th49; end; theorem Th53: x*'one = x proof set y = one; A1: (numerator x)*^1 = numerator x & (denominator x)*^1 = denominator x by ORDINAL2:39; numerator y = 1 & denominator y = 1 by Def8,Def9; hence thesis by A1,Th39; end; theorem Th54: x <> {} implies ex y st x*'y = 1 proof set nx = numerator x, dx = denominator x; A1: dx <> {} by Th35; assume x <> {}; then A2: nx <> {} by Th37; take y = dx/nx; nx, dx are_coprime by Th34; then denominator y = nx & numerator y = dx by A2,Th43; hence thesis by A2,A1,Th41,ORDINAL3:31; end; theorem Th55: x <> {} implies ex z st y = x*'z proof reconsider o = one as Element of RAT+; assume x <> {}; then consider z such that A1: x*'z = 1 by Th54; take z*'y; thus y = y*'o by Th53 .= x*'(z*'y) by A1,Th52; end; theorem Th56: x <> {} & x*'y = x*'z implies y = z proof assume x <> {}; then consider r being Element of RAT+ such that A1: x*'r = 1 by Th54; r*'(x*'y) = one*'y by A1,Th52; then A2: r*'(x*'y) = y by Th53; r*'(x*'z) = one*'z by A1,Th52; hence thesis by A2,Th53; end; theorem Th57: x*'(y+z) = x*'y+x*'z proof set nx = numerator x, ny = numerator y, nz = numerator z; set dx = denominator x, dy = denominator y, dz = denominator z; A1: dx <> {} by Th35; dz <> {} by Th35; then A2: dx*^dz <> {} by A1,ORDINAL3:31; dy <> {} by Th35; then A3: dx*^dy <> {} by A1,ORDINAL3:31; x = nx/dx by Th39; hence x*'(y+z) = (nx*^(ny*^dz+^dy*^nz))/(dx*^(dy*^dz)) by Th49 .= (nx*^(ny*^dz)+^nx*^(dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:46 .= (nx*^ny*^dz+^nx*^(dy*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50 .= (nx*^ny*^dz+^dy*^(nx*^nz))/(dx*^(dy*^dz)) by ORDINAL3:50 .= (nx*^ny*^dz+^dy*^(nx*^nz))/(dy*^(dx*^dz)) by ORDINAL3:50 .= (dx*^((nx*^ny)*^dz+^(dy*^(nx*^nz))))/(dx*^(dy*^(dx*^dz))) by Th35,Th44 .= (dx*^((nx*^ny)*^dz)+^dx*^(dy*^(nx*^nz)))/(dx*^(dy*^(dx*^dz))) by ORDINAL3:46 .= (dx*^((nx*^ny)*^dz)+^(dx*^dy)*^(nx*^nz))/(dx*^(dy*^(dx*^dz))) by ORDINAL3:50 .= ((nx*^ny)*^(dx*^dz)+^(dx*^dy)*^(nx*^nz))/(dx*^(dy*^(dx*^dz))) by ORDINAL3:50 .= ((nx*^ny)*^(dx*^dz)+^(dx*^dy)*^(nx*^nz))/((dx*^dy)*^(dx*^dz)) by ORDINAL3:50 .= x*'y+x*'z by A2,A3,Th46; end; theorem Th58: for i,j being ordinal Element of RAT+ holds i+j = i+^j proof let i,j be ordinal Element of RAT+; set ni = numerator i, nj = numerator j; A1: j in omega by ORDINAL1:def 12; then A2: denominator j = 1 by Def9; A3: i in omega by ORDINAL1:def 12; then denominator i = 1 by Def9; hence i+j = (ni*^1+^1*^nj)/1 by A2,ORDINAL2:39 .= (ni+^1*^nj)/1 by ORDINAL2:39 .= (ni+^nj)/1 by ORDINAL2:39 .= ni+^nj by Th40 .= i+^nj by A3,Def8 .= i+^j by A1,Def8; end; theorem for i,j being ordinal Element of RAT+ holds i*'j = i*^j proof let i,j be ordinal Element of RAT+; set ni = numerator i, nj = numerator j; A1: j in omega by ORDINAL1:def 12; then A2: denominator j = 1 by Def9; A3: i in omega by ORDINAL1:def 12; then denominator i = 1 by Def9; hence i*'j = (ni*^nj)/1 by A2,ORDINAL2:39 .= ni*^nj by Th40 .= i*^nj by A3,Def8 .= i*^j by A1,Def8; end; theorem Th60: ex y st x = y+y proof set 02 = one+one; 02 = 1+^1 by Th58; then 02 <> {} by ORDINAL3:26; then consider z such that A1: 02*'z = 1 by Th54; take y = z*'x; thus x = one*'x by Th53 .= 02*'y by A1,Th52 .= one*'y+one*'y by Th57 .= y+one*'y by Th53 .= y+y by Th53; end; definition let x,y be Element of RAT+; pred x <=' y means : Def13: ex z being Element of RAT+ st y = x+z; connectedness proof let x,y be Element of RAT+; set nx = numerator x, ny = numerator y; set dx = denominator x, dy = denominator y; A1: dx <> {} & dy <> {} by Th35; A2: nx/dx = x & ny/dy = y by Th39; nx*^dy c= ny*^dx or ny*^dx c= nx*^dy; then A3: ny*^dx = nx*^dy+^(ny*^dx -^ nx*^dy) or nx*^dy = ny*^dx+^(nx*^dy -^ ny *^dx) by ORDINAL3:def 5; nx*^dy/(dx*^dy) = nx/dx & ny*^dx/(dx*^dy) = ny/dy by Th35,Th44; then x = y+((nx*^dy -^ ny*^dx)/(dx*^dy)) or y = x+((ny*^dx -^ nx*^dy)/(dx *^dy)) by A1,A2,A3,Th47,ORDINAL3:31; hence thesis; end; end; notation let x,y be Element of RAT+; antonym y < x for x <=' y; end; reserve r,s,t for Element of RAT+; theorem not ex y being object st [{},y] in RAT+ proof given y being object such that A1: [{},y] in RAT+; consider i,j being Element of omega such that A2: [{},y] = [i,j] and A3: i,j are_coprime and j <> {} and A4: j <> 1 by A1,Th29,Th32; i = {} by A2,XTUPLE_0:1; hence thesis by A3,A4,Th3; end; theorem Th62: s + t = r + t implies s = r proof assume A1: s + t = r + t; set r1 = numerator r, r2 = denominator r; set t1 = numerator t, t2 = denominator t; set s1 = numerator s, s2 = denominator s; A2: t2 <> {} by Th35; A3: s2 <> {} by Th35; then A4: s2*^t2 <> {} by A2,ORDINAL3:31; A5: r2 <> {} by Th35; then r2*^t2 <> {} by A2,ORDINAL3:31; then (s1*^t2+^s2*^t1)*^(r2*^t2) = (r1*^t2+^r2*^t1)*^(s2*^t2) by A1,A4,Th45 .= (r1*^t2+^r2*^t1)*^s2*^t2 by ORDINAL3:50; then (s1*^t2+^s2*^t1)*^r2*^t2 = (r1*^t2+^r2*^t1)*^s2*^t2 by ORDINAL3:50; then (s1*^t2+^s2*^t1)*^r2 = (r1*^t2+^r2*^t1)*^s2 by A2,ORDINAL3:33 .= r1*^t2*^s2+^r2*^t1*^s2 by ORDINAL3:46; then s1*^t2*^r2+^s2*^t1*^r2 = r1*^t2*^s2+^r2*^t1*^s2 by ORDINAL3:46 .= r1*^t2*^s2+^s2*^t1*^r2 by ORDINAL3:50; then s1*^t2*^r2 = r1*^t2*^s2 by ORDINAL3:21 .= r1*^s2*^t2 by ORDINAL3:50; then s1*^r2*^t2 = r1*^s2*^t2 by ORDINAL3:50; then s1*^r2 = r1*^s2 by A2,ORDINAL3:33; then s1/s2 = r1/r2 by A3,A5,Th45 .= r by Th39; hence thesis by Th39; end; theorem Th63: r+s = {} implies r = {} proof set nr = numerator r, dr = denominator r; set ns = numerator s, ds = denominator s; assume A1: r+s = {}; denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1; then A2: (nr*^ds+^ns*^dr)/(dr*^ds) = {}/1 by A1,Th39; A3: ds <> {} by Th35; dr <> {} by Th35; then dr*^ds <> {} by A3,ORDINAL3:31; then (nr*^ds+^ns*^dr)*^1 = (dr*^ds)*^{} by A2,Th45,Lm4 .= {} by ORDINAL2:35; then nr*^ds+^ns*^dr = {} by ORDINAL3:31,Lm4; then nr*^ds = {} by ORDINAL3:26; then nr = {} by A3,ORDINAL3:31; hence thesis by Th37; end; theorem Th64: {} <=' s proof take s; thus thesis by Th50; end; theorem s <=' {} implies s = {} by Th63; theorem Th66: r <=' s & s <=' r implies r = s proof given x such that A1: s = r+x; given y such that A2: r = s+y; r+{} = r by Th50 .= r+(x+y) by A1,A2,Th51; then x = {} by Th62,Th63; hence thesis by A1,Th50; end; theorem Th67: r <=' s & s <=' t implies r <=' t proof given x such that A1: s = r+x; given y such that A2: t = s+y; take x+y; thus thesis by A1,A2,Th51; end; theorem r < s iff r <=' s & r <> s by Th66; theorem r < s & s <=' t or r <=' s & s < t implies r < t by Th67; theorem r < s & s < t implies r < t by Th67; theorem Th71: x in omega & x+y in omega implies y in omega proof assume that A1: x in omega and A2: x+y in omega; A3: denominator (x+y) = 1 by A2,Def9; set nx = numerator x, dx = denominator x; A4: dx = 1 by A1,Def9; set ny = numerator y, dy = denominator y; A5: x+y = numerator (x+y)/denominator (x+y) & (nx*^dy+^ny*^dx)*^1 = nx*^dy+^ ny*^ dx by Th39,ORDINAL2:39; dy <> {} by Th35; then dx*^dy <> {} by A4,ORDINAL3:31,Lm4; then nx*^dy+^ny*^dx = dx*^dy*^numerator (x+y) by A3,A5,Th45,Lm4 .= dy*^numerator (x+y) by A4,ORDINAL2:39; then nx*^dy+^ny = dy*^numerator (x+y) by A4,ORDINAL2:39; then ny = (dy*^numerator (x+y))-^nx*^dy by ORDINAL3:52; then ny = dy*^((numerator (x+y))-^nx) by ORDINAL3:63; then A6: dy divides ny; A7: ny,dy are_coprime by Th34; for m being natural Ordinal st m divides dy & m divides ny holds m divides dy; then dy hcf ny = dy by A6,Def5; then A8: dy = 1 by A7,Th20; y = ny/dy by Th39; then y = ny by A8,Th40; hence thesis; end; theorem Th72: for i being ordinal Element of RAT+ st i < x & x < i+one holds not x in omega proof let i be ordinal Element of RAT+; assume that A1: i < x and A2: x < i+one and A3: x in omega; consider z such that A4: i+one = x+z by A2,Def13; i+one = i+^1 by Th58; then i+one in omega by Th31; then reconsider z9 = z as Element of omega by A3,A4,Th71; consider y such that A5: x = i+y by A1,Def13; i in omega by Th31; then reconsider y9 = y as Element of omega by A3,A5,Th71; i+one = i+(y+z) by A5,A4,Th51; then 1 = y+z by Th62 .= y9+^z9 by Th58; then y9 c= 1 by ORDINAL3:24; then y = {} or y = 1 by ORDINAL3:16; then i = x or i+one = x by A5,Th50; hence contradiction by A1,A2; end; theorem Th73: t <> {} implies ex r st r < t & not r in omega proof assume A1: t <> {}; A2: 1+^1 = succ 1 by ORDINAL2:31; per cases; suppose A3: one <=' t; consider r such that A4: one = r+r by Th60; take r; r <=' one & r <> 1 by A2,A4,Th58; then r < one by Th66; hence r < t by A3,Th67; A5: 1*^1 = 1 by ORDINAL2:39; assume r in omega; then A6: denominator r = 1 by Def9; then (numerator r)*^denominator r = numerator r by ORDINAL2:39; then A7: 1 = (numerator r)+^numerator r by A4,A6,A5,Th40; then numerator r c= 1 by ORDINAL3:24; then numerator r = {} or numerator r = 1 by ORDINAL3:16; hence contradiction by A2,A7,ORDINAL2:27; end; suppose A8: t < one; consider r such that A9: t = r+r by Th60; A10: {} <=' r by Th64; r <> {} by A1,A9,Th50; then A11: {} < r by A10,Th66; take r; A12: 1 = {}+one by Th50; A13: r <=' t by A9; now assume r = t; then t+{} = t+t by A9,Th50; hence contradiction by A1,Th62; end; hence r < t by A13,Th66; r < one by A8,A13,Th67; hence thesis by A11,A12,Th72; end; end; theorem {s: s < t} in RAT+ iff t = {} proof hereby assume A1: {s: s < t} in RAT+ & t <> {}; then consider r such that A2: r < t and A3: not r in omega by Th73; {} <=' t by Th64; then {} < t by A1,Th66; then A4: {} in {s: s < t}; r in {s: s < t} by A2; then {s: s < t} in omega implies r is Ordinal; then ex i,j being Element of omega st {s: s < t} = [i,j] & i,j are_coprime & j <> {} & j <> 1 by A1,A3,Th29,Th31; hence contradiction by A4,TARSKI:def 2; end; assume A5: t = {}; {s: s < t} c= {} proof let a be object; assume a in {s: s < t}; then ex s st a = s & s < t; hence thesis by A5,Th64; end; then {s: s < t} = {}; hence thesis; end; theorem for A being Subset of RAT+ st (ex t st t in A & t <> {}) & for r,s st r in A & s <=' r holds s in A ex r1,r2,r3 being Element of RAT+ st r1 in A & r2 in A & r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 proof let A be Subset of RAT+; given t such that A1: t in A and A2: t <> {}; assume A3: for r,s st r in A & s <=' r holds s in A; consider x such that A4: t = x+x by Th60; take {}, x, t; x <=' t by A4; hence {} in A & x in A & t in A by A1,A3,Th64; thus {} <> x by A2,A4,Th50; hereby assume x = t; then t+{} = t+t by A4,Th50; hence contradiction by A2,Th62; end; thus thesis by A2; end; theorem Th76: s + t <=' r + t iff s <=' r proof thus s + t <=' r + t implies s <=' r proof given z such that A1: r+t = s+t+z; take z; r+t = s+z+t by A1,Th51; hence thesis by Th62; end; given z such that A2: r = s+z; take z; thus thesis by A2,Th51; end; theorem s <=' s + t; theorem r*'s = {} implies r = {} or s = {} proof set nr = numerator r, dr = denominator r; set ns = numerator s, ds = denominator s; assume A1: r*'s = {}; dr <> {} & ds <> {} by Th35; then A2: dr*^ds <> {} by ORDINAL3:31; denominator {} = 1 & numerator {} = {} by Def8,Def9,Lm1; then (nr*^ns)/(dr*^ds) = {}/1 by A1,Th39; then (nr*^ns)*^1 = (dr*^ds)*^{} by A2,Th45,Lm4 .= {} by ORDINAL2:35; then nr*^ns = {} by ORDINAL3:31,Lm4; then nr = {} or ns = {} by ORDINAL3:31; hence thesis by Th37; end; theorem Th79: r <=' s *' t implies ex t0 being Element of RAT+ st r = s *' t0 & t0 <=' t proof given x such that A1: s*'t = r+x; per cases; suppose A2: s = {}; take t; s*'t = {} by A2,Th48; hence thesis by A1,Th63; end; suppose A3: s <> {}; then consider t1 being Element of RAT+ such that A4: x = s*'t1 by Th55; consider t0 being Element of RAT+ such that A5: r = s*'t0 by A3,Th55; take t0; thus r = s*'t0 by A5; take t1; s*'t = s*'(t0+t1) by A1,A5,A4,Th57; hence thesis by A3,Th56; end; end; theorem t <> {} & s *' t <=' r *' t implies s <=' r proof assume that A1: t <> {} and A2: s *' t <=' r *' t; ex x st s*'t = t*'x & x <=' r by A2,Th79; hence thesis by A1,Th56; end; theorem for r1,r2,s1,s2 being Element of RAT+ st r1+r2 = s1+s2 holds r1 <=' s1 or r2 <=' s2 proof let r1,r2,s1,s2 be Element of RAT+ such that A1: r1+r2 = s1+s2; assume that A2: s1 < r1 and A3: s2 < r2; s1+s2 < r1+s2 by A2,Th76; hence thesis by A1,A3,Th76; end; theorem Th82: s <=' r implies s *' t <=' r *' t proof given x such that A1: r = s+x; take x*'t; thus thesis by A1,Th57; end; theorem for r1,r2,s1,s2 being Element of RAT+ st r1*'r2 = s1*'s2 holds r1 <=' s1 or r2 <=' s2 proof let r1,r2,s1,s2 be Element of RAT+ such that A1: r1*'r2 = s1*'s2; A2: {} <=' s1 by Th64; assume that A3: s1 < r1 and A4: s2 < r2; s2 <> r2 & s1*'s2 <=' r1*'s2 by A3,A4,Th82; then s1*'s2 < r1*'s2 by A1,A3,A2,Th56,Th66; hence thesis by A1,A4,Th82; end; theorem r = {} iff r + s = s proof s+{} = s by Th50; hence thesis by Th62; end; theorem for s1,t1,s2,t2 being Element of RAT+ st s1 + t1 = s2 + t2 & s1 <=' s2 holds t2 <=' t1 proof let s1,t1,s2,t2 be Element of RAT+ such that A1: s1 + t1 = s2 + t2; given x such that A2: s2 = s1+x; take x; s1+t1 = s1+(x+t2) by A1,A2,Th51; hence thesis by Th62; end; theorem Th86: r <=' s & s <=' r + t implies ex t0 being Element of RAT+ st s = r + t0 & t0 <=' t by Th76; theorem r <=' s + t implies ex s0,t0 being Element of RAT+ st r = s0 + t0 & s0 <=' s & t0 <=' t proof assume A1: r <=' s + t; per cases; suppose s <=' r; then s <=' s & ex t0 being Element of RAT+ st r = s + t0 & t0 <=' t by A1,Th86; hence thesis; end; suppose A2: r <=' s; r = r+{} & {} <=' t by Th50,Th64; hence thesis by A2; end; end; theorem r < s & r < t implies ex t0 being Element of RAT+ st t0 <=' s & t0 <=' t & r < t0 proof s <=' t & s <=' s or t <=' s & t <=' t; hence thesis; end; theorem r <=' s & s <=' t & s <> t implies r <> t by Th66; theorem s < r + t & t <> {} implies ex r0,t0 being Element of RAT+ st s = r0 + t0 & r0 <=' r & t0 <=' t & t0 <> t proof assume that A1: s < r + t and A2: t <> {}; per cases; suppose r <=' s; then consider t0 being Element of RAT+ such that A3: s = r + t0 & t0 <=' t by A1,Th86; take r,t0; thus thesis by A1,A3; end; suppose A4: s <=' r; s = s+{} & {} <=' t by Th50,Th64; hence thesis by A2,A4; end; end; theorem for A being non empty Subset of RAT+ st A in RAT+ ex s st s in A & for r st r in A holds r <=' s proof let A be non empty Subset of RAT+; A1: now given i,j being Element of omega such that A2: A = [i,j] and A3: i,j are_coprime and j <> {} and A4: j <> 1; A5: now assume {i} in omega; then {} in {i} by ORDINAL3:8; then {} = i by TARSKI:def 1; hence contradiction by A3,A4,Th3; end; {i} in A by A2,TARSKI:def 2; then consider i1,j1 being Element of omega such that A6: {i} = [i1,j1] and A7: i1,j1 are_coprime and j1 <> {} and A8: j1 <> 1 by A5,Th29; {i1,j1} in {i} by A6,TARSKI:def 2; then A9: i = {i1,j1} by TARSKI:def 1; {i1} in {i} by A6,TARSKI:def 2; then i = {i1} by TARSKI:def 1; then j1 in {i1} by A9,TARSKI:def 2; then A10: j1 = i1 by TARSKI:def 1; j1 = j1*^1 by ORDINAL2:39; hence contradiction by A7,A8,A10; end; assume A in RAT+; then reconsider B = A as Element of omega by A1,Th29; A11: {} in B by ORDINAL3:8; now assume B is limit_ordinal; then omega c= B by A11,ORDINAL1:def 11; hence contradiction by ORDINAL1:5; end; then consider C such that A12: B = succ C by ORDINAL1:29; C in B by A12,ORDINAL1:6; then reconsider C as ordinal Element of RAT+; take C; thus C in A by A12,ORDINAL1:6; let r; assume A13: r in A; then r in B; then reconsider r as ordinal Element of RAT+; C-^r in omega by ORDINAL1:def 12; then reconsider x = C-^r as ordinal Element of RAT+ by Lm6; r c= C by A12,A13,ORDINAL1:22; then C = r+^x by ORDINAL3:def 5 .= r+x by Th58; hence thesis; end; theorem ex t st r + t = s or s + t = r proof r <=' s or s <=' r; hence thesis; end; theorem r < s implies ex t st r < t & t < s proof assume A1: r < s; then consider x such that A2: s = r+x by Def13; consider y such that A3: x = y+y by Th60; take t = r+y; A4: s = t+y by A2,A3,Th51; then A5: t <=' s; r <=' t; hence r < t by A1,A4,Th66; r <> s by A1; then s <> t by A4,Th62; hence thesis by A5,Th66; end; theorem ex s st r < s proof take s = r+one; s+{} = s by Th50; then A1: r <> s by Th62; r <=' s; hence thesis by A1,Th66; end; theorem t <> {} implies ex s st s in omega & r <=' s *' t proof set y=((numerator r)*^(((numerator t)*^denominator r)-^1))/denominator r; A1: denominator r <> {} by Th35; (denominator t)*^(numerator r) in omega by ORDINAL1:def 12; then reconsider s = (denominator t)*^(numerator r) as ordinal Element of RAT+ by Lm6; assume t <> {}; then numerator t <> {} by Th37; then {} in (numerator t)*^denominator r by A1,ORDINAL3:8,31; then one c= (numerator t)*^denominator r by Lm3,ORDINAL1:21; then (numerator t)*^denominator r = 1+^(((numerator t)*^denominator r)-^ 1) by ORDINAL3:def 5; then s*^((numerator t)*^denominator r) = (denominator t)*^ ((numerator r)*^(1 +^(((numerator t)*^denominator r)-^1))) by ORDINAL3:50 .= (denominator t)*^((numerator r)*^1+^ (numerator r)*^(((numerator t)*^ denominator r)-^1)) by ORDINAL3:46; then A2: s*^(numerator t)*^denominator r = (denominator t)*^((numerator r)*^1+^ (numerator r)*^(((numerator t)*^denominator r)-^1)) by ORDINAL3:50; take s; thus s in omega by ORDINAL1:def 12; take y; denominator t <> {} by Th35; then (s*^(numerator t))/denominator t = ((numerator r)*^1+^ (numerator r)*^( ((numerator t)*^denominator r)-^1))/denominator r by A1,A2,Th45 .= (((numerator r)*^1)/denominator r)+y by Th35,Th47 .= ((numerator r)/denominator r)+y by ORDINAL2:39 .= r+y by Th39; then r+y = (s*^(numerator t))/(1*^denominator t) by ORDINAL2:39 .= (s/1)*'((numerator t)/denominator t) by Th49 .= s*'((numerator t)/denominator t) by Th40; hence thesis by Th39; end; scheme DisNat { n0,n1,n2() -> Element of RAT+, P[set] }: ex s st s in omega & P[s] & not P[s + n1()] provided A1: n1() = 1 and A2: n0() = {} and A3: n2() in omega and A4: P[n0()] and A5: not P[n2()] proof defpred P1[Ordinal] means not P[\$1] & \$1 in omega; A6: ex A st P1[A] by A3,A5; consider A such that A7: P1[A] and A8: for B st P1[B] holds A c= B from ORDINAL1:sch 1(A6); A9: {} in A by A2,A4,A7,ORDINAL3:8; now assume A is limit_ordinal; then omega c= A by A9,ORDINAL1:def 11; then A in A by A7; hence contradiction; end; then consider B being Ordinal such that A10: A = succ B by ORDINAL1:29; A11: B in A by A10,ORDINAL1:8; then A12: B in omega by A7,ORDINAL1:10; then reconsider s = B as ordinal Element of RAT+ by Lm6; take s; thus s in omega & P[s] by A8,A11,A12,ORDINAL1:5; A = B+^1 by A10,ORDINAL2:31; hence thesis by A1,A7,Th58; end;