begin
Lm1:
{} in omega
by ORDINAL1:def 12;
Lm2:
1 in omega
;
:: deftheorem defines one ARYTM_3:def 1 :
begin
:: deftheorem Def2 defines are_relative_prime ARYTM_3:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th6:
theorem Th7:
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
:: deftheorem Def3 defines divides ARYTM_3:def 3 :
theorem Th9:
theorem Th10:
theorem Th11:
theorem
canceled;
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
Lm3:
1 = succ {}
;
:: deftheorem Def4 defines lcm ARYTM_3:def 4 :
theorem Th17:
theorem Th18:
:: deftheorem Def5 defines hcf ARYTM_3:def 5 :
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
:: deftheorem defines RED ARYTM_3:def 6 :
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
set RATplus = { [a,b] where a, b is Element of omega : ( a,b are_relative_prime & b <> {} ) } ;
1,1 are_relative_prime
by Th6;
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 <> {} )
begin
:: deftheorem defines RAT+ ARYTM_3:def 7 :
Lm5:
omega c= RAT+
by XBOOLE_1:7;
theorem
canceled;
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
definition
let x be
Element of
RAT+ ;
func numerator x -> Element of
omega means :
Def8:
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] ) )
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 ZFMISC_1:33;
func denominator x -> Element of
omega means :
Def9:
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] ) )
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 ZFMISC_1:33;
end;
:: deftheorem Def8 defines numerator ARYTM_3:def 8 :
:: deftheorem Def9 defines denominator ARYTM_3:def 9 :
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem
definition
let i,
j be
natural Ordinal;
func i / j -> Element of
RAT+ equals :
Def10:
{} if j = {} RED i,
j if RED j,
i = 1
otherwise [(RED i,j),(RED j,i)];
coherence
( ( 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+ ) )
consistency
for b1 being Element of RAT+ st j = {} & RED j,i = 1 holds
( b1 = {} iff b1 = RED i,j )
by Th31;
end;
:: deftheorem Def10 defines / ARYTM_3:def 10 :
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
:: deftheorem defines + ARYTM_3:def 11 :
:: deftheorem defines *' ARYTM_3:def 12 :
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem Th66:
:: deftheorem Def13 defines <=' ARYTM_3:def 13 :
theorem
canceled;
theorem
theorem Th69:
theorem Th70:
theorem Th71:
theorem
theorem Th73:
theorem Th74:
theorem
theorem
theorem
theorem Th78:
theorem Th79:
theorem Th80:
theorem
theorem
theorem Th83:
theorem
canceled;
theorem
theorem
theorem Th87:
theorem
theorem
theorem Th90:
theorem
theorem
theorem
theorem Th94:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem