:: ARYTM_3 semantic presentation

Lemma1: 1 in omega
;

definition
func one -> set equals :: ARYTM_3:def 1
1;
correctness
coherence
1 is set ;
;
end;

:: deftheorem Def1 defines one ARYTM_3:def 1 :
one = 1;

registration
cluster empty -> natural set ;
coherence
for b1 being Ordinal holds
( b1 is empty implies b1 is natural ) by ORDINAL2:19, ORDINAL1:def 13;
cluster one -> non empty natural ;
coherence
( one is natural & not one is empty ) by ORDINAL1:def 13;
cluster -> natural Element of omega ;
coherence
for b1 being Element of omega holds b1 is natural by ORDINAL1:def 13;
end;

registration
cluster non empty natural set ;
existence
ex b1 being Ordinal st
( not b1 is empty & b1 is natural )
proof
take 1 ;
thus ( not 1 is empty & 1 is natural ) ;
end;
end;

registration
let c1 be natural Ordinal;
cluster succ a1 -> natural ;
coherence
succ c1 is natural
proof
c1 in omega by ORDINAL1:def 13;
hence succ c1 in omega by ORDINAL1:41, ORDINAL2:19; :: according to ORDINAL1:def 13
end;
end;

scheme :: ARYTM_3:sch 1
s1{ P1[ set ] } :
for b1 being natural Ordinal holds P1[b1]
provided
E2: P1[ {} ] and E3: for b1 being natural Ordinal holds
( P1[b1] implies P1[ succ b1] )
proof
defpred S1[ Ordinal] means ( a1 is natural implies P1[a1] );
E4: S1[ {} ] by E2;
E5: now
let c1 be Ordinal;
assume E6: S1[c1] ;
now
assume succ c1 is natural ;
then ( succ c1 in omega & c1 in succ c1 ) by ORDINAL1:10, ORDINAL1:def 13;
then c1 is Element of omega by ORDINAL1:19;
hence S1[ succ c1] by E3, E6;
end;
hence S1[ succ c1] ;
end;
E6: now
let c1 be Ordinal;
E7: {} c= c1 by XBOOLE_1:2;
assume c1 <> {} ;
then {} c< c1 by E7, XBOOLE_0:def 8;
then E8: {} in c1 by ORDINAL1:21;
assume c1 is_limit_ordinal ;
then ( omega c= c1 & not c1 in c1 ) by E8, ORDINAL1:def 12;
then not c1 in omega ;
hence ( ( for b1 being Ordinal holds
( b1 in c1 implies S1[b1] ) ) implies S1[c1] ) by ORDINAL1:def 13;
end;
for b1 being Ordinal holds
S1[b1] from ORDINAL2:sch 1(E4, E5, E6);
 hence for b1 being natural Ordinal holds P1[b1] ;
end;

registration
let c1, c2 be natural Ordinal;
cluster a1 +^ a2 -> natural ;
coherence
c1 +^ c2 is natural
proof
defpred S1[ natural Ordinal] means c1 +^ a1 is natural;
E2: S1[ {} ] by ORDINAL2:44;
E3: now
let c3 be natural Ordinal;
assume S1[c3] ;
then reconsider c4 = c1 +^ c3 as natural Ordinal ;
c1 +^ (succ c3) = succ c4 by ORDINAL2:45;
hence S1[ succ c3] ;
end;
for b1 being natural Ordinal holds
S1[b1] from ARYTM_3:sch 1(E2, E3);
 hence c1 +^ c2 is natural ;
end;
end;

theorem Th1: :: ARYTM_3:1
for b1, b2 being Ordinal holds
( b1 +^ b2 is natural implies ( b1 in omega & b2 in omega ) )
proof
let c1, c2 be Ordinal;
assume E3: c1 +^ c2 in omega ; :: according to ORDINAL1:def 13
( c1 c= c1 +^ c2 & c2 c= c1 +^ c2 ) by ORDINAL3:27;
hence ( c1 in omega & c2 in omega ) by E3, ORDINAL1:22;
end;

registration
let c1, c2 be natural Ordinal;
cluster a1 -^ a2 -> natural ;
coherence
c1 -^ c2 is natural
proof
not ( c2 c= c1 & not c2 c= c1 ) ;
then ( c1 -^ c2 = {} or c1 = c2 +^ (c1 -^ c2) ) by ORDINAL3:def 6;
hence c1 -^ c2 in omega by Th1, ORDINAL1:def 12; :: according to ORDINAL1:def 13
end;
cluster a1 *^ a2 -> natural ;
coherence
c1 *^ c2 is natural
proof
defpred S1[ natural Ordinal] means a1 *^ c2 is natural;
E3: S1[ {} ] by ORDINAL2:52;
E4: now
let c3 be natural Ordinal;
assume S1[c3] ;
then reconsider c4 = c3 *^ c2 as natural Ordinal ;
(succ c3) *^ c2 = c4 +^ c2 by ORDINAL2:53;
hence S1[ succ c3] ;
end;
for b1 being natural Ordinal holds
S1[b1] from ARYTM_3:sch 1(E3, E4);
 hence c1 *^ c2 is natural ;
end;
end;

theorem Th2: :: ARYTM_3:2
for b1, b2 being Ordinal holds
( b1 *^ b2 is natural & not b1 *^ b2 is empty implies ( b1 in omega & b2 in omega ) )
proof
let c1, c2 be Ordinal;
assume E4: c1 *^ c2 in omega ; :: according to ORDINAL1:def 13
assume not c1 *^ c2 is empty ;
then ( c1 <> {} & c2 <> {} ) by ORDINAL2:52, ORDINAL2:55;
then ( c1 c= c1 *^ c2 & c2 c= c1 *^ c2 ) by ORDINAL3:39;
hence ( c1 in omega & c2 in omega ) by E4, ORDINAL1:22;
end;

theorem Th3: :: ARYTM_3:3
for b1, b2 being natural Ordinal holds b1 +^ b2 = b2 +^ b1
proof
let c1 be natural Ordinal;
defpred S1[ natural Ordinal] means c1 +^ a1 = a1 +^ c1;
c1 +^ {} = c1 by ORDINAL2:44
.= {} +^ c1 by ORDINAL2:47 ;
then E5: S1[ {} ] ;
E6: now
let c2 be natural Ordinal;
assume E7: S1[c2] ;
defpred S2[ natural Ordinal] means (succ c2) +^ a1 = succ (c2 +^ a1);
(succ c2) +^ {} = succ c2 by ORDINAL2:44
.= succ (c2 +^ {} ) by ORDINAL2:44 ;
then E8: S2[ {} ] ;
E9: now
let c3 be natural Ordinal;
assume E10: S2[c3] ;
(succ c2) +^ (succ c3) = succ ((succ c2) +^ c3) by ORDINAL2:45
.= succ (c2 +^ (succ c3)) by E10, ORDINAL2:45 ;
hence S2[ succ c3] ;
end;
E10: for b1 being natural Ordinal holds
S2[b1] from ARYTM_3:sch 1(E8, E9);
c1 +^ (succ c2) = succ (c2 +^ c1) by E7, ORDINAL2:45
.= (succ c2) +^ c1 by E10 ;
hence S1[ succ c2] ;
end;
for b1 being natural Ordinal holds
S1[b1] from ARYTM_3:sch 1(E5, E6);
 hence for b1 being natural Ordinal holds c1 +^ b1 = b1 +^ c1 ;
end;

theorem Th4: :: ARYTM_3:4
for b1, b2 being natural Ordinal holds b1 *^ b2 = b2 *^ b1
proof
let c1 be natural Ordinal;
defpred S1[ natural Ordinal] means c1 *^ a1 = a1 *^ c1;
c1 *^ {} = {} by ORDINAL2:55
.= {} *^ c1 by ORDINAL2:52 ;
then E6: S1[ {} ] ;
E7: now
let c2 be natural Ordinal;
defpred S2[ natural Ordinal] means a1 *^ (succ c2) = (a1 *^ c2) +^ a1;
assume E8: S1[c2] ;
{} *^ (succ c2) = {} by ORDINAL2:52
.= {} +^ {} by ORDINAL2:44
.= ({} *^ c2) +^ {} by ORDINAL2:52 ;
then E9: S2[ {} ] ;
E10: now
let c3 be natural Ordinal;
assume E11: S2[c3] ;
(succ c3) *^ (succ c2) = (c3 *^ (succ c2)) +^ (succ c2) by ORDINAL2:53
.= (c3 *^ c2) +^ (c3 +^ (succ c2)) by E11, ORDINAL3:33
.= (c3 *^ c2) +^ (succ (c3 +^ c2)) by ORDINAL2:45
.= succ ((c3 *^ c2) +^ (c3 +^ c2)) by ORDINAL2:45
.= succ ((c3 *^ c2) +^ (c2 +^ c3)) by Th3
.= succ (((c3 *^ c2) +^ c2) +^ c3) by ORDINAL3:33
.= succ (((succ c3) *^ c2) +^ c3) by ORDINAL2:53
.= ((succ c3) *^ c2) +^ (succ c3) by ORDINAL2:45 ;
hence S2[ succ c3] ;
end;
for b1 being natural Ordinal holds
S2[b1] from ARYTM_3:sch 1(E9, E10);
then c1 *^ (succ c2) = (c2 *^ c1) +^ c1 by E8
.= (succ c2) *^ c1 by ORDINAL2:53 ;
hence S1[ succ c2] ;
end;
for b1 being natural Ordinal holds
S1[b1] from ARYTM_3:sch 1(E6, E7);
 hence for b1 being natural Ordinal holds c1 *^ b1 = b1 *^ c1 ;
end;

definition
let c1, c2 be natural Ordinal;
redefine func +^ as c1 +^ c2 -> set ;
commutativity
for b1, b2 being natural Ordinal holds b1 +^ b2 = b2 +^ b1 by Th3;
redefine func *^ as c1 *^ c2 -> set ;
commutativity
for b1, b2 being natural Ordinal holds b1 *^ b2 = b2 *^ b1 by Th4;
end;

definition
let c1, c2 be Ordinal;
pred c1,c2 are_relative_prime means :Def2: :: ARYTM_3:def 2
for b1, b2, b3 being Ordinal holds
( a1 = b1 *^ b2 & a2 = b1 *^ b3 implies b1 = 1 );
symmetry
for b1, b2 being Ordinal holds
( ( for b3, b4, b5 being Ordinal holds
( b1 = b3 *^ b4 & b2 = b3 *^ b5 implies b3 = 1 ) ) implies for b3, b4, b5 being Ordinal holds
( b2 = b3 *^ b4 & b1 = b3 *^ b5 implies b3 = 1 ) ) ;
end;

:: deftheorem Def2 defines are_relative_prime ARYTM_3:def 2 :
for b1, b2 being Ordinal holds
( b1,b2 are_relative_prime iff for b3, b4, b5 being Ordinal holds
( b1 = b3 *^ b4 & b2 = b3 *^ b5 implies b3 = 1 ) );

theorem Th5: :: ARYTM_3:5
not {} , {} are_relative_prime
proof
take {} ; :: according to ARYTM_3:def 2
take {} ;
take {} ;
thus ( {} = {} *^ {} & {} = {} *^ {} & not {} = 1 ) by ORDINAL2:52;
end;

theorem Th6: :: ARYTM_3:6
for b1 being Ordinal holds 1,b1 are_relative_prime
proof
let c1 be Ordinal;
let c2, c3, c4 be Ordinal; :: according to ARYTM_3:def 2
thus ( 1 = c2 *^ c3 & c1 = c2 *^ c4 implies c2 = 1 ) by ORDINAL3:41;
end;

theorem Th7: :: ARYTM_3:7
for b1 being Ordinal holds
( {} ,b1 are_relative_prime implies b1 = 1 )
proof
let c1 be Ordinal;
assume E10: ( {} ,c1 are_relative_prime & c1 <> 1 ) ;
then ( c1 in 1 or 1 in c1 ) by ORDINAL1:24;
then ( 1 in c1 & {} = c1 *^ {} & c1 = c1 *^ 1 ) by E10, Th5, ORDINAL2:55, ORDINAL2:56, ORDINAL3:17;
hence not verum by E10, Def2;
end;

defpred S1[ set ] means ex b1 being Ordinal st
( b1 c= a1 & a1 in omega & a1 <> {} & ( for b2, b3, b4 being natural Ordinal holds
not ( b3,b4 are_relative_prime & a1 = b2 *^ b3 & b1 = b2 *^ b4 ) ) );

theorem Th8: :: ARYTM_3:8
for b1, b2 being natural Ordinal holds
not ( not ( not b1 <> {} & not b2 <> {} ) & ( for b3, b4, b5 being natural Ordinal holds
not ( b4,b5 are_relative_prime & b1 = b3 *^ b4 & b2 = b3 *^ b5 ) ) )
proof
let c1, c2 be natural Ordinal;
assume that
E10: not ( not c1 <> {} & not c2 <> {} ) and
E11: for b1, b2, b3 being natural Ordinal holds
not ( b2,b3 are_relative_prime & c1 = b1 *^ b2 & c2 = b1 *^ b3 ) ;
E12: ex b1 being Ordinal st
S1[b1]
proof
per cases ( c1 c= c2 or c2 c= c1 ) ;
suppose E13: c1 c= c2 ;
take c3 = c2;
take c4 = c1;
thus ( c4 c= c3 & c3 in omega & c3 <> {} ) by E10, E13, ORDINAL1:def 13, XBOOLE_1:3;
thus for b1, b2, b3 being natural Ordinal holds
not ( b2,b3 are_relative_prime & c3 = b1 *^ b2 & c4 = b1 *^ b3 ) by E11;
end;
suppose E13: c2 c= c1 ;
take c3 = c1;
take c4 = c2;
thus ( c4 c= c3 & c3 in omega & c3 <> {} ) by E10, E13, ORDINAL1:def 13, XBOOLE_1:3;
thus for b1, b2, b3 being natural Ordinal holds
not ( b2,b3 are_relative_prime & c3 = b1 *^ b2 & c4 = b1 *^ b3 ) by E11;
end;
end;
end;
consider c3 being Ordinal such that
E13: S1[c3] and
E14: for b1 being Ordinal holds
( S1[b1] implies c3 c= b1 ) from ORDINAL1:sch 1(E12);
 consider c4 being Ordinal such that
E15: ( c4 c= c3 & c3 in omega & c3 <> {} & ( for b1, b2, b3 being natural Ordinal holds
not ( b2,b3 are_relative_prime & c3 = b1 *^ b2 & c4 = b1 *^ b3 ) ) ) by E13;
reconsider c5 = c3, c6 = c4 as Element of omega by E15, ORDINAL1:22;
( c5 = 1 *^ c5 & c6 = 1 *^ c6 ) by ORDINAL2:56;
then not c5,c6 are_relative_prime by E15;
then consider c7, c8, c9 being Ordinal such that
E16: ( c5 = c7 *^ c8 & c6 = c7 *^ c9 & c7 <> 1 ) by Def2;
E17: ( c8 <> {} & c7 <> {} ) by E15, E16, ORDINAL2:52, ORDINAL2:55;
then ( c7 c= c5 & c8 c= c5 & c9 c= c6 ) by E16, ORDINAL3:39;
then reconsider c10 = c7, c11 = c8, c12 = c9 as Element of omega by ORDINAL1:22;
( c5 = c11 *^ c10 & c6 = c12 *^ c10 ) by E16;
then E18: c12 c= c11 by E15, E17, ORDINAL3:38;
now
let c13, c14, c15 be natural Ordinal;
assume E19: ( c14,c15 are_relative_prime & c11 = c13 *^ c14 & c12 = c13 *^ c15 ) ;
then ( c5 = (c10 *^ c13) *^ c14 & c6 = (c10 *^ c13) *^ c15 ) by E16, ORDINAL3:58;
hence not verum by E15, E19;
end;
then E19: c5 c= c11 by E14, E17, E18;
( 1 in c10 or c10 in 1 ) by E16, ORDINAL1:24;
then 1 *^ c11 in c5 by E16, E17, ORDINAL3:17, ORDINAL3:22;
then c11 in c5 by ORDINAL2:56;
hence not verum by E19, ORDINAL1:7;
end;

registration
let c1, c2 be natural Ordinal;
cluster a1 div^ a2 -> natural ;
coherence
c1 div^ c2 is natural
proof
E10: ( c2 in 1 or 1 c= c2 ) by ORDINAL1:26;
( c2 = {} implies ( c1 div^ c2 = {} & {} *^ 1 = {} ) ) by ORDINAL2:52, ORDINAL3:def 7;
then (c1 div^ c2) *^ 1 c= (c1 div^ c2) *^ c2 by E10, ORDINAL3:17, ORDINAL3:23, XBOOLE_1:2;
then ( c1 div^ c2 c= (c1 div^ c2) *^ c2 & (c1 div^ c2) *^ c2 c= c1 ) by ORDINAL2:56, ORDINAL3:77;
then ( c1 div^ c2 c= c1 & c1 in omega ) by ORDINAL1:def 13, XBOOLE_1:1;
hence c1 div^ c2 in omega by ORDINAL1:22; :: according to ORDINAL1:def 13
end;
cluster a1 mod^ a2 -> natural ;
coherence
c1 mod^ c2 is natural
proof
((c1 div^ c2) *^ c2) +^ (c1 mod^ c2) = c1 by ORDINAL3:78;
then ( c1 mod^ c2 c= c1 & c1 in omega ) by ORDINAL1:def 13, ORDINAL3:27;
hence c1 mod^ c2 in omega by ORDINAL1:22; :: according to ORDINAL1:def 13
end;
end;

definition
let c1, c2 be Ordinal;
pred c1 divides c2 means :Def3: :: ARYTM_3:def 3
ex b1 being Ordinal st a2 = a1 *^ b1;
reflexivity
for b1 being Ordinal holds
ex b2 being Ordinal st b1 = b1 *^ b2
proof
let c3 be Ordinal;
take 1 ;
thus c3 = c3 *^ 1 by ORDINAL2:56;
end;
end;

:: deftheorem Def3 defines divides ARYTM_3:def 3 :
for b1, b2 being Ordinal holds
( b1 divides b2 iff ex b3 being Ordinal st b2 = b1 *^ b3 );

theorem Th9: :: ARYTM_3:9
for b1, b2 being natural Ordinal holds
( b1 divides b2 iff ex b3 being natural Ordinal st b2 = b1 *^ b3 )
proof
let c1, c2 be natural Ordinal;
thus not ( c1 divides c2 & ( for b1 being natural Ordinal holds
not c2 = c1 *^ b1 ) )
proof
given c3 being Ordinal such that E12: c2 = c1 *^ c3 ; :: according to ARYTM_3:def 3
per cases not ( not c2 = {} & not c2 <> {} ) ;
suppose c2 = {} ;
then c2 = c1 *^ {} by ORDINAL2:55;
hence ex b1 being natural Ordinal st c2 = c1 *^ b1 ;
end;
suppose c2 <> {} ;
then c3 is Element of omega by E12, Th2;
hence ex b1 being natural Ordinal st c2 = c1 *^ b1 by E12;
end;
end;
end;
thus ( ex b1 being natural Ordinal st c2 = c1 *^ b1 implies c1 divides c2 ) by Def3;
end;

theorem Th10: :: ARYTM_3:10
for b1, b2 being natural Ordinal holds
( {} in b1 implies b2 mod^ b1 in b1 )
proof
let c1, c2 be natural Ordinal;
assume {} in c1 ;
then consider c3 being Ordinal such that
E13: ( c2 = ((c2 div^ c1) *^ c1) +^ c3 & c3 in c1 ) by ORDINAL3:def 7;
c2 mod^ c1 = c2 -^ ((c2 div^ c1) *^ c1) by ORDINAL3:def 8;
hence c2 mod^ c1 in c1 by E13, ORDINAL3:65;
end;

theorem Th11: :: ARYTM_3:11
for b1, b2 being natural Ordinal holds
( b2 divides b1 iff b1 = b2 *^ (b1 div^ b2) )
proof
let c1, c2 be natural Ordinal;
assume E14: not ( c2 divides c1 iff c1 = c2 *^ (c1 div^ c2) ) ;
then consider c3 being natural Ordinal such that
E15: c1 = c2 *^ c3 by Th9;
( {} *^ c3 = {} & {} *^ (c1 div^ c2) = {} ) by ORDINAL2:52;
then {} <> c2 by E14, E15;
then ( {} in c2 & c1 = (c3 *^ c2) +^ {} ) by E15, ORDINAL2:44, ORDINAL3:10;
hence not verum by E14, E15, Def3, ORDINAL3:def 7;
end;

theorem Th12: :: ARYTM_3:12
canceled;

theorem Th13: :: ARYTM_3:13
for b1, b2 being natural Ordinal holds
( b1 divides b2 & b2 divides b1 implies b1 = b2 )
proof
let c1, c2 be natural Ordinal;
assume ( c1 divides c2 & c2 divides c1 ) ;
then E15: ( c2 = c1 *^ (c2 div^ c1) & c1 = c2 *^ (c1 div^ c2) ) by Th11;
then E16: ( c1 *^ 1 = c1 & c1 = c1 *^ ((c2 div^ c1) *^ (c1 div^ c2)) ) by ORDINAL2:56, ORDINAL3:58;
E17: ( c1 = {} implies c1 = c2 ) by E15, ORDINAL2:52;
( (c2 div^ c1) *^ (c1 div^ c2) = 1 implies c1 = c2 )
proof
assume (c2 div^ c1) *^ (c1 div^ c2) = 1 ;
then c2 div^ c1 = 1 by ORDINAL3:41;
hence c1 = c2 by E15, ORDINAL2:56;
end;
hence c1 = c2 by E16, E17, ORDINAL3:36;
end;

theorem Th14: :: ARYTM_3:14
for b1 being natural Ordinal holds
( b1 divides {} & 1 divides b1 )
proof
let c1 be natural Ordinal;
{} = c1 *^ {} by ORDINAL2:52;
hence c1 divides {} by Def3;
c1 = 1 *^ c1 by ORDINAL2:56;
hence 1 divides c1 by Def3;
end;

theorem Th15: :: ARYTM_3:15
for b1, b2 being natural Ordinal holds
( {} in b2 & b1 divides b2 implies b1 c= b2 )
proof
let c1, c2 be natural Ordinal;
assume E17: {} in c2 ;
given c3 being Ordinal such that E18: c2 = c1 *^ c3 ; :: according to ARYTM_3:def 3
c3 <> {} by E17, E18, ORDINAL2:55;
hence c1 c= c2 by E18, ORDINAL3:39;
end;

theorem Th16: :: ARYTM_3:16
for b1, b2, b3 being natural Ordinal holds
( b1 divides b2 & b1 divides b2 +^ b3 implies b1 divides b3 )
proof
let c1, c2, c3 be natural Ordinal;
assume c1 divides c2 ;
then consider c4 being natural Ordinal such that
E18: c2 = c1 *^ c4 by Th9;
assume c1 divides c2 +^ c3 ;
then consider c5 being natural Ordinal such that
E19: c2 +^ c3 = c1 *^ c5 by Th9;
assume E20: not c1 divides c3 ;
c3 = (c1 *^ c5) -^ (c1 *^ c4) by E18, E19, ORDINAL3:65
.= (c5 -^ c4) *^ c1 by ORDINAL3:76 ;
hence not verum by E20, Def3;
end;

Lemma18: 1 = succ 0
;

definition
let c1, c2 be natural Ordinal;
func c1 lcm c2 -> Element of omega means :Def4: :: ARYTM_3:def 4
( a1 divides a3 & a2 divides a3 & ( for b1 being natural Ordinal holds
( a1 divides b1 & a2 divides b1 implies a3 divides b1 ) ) );
existence
ex b1 being Element of omega st
( c1 divides b1 & c2 divides b1 & ( for b2 being natural Ordinal holds
( c1 divides b2 & c2 divides b2 implies b1 divides b2 ) ) )
proof
per cases not ( not c1 = {} & not c2 = {} & not ( c1 <> {} & c2 <> {} ) ) ;
suppose E19: ( c1 = {} or c2 = {} ) ;
reconsider c3 = {} as Element of omega by ORDINAL1:def 13;
take c3 ;
thus ( c1 divides c3 & c2 divides c3 ) by Th14;
let c4 be natural Ordinal;
assume ( c1 divides c4 & c2 divides c4 ) ;
hence c3 divides c4 by E19;
end;
suppose E19: ( c1 <> {} & c2 <> {} ) ;
E20: ( c1 divides c1 *^ c2 & c2 divides c1 *^ c2 ) by Def3;
defpred S2[ Ordinal] means ex b1 being natural Ordinal st
( a1 = b1 & c1 divides b1 & c2 divides b1 & c1 c= b1 );
{} c= c2 by XBOOLE_1:2;
then {} c< c2 by E19, XBOOLE_0:def 8;
then {} in c2 by ORDINAL1:21;
then 1 c= c2 by ORDINAL1:33, Lemma18;
then ( c1 *^ 1 = c1 & c1 *^ 1 c= c1 *^ c2 ) by ORDINAL2:56, ORDINAL2:58;
then E21: ex b1 being Ordinal st
S2[b1] by E20;
consider c3 being Ordinal such that
E22: S2[c3] and
E23: for b1 being Ordinal holds
( S2[b1] implies c3 c= b1 ) from ORDINAL1:sch 1(E21);
consider c4 being natural Ordinal such that
E24: ( c3 = c4 & c1 divides c4 & c2 divides c4 & c1 c= c4 ) by E22;
reconsider c5 = c4 as Element of omega by ORDINAL1:def 13;
take c5 ;
thus ( c1 divides c5 & c2 divides c5 ) by E24;
let c6 be natural Ordinal;
assume E25: ( c1 divides c6 & c2 divides c6 ) ;
now
{} c= c1 by XBOOLE_1:2;
then {} c< c1 by E19, XBOOLE_0:def 8;
then E26: {} in c1 by ORDINAL1:21;
E27: c6 = (c5 *^ (c6 div^ c5)) +^ (c6 mod^ c5) by ORDINAL3:78;
( c5 = c1 *^ (c5 div^ c1) & c5 = c2 *^ (c5 div^ c2) ) by E24, Th11;
then ( c5 *^ (c6 div^ c5) = c1 *^ ((c5 div^ c1) *^ (c6 div^ c5)) & c5 *^ (c6 div^ c5) = c2 *^ ((c5 div^ c2) *^ (c6 div^ c5)) ) by ORDINAL3:58;
then ( c1 divides c5 *^ (c6 div^ c5) & c2 divides c5 *^ (c6 div^ c5) ) by Def3;
then E28: ( c1 divides c6 mod^ c5 & c2 divides c6 mod^ c5 ) by E25, E27, Th16;
now
assume E29: c6 mod^ c5 <> {} ;
{} c= c6 mod^ c5 by XBOOLE_1:2;
then {} c< c6 mod^ c5 by E29, XBOOLE_0:def 8;
then {} in c6 mod^ c5 by ORDINAL1:21;
then c1 c= c6 mod^ c5 by E28, Th15;
then c5 c= c6 mod^ c5 by E23, E24, E28;
then not c6 mod^ c5 in c5 by ORDINAL1:7;
hence not verum by E24, E26, Th10;
end;
then c6 = c5 *^ (c6 div^ c5) by E27, ORDINAL2:44;
hence c5 divides c6 by Th11;
end;
hence c5 divides c6 ;
end;
end;
end;
uniqueness
for b1, b2 being Element of omega holds
( c1 divides b1 & c2 divides b1 & ( for b3 being natural Ordinal holds
( c1 divides b3 & c2 divides b3 implies b1 divides b3 ) ) & c1 divides b2 & c2 divides b2 & ( for b3 being natural Ordinal holds
( c1 divides b3 & c2 divides b3 implies b2 divides b3 ) ) implies b1 = b2 )
proof
let c3, c4 be Element of omega ;
assume that
E19: ( c1 divides c3 & c2 divides c3 & ( for b1 being natural Ordinal holds
( c1 divides b1 & c2 divides b1 implies c3 divides b1 ) ) ) and
E20: ( c1 divides c4 & c2 divides c4 & ( for b1 being natural Ordinal holds
( c1 divides b1 & c2 divides b1 implies c4 divides b1 ) ) ) ;
( c3 divides c4 & c4 divides c3 ) by E19, E20;
hence c3 = c4 by Th13;
end;
commutativity
for b1 being Element of omega
for b2, b3 being natural Ordinal holds
( b2 divides b1 & b3 divides b1 & ( for b4 being natural Ordinal holds
( b2 divides b4 & b3 divides b4 implies b1 divides b4 ) ) implies ( b3 divides b1 & b2 divides b1 & ( for b4 being natural Ordinal holds
( b3 divides b4 & b2 divides b4 implies b1 divides b4 ) ) ) ) ;
end;

:: deftheorem Def4 defines lcm ARYTM_3:def 4 :
for b1, b2 being natural Ordinal
for b3 being Element of omega holds
( b3 = b1 lcm b2 iff ( b1 divides b3 & b2 divides b3 & ( for b4 being natural Ordinal holds
( b1 divides b4 & b2 divides b4 implies b3 divides b4 ) ) ) );

theorem Th17: :: ARYTM_3:17
for b1, b2 being natural Ordinal holds b1 lcm b2 divides b1 *^ b2
proof
let c1, c2 be natural Ordinal;
( c1 divides c1 *^ c2 & c2 divides c1 *^ c2 ) by Def3;
hence c1 lcm c2 divides c1 *^ c2 by Def4;
end;

theorem Th18: :: ARYTM_3:18
for b1, b2 being natural Ordinal holds
( b1 <> {} implies (b2 *^ b1) div^ (b2 lcm b1) divides b2 )
proof
let c1, c2 be natural Ordinal;
assume E22: c1 <> {} ;
take (c2 lcm c1) div^ c1 ; :: according to ARYTM_3:def 3
( c2 lcm c1 divides c2 *^ c1 & c1 divides c2 lcm c1 ) by Def4, Th17;
then ( c2 *^ c1 = (c2 lcm c1) *^ ((c2 *^ c1) div^ (c2 lcm c1)) & c2 lcm c1 = c1 *^ ((c2 lcm c1) div^ c1) ) by Th11;
then c1 *^ c2 = c1 *^ (((c2 lcm c1) div^ c1) *^ ((c2 *^ c1) div^ (c2 lcm c1))) by ORDINAL3:58;
hence c2 = ((c2 *^ c1) div^ (c2 lcm c1)) *^ ((c2 lcm c1) div^ c1) by E22, ORDINAL3:36;
end;

definition
let c1, c2 be natural Ordinal;
func c1 hcf c2 -> Element of omega means :Def5: :: ARYTM_3:def 5
( a3 divides a1 & a3 divides a2 & ( for b1 being natural Ordinal holds
( b1 divides a1 & b1 divides a2 implies b1 divides a3 ) ) );
existence
ex b1 being Element of omega st
( b1 divides c1 & b1 divides c2 & ( for b2 being natural Ordinal holds
( b2 divides c1 & b2 divides c2 implies b2 divides b1 ) ) )
proof
per cases not ( not c1 = {} & not c2 = {} & not ( c1 <> {} & c2 <> {} ) ) ;
suppose E22: ( c1 = {} or c2 = {} ) ;
then reconsider c3 = c1 \/ c2 as Element of omega by ORDINAL1:def 13;
take c3 ;
thus ( c3 divides c1 & c3 divides c2 ) by E22, Th14;
thus for b1 being natural Ordinal holds
( b1 divides c1 & b1 divides c2 implies b1 divides c3 ) by E22;
end;
suppose E22: ( c1 <> {} & c2 <> {} ) ;
reconsider c3 = (c1 *^ c2) div^ (c1 lcm c2) as Element of omega by ORDINAL1:def 13;
take c3 ;
thus ( c3 divides c1 & c3 divides c2 ) by E22, Th18;
let c4 be natural Ordinal;
set c5 = c4 *^ ((c1 div^ c4) *^ (c2 div^ c4));
assume ( c4 divides c1 & c4 divides c2 ) ;
then E23: ( c1 = c4 *^ (c1 div^ c4) & c2 = c4 *^ (c2 div^ c4) ) by Th11;
then (c4 *^ (c1 div^ c4)) *^ (c2 div^ c4) = c2 *^ (c1 div^ c4) by ORDINAL3:58;
then ( c1 divides (c4 *^ (c1 div^ c4)) *^ (c2 div^ c4) & c2 divides (c4 *^ (c1 div^ c4)) *^ (c2 div^ c4) ) by E23, Def3;
then E24: ( c1 lcm c2 divides (c4 *^ (c1 div^ c4)) *^ (c2 div^ c4) & c4 *^ ((c1 div^ c4) *^ (c2 div^ c4)) = (c4 *^ (c1 div^ c4)) *^ (c2 div^ c4) ) by Def4, ORDINAL3:58;
then E25: c4 *^ ((c1 div^ c4) *^ (c2 div^ c4)) = (c1 lcm c2) *^ ((c4 *^ ((c1 div^ c4) *^ (c2 div^ c4))) div^ (c1 lcm c2)) by <