:: 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;