:: Euler's Function :: by Yoshinori Fujisawa and Yasushi Fuwa :: :: Received December 10, 1997 :: Copyright (c) 1997-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies 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 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; constructors BINOP_1, XXREAL_0, REAL_1, NAT_1, NAT_D, NEWTON, WELLORD2, RELSET_1, MEMBERED; registrations ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, NEWTON, MEMBERED; 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 n,n are_coprime iff n = 1; theorem :: EULER_1:2 for k,n be Nat holds k <> 0 & k < n & n is prime implies k,n are_coprime; theorem :: EULER_1:3 n is prime & k in {kk where kk is Element of NAT: n,kk are_coprime & kk >= 1 & kk <= n} iff n is prime & k in Segm n & not k in {0}; theorem :: EULER_1:4 for A being finite set, x being set st x in A holds card(A \ {x}) = card A - card{x}; :: dlaczego nie card A - 1 :: !!! ??? theorem :: EULER_1:5 a gcd b = 1 implies for c holds a*c gcd b*c = c; theorem :: EULER_1:6 a <> 0 & c <> 0 & a*c gcd b*c = c implies a,b are_coprime; theorem :: EULER_1:7 a gcd b = 1 implies (a + b) gcd b = 1; theorem :: EULER_1:8 for a, b, c be Nat holds (a + b*c) gcd b = a gcd b; theorem :: EULER_1:9 m,n are_coprime 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:10 m,n are_coprime implies for k holds ex i,j st i*m + j*n = k; theorem :: EULER_1:11 ::: KNASTER:13 for A be set, B being non empty set, f being Function of A, B st f is bijective holds card A = card B; theorem :: EULER_1:12 for i,k,n being Integer holds (i + k*n) mod n = i mod n; theorem :: EULER_1:13 c divides a*b & a,c are_coprime implies c divides b; theorem :: EULER_1:14 a <> 0 & c <> 0 & a,c are_coprime & b,c are_coprime implies a*b,c are_coprime; theorem :: EULER_1:15 x <> 0 & i >= 0 implies i*x gcd i*y = i*(x gcd y); theorem :: EULER_1:16 for x st a <> 0 holds (a + x*b) gcd b = a gcd b; begin :: Euler's function definition let n be Nat; func Euler n -> Element of NAT equals :: EULER_1:def 1 card {k where k is Element of NAT: n,k are_coprime & k >= 1 & k <= n}; end; theorem :: EULER_1:17 Euler 1 = 1; theorem :: EULER_1:18 Euler 2 = 1; theorem :: EULER_1:19 n > 1 implies Euler n <= n - 1; theorem :: EULER_1:20 n is prime implies Euler n = n - 1; theorem :: EULER_1:21 m > 1 & n > 1 & m,n are_coprime implies Euler (m*n) = Euler m * Euler n;