:: ARYTM_3 semantic presentation

E1: one in omega
by ORDINAL1:41, ORDINAL2:19;

registration
let c1 be Ordinal;
cluster -> ordinal Element of a1;
coherence
for b1 being Element of c1 holds b1 is ordinal
proof
let c2 be Element of c1;
not ( not c1 is empty & c1 is empty ) ;
hence c2 is ordinal by ORDINAL1:23, SUBSET_1:def 2;
end;
end;

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

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

registration
let c1 be natural Ordinal;
cluster succ a1 -> natural ;
coherence
succ c1 is natural
proof
c1 in omega by ORDINAL2:def 21;
hence succ c1 in omega by ORDINAL1:41, ORDINAL2:19; :: uses ORDINAL2:def 21
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, ORDINAL2:def 21;
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 is_limit_ordinal ;
then ( omega c= c1 & not c1 in c1 ) by E8, ORDINAL2:def 5;
then not c1 in omega ;
hence ( for b1 being Ordinal holds
( b1 in c1 implies S1[b1] ) implies S1[c1] ) by ORDINAL2:def 21;
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 E2: :: 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 ; :: uses ORDINAL2:def 21
( 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 E2, ORDINAL2:def 5; :: uses ORDINAL2:def 21
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 E3: :: ARYTM_3:2
for b1, b2 being Ordinal holds
( ( b1 *^ b2 is natural ) implies ( b1 *^ b2 is empty or ( b1 in omega & b2 in omega ) ) )
proof
let c1, c2 be Ordinal;
assume E4: c1 *^ c2 in omega ; :: uses ORDINAL2:def 21
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 E4: :: 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 E5: :: 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 E4
.= 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 a1 +^ a2 -> set ;
commutativity
for b1, b2 being natural Ordinal holds b1 +^ b2 = b2 +^ b1 by E4;
redefine func *^ as a1 *^ a2 -> set ;
commutativity
for b1, b2 being natural Ordinal holds b1 *^ b2 = b2 *^ b1 by E5;
end;

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

:: deftheorem E6 defines are_relative_prime ARYTM_3:def 1 :
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 = one ) ) );

theorem E7: :: ARYTM_3:5
not {} , {} are_relative_prime
proof
take {} ; :: uses ARYTM_3:def 1
take {} ;
take {} ;
thus ( {} = {} *^ {} & {} = {} *^ {} & not {} = one ) by ORDINAL2:52;
end;

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

theorem E9: :: ARYTM_3:7
for b1 being Ordinal holds
( {} ,b1 are_relative_prime implies b1 = one )
proof
let c1 be Ordinal;
assume E10: ( {} ,c1 are_relative_prime & c1 <> one ) ;
then ( c1 in one or one in c1 ) by ORDINAL1:24;
then ( one in c1 & {} = c1 *^ {} & c1 = c1 *^ one ) by E10, E7, ORDINAL2:55, ORDINAL2:56, ORDINAL3:17;
hence not verum by E10, E6;
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 :: 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, ORDINAL2:def 21, 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, ORDINAL2:def 21, 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 = one *^ c5 & c6 = one *^ 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 <> one ) by E6;
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;
( one in c10 or c10 in one ) by E16, ORDINAL1:24;
then one *^ 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 one or one c= c2 ) by ORDINAL1:26;
( c2 = {} implies ( c1 div^ c2 = {} & {} *^ one = {} ) ) by ORDINAL2:52, ORDINAL3:def 7;
then (c1 div^ c2) *^ one 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 ORDINAL2:def 21, XBOOLE_1:1;
hence c1 div^ c2 in omega by ORDINAL1:22; :: uses ORDINAL2:def 21
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 ORDINAL2:def 21, ORDINAL3:27;
hence c1 mod^ c2 in omega by ORDINAL1:22; :: uses ORDINAL2:def 21
end;
end;

definition
let c1, c2 be Ordinal;
pred a1 divides a2 means :E10: :: ARYTM_3:def 2
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 one ;
thus c3 = c3 *^ one by ORDINAL2:56;
end;
end;

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

theorem E11: :: 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 ; :: uses ARYTM_3:def 2
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, E3;
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 E10;
end;

theorem E12: :: 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 E13: :: 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 E11;
( {} *^ 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, E10, ORDINAL3:def 7;
end;

theorem :: ARYTM_3:12
canceled;

theorem E14: :: 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 E13;
then E16: ( c1 *^ one = 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) = one implies c1 = c2 )
proof
assume (c2 div^ c1) *^ (c1 div^ c2) = one ;
then c2 div^ c1 = one by ORDINAL3:41;
hence c1 = c2 by E15, ORDINAL2:56;
end;
hence c1 = c2 by E16, E17, ORDINAL3:36;
end;

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

theorem E16: :: 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 ; :: uses ARYTM_3:def 2
c3 <> {} by E17, E18, ORDINAL2:55;
hence c1 c= c2 by E18, ORDINAL3:39;
end;

theorem E17: :: 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 E11;
assume c1 divides c2 +^ c3 ;
then consider c5 being natural Ordinal such that
E19: c2 +^ c3 = c1 *^ c5 by E11;
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, E10;
end;

definition
let c1, c2 be natural Ordinal;
func a1 lcm a2 -> Element of omega means :E18: :: ARYTM_3:def 3
( 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 E18: ( c1 = {} or c2 = {} ) ;
reconsider c3 = {} as Element of omega by ORDINAL2:def 21;
take c3 ;
thus ( c1 divides c3 & c2 divides c3 ) by E15;
let c4 be natural Ordinal;
assume ( c1 divides c4 & c2 divides c4 ) ;
hence c3 divides c4 by E18;
end;
suppose E18: ( c1 <> {} & c2 <> {} ) ;
E19: ( c1 divides c1 *^ c2 & c2 divides c1 *^ c2 ) by E10;
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 E18, XBOOLE_0:def 8;
then {} in c2 by ORDINAL1:21;
then one c= c2 by ORDINAL1:33;
then ( c1 *^ one = c1 & c1 *^ one c= c1 *^ c2 ) by ORDINAL2:56, ORDINAL2:58;
then E20: ex b1 being Ordinal st
S2[b1] by E19;
consider c3 being Ordinal such that
E21: S2[c3]
and E22: for b1 being Ordinal holds
( S2[b1] implies c3 c= b1 ) from ORDINAL1:sch 1(E20);
consider c4 being natural Ordinal such that
E23: ( c3 = c4 & c1 divides c4 & c2 divides c4 & c1 c= c4 ) by E21;
reconsider c5 = c4 as Element of omega by ORDINAL2:def 21;
take c5 ;
thus ( c1 divides c5 & c2 divides c5 ) by E23;
let c6 be natural Ordinal;
assume E24: ( c1 divides c6 & c2 divides c6 ) ;
now
{} c= c1 by XBOOLE_1:2;
then {} c< c1 by E18, XBOOLE_0:def 8;
then E25: {} in c1 by ORDINAL1:21;
E26: c6 = (c5 *^ (c6 div^ c5)) +^ (c6 mod^ c5) by ORDINAL3:78;
( c5 = c1 *^ (c5 div^ c1) & c5 = c2 *^ (c5 div^ c2) ) by E23, E13;
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 E10;
then E27: ( c1 divides c6 mod^ c5 & c2 divides c6 mod^ c5 ) by E24, E26, E17;
now
assume E28: c6 mod^ c5 <> {} ;
{} c= c6 mod^ c5 by XBOOLE_1:2;
then {} c< c6 mod^ c5 by E28, XBOOLE_0:def 8;
then {} in c6 mod^ c5 by ORDINAL1:21;
then c1 c= c6 mod^ c5 by E27, E16;
then c5 c= c6 mod^ c5 by E22, E23, E27;
then not c6 mod^ c5 in c5 by ORDINAL1:7;
hence not verum by E23, E25, E12;
end;
then c6 = c5 *^ (c6 div^ c5) by E26, ORDINAL2:44;
hence c5 divides c6 by E13;
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 E18: ( c1 divides c3 & c2 divides c3 & for b1 being natural Ordinal holds
( ( c1 divides b1 & c2 divides b1 ) implies ( c3 divides b1 ) ) )
and E19: ( 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 E18, E19;
hence c3 = c4 by E14;
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 E18 defines lcm ARYTM_3:def 3 :
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 E19: :: 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 E10;
hence c1 lcm c2 divides c1 *^ c2 by E18;
end;

theorem E20: :: 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 E21: c1 <> {} ;
take (c2 lcm c1) div^ c1 ; :: uses ARYTM_3:def 2
( c2 lcm c1 divides c2 *^ c1 & c1 divides c2 lcm c1 ) by E18, E19;
then ( c2 *^ c1 = (c2 lcm c1) *^ ((c2 *^ c1) div^ (c2 lcm c1)) & c2 lcm c1 = c1 *^ ((c2 lcm c1) div^ c1) ) by E13;
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 E21, ORDINAL3:36;
end;

definition
let c1, c2 be natural Ordinal;
func a1 hcf a2 -> Element of omega means :E21: :: ARYTM_3:def 4
( 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 E21: ( c1 = {} or c2 = {} ) ;
then reconsider c3 = c1 \/ c2 as Element of omega by ORDINAL2:def 21;
take c3 ;
thus ( c3 divides c1 & c3 divides c2 ) by E21, E15;
thus for b1 being natural Ordinal holds
( ( b1 divides c1 & b1 divides c2 ) implies ( b1 divides c3 ) ) by E21;
end;
suppose E21: ( c1 <> {} & c2 <> {} ) ;
reconsider c3 = (c1 *^ c2) div^ (c1 lcm c2) as Element of omega by ORDINAL2:def 21;
take c3 ;
thus ( c3 divides c1 & c3 divides c2 ) by E21, E20;
let c4 be natural Ordinal;
set c5 = c4 *^ ((c1 div^ c4) *^ (c2 div^ c4));
assume ( c4 divides c1 & c4 divides c2 ) ;
then E22: ( c1 = c4 *^ (c1 div^ c4) & c2 = c4 *^ (c2 div^ c4) ) by E13;
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 E22, E10;
then E23: ( 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 E18, ORDINAL3:58;
then E24: c4 *^ ((c1 div^ c4) *^ (c2 div^ c4)) = (c1 lcm c2) *^ ((c4 *^ ((c1 div^ c4) *^ (c2 div^ c4))) div^ (c1 lcm c2)) by E13;
then E25: (c4 *^ ((c1 div^ c4) *^ (c2 div^ c4))) *^ c4 = (c1 lcm c2) *^ (c4 *^ ((c4 *^ ((c1 div^ c4) *^ (c2 div^ c4))) div^ (c1 lcm c2))) by ORDINAL3:58;
E26: ( c4 <> {} & c1 div^ c4 <> {} & c2 div^ c4 <> {} ) by E21, E22, ORDINAL2:52;
then (c1 div^ c4) *^ (c2 div^ c4) <> {} by ORDINAL3:34;
then c4 *^ ((c1 div^ c4) *^ (c2 div^ c4)) <> {} by E26, ORDINAL3:34;
then c1 lcm c2 <> {} by E24, ORDINAL2:52;
then ( c1 *^ c2 = (c1 lcm c2) *^ (c4 *^ ((c4 *^ ((c1 div^ c4) *^ (c2 div^ c4))) div^ (c1 lcm c2))) & c1 *^ c2 = (c1 *^ c2) +^ {} & {} in c1 lcm c2 ) by E22, E23, E25, ORDINAL2:44, ORDINAL3:10, ORDINAL3:58;
then c3 = c4 *^ ((c4 *^ ((c1 div^ c4) *^ (c2 div^ c4))) div^ (c1 lcm c2)) by ORDINAL3:79;
hence c4 divides c3 by E10;
end;
end;
end;
uniqueness
for b1, b2 being Element of omega holds
( ( b1 divides c1 & b1 divides c2 & for b3 being natural Ordinal holds
( ( b3 divides c1 & b3 divides c2 ) implies ( b3 divides b1 ) ) & b2 divides c1 & b2 divides c2 & for b3 being natural Ordinal holds
( ( b3 divides c1 & b3 divides c2 ) implies ( b3 divides b2 ) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Element of omega ;
assume that E21: ( c3 divides c1 & c3 divides c2 & for b1 being natural Ordinal holds
( ( b1 divides c1 & b1 divides c2 ) implies ( b1 divides c3 ) ) )
and E22: ( c4 divides c1 & c4 divides c2 & for b1 being natural Ordinal holds
( ( b1 divides c1 & b1 divides c2 ) implies ( b1 divides c4 ) ) ) ;
( c3 divides c4 & c4 divides c3 ) by E21, E22;
hence c3 = c4 by E14;
end;
commutativity
for b1 being Element of omega
for b2, b3 being natural Ordinal holds
( ( b1 divides b2 & b1 divides b3 & for b4 being natural Ordinal holds
( ( b4 divides b2 & b4 divides b3 ) implies ( b4 divides b1 ) ) ) implies ( ( b1 divides b3 & b1 divides b2 & for b4 being natural Ordinal holds
( ( b4 divides b3 & b4 divides b2 ) implies ( b4 divides b1 ) ) ) ) ) ;
end;

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

theorem E22: :: ARYTM_3:19
for b1 being natural Ordinal holds
( b1 hcf {} = b1 & b1 lcm {} = {} )
proof
let c1 be natural Ordinal;
reconsider c2 = c1, c3 = {} as Element of omega by ORDINAL2:def 21;
E23: ( c2 divides c1 & c2 divides {} & for b1 being natural Ordinal holds
( ( b1 divides c1 & b1 divides {} ) implies ( b1 divides c2 ) ) ) by E15;
( c1 divides c3 & {} divides c3 & for b1 being natural Ordinal holds
( ( c1 divides b1 & {} divides b1 ) implies ( c3 divides b1 ) ) ) by E15;
hence ( c1 hcf {}