Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### The Euler's Function

**by****Yoshinori Fujisawa, and****Yasushi Fuwa**- Received December 10, 1997
- MML identifier: EULER_1

- [ Mizar article, MML identifier index ]

environ vocabulary INT_1, INT_2, ARYTM_3, ABSVALUE, NAT_1, ARYTM_1, ORDINAL2, ARYTM, FILTER_0, FINSET_1, CARD_1, BOOLE, FUNCT_1, SGRAPH1, RELAT_1, FINSEQ_1, EULER_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, CARD_1, INT_1, GROUP_1, NAT_1, INT_2, FINSEQ_1, FINSET_1, RELAT_1, FUNCT_1, FUNCT_2; constructors NAT_1, GROUP_1, INT_2, REAL_1, DOMAIN_1, MEMBERED; clusters SUBSET_1, FINSET_1, INT_1, CARD_1, XREAL_0, FINSEQ_1, RELSET_1, ARYTM_3, MEMBERED, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminary reserve a,b,c,k,l,m,n for Nat, i,j,x,y for Integer; theorem :: EULER_1:1 for k, n being natural number holds k in n iff k < n; theorem :: EULER_1:2 n,n are_relative_prime iff n = 1; theorem :: EULER_1:3 k <> 0 & k < n & n is prime implies k,n are_relative_prime; theorem :: EULER_1:4 n is prime & k in {kk where kk is Nat:n,kk are_relative_prime & kk >= 1 & kk <= n} iff n is prime & k in n & not k in {0}; theorem :: EULER_1:5 for A being finite set, x being set st x in A holds Card(A \ {x}) = Card A - Card{x}; theorem :: EULER_1:6 a hcf b = 1 implies for c holds a*c hcf b*c = c; theorem :: EULER_1:7 a <> 0 & b <> 0 & c <> 0 & a*c hcf b*c = c implies a,b are_relative_prime; theorem :: EULER_1:8 a hcf b = 1 implies (a + b) hcf b = 1; theorem :: EULER_1:9 for c holds (a + b*c) hcf b = a hcf b; theorem :: EULER_1:10 m,n are_relative_prime implies ex k st (ex i0,j0 being Integer st k = i0*m + j0*n & k > 0) & for l st (ex i,j being Integer st l = i*m + j*n & l > 0) holds k <= l; theorem :: EULER_1:11 m,n are_relative_prime implies for k holds ex i,j st i*m + j*n = k; theorem :: EULER_1:12 for A,B being non empty finite set holds (ex f being Function of A, B st f is one-to-one onto) implies Card A = Card B; theorem :: EULER_1:13 for i,k,n being Integer holds (i + k*n) mod n = i mod n; theorem :: EULER_1:14 a <> 0 & b <> 0 & c <> 0 & c divides a*b & a,c are_relative_prime implies c divides b; theorem :: EULER_1:15 a <> 0 & b <> 0 & c <> 0 & a,c are_relative_prime & b,c are_relative_prime implies a*b,c are_relative_prime; theorem :: EULER_1:16 x <> 0 & y <> 0 & i > 0 implies i*x gcd i*y = i*(x gcd y); theorem :: EULER_1:17 for x st a <> 0 & b <> 0 holds (a + x*b) gcd b = a gcd b; begin :: Euler's function definition let n be Nat; func Euler n -> Nat equals :: EULER_1:def 1 Card {k where k is Nat : n,k are_relative_prime & k >= 1 & k <= n}; end; theorem :: EULER_1:18 Euler 1 = 1; theorem :: EULER_1:19 Euler 2 = 1; theorem :: EULER_1:20 n > 1 implies Euler n <= n - 1; theorem :: EULER_1:21 n is prime implies Euler n = n - 1; theorem :: EULER_1:22 m > 1 & n > 1 & m,n are_relative_prime implies Euler (m*n) = Euler m * Euler n;

Back to top