:: ARYTM_3 semantic presentation begin Lm1: {} in omega by ORDINAL1:def_11; Lm2: 1 in omega ; definition func one -> set equals :: ARYTM_3:def 1 1; correctness coherence 1 is set ; ; end; :: deftheorem defines one ARYTM_3:def_1_:_ one = 1; begin definition let a, b be Ordinal; preda,b are_relative_prime means :Def2: :: ARYTM_3:def 2 for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds c = 1; symmetry for a, b being Ordinal st ( for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds c = 1 ) holds for c, d1, d2 being Ordinal st b = c *^ d1 & a = c *^ d2 holds c = 1 ; end; :: deftheorem Def2 defines are_relative_prime ARYTM_3:def_2_:_ for a, b being Ordinal holds ( a,b are_relative_prime iff for c, d1, d2 being Ordinal st a = c *^ d1 & b = c *^ d2 holds c = 1 ); theorem :: ARYTM_3:1 not {} , {} are_relative_prime proof take {} ; :: according to ARYTM_3:def_2 ::_thesis: ex d1, d2 being Ordinal st ( {} = {} *^ d1 & {} = {} *^ d2 & not {} = 1 ) take {} ; ::_thesis: ex d2 being Ordinal st ( {} = {} *^ {} & {} = {} *^ d2 & not {} = 1 ) take {} ; ::_thesis: ( {} = {} *^ {} & {} = {} *^ {} & not {} = 1 ) thus ( {} = {} *^ {} & {} = {} *^ {} & not {} = 1 ) by ORDINAL2:35; ::_thesis: verum end; theorem Th2: :: ARYTM_3:2 for A being Ordinal holds 1,A are_relative_prime proof let A be Ordinal; ::_thesis: 1,A are_relative_prime let c, d1, d2 be Ordinal; :: according to ARYTM_3:def_2 ::_thesis: ( 1 = c *^ d1 & A = c *^ d2 implies c = 1 ) thus ( 1 = c *^ d1 & A = c *^ d2 implies c = 1 ) by ORDINAL3:37; ::_thesis: verum end; theorem Th3: :: ARYTM_3:3 for A being Ordinal st {} ,A are_relative_prime holds A = 1 proof let A be Ordinal; ::_thesis: ( {} ,A are_relative_prime implies A = 1 ) A1: ( {} = A *^ {} & A = A *^ 1 ) by ORDINAL2:38, ORDINAL2:39; assume ( {} ,A are_relative_prime & A <> 1 ) ; ::_thesis: contradiction hence contradiction by A1, Def2; ::_thesis: verum end; defpred S1[ set ] means ex B being Ordinal st ( B c= $1 & $1 in omega & $1 <> {} & ( for c, d1, d2 being natural Ordinal holds ( not d1,d2 are_relative_prime or not $1 = c *^ d1 or not B = c *^ d2 ) ) ); theorem :: ARYTM_3:4 for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds ex c, d1, d2 being natural Ordinal st ( d1,d2 are_relative_prime & a = c *^ d1 & b = c *^ d2 ) proof let a, b be natural Ordinal; ::_thesis: ( ( a <> {} or b <> {} ) implies ex c, d1, d2 being natural Ordinal st ( d1,d2 are_relative_prime & a = c *^ d1 & b = c *^ d2 ) ) assume that A1: ( a <> {} or b <> {} ) and A2: for c, d1, d2 being natural Ordinal holds ( not d1,d2 are_relative_prime or not a = c *^ d1 or not b = c *^ d2 ) ; ::_thesis: contradiction A3: ex A being Ordinal st S1[A] proof percases ( a c= b or b c= a ) ; supposeA4: a c= b ; ::_thesis: ex A being Ordinal st S1[A] take A = b; ::_thesis: S1[A] take B = a; ::_thesis: ( B c= A & A in omega & A <> {} & ( for c, d1, d2 being natural Ordinal holds ( not d1,d2 are_relative_prime or not A = c *^ d1 or not B = c *^ d2 ) ) ) thus ( B c= A & A in omega & A <> {} ) by A1, A4, ORDINAL1:def_12; ::_thesis: for c, d1, d2 being natural Ordinal holds ( not d1,d2 are_relative_prime or not A = c *^ d1 or not B = c *^ d2 ) thus for c, d1, d2 being natural Ordinal holds ( not d1,d2 are_relative_prime or not A = c *^ d1 or not B = c *^ d2 ) by A2; ::_thesis: verum end; supposeA5: b c= a ; ::_thesis: ex A being Ordinal st S1[A] take A = a; ::_thesis: S1[A] take B = b; ::_thesis: ( B c= A & A in omega & A <> {} & ( for c, d1, d2 being natural Ordinal holds ( not d1,d2 are_relative_prime or not A = c *^ d1 or not B = c *^ d2 ) ) ) thus ( B c= A & A in omega & A <> {} ) by A1, A5, ORDINAL1:def_12; ::_thesis: for c, d1, d2 being natural Ordinal holds ( not d1,d2 are_relative_prime or not A = c *^ d1 or not B = c *^ d2 ) thus for c, d1, d2 being natural Ordinal holds ( not d1,d2 are_relative_prime or not A = c *^ d1 or not B = c *^ d2 ) by A2; ::_thesis: verum end; end; end; consider A being Ordinal such that A6: S1[A] and A7: for C being Ordinal st S1[C] holds A c= C from ORDINAL1:sch_1(A3); consider B being Ordinal such that A8: B c= A and A9: A in omega and A10: A <> {} and A11: for c, d1, d2 being natural Ordinal holds ( not d1,d2 are_relative_prime or not A = c *^ d1 or not B = c *^ d2 ) by A6; reconsider A = A, B = B as Element of omega by A8, A9, ORDINAL1:12; ( A = 1 *^ A & B = 1 *^ B ) by ORDINAL2:39; then not A,B are_relative_prime by A11; then consider c, d1, d2 being Ordinal such that A12: A = c *^ d1 and A13: B = c *^ d2 and A14: c <> 1 by Def2; 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 = c, d1 = d1, d2 = 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, ORDINAL3:19; then A18: d1 in A by ORDINAL2:39; A19: now__::_thesis:_for_c9,_d19,_d29_being_natural_Ordinal_st_d19,d29_are_relative_prime_&_d1_=_c9_*^_d19_holds_ not_d2_=_c9_*^_d29 let c9, d19, d29 be natural Ordinal; ::_thesis: ( d19,d29 are_relative_prime & d1 = c9 *^ d19 implies not d2 = c9 *^ d29 ) assume that A20: d19,d29 are_relative_prime and A21: ( d1 = c9 *^ d19 & d2 = c9 *^ d29 ) ; ::_thesis: contradiction ( A = (c *^ c9) *^ d19 & B = (c *^ c9) *^ d29 ) by A12, A13, A21, ORDINAL3:50; hence contradiction by A11, A20; ::_thesis: verum 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; ::_thesis: verum end; registration let m, n be natural Ordinal; clusterm div^ n -> natural ; coherence m div^ n is natural 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, ORDINAL3: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; :: according to ORDINAL1:def_12 ::_thesis: verum end; clusterm mod^ n -> natural ; coherence m mod^ n is natural 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; :: according to ORDINAL1:def_12 ::_thesis: verum end; end; definition let k, n be Ordinal; predk divides n means :Def3: :: ARYTM_3:def 3 ex a being Ordinal st n = k *^ a; reflexivity for k being Ordinal ex a being Ordinal st k = k *^ a proof let n be Ordinal; ::_thesis: ex a being Ordinal st n = n *^ a take 1 ; ::_thesis: n = n *^ 1 thus n = n *^ 1 by ORDINAL2:39; ::_thesis: verum end; end; :: deftheorem Def3 defines divides ARYTM_3:def_3_:_ for k, n being Ordinal holds ( k divides n iff ex a being Ordinal st n = k *^ a ); theorem Th5: :: ARYTM_3:5 for a, b being natural Ordinal holds ( a divides b iff ex c being natural Ordinal st b = a *^ c ) proof let a, b be natural Ordinal; ::_thesis: ( a divides b iff ex c being natural Ordinal st b = a *^ c ) thus ( a divides b implies ex c being natural Ordinal st b = a *^ c ) ::_thesis: ( ex c being natural Ordinal st b = a *^ c implies a divides b ) proof given c being Ordinal such that A1: b = a *^ c ; :: according to ARYTM_3:def_3 ::_thesis: ex c being natural Ordinal st b = a *^ c percases ( b = {} or b <> {} ) ; suppose b = {} ; ::_thesis: ex c being natural Ordinal st b = a *^ c then b = a *^ {} by ORDINAL2:38; hence ex c being natural Ordinal st b = a *^ c ; ::_thesis: verum end; suppose b <> {} ; ::_thesis: ex c being natural Ordinal st b = a *^ c then c is Element of omega by A1, ORDINAL3:75; hence ex c being natural Ordinal st b = a *^ c by A1; ::_thesis: verum end; end; end; thus ( ex c being natural Ordinal st b = a *^ c implies a divides b ) by Def3; ::_thesis: verum end; theorem Th6: :: ARYTM_3:6 for m, n being natural Ordinal st {} in m holds n mod^ m in m proof let m, n be natural Ordinal; ::_thesis: ( {} in m implies n mod^ m in m ) assume {} in m ; ::_thesis: n mod^ m in m then A1: ex C being Ordinal 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 n mod^ m in m by A1, ORDINAL3:52; ::_thesis: verum end; theorem Th7: :: ARYTM_3:7 for n, m being natural Ordinal holds ( m divides n iff n = m *^ (n div^ m) ) proof let n, m be natural Ordinal; ::_thesis: ( m divides n iff n = m *^ (n div^ m) ) assume A1: ( ( m divides n & not n = m *^ (n div^ m) ) or ( n = m *^ (n div^ m) & not m divides n ) ) ; ::_thesis: contradiction then consider a being natural Ordinal 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 contradiction by A1, A2, A3, Def3, ORDINAL3:def_6; ::_thesis: verum end; theorem Th8: :: ARYTM_3:8 for n, m being natural Ordinal st n divides m & m divides n holds n = m proof let n, m be natural Ordinal; ::_thesis: ( n divides m & m divides n implies n = m ) assume that A1: n divides m and A2: m divides n ; ::_thesis: n = m 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 ; ::_thesis: n = m then m div^ n = 1 by ORDINAL3:37; hence n = m by A3, ORDINAL2:39; ::_thesis: verum 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 n = m by A5, A4, ORDINAL3:33; ::_thesis: verum end; theorem Th9: :: ARYTM_3:9 for n being natural Ordinal holds ( n divides {} & 1 divides n ) proof let n be natural Ordinal; ::_thesis: ( n divides {} & 1 divides n ) {} = n *^ {} by ORDINAL2:35; hence n divides {} by Def3; ::_thesis: 1 divides n n = 1 *^ n by ORDINAL2:39; hence 1 divides n by Def3; ::_thesis: verum end; theorem Th10: :: ARYTM_3:10 for n, m being natural Ordinal st {} in m & n divides m holds n c= m proof let n, m be natural Ordinal; ::_thesis: ( {} in m & n divides m implies n c= m ) assume A1: {} in m ; ::_thesis: ( not n divides m or n c= m ) given a being Ordinal such that A2: m = n *^ a ; :: according to ARYTM_3:def_3 ::_thesis: n c= m a <> {} by A1, A2, ORDINAL2:38; hence n c= m by A2, ORDINAL3:36; ::_thesis: verum end; theorem Th11: :: ARYTM_3:11 for n, m, l being natural Ordinal st n divides m & n divides m +^ l holds n divides l proof let n, m, l be natural Ordinal; ::_thesis: ( n divides m & n divides m +^ l implies n divides l ) assume n divides m ; ::_thesis: ( not n divides m +^ l or n divides l ) then consider a being natural Ordinal such that A1: m = n *^ a by Th5; assume n divides m +^ l ; ::_thesis: n divides l then consider b being natural Ordinal such that A2: m +^ l = n *^ b by Th5; assume A3: not n divides l ; ::_thesis: contradiction l = (n *^ b) -^ (n *^ a) by A1, A2, ORDINAL3:52 .= (b -^ a) *^ n by ORDINAL3:63 ; hence contradiction by A3, Def3; ::_thesis: verum end; Lm3: 1 = succ {} ; definition let k, n be natural Ordinal; funck lcm n -> Element of omega means :Def4: :: ARYTM_3:def 4 ( k divides it & n divides it & ( for m being natural Ordinal st k divides m & n divides m holds it divides m ) ); existence ex b1 being Element of omega st ( k divides b1 & n divides b1 & ( for m being natural Ordinal st k divides m & n divides m holds b1 divides m ) ) proof percases ( k = {} or n = {} or ( k <> {} & n <> {} ) ) ; supposeA1: ( k = {} or n = {} ) ; ::_thesis: ex b1 being Element of omega st ( k divides b1 & n divides b1 & ( for m being natural Ordinal st k divides m & n divides m holds b1 divides m ) ) reconsider w = {} as Element of omega by ORDINAL1:def_12; take w ; ::_thesis: ( k divides w & n divides w & ( for m being natural Ordinal st k divides m & n divides m holds w divides m ) ) thus ( k divides w & n divides w ) by Th9; ::_thesis: for m being natural Ordinal st k divides m & n divides m holds w divides m let m be natural Ordinal; ::_thesis: ( k divides m & n divides m implies w divides m ) assume ( k divides m & n divides m ) ; ::_thesis: w divides m hence w divides m by A1; ::_thesis: verum end; supposeA2: ( k <> {} & n <> {} ) ; ::_thesis: ex b1 being Element of omega st ( k divides b1 & n divides b1 & ( for m being natural Ordinal st k divides m & n divides m holds b1 divides m ) ) {} 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 S2[ Ordinal] means ex m being natural Ordinal 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 ) by Def3; then A6: ex A being Ordinal st S2[A] by A4, A5, ORDINAL2:41; consider A being Ordinal such that A7: S2[A] and A8: for B being Ordinal st S2[B] holds A c= B from ORDINAL1:sch_1(A6); consider l being natural Ordinal such that A9: A = l and A10: k divides l and A11: n divides l and A12: k c= l by A7; reconsider l = l as Element of omega by ORDINAL1:def_12; take l ; ::_thesis: ( k divides l & n divides l & ( for m being natural Ordinal st k divides m & n divides m holds l divides m ) ) thus ( k divides l & n divides l ) by A10, A11; ::_thesis: for m being natural Ordinal st k divides m & n divides m holds l divides m let m be natural Ordinal; ::_thesis: ( k divides m & n divides m implies l divides m ) assume that A13: k divides m and A14: n divides m ; ::_thesis: l 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) by Def3; 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) by Def3; then A17: n divides m mod^ l by A14, A15, Th11; now__::_thesis:_not_m_mod^_l_<>_{} A18: {} c= m mod^ l ; assume m mod^ l <> {} ; ::_thesis: contradiction 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; ::_thesis: verum end; then m = l *^ (m div^ l) by A15, ORDINAL2:27; hence l divides m by Th7; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Element of omega st k divides b1 & n divides b1 & ( for m being natural Ordinal st k divides m & n divides m holds b1 divides m ) & k divides b2 & n divides b2 & ( for m being natural Ordinal st k divides m & n divides m holds b2 divides m ) holds b1 = b2 proof let m1, m2 be Element of omega ; ::_thesis: ( k divides m1 & n divides m1 & ( for m being natural Ordinal st k divides m & n divides m holds m1 divides m ) & k divides m2 & n divides m2 & ( for m being natural Ordinal st k divides m & n divides m holds m2 divides m ) implies m1 = m2 ) assume ( k divides m1 & n divides m1 & ( for m being natural Ordinal st k divides m & n divides m holds m1 divides m ) & k divides m2 & n divides m2 & ( for m being natural Ordinal st k divides m & n divides m holds m2 divides m ) ) ; ::_thesis: m1 = m2 then ( m1 divides m2 & m2 divides m1 ) ; hence m1 = m2 by Th8; ::_thesis: verum end; commutativity for b1 being Element of omega for k, n being natural Ordinal st k divides b1 & n divides b1 & ( for m being natural Ordinal st k divides m & n divides m holds b1 divides m ) holds ( n divides b1 & k divides b1 & ( for m being natural Ordinal st n divides m & k divides m holds b1 divides m ) ) ; end; :: deftheorem Def4 defines lcm ARYTM_3:def_4_:_ for k, n being natural Ordinal for b3 being Element of omega holds ( b3 = k lcm n iff ( k divides b3 & n divides b3 & ( for m being natural Ordinal st k divides m & n divides m holds b3 divides m ) ) ); theorem Th12: :: ARYTM_3:12 for m, n being natural Ordinal holds m lcm n divides m *^ n proof let m, n be natural Ordinal; ::_thesis: m lcm n divides m *^ n ( m divides m *^ n & n divides m *^ n ) by Def3; hence m lcm n divides m *^ n by Def4; ::_thesis: verum end; theorem Th13: :: ARYTM_3:13 for n, m being natural Ordinal st n <> {} holds (m *^ n) div^ (m lcm n) divides m proof let n, m be natural Ordinal; ::_thesis: ( n <> {} implies (m *^ n) div^ (m lcm n) divides m ) assume A1: n <> {} ; ::_thesis: (m *^ n) div^ (m lcm n) divides m take (m lcm n) div^ n ; :: according to ARYTM_3:def_3 ::_thesis: m = ((m *^ n) div^ (m lcm n)) *^ ((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; ::_thesis: verum end; definition let k, n be natural Ordinal; funck hcf n -> Element of omega means :Def5: :: ARYTM_3:def 5 ( it divides k & it divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides it ) ); existence ex b1 being Element of omega st ( b1 divides k & b1 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides b1 ) ) proof percases ( k = {} or n = {} or ( k <> {} & n <> {} ) ) ; supposeA1: ( k = {} or n = {} ) ; ::_thesis: ex b1 being Element of omega st ( b1 divides k & b1 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides b1 ) ) then reconsider m = k \/ n as Element of omega by ORDINAL1:def_12; take m ; ::_thesis: ( m divides k & m divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides m ) ) thus ( m divides k & m divides n ) by A1, Th9; ::_thesis: for m being natural Ordinal st m divides k & m divides n holds m divides m thus for m being natural Ordinal st m divides k & m divides n holds m divides m by A1; ::_thesis: verum end; supposeA2: ( k <> {} & n <> {} ) ; ::_thesis: ex b1 being Element of omega st ( b1 divides k & b1 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides b1 ) ) reconsider l = (k *^ n) div^ (k lcm n) as Element of omega by ORDINAL1:def_12; take l ; ::_thesis: ( l divides k & l divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides l ) ) thus ( l divides k & l divides n ) by A2, Th13; ::_thesis: for m being natural Ordinal st m divides k & m divides n holds m divides l let m be natural Ordinal; ::_thesis: ( m divides k & m divides n implies m divides l ) assume that A3: m divides k and A4: m divides n ; ::_thesis: m divides l 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) by Def3; set mm = m *^ ((k div^ m) *^ (n div^ m)); A8: m *^ ((k div^ m) *^ (n div^ m)) = (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, Def3; then k lcm n divides (m *^ (k div^ m)) *^ (n div^ m) by A7, Def4; then A11: m *^ ((k div^ m) *^ (n div^ m)) = (k lcm n) *^ ((m *^ ((k div^ m) *^ (n div^ m))) 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; (m *^ ((k div^ m) *^ (n div^ m))) *^ m = (k lcm n) *^ (m *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n))) by A11, ORDINAL3:50; then k *^ n = (k lcm n) *^ (m *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n))) by A9, A5, A8, ORDINAL3:50; then l = m *^ ((m *^ ((k div^ m) *^ (n div^ m))) div^ (k lcm n)) by A12, ORDINAL3:66; hence m divides l by Def3; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Element of omega st b1 divides k & b1 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides b1 ) & b2 divides k & b2 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides b2 ) holds b1 = b2 proof let m1, m2 be Element of omega ; ::_thesis: ( m1 divides k & m1 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides m1 ) & m2 divides k & m2 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides m2 ) implies m1 = m2 ) assume ( m1 divides k & m1 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides m1 ) & m2 divides k & m2 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides m2 ) ) ; ::_thesis: m1 = m2 then ( m1 divides m2 & m2 divides m1 ) ; hence m1 = m2 by Th8; ::_thesis: verum end; commutativity for b1 being Element of omega for k, n being natural Ordinal st b1 divides k & b1 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides b1 ) holds ( b1 divides n & b1 divides k & ( for m being natural Ordinal st m divides n & m divides k holds m divides b1 ) ) ; end; :: deftheorem Def5 defines hcf ARYTM_3:def_5_:_ for k, n being natural Ordinal for b3 being Element of omega holds ( b3 = k hcf n iff ( b3 divides k & b3 divides n & ( for m being natural Ordinal st m divides k & m divides n holds m divides b3 ) ) ); theorem Th14: :: ARYTM_3:14 for a being natural Ordinal holds ( a hcf {} = a & a lcm {} = {} ) proof let a be natural Ordinal; ::_thesis: ( a hcf {} = a & a lcm {} = {} ) reconsider e = a, c = {} as Element of omega by ORDINAL1:def_12; A1: for b being natural Ordinal st a divides b & {} divides b holds c divides b ; ( ( for n being natural Ordinal st n divides a & n divides {} holds n divides e ) & a divides c ) by Th9; hence ( a hcf {} = a & a lcm {} = {} ) by A1, Def4, Def5; ::_thesis: verum end; theorem Th15: :: ARYTM_3:15 for a, b being natural Ordinal st a hcf b = {} holds a = {} proof let a, b be natural Ordinal; ::_thesis: ( a hcf b = {} implies a = {} ) a hcf b divides a by Def5; then a = (a hcf b) *^ (a div^ (a hcf b)) by Th7; hence ( a hcf b = {} implies a = {} ) by ORDINAL2:35; ::_thesis: verum end; theorem Th16: :: ARYTM_3:16 for a being natural Ordinal holds ( a hcf a = a & a lcm a = a ) proof let a be natural Ordinal; ::_thesis: ( a hcf a = a & a lcm a = a ) reconsider c = a as Element of omega by ORDINAL1:def_12; for b being natural Ordinal st b divides a & b divides a holds b divides c ; hence a hcf a = a by Def5; ::_thesis: a lcm a = a for b being natural Ordinal st a divides b & a divides b holds c divides b ; hence a lcm a = a by Def4; ::_thesis: verum end; theorem Th17: :: ARYTM_3:17 for a, c, b being natural Ordinal holds (a *^ c) hcf (b *^ c) = (a hcf b) *^ c proof let a, c, b be natural Ordinal; ::_thesis: (a *^ c) hcf (b *^ c) = (a hcf b) *^ c percases ( c = {} or ( c <> {} & a <> {} ) or a = {} ) ; supposeA1: c = {} ; ::_thesis: (a *^ c) hcf (b *^ c) = (a hcf b) *^ c then A2: (a hcf b) *^ c = {} by ORDINAL2:35; ( a *^ c = {} & b *^ c = {} ) by A1, ORDINAL2:35; hence (a *^ c) hcf (b *^ c) = (a hcf b) *^ c by A2, Th16; ::_thesis: verum end; supposeA3: ( c <> {} & a <> {} ) ; ::_thesis: (a *^ c) hcf (b *^ c) = (a hcf b) *^ c 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 by Def3; 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 by Def3; then d divides (a *^ c) hcf (b *^ c) by A4, Def5; then A5: (a *^ c) hcf (b *^ c) = d *^ (((a *^ c) hcf (b *^ c)) div^ d) by Th7 .= ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c by ORDINAL3:50 ; then ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c divides b *^ c by Def5; then (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c) *^ ((b *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c)) = b *^ c by Th7; then (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ ((b *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c))) *^ c = b *^ c by ORDINAL3:50; then ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ ((b *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c)) = b by A3, ORDINAL3:33; then A6: (a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d) divides b by Def3; ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c divides a *^ c by A5, Def5; then (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c) *^ ((a *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c)) = a *^ c by Th7; then (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ ((a *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c))) *^ c = a *^ c by ORDINAL3:50; then ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ ((a *^ c) div^ (((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ c)) = a by A3, ORDINAL3:33; then (a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d) divides a by Def3; then (a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d) divides a hcf b by A6, Def5; then ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)) *^ ((a hcf b) div^ ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d))) = a hcf b by Th7; then (a hcf b) *^ ((((a *^ c) hcf (b *^ c)) div^ d) *^ ((a hcf b) div^ ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d)))) = a hcf b by ORDINAL3:50 .= (a hcf b) *^ 1 by ORDINAL2:39 ; then ( a hcf b = {} or (((a *^ c) hcf (b *^ c)) div^ d) *^ ((a hcf b) div^ ((a hcf b) *^ (((a *^ c) hcf (b *^ c)) div^ d))) = 1 ) by ORDINAL3:33; then ((a *^ c) hcf (b *^ c)) div^ d = 1 by A3, Th15, ORDINAL3:37; hence (a *^ c) hcf (b *^ c) = (a hcf b) *^ c by A5, ORDINAL2:39; ::_thesis: verum end; suppose a = {} ; ::_thesis: (a *^ c) hcf (b *^ c) = (a hcf b) *^ c then ( a hcf b = b & a *^ c = {} ) by Th14, ORDINAL2:35; hence (a *^ c) hcf (b *^ c) = (a hcf b) *^ c by Th14; ::_thesis: verum end; end; end; theorem Th18: :: ARYTM_3:18 for b, a being natural Ordinal st b <> {} holds ( a hcf b <> {} & b div^ (a hcf b) <> {} ) proof let b, a be natural Ordinal; ::_thesis: ( b <> {} implies ( a hcf b <> {} & b div^ (a hcf b) <> {} ) ) a hcf b divides b by Def5; then b = (a hcf b) *^ (b div^ (a hcf b)) by Th7; hence ( b <> {} implies ( a hcf b <> {} & b div^ (a hcf b) <> {} ) ) by ORDINAL2:35; ::_thesis: verum end; theorem Th19: :: ARYTM_3:19 for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds a div^ (a hcf b),b div^ (a hcf b) are_relative_prime proof let a, b be natural Ordinal; ::_thesis: ( ( a <> {} or b <> {} ) implies a div^ (a hcf b),b div^ (a hcf b) are_relative_prime ) assume A1: ( a <> {} or b <> {} ) ; ::_thesis: a div^ (a hcf b),b div^ (a hcf b) are_relative_prime set ab = a hcf b; A2: ( 1 *^ a = a & 1 *^ b = b ) by ORDINAL2:39; percases ( a = {} or b = {} or ( a <> {} & b <> {} ) ) ; suppose ( a = {} or b = {} ) ; ::_thesis: a div^ (a hcf b),b div^ (a hcf b) are_relative_prime then ( ( a hcf b = b & b div^ b = 1 ) or ( a hcf b = a & a div^ a = 1 ) ) by A1, A2, Th14, ORDINAL3:68; hence a div^ (a hcf b),b div^ (a hcf b) are_relative_prime by Th2; ::_thesis: verum end; supposeA3: ( a <> {} & b <> {} ) ; ::_thesis: a div^ (a hcf b),b div^ (a hcf b) are_relative_prime a hcf b divides b by Def5; then A4: b = (a hcf b) *^ (b div^ (a hcf b)) by Th7; then A5: b div^ (a hcf b) <> {} by A3, ORDINAL2:35; let c, d1, d2 be Ordinal; :: according to ARYTM_3:def_2 ::_thesis: ( a div^ (a hcf b) = c *^ d1 & b div^ (a hcf b) = c *^ d2 implies c = 1 ) assume that A6: a div^ (a hcf b) = c *^ d1 and A7: b div^ (a hcf b) = c *^ d2 ; ::_thesis: c = 1 a hcf b divides a by Def5; then A8: a = (a hcf b) *^ (a div^ (a hcf b)) by Th7; then a div^ (a hcf b) <> {} by A3, ORDINAL2:35; then reconsider c = c, d1 = d1, d2 = d2 as Element of omega by A6, A7, A5, ORDINAL3:75; b = ((a hcf b) *^ c) *^ d2 by A4, A7, ORDINAL3:50; then A9: (a hcf b) *^ c divides b by Def3; a = ((a hcf b) *^ c) *^ d1 by A8, A6, ORDINAL3:50; then (a hcf b) *^ c divides a by Def3; then (a hcf b) *^ c divides a hcf b by A9, Def5; then a hcf b = ((a hcf b) *^ c) *^ ((a hcf b) div^ ((a hcf b) *^ c)) by Th7; then a hcf b = (a hcf b) *^ (c *^ ((a hcf b) div^ ((a hcf b) *^ c))) by ORDINAL3:50; then A10: (a hcf b) *^ 1 = (a hcf b) *^ (c *^ ((a hcf b) div^ ((a hcf b) *^ c))) by ORDINAL2:39; a hcf b <> {} by A3, A8, ORDINAL2:35; then 1 = c *^ ((a hcf b) div^ ((a hcf b) *^ c)) by A10, ORDINAL3:33; hence c = 1 by ORDINAL3:37; ::_thesis: verum end; end; end; theorem Th20: :: ARYTM_3:20 for a, b being natural Ordinal holds ( a,b are_relative_prime iff a hcf b = 1 ) proof let a, b be natural Ordinal; ::_thesis: ( a,b are_relative_prime iff a hcf b = 1 ) 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_relative_prime implies a hcf b = 1 ) by A1, Def2; ::_thesis: ( a hcf b = 1 implies a,b are_relative_prime ) assume A2: a hcf b = 1 ; ::_thesis: a,b are_relative_prime let c, d1, d2 be Ordinal; :: according to ARYTM_3:def_2 ::_thesis: ( a = c *^ d1 & b = c *^ d2 implies c = 1 ) assume A3: ( a = c *^ d1 & b = c *^ d2 ) ; ::_thesis: c = 1 ( a <> {} or b <> {} ) by A2, Th14; then reconsider c = c as Element of omega by A3, ORDINAL3:75; ( c divides a & c divides b ) by A3, Def3; then c divides 1 by A2, Def5; then ex d being natural Ordinal st 1 = c *^ d by Th5; hence c = 1 by ORDINAL3:37; ::_thesis: verum end; definition let a, b be natural Ordinal; func RED (a,b) -> Element of omega equals :: ARYTM_3:def 6 a div^ (a hcf b); coherence a div^ (a hcf b) is Element of omega by ORDINAL1:def_12; end; :: deftheorem defines RED ARYTM_3:def_6_:_ for a, b being natural Ordinal holds RED (a,b) = a div^ (a hcf b); theorem Th21: :: ARYTM_3:21 for a, b being natural Ordinal holds (RED (a,b)) *^ (a hcf b) = a proof let a, b be natural Ordinal; ::_thesis: (RED (a,b)) *^ (a hcf b) = a a hcf b divides a by Def5; hence (RED (a,b)) *^ (a hcf b) = a by Th7; ::_thesis: verum end; theorem :: ARYTM_3:22 for a, b being natural Ordinal st ( a <> {} or b <> {} ) holds RED (a,b), RED (b,a) are_relative_prime by Th19; theorem Th23: :: ARYTM_3:23 for a, b being natural Ordinal st a,b are_relative_prime holds RED (a,b) = a proof let a, b be natural Ordinal; ::_thesis: ( a,b are_relative_prime implies RED (a,b) = a ) assume a,b are_relative_prime ; ::_thesis: RED (a,b) = a then a hcf b = 1 by Th20; hence RED (a,b) = a by ORDINAL3:71; ::_thesis: verum end; theorem Th24: :: ARYTM_3:24 for a being natural Ordinal holds ( RED (a,1) = a & RED (1,a) = 1 ) proof let a be natural Ordinal; ::_thesis: ( RED (a,1) = a & RED (1,a) = 1 ) a,1 are_relative_prime by Th2; then a hcf 1 = 1 by Th20; hence ( RED (a,1) = a & RED (1,a) = 1 ) by ORDINAL3:71; ::_thesis: verum end; theorem :: ARYTM_3:25 for b, a being natural Ordinal st b <> {} holds RED (b,a) <> {} by Th18; theorem Th26: :: ARYTM_3:26 for a being natural Ordinal holds ( RED ({},a) = {} & ( a <> {} implies RED (a,{}) = 1 ) ) proof let a be natural Ordinal; ::_thesis: ( RED ({},a) = {} & ( a <> {} implies RED (a,{}) = 1 ) ) thus RED ({},a) = {} by ORDINAL3:70; ::_thesis: ( a <> {} implies RED (a,{}) = 1 ) assume A1: a <> {} ; ::_thesis: RED (a,{}) = 1 thus RED (a,{}) = a div^ a by Th14 .= (a *^ 1) div^ a by ORDINAL2:39 .= 1 by A1, ORDINAL3:68 ; ::_thesis: verum end; theorem Th27: :: ARYTM_3:27 for a being natural Ordinal st a <> {} holds RED (a,a) = 1 proof let a be natural Ordinal; ::_thesis: ( a <> {} implies RED (a,a) = 1 ) assume A1: a <> {} ; ::_thesis: RED (a,a) = 1 thus RED (a,a) = a div^ a by Th16 .= (a *^ 1) div^ a by ORDINAL2:39 .= 1 by A1, ORDINAL3:68 ; ::_thesis: verum end; theorem Th28: :: ARYTM_3:28 for c, a, b being natural Ordinal st c <> {} holds RED ((a *^ c),(b *^ c)) = RED (a,b) proof let c, a, b be natural Ordinal; ::_thesis: ( c <> {} implies RED ((a *^ c),(b *^ c)) = RED (a,b) ) assume A1: c <> {} ; ::_thesis: RED ((a *^ c),(b *^ c)) = RED (a,b) ( 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, ORDINAL3:70 ; ::_thesis: verum end; set RATplus = { [a,b] where a, b is Element of omega : ( a,b are_relative_prime & b <> {} ) } ; 1,1 are_relative_prime by Th2; then [1,1] in { [a,b] where a, b is Element of omega : ( a,b are_relative_prime & b <> {} ) } ; then reconsider RATplus = { [a,b] where a, b is Element of omega : ( a,b are_relative_prime & b <> {} ) } as non empty set ; Lm4: for a, b being natural Ordinal st [a,b] in RATplus holds ( a,b are_relative_prime & b <> {} ) proof let a, b be natural Ordinal; ::_thesis: ( [a,b] in RATplus implies ( a,b are_relative_prime & b <> {} ) ) assume [a,b] in RATplus ; ::_thesis: ( a,b are_relative_prime & b <> {} ) then consider c, d being Element of omega such that A1: [a,b] = [c,d] and A2: ( c,d are_relative_prime & d <> {} ) ; a = c by A1, XTUPLE_0:1; hence ( a,b are_relative_prime & b <> {} ) by A1, A2, XTUPLE_0:1; ::_thesis: verum end; begin definition func RAT+ -> set equals :: ARYTM_3:def 7 ( { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega; correctness coherence ( { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega is set ; ; end; :: deftheorem defines RAT+ ARYTM_3:def_7_:_ RAT+ = ( { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega; Lm5: omega c= RAT+ by XBOOLE_1:7; registration cluster RAT+ -> non empty ; coherence not RAT+ is empty ; end; registration cluster non empty ordinal for Element of RAT+ ; existence ex b1 being Element of RAT+ st ( not b1 is empty & b1 is ordinal ) by Lm2, Lm5; end; theorem Th29: :: ARYTM_3:29 for x being Element of RAT+ holds ( x in omega or ex i, j being Element of omega st ( x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) ) proof let x be Element of RAT+ ; ::_thesis: ( x in omega or ex i, j being Element of omega st ( x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) ) assume not x in omega ; ::_thesis: ex i, j being Element of omega st ( x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) then A1: x in RATplus \ { [k,1] where k is Element of omega : verum } by XBOOLE_0:def_3; then A2: not x in { [k,1] where k is Element of omega : verum } 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_relative_prime & b <> {} ) ; [a,1] in { [k,1] where k is Element of omega : verum } ; hence ex i, j being Element of omega st ( x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) by A2, A3; ::_thesis: verum end; theorem Th30: :: ARYTM_3:30 for i, j being set holds [i,j] is not Ordinal proof given i, j being set such that A1: [i,j] is Ordinal ; ::_thesis: contradiction {} in [i,j] by A1, ORDINAL3:8; hence contradiction by TARSKI:def_2; ::_thesis: verum end; theorem Th31: :: ARYTM_3:31 for A being Ordinal st A in RAT+ holds A in omega proof let A be Ordinal; ::_thesis: ( A in RAT+ implies A in omega ) assume ( A in RAT+ & not A in omega ) ; ::_thesis: contradiction then ex i, j being Element of omega st ( A = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) by Th29; hence contradiction by Th30; ::_thesis: verum end; registration cluster ordinal -> ordinal natural for Element of RAT+ ; coherence for b1 being ordinal Element of RAT+ holds b1 is natural proof let x be ordinal Element of RAT+ ; ::_thesis: x is natural assume not x in omega ; :: according to ORDINAL1:def_12 ::_thesis: contradiction then A1: ex i, j being Element of omega st ( x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) by Th29; then {} in x by ORDINAL3:8; hence contradiction by A1, TARSKI:def_2; ::_thesis: verum end; end; theorem Th32: :: ARYTM_3:32 for i, j being set holds not [i,j] in omega proof given i, j being set such that A1: [i,j] in omega ; ::_thesis: contradiction reconsider a = [i,j] as Element of omega by A1; {} in a by ORDINAL3:8; hence contradiction by TARSKI:def_2; ::_thesis: verum end; theorem Th33: :: ARYTM_3:33 for i, j being Element of omega holds ( [i,j] in RAT+ iff ( i,j are_relative_prime & j <> {} & j <> 1 ) ) proof let i, j be Element of omega ; ::_thesis: ( [i,j] in RAT+ iff ( i,j are_relative_prime & j <> {} & j <> 1 ) ) A1: not [i,j] in omega by Th32; hereby ::_thesis: ( i,j are_relative_prime & j <> {} & j <> 1 implies [i,j] in RAT+ ) assume [i,j] in RAT+ ; ::_thesis: ( i,j are_relative_prime & j <> {} & j <> 1 ) then A2: [i,j] in RATplus \ { [k,1] where k is Element of omega : verum } by A1, XBOOLE_0:def_3; hence ( i,j are_relative_prime & j <> {} ) by Lm4; ::_thesis: j <> 1 not [i,j] in { [k,1] where k is Element of omega : verum } by A2, XBOOLE_0:def_5; hence j <> 1 ; ::_thesis: verum end; assume ( i,j are_relative_prime & j <> {} ) ; ::_thesis: ( not j <> 1 or [i,j] in RAT+ ) then A3: [i,j] in RATplus ; assume j <> 1 ; ::_thesis: [i,j] in RAT+ then for k being Element of omega holds not [i,j] = [k,1] by XTUPLE_0:1; then not [i,j] in { [k,1] where k is Element of omega : verum } ; then [i,j] in RATplus \ { [k,1] where k is Element of omega : verum } by A3, XBOOLE_0:def_5; hence [i,j] in RAT+ by XBOOLE_0:def_3; ::_thesis: verum end; definition let x be Element of RAT+ ; func numerator x -> Element of omega means :Def8: :: ARYTM_3:def 8 it = x if x in omega otherwise ex a being natural Ordinal st x = [it,a]; existence ( ( x in omega implies ex b1 being Element of omega st b1 = x ) & ( not x in omega implies ex b1 being Element of omega ex a being natural Ordinal st x = [b1,a] ) ) proof thus ( x in omega implies ex a being Element of omega st a = x ) ; ::_thesis: ( not x in omega implies ex b1 being Element of omega ex a being natural Ordinal st x = [b1,a] ) assume not x in omega ; ::_thesis: ex b1 being Element of omega ex a being natural Ordinal st x = [b1,a] then x in RATplus \ { [k,1] where k is Element of omega : verum } 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_relative_prime and b <> {} ; take a ; ::_thesis: ex a being natural Ordinal st x = [a,a] take b ; ::_thesis: x = [a,b] thus x = [a,b] by A1; ::_thesis: verum end; correctness consistency for b1 being Element of omega holds verum; uniqueness for b1, b2 being Element of omega holds ( ( x in omega & b1 = x & b2 = x implies b1 = b2 ) & ( not x in omega & ex a being natural Ordinal st x = [b1,a] & ex a being natural Ordinal st x = [b2,a] implies b1 = b2 ) ); by XTUPLE_0:1; func denominator x -> Element of omega means :Def9: :: ARYTM_3:def 9 it = 1 if x in omega otherwise ex a being natural Ordinal st x = [a,it]; existence ( ( x in omega implies ex b1 being Element of omega st b1 = 1 ) & ( not x in omega implies ex b1 being Element of omega ex a being natural Ordinal st x = [a,b1] ) ) proof thus ( x in omega implies ex a being Element of omega st a = 1 ) ; ::_thesis: ( not x in omega implies ex b1 being Element of omega ex a being natural Ordinal st x = [a,b1] ) assume not x in omega ; ::_thesis: ex b1 being Element of omega ex a being natural Ordinal st x = [a,b1] then x in RATplus \ { [k,1] where k is Element of omega : verum } 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_relative_prime and b <> {} ; take b ; ::_thesis: ex a being natural Ordinal st x = [a,b] take a ; ::_thesis: x = [a,b] thus x = [a,b] by A2; ::_thesis: verum end; correctness consistency for b1 being Element of omega holds verum; uniqueness for b1, b2 being Element of omega holds ( ( x in omega & b1 = 1 & b2 = 1 implies b1 = b2 ) & ( not x in omega & ex a being natural Ordinal st x = [a,b1] & ex a being natural Ordinal st x = [a,b2] implies b1 = b2 ) ); by XTUPLE_0:1; end; :: deftheorem Def8 defines numerator ARYTM_3:def_8_:_ for x being Element of RAT+ for b2 being Element of omega holds ( ( x in omega implies ( b2 = numerator x iff b2 = x ) ) & ( not x in omega implies ( b2 = numerator x iff ex a being natural Ordinal st x = [b2,a] ) ) ); :: deftheorem Def9 defines denominator ARYTM_3:def_9_:_ for x being Element of RAT+ for b2 being Element of omega holds ( ( x in omega implies ( b2 = denominator x iff b2 = 1 ) ) & ( not x in omega implies ( b2 = denominator x iff ex a being natural Ordinal st x = [a,b2] ) ) ); theorem Th34: :: ARYTM_3:34 for x being Element of RAT+ holds numerator x, denominator x are_relative_prime proof let x be Element of RAT+ ; ::_thesis: numerator x, denominator x are_relative_prime percases ( x in omega or not x in omega ) ; suppose x in omega ; ::_thesis: numerator x, denominator x are_relative_prime then denominator x = 1 by Def9; hence numerator x, denominator x are_relative_prime by Th2; ::_thesis: verum end; supposeA1: not x in omega ; ::_thesis: numerator x, denominator x are_relative_prime then consider i, j being Element of omega such that A2: x = [i,j] and A3: i,j are_relative_prime and j <> {} and j <> 1 by Th29; i = numerator x by A1, A2, Def8; hence numerator x, denominator x are_relative_prime by A1, A2, A3, Def9; ::_thesis: verum end; end; end; theorem Th35: :: ARYTM_3:35 for x being Element of RAT+ holds denominator x <> {} proof let x be Element of RAT+ ; ::_thesis: denominator x <> {} percases ( x in omega or not x in omega ) ; suppose x in omega ; ::_thesis: denominator x <> {} hence denominator x <> {} by Def9; ::_thesis: verum end; supposeA1: not x in omega ; ::_thesis: denominator x <> {} then ex i, j being Element of omega st ( x = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) by Th29; hence denominator x <> {} by A1, Def9; ::_thesis: verum end; end; end; theorem Th36: :: ARYTM_3:36 for x being Element of RAT+ st not x in omega holds ( x = [(numerator x),(denominator x)] & denominator x <> 1 ) proof let x be Element of RAT+ ; ::_thesis: ( not x in omega implies ( x = [(numerator x),(denominator x)] & denominator x <> 1 ) ) assume A1: not x in omega ; ::_thesis: ( x = [(numerator x),(denominator x)] & denominator x <> 1 ) then consider i, j being Element of omega such that A2: x = [i,j] and i,j are_relative_prime and j <> {} and A3: j <> 1 by Th29; i = numerator x by A1, A2, Def8; hence ( x = [(numerator x),(denominator x)] & denominator x <> 1 ) by A1, A2, A3, Def9; ::_thesis: verum end; theorem Th37: :: ARYTM_3:37 for x being Element of RAT+ holds ( x <> {} iff numerator x <> {} ) proof let x be Element of RAT+ ; ::_thesis: ( x <> {} iff numerator x <> {} ) hereby ::_thesis: ( numerator x <> {} implies x <> {} ) assume that A1: x <> {} and A2: numerator x = {} ; ::_thesis: contradiction A3: not x in omega by A1, A2, Def8; then consider i, j being Element of omega such that A4: x = [i,j] and A5: i,j are_relative_prime and j <> {} and A6: j <> 1 by Th29; i = {} by A2, A3, A4, Def8; hence contradiction by A5, A6, Th3; ::_thesis: verum end; {} in omega by ORDINAL1:def_11; hence ( numerator x <> {} implies x <> {} ) by Def8; ::_thesis: verum end; theorem :: ARYTM_3:38 for x being Element of RAT+ holds ( x in omega iff denominator x = 1 ) by Def9, Th36; definition let i, j be natural Ordinal; funci / j -> Element of RAT+ equals :Def10: :: ARYTM_3:def 10 {} if j = {} RED (i,j) if RED (j,i) = 1 otherwise [(RED (i,j)),(RED (j,i))]; coherence ( ( j = {} implies {} is Element of RAT+ ) & ( RED (j,i) = 1 implies RED (i,j) is Element of RAT+ ) & ( not j = {} & not RED (j,i) = 1 implies [(RED (i,j)),(RED (j,i))] is Element of RAT+ ) ) proof A1: now__::_thesis:_(_j_<>_{}_&_RED_(j,i)_<>_1_implies_[(RED_(i,j)),(RED_(j,i))]_in_RAT+_) assume j <> {} ; ::_thesis: ( RED (j,i) <> 1 implies [(RED (i,j)),(RED (j,i))] in RAT+ ) then ( RED (i,j), RED (j,i) are_relative_prime & RED (j,i) <> {} ) by Th18, Th19; hence ( RED (j,i) <> 1 implies [(RED (i,j)),(RED (j,i))] in RAT+ ) by Th33; ::_thesis: verum end; RED (i,j) in omega ; hence ( ( j = {} implies {} is Element of RAT+ ) & ( RED (j,i) = 1 implies RED (i,j) is Element of RAT+ ) & ( not j = {} & not RED (j,i) = 1 implies [(RED (i,j)),(RED (j,i))] is Element of RAT+ ) ) by A1, Lm1, Lm5; ::_thesis: verum end; consistency for b1 being Element of RAT+ st j = {} & RED (j,i) = 1 holds ( b1 = {} iff b1 = RED (i,j) ) by Th26; end; :: deftheorem Def10 defines / ARYTM_3:def_10_:_ for i, j being natural Ordinal holds ( ( j = {} implies i / j = {} ) & ( RED (j,i) = 1 implies i / j = RED (i,j) ) & ( not j = {} & not RED (j,i) = 1 implies i / j = [(RED (i,j)),(RED (j,i))] ) ); notation let i, j be natural Ordinal; synonym quotient (i,j) for i / j; end; theorem Th39: :: ARYTM_3:39 for x being Element of RAT+ holds (numerator x) / (denominator x) = x proof let x be Element of RAT+ ; ::_thesis: (numerator x) / (denominator x) = x A1: denominator x <> {} by Th35; A2: RED ((numerator x),(denominator x)) = numerator x by Th23, Th34; numerator x, denominator x are_relative_prime by Th34; then A3: RED ((denominator x),(numerator x)) = denominator x by Th23; percases ( denominator x = 1 or denominator x <> 1 ) ; supposeA4: denominator x = 1 ; ::_thesis: (numerator x) / (denominator x) = x then x in omega by Th36; then numerator x = x by Def8; hence (numerator x) / (denominator x) = x by A2, A3, A4, Def10; ::_thesis: verum end; supposeA5: denominator x <> 1 ; ::_thesis: (numerator x) / (denominator x) = x then not x in omega by Def9; then x = [(numerator x),(denominator x)] by Th36; hence (numerator x) / (denominator x) = x by A1, A2, A3, A5, Def10; ::_thesis: verum end; end; end; theorem Th40: :: ARYTM_3:40 for b, a being natural Ordinal holds ( {} / b = {} & a / 1 = a ) proof let b, a be natural Ordinal; ::_thesis: ( {} / b = {} & a / 1 = a ) A1: ( b <> {} implies RED (b,{}) = 1 ) by Th26; RED ({},b) = {} by Th26; hence {} / b = {} by A1, Def10; ::_thesis: a / 1 = a ( RED (1,a) = 1 & RED (a,1) = a ) by Th24; hence a / 1 = a by Def10; ::_thesis: verum end; theorem Th41: :: ARYTM_3:41 for a being natural Ordinal st a <> {} holds a / a = 1 proof let a be natural Ordinal; ::_thesis: ( a <> {} implies a / a = 1 ) assume a <> {} ; ::_thesis: a / a = 1 then RED (a,a) = 1 by Th27; hence a / a = 1 by Def10; ::_thesis: verum end; theorem Th42: :: ARYTM_3:42 for b, a being natural Ordinal st b <> {} holds ( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) ) proof let b, a be natural Ordinal; ::_thesis: ( b <> {} implies ( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) ) ) assume A1: b <> {} ; ::_thesis: ( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) ) percases ( RED (b,a) = 1 or RED (b,a) <> 1 ) ; supposeA2: RED (b,a) = 1 ; ::_thesis: ( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) ) then a / b = RED (a,b) by Def10; hence ( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) ) by A2, Def8, Def9; ::_thesis: verum end; supposeA3: RED (b,a) <> 1 ; ::_thesis: ( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) ) 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 ( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) ) by A4, Def8, Def9; ::_thesis: verum end; end; end; theorem Th43: :: ARYTM_3:43 for i, j being Element of omega st i,j are_relative_prime & j <> {} holds ( numerator (i / j) = i & denominator (i / j) = j ) proof let i, j be Element of omega ; ::_thesis: ( i,j are_relative_prime & j <> {} implies ( numerator (i / j) = i & denominator (i / j) = j ) ) assume i,j are_relative_prime ; ::_thesis: ( not j <> {} or ( numerator (i / j) = i & denominator (i / j) = j ) ) then ( RED (i,j) = i & RED (j,i) = j ) by Th23; hence ( not j <> {} or ( numerator (i / j) = i & denominator (i / j) = j ) ) by Th42; ::_thesis: verum end; theorem Th44: :: ARYTM_3:44 for c, a, b being natural Ordinal st c <> {} holds (a *^ c) / (b *^ c) = a / b proof let c, a, b be natural Ordinal; ::_thesis: ( c <> {} implies (a *^ c) / (b *^ c) = a / b ) assume A1: c <> {} ; ::_thesis: (a *^ c) / (b *^ c) = a / b percases ( b = {} or b <> {} ) ; suppose b = {} ; ::_thesis: (a *^ c) / (b *^ c) = a / b then ( a / b = {} & b *^ c = {} ) by Def10, ORDINAL2:35; hence (a *^ c) / (b *^ c) = a / b by Def10; ::_thesis: verum end; supposeA2: b <> {} ; ::_thesis: (a *^ c) / (b *^ c) = a / 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 ; ::_thesis: verum end; end; end; theorem Th45: :: ARYTM_3:45 for l, j, i, k being natural Ordinal st j <> {} & l <> {} holds ( i / j = k / l iff i *^ l = j *^ k ) proof let l, j, i, k be natural Ordinal; ::_thesis: ( j <> {} & l <> {} implies ( i / j = k / l iff i *^ l = j *^ k ) ) assume that A1: j <> {} and A2: l <> {} ; ::_thesis: ( i / j = k / l iff i *^ l = j *^ k ) set x = i / j; set y = k / l; set ny = numerator (k / l); set dy = denominator (k / l); A3: numerator (k / l) = RED (k,l) by A2, Th42; set nx = numerator (i / j); set dx = denominator (i / j); A4: denominator (i / j) = RED (j,i) by A1, Th42; A5: denominator (k / l) = RED (l,k) by A2, Th42; A6: numerator (i / j) = RED (i,j) by A1, Th42; hereby ::_thesis: ( i *^ l = j *^ k implies i / j = k / l ) assume i / j = k / l ; ::_thesis: i *^ l = j *^ k then ( i = (numerator (k / l)) *^ (i hcf j) & l = (denominator (i / j)) *^ (l hcf k) ) by A6, A5, Th21; hence i *^ l = (((numerator (k / l)) *^ (i hcf j)) *^ (denominator (i / j))) *^ (l hcf k) by ORDINAL3:50 .= ((numerator (k / l)) *^ ((i hcf j) *^ (denominator (i / j)))) *^ (l hcf k) by ORDINAL3:50 .= ((numerator (k / l)) *^ j) *^ (l hcf k) by A4, Th21 .= j *^ ((numerator (k / l)) *^ (l hcf k)) by ORDINAL3:50 .= j *^ k by A3, Th21 ; ::_thesis: verum end; assume A7: i *^ l = j *^ k ; ::_thesis: i / j = k / l then denominator (i / j) = RED ((j *^ l),(j *^ k)) by A2, A4, Th28; then A8: denominator (i / j) = denominator (k / l) by A1, A5, Th28; numerator (i / j) = RED ((j *^ k),(j *^ l)) by A2, A6, A7, Th28; then numerator (i / j) = numerator (k / l) by A1, A3, Th28; then i / j = (numerator (k / l)) / (denominator (k / l)) by A8, Th39; hence i / j = k / l by Th39; ::_thesis: verum end; definition let x, y be Element of RAT+ ; funcx + y -> Element of RAT+ equals :: ARYTM_3:def 11 (((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y)); coherence (((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y)) is Element of RAT+ ; commutativity for b1, x, y being Element of RAT+ st b1 = (((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y)) holds b1 = (((numerator y) *^ (denominator x)) +^ ((numerator x) *^ (denominator y))) / ((denominator y) *^ (denominator x)) ; funcx *' y -> Element of RAT+ equals :: ARYTM_3:def 12 ((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y)); coherence ((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y)) is Element of RAT+ ; commutativity for b1, x, y being Element of RAT+ st b1 = ((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y)) holds b1 = ((numerator y) *^ (numerator x)) / ((denominator y) *^ (denominator x)) ; end; :: deftheorem defines + ARYTM_3:def_11_:_ for x, y being Element of RAT+ holds x + y = (((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y)); :: deftheorem defines *' ARYTM_3:def_12_:_ for x, y being Element of RAT+ holds x *' y = ((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y)); theorem Th46: :: ARYTM_3:46 for l, j, i, k being natural Ordinal st j <> {} & l <> {} holds (i / j) + (k / l) = ((i *^ l) +^ (j *^ k)) / (j *^ l) proof let l, j, i, k be natural Ordinal; ::_thesis: ( j <> {} & l <> {} implies (i / j) + (k / l) = ((i *^ l) +^ (j *^ k)) / (j *^ l) ) assume that A1: j <> {} and A2: l <> {} ; ::_thesis: (i / j) + (k / l) = ((i *^ l) +^ (j *^ k)) / (j *^ 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 ; ::_thesis: verum end; theorem Th47: :: ARYTM_3:47 for k, i, j being natural Ordinal st k <> {} holds (i / k) + (j / k) = (i +^ j) / k proof let k, i, j be natural Ordinal; ::_thesis: ( k <> {} implies (i / k) + (j / k) = (i +^ j) / k ) assume A1: k <> {} ; ::_thesis: (i / k) + (j / k) = (i +^ j) / 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 ; ::_thesis: verum end; registration cluster empty for Element of RAT+ ; existence ex b1 being Element of RAT+ st b1 is empty by Lm1, Lm5; end; definition :: original: {} redefine func {} -> Element of RAT+ ; coherence {} is Element of RAT+ by Lm1, Lm5; :: original: one redefine func one -> non empty ordinal Element of RAT+ ; coherence one is non empty ordinal Element of RAT+ by Lm2, Lm5; end; theorem Th48: :: ARYTM_3:48 for x being Element of RAT+ holds x *' {} = {} proof let x be Element of RAT+ ; ::_thesis: x *' {} = {} ( numerator {} = {} & (numerator x) *^ {} = {} ) by Def8, Lm1, ORDINAL2:35; hence x *' {} = {} by Th40; ::_thesis: verum end; theorem Th49: :: ARYTM_3:49 for l, i, j, k being natural Ordinal holds (i / j) *' (k / l) = (i *^ k) / (j *^ l) proof let l, i, j, k be natural Ordinal; ::_thesis: (i / j) *' (k / l) = (i *^ k) / (j *^ l) percases ( ( j <> {} & l <> {} ) or j = {} or l = {} ) ; supposeA1: ( j <> {} & l <> {} ) ; ::_thesis: (i / j) *' (k / l) = (i *^ k) / (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 ; ::_thesis: verum end; supposeA3: ( j = {} or l = {} ) ; ::_thesis: (i / j) *' (k / l) = (i *^ k) / (j *^ l) then ( i / j = {} or k / l = {} ) by Def10; then A4: (i / j) *' (k / l) = {} by Th48; j *^ l = {} by A3, ORDINAL2:35; hence (i / j) *' (k / l) = (i *^ k) / (j *^ l) by A4, Def10; ::_thesis: verum end; end; end; theorem Th50: :: ARYTM_3:50 for x being Element of RAT+ holds x + {} = x proof let x be Element of RAT+ ; ::_thesis: x + {} = x A1: ( (numerator x) *^ 1 = numerator x & {} *^ (denominator x) = {} ) by ORDINAL2:35, ORDINAL2:39; A2: ( (denominator x) *^ 1 = denominator x & (numerator x) +^ {} = numerator x ) by ORDINAL2:27, ORDINAL2:39; ( denominator {} = 1 & numerator {} = {} ) by Def8, Def9, Lm1; hence x + {} = x by A1, A2, Th39; ::_thesis: verum end; theorem Th51: :: ARYTM_3:51 for x, y, z being Element of RAT+ holds (x + y) + z = x + (y + z) proof let x, y, z be Element of RAT+ ; ::_thesis: (x + y) + z = x + (y + z) set nx = numerator x; set ny = numerator y; set nz = numerator z; set dx = denominator x; set dy = denominator y; set dz = denominator z; A1: denominator y <> {} by Th35; A2: denominator z <> {} by Th35; then A3: (denominator y) *^ (denominator z) <> {} by A1, ORDINAL3:31; A4: denominator x <> {} by Th35; then A5: (denominator x) *^ (denominator y) <> {} by A1, ORDINAL3:31; thus (x + y) + z = ((((numerator x) *^ (denominator y)) +^ ((denominator x) *^ (numerator y))) / ((denominator x) *^ (denominator y))) + ((numerator z) / (denominator z)) by Th39 .= (((((numerator x) *^ (denominator y)) +^ ((denominator x) *^ (numerator y))) *^ (denominator z)) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by A2, A5, Th46 .= (((((numerator x) *^ (denominator y)) *^ (denominator z)) +^ (((denominator x) *^ (numerator y)) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:46 .= ((((numerator x) *^ ((denominator y) *^ (denominator z))) +^ (((denominator x) *^ (numerator y)) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:50 .= ((((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ ((numerator y) *^ (denominator z)))) +^ (((denominator x) *^ (denominator y)) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:50 .= ((((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ ((numerator y) *^ (denominator z)))) +^ ((denominator x) *^ ((denominator y) *^ (numerator z)))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:50 .= (((numerator x) *^ ((denominator y) *^ (denominator z))) +^ (((denominator x) *^ ((numerator y) *^ (denominator z))) +^ ((denominator x) *^ ((denominator y) *^ (numerator z))))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:30 .= (((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ (((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z))))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:46 .= (((numerator x) *^ ((denominator y) *^ (denominator z))) +^ ((denominator x) *^ (((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z))))) / ((denominator x) *^ ((denominator y) *^ (denominator z))) by ORDINAL3:50 .= ((((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z))) / ((denominator y) *^ (denominator z))) + ((numerator x) / (denominator x)) by A4, A3, Th46 .= x + (y + z) by Th39 ; ::_thesis: verum end; theorem Th52: :: ARYTM_3:52 for x, y, z being Element of RAT+ holds (x *' y) *' z = x *' (y *' z) proof let x, y, z be Element of RAT+ ; ::_thesis: (x *' y) *' z = x *' (y *' z) set nx = numerator x; set ny = numerator y; set nz = numerator z; set dx = denominator x; set dy = denominator y; set dz = denominator z; A1: x = (numerator x) / (denominator x) by Th39; z = (numerator z) / (denominator z) by Th39; hence (x *' y) *' z = (((numerator x) *^ (numerator y)) *^ (numerator z)) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by Th49 .= ((numerator x) *^ ((numerator y) *^ (numerator z))) / (((denominator x) *^ (denominator y)) *^ (denominator z)) by ORDINAL3:50 .= ((numerator x) *^ ((numerator y) *^ (numerator z))) / ((denominator x) *^ ((denominator y) *^ (denominator z))) by ORDINAL3:50 .= x *' (y *' z) by A1, Th49 ; ::_thesis: verum end; theorem Th53: :: ARYTM_3:53 for x being Element of RAT+ holds x *' one = x proof let x be Element of RAT+ ; ::_thesis: x *' one = x set y = one ; A1: ( (numerator x) *^ 1 = numerator x & (denominator x) *^ 1 = denominator x ) by ORDINAL2:39; ( numerator one = 1 & denominator one = 1 ) by Def8, Def9; hence x *' one = x by A1, Th39; ::_thesis: verum end; theorem Th54: :: ARYTM_3:54 for x being Element of RAT+ st x <> {} holds ex y being Element of RAT+ st x *' y = 1 proof let x be Element of RAT+ ; ::_thesis: ( x <> {} implies ex y being Element of RAT+ st x *' y = 1 ) set nx = numerator x; set dx = denominator x; A1: denominator x <> {} by Th35; assume x <> {} ; ::_thesis: ex y being Element of RAT+ st x *' y = 1 then A2: numerator x <> {} by Th37; take y = (denominator x) / (numerator x); ::_thesis: x *' y = 1 numerator x, denominator x are_relative_prime by Th34; then ( denominator y = numerator x & numerator y = denominator x ) by A2, Th43; hence x *' y = 1 by A2, A1, Th41, ORDINAL3:31; ::_thesis: verum end; theorem Th55: :: ARYTM_3:55 for x, y being Element of RAT+ st x <> {} holds ex z being Element of RAT+ st y = x *' z proof let x, y be Element of RAT+ ; ::_thesis: ( x <> {} implies ex z being Element of RAT+ st y = x *' z ) reconsider o = one as Element of RAT+ ; assume x <> {} ; ::_thesis: ex z being Element of RAT+ st y = x *' z then consider z being Element of RAT+ such that A1: x *' z = 1 by Th54; take z *' y ; ::_thesis: y = x *' (z *' y) thus y = y *' o by Th53 .= x *' (z *' y) by A1, Th52 ; ::_thesis: verum end; theorem Th56: :: ARYTM_3:56 for x, y, z being Element of RAT+ st x <> {} & x *' y = x *' z holds y = z proof let x, y, z be Element of RAT+ ; ::_thesis: ( x <> {} & x *' y = x *' z implies y = z ) assume x <> {} ; ::_thesis: ( not x *' y = x *' z or y = z ) 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 ( not x *' y = x *' z or y = z ) by A2, Th53; ::_thesis: verum end; theorem Th57: :: ARYTM_3:57 for x, y, z being Element of RAT+ holds x *' (y + z) = (x *' y) + (x *' z) proof let x, y, z be Element of RAT+ ; ::_thesis: x *' (y + z) = (x *' y) + (x *' z) set nx = numerator x; set ny = numerator y; set nz = numerator z; set dx = denominator x; set dy = denominator y; set dz = denominator z; A1: denominator x <> {} by Th35; denominator z <> {} by Th35; then A2: (denominator x) *^ (denominator z) <> {} by A1, ORDINAL3:31; denominator y <> {} by Th35; then A3: (denominator x) *^ (denominator y) <> {} by A1, ORDINAL3:31; x = (numerator x) / (denominator x) by Th39; hence x *' (y + z) = ((numerator x) *^ (((numerator y) *^ (denominator z)) +^ ((denominator y) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ (denominator z))) by Th49 .= (((numerator x) *^ ((numerator y) *^ (denominator z))) +^ ((numerator x) *^ ((denominator y) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ (denominator z))) by ORDINAL3:46 .= ((((numerator x) *^ (numerator y)) *^ (denominator z)) +^ ((numerator x) *^ ((denominator y) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ (denominator z))) by ORDINAL3:50 .= ((((numerator x) *^ (numerator y)) *^ (denominator z)) +^ ((denominator y) *^ ((numerator x) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ (denominator z))) by ORDINAL3:50 .= ((((numerator x) *^ (numerator y)) *^ (denominator z)) +^ ((denominator y) *^ ((numerator x) *^ (numerator z)))) / ((denominator y) *^ ((denominator x) *^ (denominator z))) by ORDINAL3:50 .= ((denominator x) *^ ((((numerator x) *^ (numerator y)) *^ (denominator z)) +^ ((denominator y) *^ ((numerator x) *^ (numerator z))))) / ((denominator x) *^ ((denominator y) *^ ((denominator x) *^ (denominator z)))) by Th35, Th44 .= (((denominator x) *^ (((numerator x) *^ (numerator y)) *^ (denominator z))) +^ ((denominator x) *^ ((denominator y) *^ ((numerator x) *^ (numerator z))))) / ((denominator x) *^ ((denominator y) *^ ((denominator x) *^ (denominator z)))) by ORDINAL3:46 .= (((denominator x) *^ (((numerator x) *^ (numerator y)) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ ((numerator x) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ ((denominator x) *^ (denominator z)))) by ORDINAL3:50 .= ((((numerator x) *^ (numerator y)) *^ ((denominator x) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ ((numerator x) *^ (numerator z)))) / ((denominator x) *^ ((denominator y) *^ ((denominator x) *^ (denominator z)))) by ORDINAL3:50 .= ((((numerator x) *^ (numerator y)) *^ ((denominator x) *^ (denominator z))) +^ (((denominator x) *^ (denominator y)) *^ ((numerator x) *^ (numerator z)))) / (((denominator x) *^ (denominator y)) *^ ((denominator x) *^ (denominator z))) by ORDINAL3:50 .= (x *' y) + (x *' z) by A2, A3, Th46 ; ::_thesis: verum end; theorem Th58: :: ARYTM_3:58 for i, j being ordinal Element of RAT+ holds i + j = i +^ j proof let i, j be ordinal Element of RAT+ ; ::_thesis: i + j = i +^ j set ni = numerator i; set 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 = (((numerator i) *^ 1) +^ (1 *^ (numerator j))) / 1 by A2, ORDINAL2:39 .= ((numerator i) +^ (1 *^ (numerator j))) / 1 by ORDINAL2:39 .= ((numerator i) +^ (numerator j)) / 1 by ORDINAL2:39 .= (numerator i) +^ (numerator j) by Th40 .= i +^ (numerator j) by A3, Def8 .= i +^ j by A1, Def8 ; ::_thesis: verum end; theorem :: ARYTM_3:59 for i, j being ordinal Element of RAT+ holds i *' j = i *^ j proof let i, j be ordinal Element of RAT+ ; ::_thesis: i *' j = i *^ j set ni = numerator i; set 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 = ((numerator i) *^ (numerator j)) / 1 by A2, ORDINAL2:39 .= (numerator i) *^ (numerator j) by Th40 .= i *^ (numerator j) by A3, Def8 .= i *^ j by A1, Def8 ; ::_thesis: verum end; theorem Th60: :: ARYTM_3:60 for x being Element of RAT+ ex y being Element of RAT+ st x = y + y proof let x be Element of RAT+ ; ::_thesis: ex y being Element of RAT+ st x = y + y set 02 = one + one; one + one = 1 +^ 1 by Th58; then one + one <> {} by ORDINAL3:26; then consider z being Element of RAT+ such that A1: (one + one) *' z = 1 by Th54; take y = z *' x; ::_thesis: x = y + y thus x = one *' x by Th53 .= (one + one) *' y by A1, Th52 .= (one *' y) + (one *' y) by Th57 .= y + (one *' y) by Th53 .= y + y by Th53 ; ::_thesis: verum end; definition let x, y be Element of RAT+ ; predx <=' y means :Def13: :: ARYTM_3:def 13 ex z being Element of RAT+ st y = x + z; connectedness for x, y being Element of RAT+ st ( for z being Element of RAT+ holds not y = x + z ) holds ex z being Element of RAT+ st x = y + z proof let x, y be Element of RAT+ ; ::_thesis: ( ( for z being Element of RAT+ holds not y = x + z ) implies ex z being Element of RAT+ st x = y + z ) set nx = numerator x; set ny = numerator y; set dx = denominator x; set dy = denominator y; A1: ( denominator x <> {} & denominator y <> {} ) by Th35; A2: ( (numerator x) / (denominator x) = x & (numerator y) / (denominator y) = y ) by Th39; ( (numerator x) *^ (denominator y) c= (numerator y) *^ (denominator x) or (numerator y) *^ (denominator x) c= (numerator x) *^ (denominator y) ) ; then A3: ( (numerator y) *^ (denominator x) = ((numerator x) *^ (denominator y)) +^ (((numerator y) *^ (denominator x)) -^ ((numerator x) *^ (denominator y))) or (numerator x) *^ (denominator y) = ((numerator y) *^ (denominator x)) +^ (((numerator x) *^ (denominator y)) -^ ((numerator y) *^ (denominator x))) ) by ORDINAL3:def_5; ( ((numerator x) *^ (denominator y)) / ((denominator x) *^ (denominator y)) = (numerator x) / (denominator x) & ((numerator y) *^ (denominator x)) / ((denominator x) *^ (denominator y)) = (numerator y) / (denominator y) ) by Th35, Th44; then ( x = y + ((((numerator x) *^ (denominator y)) -^ ((numerator y) *^ (denominator x))) / ((denominator x) *^ (denominator y))) or y = x + ((((numerator y) *^ (denominator x)) -^ ((numerator x) *^ (denominator y))) / ((denominator x) *^ (denominator y))) ) by A1, A2, A3, Th47, ORDINAL3:31; hence ( ( for z being Element of RAT+ holds not y = x + z ) implies ex z being Element of RAT+ st x = y + z ) ; ::_thesis: verum end; end; :: deftheorem Def13 defines <=' ARYTM_3:def_13_:_ for x, y being Element of RAT+ holds ( x <=' y iff ex z being Element of RAT+ st y = x + z ); notation let x, y be Element of RAT+ ; antonym y < x for x <=' y; end; theorem :: ARYTM_3:61 for y being set holds not [{},y] in RAT+ proof given y being set such that A1: [{},y] in RAT+ ; ::_thesis: contradiction consider i, j being Element of omega such that A2: [{},y] = [i,j] and A3: i,j are_relative_prime and j <> {} and A4: j <> 1 by A1, Th29, Th32; i = {} by A2, XTUPLE_0:1; hence contradiction by A3, A4, Th3; ::_thesis: verum end; theorem Th62: :: ARYTM_3:62 for s, t, r being Element of RAT+ st s + t = r + t holds s = r proof let s, t, r be Element of RAT+ ; ::_thesis: ( s + t = r + t implies s = r ) assume A1: s + t = r + t ; ::_thesis: s = r set r1 = numerator r; set r2 = denominator r; set t1 = numerator t; set t2 = denominator t; set s1 = numerator s; set s2 = denominator s; A2: denominator t <> {} by Th35; A3: denominator s <> {} by Th35; then A4: (denominator s) *^ (denominator t) <> {} by A2, ORDINAL3:31; A5: denominator r <> {} by Th35; then (denominator r) *^ (denominator t) <> {} by A2, ORDINAL3:31; then (((numerator s) *^ (denominator t)) +^ ((denominator s) *^ (numerator t))) *^ ((denominator r) *^ (denominator t)) = (((numerator r) *^ (denominator t)) +^ ((denominator r) *^ (numerator t))) *^ ((denominator s) *^ (denominator t)) by A1, A4, Th45 .= ((((numerator r) *^ (denominator t)) +^ ((denominator r) *^ (numerator t))) *^ (denominator s)) *^ (denominator t) by ORDINAL3:50 ; then ((((numerator s) *^ (denominator t)) +^ ((denominator s) *^ (numerator t))) *^ (denominator r)) *^ (denominator t) = ((((numerator r) *^ (denominator t)) +^ ((denominator r) *^ (numerator t))) *^ (denominator s)) *^ (denominator t) by ORDINAL3:50; then (((numerator s) *^ (denominator t)) +^ ((denominator s) *^ (numerator t))) *^ (denominator r) = (((numerator r) *^ (denominator t)) +^ ((denominator r) *^ (numerator t))) *^ (denominator s) by A2, ORDINAL3:33 .= (((numerator r) *^ (denominator t)) *^ (denominator s)) +^ (((denominator r) *^ (numerator t)) *^ (denominator s)) by ORDINAL3:46 ; then (((numerator s) *^ (denominator t)) *^ (denominator r)) +^ (((denominator s) *^ (numerator t)) *^ (denominator r)) = (((numerator r) *^ (denominator t)) *^ (denominator s)) +^ (((denominator r) *^ (numerator t)) *^ (denominator s)) by ORDINAL3:46 .= (((numerator r) *^ (denominator t)) *^ (denominator s)) +^ (((denominator s) *^ (numerator t)) *^ (denominator r)) by ORDINAL3:50 ; then ((numerator s) *^ (denominator t)) *^ (denominator r) = ((numerator r) *^ (denominator t)) *^ (denominator s) by ORDINAL3:21 .= ((numerator r) *^ (denominator s)) *^ (denominator t) by ORDINAL3:50 ; then ((numerator s) *^ (denominator r)) *^ (denominator t) = ((numerator r) *^ (denominator s)) *^ (denominator t) by ORDINAL3:50; then (numerator s) *^ (denominator r) = (numerator r) *^ (denominator s) by A2, ORDINAL3:33; then (numerator s) / (denominator s) = (numerator r) / (denominator r) by A3, A5, Th45 .= r by Th39 ; hence s = r by Th39; ::_thesis: verum end; theorem Th63: :: ARYTM_3:63 for r, s being Element of RAT+ st r + s = {} holds r = {} proof let r, s be Element of RAT+ ; ::_thesis: ( r + s = {} implies r = {} ) set nr = numerator r; set dr = denominator r; set ns = numerator s; set ds = denominator s; assume A1: r + s = {} ; ::_thesis: r = {} ( denominator {} = 1 & numerator {} = {} ) by Def8, Def9, Lm1; then A2: (((numerator r) *^ (denominator s)) +^ ((numerator s) *^ (denominator r))) / ((denominator r) *^ (denominator s)) = {} / 1 by A1, Th39; A3: denominator s <> {} by Th35; denominator r <> {} by Th35; then (denominator r) *^ (denominator s) <> {} by A3, ORDINAL3:31; then (((numerator r) *^ (denominator s)) +^ ((numerator s) *^ (denominator r))) *^ 1 = ((denominator r) *^ (denominator s)) *^ {} by A2, Th45 .= {} by ORDINAL2:35 ; then ((numerator r) *^ (denominator s)) +^ ((numerator s) *^ (denominator r)) = {} by ORDINAL3:31; then (numerator r) *^ (denominator s) = {} by ORDINAL3:26; then numerator r = {} by A3, ORDINAL3:31; hence r = {} by Th37; ::_thesis: verum end; theorem Th64: :: ARYTM_3:64 for s being Element of RAT+ holds {} <=' s proof let s be Element of RAT+ ; ::_thesis: {} <=' s take s ; :: according to ARYTM_3:def_13 ::_thesis: s = {} + s thus s = {} + s by Th50; ::_thesis: verum end; theorem :: ARYTM_3:65 for s being Element of RAT+ st s <=' {} holds s = {} proof let s be Element of RAT+ ; ::_thesis: ( s <=' {} implies s = {} ) assume ex r being Element of RAT+ st {} = s + r ; :: according to ARYTM_3:def_13 ::_thesis: s = {} hence s = {} by Th63; ::_thesis: verum end; theorem Th66: :: ARYTM_3:66 for r, s being Element of RAT+ st r <=' s & s <=' r holds r = s proof let r, s be Element of RAT+ ; ::_thesis: ( r <=' s & s <=' r implies r = s ) given x being Element of RAT+ such that A1: s = r + x ; :: according to ARYTM_3:def_13 ::_thesis: ( not s <=' r or r = s ) given y being Element of RAT+ such that A2: r = s + y ; :: according to ARYTM_3:def_13 ::_thesis: r = s r + {} = r by Th50 .= r + (x + y) by A1, A2, Th51 ; then x = {} by Th62, Th63; hence r = s by A1, Th50; ::_thesis: verum end; theorem Th67: :: ARYTM_3:67 for r, s, t being Element of RAT+ st r <=' s & s <=' t holds r <=' t proof let r, s, t be Element of RAT+ ; ::_thesis: ( r <=' s & s <=' t implies r <=' t ) given x being Element of RAT+ such that A1: s = r + x ; :: according to ARYTM_3:def_13 ::_thesis: ( not s <=' t or r <=' t ) given y being Element of RAT+ such that A2: t = s + y ; :: according to ARYTM_3:def_13 ::_thesis: r <=' t take x + y ; :: according to ARYTM_3:def_13 ::_thesis: t = r + (x + y) thus t = r + (x + y) by A1, A2, Th51; ::_thesis: verum end; theorem :: ARYTM_3:68 for r, s being Element of RAT+ holds ( r < s iff ( r <=' s & r <> s ) ) by Th66; theorem :: ARYTM_3:69 for r, s, t being Element of RAT+ st ( ( r < s & s <=' t ) or ( r <=' s & s < t ) ) holds r < t by Th67; theorem :: ARYTM_3:70 for r, s, t being Element of RAT+ st r < s & s < t holds r < t by Th67; theorem Th71: :: ARYTM_3:71 for x, y being Element of RAT+ st x in omega & x + y in omega holds y in omega proof let x, y be Element of RAT+ ; ::_thesis: ( x in omega & x + y in omega implies y in omega ) assume that A1: x in omega and A2: x + y in omega ; ::_thesis: y in omega A3: denominator (x + y) = 1 by A2, Def9; set nx = numerator x; set dx = denominator x; A4: denominator x = 1 by A1, Def9; set ny = numerator y; set dy = denominator y; A5: ( x + y = (numerator (x + y)) / (denominator (x + y)) & (((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) *^ 1 = ((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x)) ) by Th39, ORDINAL2:39; denominator y <> {} by Th35; then (denominator x) *^ (denominator y) <> {} by A4, ORDINAL3:31; then ((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x)) = ((denominator x) *^ (denominator y)) *^ (numerator (x + y)) by A3, A5, Th45 .= (denominator y) *^ (numerator (x + y)) by A4, ORDINAL2:39 ; then ((numerator x) *^ (denominator y)) +^ (numerator y) = (denominator y) *^ (numerator (x + y)) by A4, ORDINAL2:39; then numerator y = ((denominator y) *^ (numerator (x + y))) -^ ((numerator x) *^ (denominator y)) by ORDINAL3:52; then numerator y = (denominator y) *^ ((numerator (x + y)) -^ (numerator x)) by ORDINAL3:63; then A6: denominator y divides numerator y by Def3; A7: numerator y, denominator y are_relative_prime by Th34; for m being natural Ordinal st m divides denominator y & m divides numerator y holds m divides denominator y ; then (denominator y) hcf (numerator y) = denominator y by A6, Def5; then A8: denominator y = 1 by A7, Th20; y = (numerator y) / (denominator y) by Th39; then y = numerator y by A8, Th40; hence y in omega ; ::_thesis: verum end; theorem Th72: :: ARYTM_3:72 for x being Element of RAT+ for i being ordinal Element of RAT+ st i < x & x < i + one holds not x in omega proof let x be Element of RAT+ ; ::_thesis: for i being ordinal Element of RAT+ st i < x & x < i + one holds not x in omega let i be ordinal Element of RAT+ ; ::_thesis: ( i < x & x < i + one implies not x in omega ) assume that A1: i < x and A2: x < i + one and A3: x in omega ; ::_thesis: contradiction consider z being Element of RAT+ 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 being Element of RAT+ 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; ::_thesis: verum end; theorem Th73: :: ARYTM_3:73 for t being Element of RAT+ st t <> {} holds ex r being Element of RAT+ st ( r < t & not r in omega ) proof let t be Element of RAT+ ; ::_thesis: ( t <> {} implies ex r being Element of RAT+ st ( r < t & not r in omega ) ) assume A1: t <> {} ; ::_thesis: ex r being Element of RAT+ st ( r < t & not r in omega ) A2: 1 +^ 1 = succ 1 by ORDINAL2:31; percases ( one <=' t or t < one ) ; supposeA3: one <=' t ; ::_thesis: ex r being Element of RAT+ st ( r < t & not r in omega ) consider r being Element of RAT+ such that A4: one = r + r by Th60; take r ; ::_thesis: ( r < t & not r in omega ) ( r <=' one & r <> 1 ) by A2, A4, Def13, Th58; then r < one by Th66; hence r < t by A3, Th67; ::_thesis: not r in omega A5: 1 *^ 1 = 1 by ORDINAL2:39; assume r in omega ; ::_thesis: contradiction 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; ::_thesis: verum end; supposeA8: t < one ; ::_thesis: ex r being Element of RAT+ st ( r < t & not r in omega ) consider r being Element of RAT+ 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 ; ::_thesis: ( r < t & not r in omega ) A12: 1 = {} + one by Th50; A13: r <=' t by A9, Def13; now__::_thesis:_not_r_=_t assume r = t ; ::_thesis: contradiction then t + {} = t + t by A9, Th50; hence contradiction by A1, Th62; ::_thesis: verum end; hence r < t by A13, Th66; ::_thesis: not r in omega r < one by A8, A13, Th67; hence not r in omega by A11, A12, Th72; ::_thesis: verum end; end; end; theorem :: ARYTM_3:74 for t being Element of RAT+ holds ( { s where s is Element of RAT+ : s < t } in RAT+ iff t = {} ) proof let t be Element of RAT+ ; ::_thesis: ( { s where s is Element of RAT+ : s < t } in RAT+ iff t = {} ) hereby ::_thesis: ( t = {} implies { s where s is Element of RAT+ : s < t } in RAT+ ) assume A1: ( { s where s is Element of RAT+ : s < t } in RAT+ & t <> {} ) ; ::_thesis: contradiction then consider r being Element of RAT+ 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 where s is Element of RAT+ : s < t } ; r in { s where s is Element of RAT+ : s < t } by A2; then ( { s where s is Element of RAT+ : s < t } in omega implies r is Ordinal ) ; then ex i, j being Element of omega st ( { s where s is Element of RAT+ : s < t } = [i,j] & i,j are_relative_prime & j <> {} & j <> 1 ) by A1, A3, Th29, Th31; hence contradiction by A4, TARSKI:def_2; ::_thesis: verum end; assume A5: t = {} ; ::_thesis: { s where s is Element of RAT+ : s < t } in RAT+ { s where s is Element of RAT+ : s < t } c= {} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { s where s is Element of RAT+ : s < t } or a in {} ) assume a in { s where s is Element of RAT+ : s < t } ; ::_thesis: a in {} then ex s being Element of RAT+ st ( a = s & s < t ) ; hence a in {} by A5, Th64; ::_thesis: verum end; then { s where s is Element of RAT+ : s < t } = {} ; hence { s where s is Element of RAT+ : s < t } in RAT+ ; ::_thesis: verum end; theorem :: ARYTM_3:75 for A being Subset of RAT+ st ex t being Element of RAT+ st ( t in A & t <> {} ) & ( for r, s being Element of RAT+ st r in A & s <=' r holds s in A ) holds 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+; ::_thesis: ( ex t being Element of RAT+ st ( t in A & t <> {} ) & ( for r, s being Element of RAT+ st r in A & s <=' r holds s in A ) implies ex r1, r2, r3 being Element of RAT+ st ( r1 in A & r2 in A & r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) ) given t being Element of RAT+ such that A1: t in A and A2: t <> {} ; ::_thesis: ( ex r, s being Element of RAT+ st ( r in A & s <=' r & not s in A ) or ex r1, r2, r3 being Element of RAT+ st ( r1 in A & r2 in A & r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) ) assume A3: for r, s being Element of RAT+ st r in A & s <=' r holds s in A ; ::_thesis: ex r1, r2, r3 being Element of RAT+ st ( r1 in A & r2 in A & r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) consider x being Element of RAT+ such that A4: t = x + x by Th60; take {} ; ::_thesis: ex r2, r3 being Element of RAT+ st ( {} in A & r2 in A & r3 in A & {} <> r2 & r2 <> r3 & r3 <> {} ) take x ; ::_thesis: ex r3 being Element of RAT+ st ( {} in A & x in A & r3 in A & {} <> x & x <> r3 & r3 <> {} ) take t ; ::_thesis: ( {} in A & x in A & t in A & {} <> x & x <> t & t <> {} ) x <=' t by A4, Def13; hence ( {} in A & x in A & t in A ) by A1, A3, Th64; ::_thesis: ( {} <> x & x <> t & t <> {} ) thus {} <> x by A2, A4, Th50; ::_thesis: ( x <> t & t <> {} ) hereby ::_thesis: t <> {} assume x = t ; ::_thesis: contradiction then t + {} = t + t by A4, Th50; hence contradiction by A2, Th62; ::_thesis: verum end; thus t <> {} by A2; ::_thesis: verum end; theorem Th76: :: ARYTM_3:76 for s, t, r being Element of RAT+ holds ( s + t <=' r + t iff s <=' r ) proof let s, t, r be Element of RAT+ ; ::_thesis: ( s + t <=' r + t iff s <=' r ) thus ( s + t <=' r + t implies s <=' r ) ::_thesis: ( s <=' r implies s + t <=' r + t ) proof given z being Element of RAT+ such that A1: r + t = (s + t) + z ; :: according to ARYTM_3:def_13 ::_thesis: s <=' r take z ; :: according to ARYTM_3:def_13 ::_thesis: r = s + z r + t = (s + z) + t by A1, Th51; hence r = s + z by Th62; ::_thesis: verum end; given z being Element of RAT+ such that A2: r = s + z ; :: according to ARYTM_3:def_13 ::_thesis: s + t <=' r + t take z ; :: according to ARYTM_3:def_13 ::_thesis: r + t = (s + t) + z thus r + t = (s + t) + z by A2, Th51; ::_thesis: verum end; theorem :: ARYTM_3:77 for s, t being Element of RAT+ holds s <=' s + t proof let s, t be Element of RAT+ ; ::_thesis: s <=' s + t take t ; :: according to ARYTM_3:def_13 ::_thesis: s + t = s + t thus s + t = s + t ; ::_thesis: verum end; theorem :: ARYTM_3:78 for r, s being Element of RAT+ holds ( not r *' s = {} or r = {} or s = {} ) proof let r, s be Element of RAT+ ; ::_thesis: ( not r *' s = {} or r = {} or s = {} ) set nr = numerator r; set dr = denominator r; set ns = numerator s; set ds = denominator s; assume A1: r *' s = {} ; ::_thesis: ( r = {} or s = {} ) ( denominator r <> {} & denominator s <> {} ) by Th35; then A2: (denominator r) *^ (denominator s) <> {} by ORDINAL3:31; ( denominator {} = 1 & numerator {} = {} ) by Def8, Def9, Lm1; then ((numerator r) *^ (numerator s)) / ((denominator r) *^ (denominator s)) = {} / 1 by A1, Th39; then ((numerator r) *^ (numerator s)) *^ 1 = ((denominator r) *^ (denominator s)) *^ {} by A2, Th45 .= {} by ORDINAL2:35 ; then (numerator r) *^ (numerator s) = {} by ORDINAL3:31; then ( numerator r = {} or numerator s = {} ) by ORDINAL3:31; hence ( r = {} or s = {} ) by Th37; ::_thesis: verum end; theorem Th79: :: ARYTM_3:79 for r, s, t being Element of RAT+ st r <=' s *' t holds ex t0 being Element of RAT+ st ( r = s *' t0 & t0 <=' t ) proof let r, s, t be Element of RAT+ ; ::_thesis: ( r <=' s *' t implies ex t0 being Element of RAT+ st ( r = s *' t0 & t0 <=' t ) ) given x being Element of RAT+ such that A1: s *' t = r + x ; :: according to ARYTM_3:def_13 ::_thesis: ex t0 being Element of RAT+ st ( r = s *' t0 & t0 <=' t ) percases ( s = {} or s <> {} ) ; supposeA2: s = {} ; ::_thesis: ex t0 being Element of RAT+ st ( r = s *' t0 & t0 <=' t ) take t ; ::_thesis: ( r = s *' t & t <=' t ) s *' t = {} by A2, Th48; hence ( r = s *' t & t <=' t ) by A1, Th63; ::_thesis: verum end; supposeA3: s <> {} ; ::_thesis: ex t0 being Element of RAT+ st ( r = s *' t0 & t0 <=' t ) 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 ; ::_thesis: ( r = s *' t0 & t0 <=' t ) thus r = s *' t0 by A5; ::_thesis: t0 <=' t take t1 ; :: according to ARYTM_3:def_13 ::_thesis: t = t0 + t1 s *' t = s *' (t0 + t1) by A1, A5, A4, Th57; hence t = t0 + t1 by A3, Th56; ::_thesis: verum end; end; end; theorem :: ARYTM_3:80 for t, s, r being Element of RAT+ st t <> {} & s *' t <=' r *' t holds s <=' r proof let t, s, r be Element of RAT+ ; ::_thesis: ( t <> {} & s *' t <=' r *' t implies s <=' r ) assume that A1: t <> {} and A2: s *' t <=' r *' t ; ::_thesis: s <=' r ex x being Element of RAT+ st ( s *' t = t *' x & x <=' r ) by A2, Th79; hence s <=' r by A1, Th56; ::_thesis: verum end; theorem :: ARYTM_3:81 for r1, r2, s1, s2 being Element of RAT+ holds ( not r1 + r2 = s1 + s2 or r1 <=' s1 or r2 <=' s2 ) proof let r1, r2, s1, s2 be Element of RAT+ ; ::_thesis: ( not r1 + r2 = s1 + s2 or r1 <=' s1 or r2 <=' s2 ) assume A1: r1 + r2 = s1 + s2 ; ::_thesis: ( r1 <=' s1 or r2 <=' s2 ) assume that A2: s1 < r1 and A3: s2 < r2 ; ::_thesis: contradiction s1 + s2 < r1 + s2 by A2, Th76; hence contradiction by A1, A3, Th76; ::_thesis: verum end; theorem Th82: :: ARYTM_3:82 for s, r, t being Element of RAT+ st s <=' r holds s *' t <=' r *' t proof let s, r, t be Element of RAT+ ; ::_thesis: ( s <=' r implies s *' t <=' r *' t ) given x being Element of RAT+ such that A1: r = s + x ; :: according to ARYTM_3:def_13 ::_thesis: s *' t <=' r *' t take x *' t ; :: according to ARYTM_3:def_13 ::_thesis: r *' t = (s *' t) + (x *' t) thus r *' t = (s *' t) + (x *' t) by A1, Th57; ::_thesis: verum end; theorem :: ARYTM_3:83 for r1, r2, s1, s2 being Element of RAT+ holds ( not r1 *' r2 = s1 *' s2 or r1 <=' s1 or r2 <=' s2 ) proof let r1, r2, s1, s2 be Element of RAT+ ; ::_thesis: ( not r1 *' r2 = s1 *' s2 or r1 <=' s1 or r2 <=' s2 ) assume A1: r1 *' r2 = s1 *' s2 ; ::_thesis: ( r1 <=' s1 or r2 <=' s2 ) A2: {} <=' s1 by Th64; assume that A3: s1 < r1 and A4: s2 < r2 ; ::_thesis: contradiction ( s2 <> r2 & s1 *' s2 <=' r1 *' s2 ) by A3, A4, Th82; then s1 *' s2 < r1 *' s2 by A1, A3, A2, Th56, Th66; hence contradiction by A1, A4, Th82; ::_thesis: verum end; theorem :: ARYTM_3:84 for r, s being Element of RAT+ holds ( r = {} iff r + s = s ) proof let r, s be Element of RAT+ ; ::_thesis: ( r = {} iff r + s = s ) s + {} = s by Th50; hence ( r = {} iff r + s = s ) by Th62; ::_thesis: verum end; theorem :: ARYTM_3:85 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+ ; ::_thesis: ( s1 + t1 = s2 + t2 & s1 <=' s2 implies t2 <=' t1 ) assume A1: s1 + t1 = s2 + t2 ; ::_thesis: ( not s1 <=' s2 or t2 <=' t1 ) given x being Element of RAT+ such that A2: s2 = s1 + x ; :: according to ARYTM_3:def_13 ::_thesis: t2 <=' t1 take x ; :: according to ARYTM_3:def_13 ::_thesis: t1 = t2 + x s1 + t1 = s1 + (x + t2) by A1, A2, Th51; hence t1 = t2 + x by Th62; ::_thesis: verum end; theorem Th86: :: ARYTM_3:86 for r, s, t being Element of RAT+ st r <=' s & s <=' r + t holds ex t0 being Element of RAT+ st ( s = r + t0 & t0 <=' t ) proof let r, s, t be Element of RAT+ ; ::_thesis: ( r <=' s & s <=' r + t implies ex t0 being Element of RAT+ st ( s = r + t0 & t0 <=' t ) ) given t0 being Element of RAT+ such that A1: s = r + t0 ; :: according to ARYTM_3:def_13 ::_thesis: ( not s <=' r + t or ex t0 being Element of RAT+ st ( s = r + t0 & t0 <=' t ) ) assume s <=' r + t ; ::_thesis: ex t0 being Element of RAT+ st ( s = r + t0 & t0 <=' t ) then t0 <=' t by A1, Th76; hence ex t0 being Element of RAT+ st ( s = r + t0 & t0 <=' t ) by A1; ::_thesis: verum end; theorem :: ARYTM_3:87 for r, s, t being Element of RAT+ st r <=' s + t holds ex s0, t0 being Element of RAT+ st ( r = s0 + t0 & s0 <=' s & t0 <=' t ) proof let r, s, t be Element of RAT+ ; ::_thesis: ( r <=' s + t implies ex s0, t0 being Element of RAT+ st ( r = s0 + t0 & s0 <=' s & t0 <=' t ) ) assume A1: r <=' s + t ; ::_thesis: ex s0, t0 being Element of RAT+ st ( r = s0 + t0 & s0 <=' s & t0 <=' t ) percases ( s <=' r or r <=' s ) ; suppose s <=' r ; ::_thesis: ex s0, t0 being Element of RAT+ st ( r = s0 + t0 & s0 <=' s & t0 <=' t ) then ( s <=' s & ex t0 being Element of RAT+ st ( r = s + t0 & t0 <=' t ) ) by A1, Th86; hence ex s0, t0 being Element of RAT+ st ( r = s0 + t0 & s0 <=' s & t0 <=' t ) ; ::_thesis: verum end; supposeA2: r <=' s ; ::_thesis: ex s0, t0 being Element of RAT+ st ( r = s0 + t0 & s0 <=' s & t0 <=' t ) ( r = r + {} & {} <=' t ) by Th50, Th64; hence ex s0, t0 being Element of RAT+ st ( r = s0 + t0 & s0 <=' s & t0 <=' t ) by A2; ::_thesis: verum end; end; end; theorem :: ARYTM_3:88 for r, s, t being Element of RAT+ st r < s & r < t holds ex t0 being Element of RAT+ st ( t0 <=' s & t0 <=' t & r < t0 ) proof let r, s, t be Element of RAT+ ; ::_thesis: ( r < s & r < t implies ex t0 being Element of RAT+ st ( t0 <=' s & t0 <=' t & r < t0 ) ) ( ( s <=' t & s <=' s ) or ( t <=' s & t <=' t ) ) ; hence ( r < s & r < t implies ex t0 being Element of RAT+ st ( t0 <=' s & t0 <=' t & r < t0 ) ) ; ::_thesis: verum end; theorem :: ARYTM_3:89 for r, s, t being Element of RAT+ st r <=' s & s <=' t & s <> t holds r <> t by Th66; theorem :: ARYTM_3:90 for s, r, t being Element of RAT+ st s < r + t & t <> {} holds ex r0, t0 being Element of RAT+ st ( s = r0 + t0 & r0 <=' r & t0 <=' t & t0 <> t ) proof let s, r, t be Element of RAT+ ; ::_thesis: ( s < r + t & t <> {} implies ex r0, t0 being Element of RAT+ st ( s = r0 + t0 & r0 <=' r & t0 <=' t & t0 <> t ) ) assume that A1: s < r + t and A2: t <> {} ; ::_thesis: ex r0, t0 being Element of RAT+ st ( s = r0 + t0 & r0 <=' r & t0 <=' t & t0 <> t ) percases ( r <=' s or s <=' r ) ; suppose r <=' s ; ::_thesis: ex r0, t0 being Element of RAT+ st ( s = r0 + t0 & r0 <=' r & t0 <=' t & t0 <> t ) then consider t0 being Element of RAT+ such that A3: ( s = r + t0 & t0 <=' t ) by A1, Th86; take r ; ::_thesis: ex t0 being Element of RAT+ st ( s = r + t0 & r <=' r & t0 <=' t & t0 <> t ) take t0 ; ::_thesis: ( s = r + t0 & r <=' r & t0 <=' t & t0 <> t ) thus ( s = r + t0 & r <=' r & t0 <=' t & t0 <> t ) by A1, A3; ::_thesis: verum end; supposeA4: s <=' r ; ::_thesis: ex r0, t0 being Element of RAT+ st ( s = r0 + t0 & r0 <=' r & t0 <=' t & t0 <> t ) ( s = s + {} & {} <=' t ) by Th50, Th64; hence ex r0, t0 being Element of RAT+ st ( s = r0 + t0 & r0 <=' r & t0 <=' t & t0 <> t ) by A2, A4; ::_thesis: verum end; end; end; theorem :: ARYTM_3:91 for A being non empty Subset of RAT+ st A in RAT+ holds ex s being Element of RAT+ st ( s in A & ( for r being Element of RAT+ st r in A holds r <=' s ) ) proof let A be non empty Subset of RAT+; ::_thesis: ( A in RAT+ implies ex s being Element of RAT+ st ( s in A & ( for r being Element of RAT+ st r in A holds r <=' s ) ) ) A1: now__::_thesis:_for_i,_j_being_Element_of_omega_holds_ (_not_A_=_[i,j]_or_not_i,j_are_relative_prime_or_not_j_<>_{}_or_not_j_<>_1_) given i, j being Element of omega such that A2: A = [i,j] and A3: i,j are_relative_prime and j <> {} and A4: j <> 1 ; ::_thesis: contradiction A5: now__::_thesis:_not_{i}_in_omega assume {i} in omega ; ::_thesis: contradiction then {} in {i} by ORDINAL3:8; then {} = i by TARSKI:def_1; hence contradiction by A3, A4, Th3; ::_thesis: verum 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_relative_prime 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, Def2; ::_thesis: verum end; assume A in RAT+ ; ::_thesis: ex s being Element of RAT+ st ( s in A & ( for r being Element of RAT+ st r in A holds r <=' s ) ) then reconsider B = A as Element of omega by A1, Th29; A11: {} in B by ORDINAL3:8; now__::_thesis:_not_B_is_limit_ordinal assume B is limit_ordinal ; ::_thesis: contradiction then omega c= B by A11, ORDINAL1:def_11; hence contradiction by ORDINAL1:5; ::_thesis: verum end; then consider C being Ordinal such that A12: B = succ C by ORDINAL1:29; C in B by A12, ORDINAL1:6; then reconsider C = C as ordinal Element of RAT+ ; take C ; ::_thesis: ( C in A & ( for r being Element of RAT+ st r in A holds r <=' C ) ) thus C in A by A12, ORDINAL1:6; ::_thesis: for r being Element of RAT+ st r in A holds r <=' C let r be Element of RAT+ ; ::_thesis: ( r in A implies r <=' C ) assume A13: r in A ; ::_thesis: r <=' C then r in B ; then reconsider r = 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 Lm5; r c= C by A12, A13, ORDINAL1:22; then C = r +^ x by ORDINAL3:def_5 .= r + x by Th58 ; hence r <=' C by Def13; ::_thesis: verum end; theorem :: ARYTM_3:92 for r, s being Element of RAT+ ex t being Element of RAT+ st ( r + t = s or s + t = r ) proof let r, s be Element of RAT+ ; ::_thesis: ex t being Element of RAT+ st ( r + t = s or s + t = r ) ( r <=' s or s <=' r ) ; hence ex t being Element of RAT+ st ( r + t = s or s + t = r ) by Def13; ::_thesis: verum end; theorem :: ARYTM_3:93 for r, s being Element of RAT+ st r < s holds ex t being Element of RAT+ st ( r < t & t < s ) proof let r, s be Element of RAT+ ; ::_thesis: ( r < s implies ex t being Element of RAT+ st ( r < t & t < s ) ) assume A1: r < s ; ::_thesis: ex t being Element of RAT+ st ( r < t & t < s ) then consider x being Element of RAT+ such that A2: s = r + x by Def13; consider y being Element of RAT+ such that A3: x = y + y by Th60; take t = r + y; ::_thesis: ( r < t & t < s ) A4: s = t + y by A2, A3, Th51; then A5: t <=' s by Def13; r <=' t by Def13; hence r < t by A1, A4, Th66; ::_thesis: t < s r <> s by A1; then s <> t by A4, Th62; hence t < s by A5, Th66; ::_thesis: verum end; theorem :: ARYTM_3:94 for r being Element of RAT+ ex s being Element of RAT+ st r < s proof let r be Element of RAT+ ; ::_thesis: ex s being Element of RAT+ st r < s take s = r + one; ::_thesis: r < s s + {} = s by Th50; then A1: r <> s by Th62; r <=' s by Def13; hence r < s by A1, Th66; ::_thesis: verum end; theorem :: ARYTM_3:95 for t, r being Element of RAT+ st t <> {} holds ex s being Element of RAT+ st ( s in omega & r <=' s *' t ) proof let t, r be Element of RAT+ ; ::_thesis: ( t <> {} implies ex s being Element of RAT+ st ( s in omega & r <=' s *' t ) ) 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 Lm5; assume t <> {} ; ::_thesis: ex s being Element of RAT+ st ( s in omega & r <=' s *' t ) then numerator t <> {} by Th37; then {} in (numerator t) *^ (denominator r) by A1, ORDINAL3:8, ORDINAL3: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 ; ::_thesis: ( s in omega & r <=' s *' t ) thus s in omega by ORDINAL1:def_12; ::_thesis: r <=' s *' t take ((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r) ; :: according to ARYTM_3:def_13 ::_thesis: s *' t = r + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) 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)) + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) by Th35, Th47 .= ((numerator r) / (denominator r)) + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) by ORDINAL2:39 .= r + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) by Th39 ; then r + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) = (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 s *' t = r + (((numerator r) *^ (((numerator t) *^ (denominator r)) -^ 1)) / (denominator r)) by Th39; ::_thesis: verum end; scheme :: ARYTM_3:sch 1 DisNat{ F1() -> Element of RAT+ , F2() -> Element of RAT+ , F3() -> Element of RAT+ , P1[ set ] } : ex s being Element of RAT+ st ( s in omega & P1[s] & P1[s + F2()] ) provided A1: F2() = 1 and A2: F1() = {} and A3: F3() in omega and A4: P1[F1()] and A5: P1[F3()] proof defpred S2[ Ordinal] means ( P1[$1] & $1 in omega ); A6: ex A being Ordinal st S2[A] by A3, A5; consider A being Ordinal such that A7: S2[A] and A8: for B being Ordinal st S2[B] holds A c= B from ORDINAL1:sch_1(A6); A9: {} in A by A2, A4, A7, ORDINAL3:8; now__::_thesis:_not_A_is_limit_ordinal assume A is limit_ordinal ; ::_thesis: contradiction then omega c= A by A9, ORDINAL1:def_11; then A in A by A7; hence contradiction ; ::_thesis: verum 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 Lm5; take s ; ::_thesis: ( s in omega & P1[s] & P1[s + F2()] ) thus ( s in omega & P1[s] ) by A8, A11, A12, ORDINAL1:5; ::_thesis: P1[s + F2()] A = B +^ 1 by A10, ORDINAL2:31; hence P1[s + F2()] by A1, A7, Th58; ::_thesis: verum end;