environ
vocabularies HIDDEN, NUMBERS, NAT_1, INT_1, CARD_1, ARYTM_3, XXREAL_0, ARYTM_1, RELAT_1, INT_2, SUBSET_1, FINSET_1, XBOOLE_0, TARSKI, COMPLEX1, FUNCT_1, FUNCT_2, FINSEQ_1, NEWTON, ZFMISC_1, EULER_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, INT_1, NAT_1, NAT_D, INT_2, FINSEQ_1, FINSET_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, XXREAL_0, NEWTON;
definitions TARSKI, FUNCT_1, FUNCT_2, XBOOLE_0;
theorems TARSKI, INT_2, AXIOMS, FINSEQ_1, CARD_1, NAT_1, ABSVALUE, CARD_2, ZFMISC_1, INT_1, FUNCT_1, FUNCT_2, PRE_FF, DOMAIN_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, NEWTON, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, NAT_D, RELAT_1;
schemes NAT_1, FUNCT_7;
registrations ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, NEWTON, MEMBERED;
constructors HIDDEN, BINOP_1, XXREAL_0, REAL_1, NAT_1, NAT_D, NEWTON, WELLORD2, RELSET_1, MEMBERED;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities TARSKI, XBOOLE_0, BINOP_1, CARD_1, ORDINAL1;
expansions FUNCT_2, XBOOLE_0;
Lm1:
for k being Nat
for j being Integer st k <> 0 & [\(j / k)/] + 1 >= j / k holds
k >= j - ([\(j / k)/] * k)
Lm2:
not 1 is prime
by INT_2:def 4;
theorem Th5:
for
a,
b being
Nat st
a gcd b = 1 holds
for
c being
Nat holds
(a * c) gcd (b * c) = c
set X = { k where k is Element of NAT : ( 1,k are_coprime & k >= 1 & k <= 1 ) } ;
for x being object holds
( x in { k where k is Element of NAT : ( 1,k are_coprime & k >= 1 & k <= 1 ) } iff x = 1 )
then Lm3:
card {1} = Euler 1
by TARSKI:def 1;
set X = { k where k is Element of NAT : ( 2,k are_coprime & k >= 1 & k <= 2 ) } ;
for x being object holds
( x in { k where k is Element of NAT : ( 2,k are_coprime & k >= 1 & k <= 2 ) } iff x = 1 )
then Lm4:
card {1} = Euler 2
by TARSKI:def 1;