:: Euler's Function
:: by Yoshinori Fujisawa and Yasushi Fuwa
::
:: Received December 10, 1997
:: Copyright (c) 1997-2019 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;