:: Euler's {T}heorem and Small {F}ermat's Theorem
:: by Yoshinori Fujisawa , Yasushi Fuwa and Hidetaka Shimizu
::
:: Received June 10, 1998
:: Copyright (c) 1998 Association of Mizar Users
Lm1:
for t being Integer holds
( t < 1 iff t <= 0 )
Lm2:
for a being Nat st a <> 0 holds
a - 1 >= 0
Lm3:
for z being Integer holds 1 gcd z = 1
theorem :: EULER_2:1
theorem Th2: :: EULER_2:2
Lm4:
for m being Nat
for z being Integer st m > 1 & 1 - m <= z & z <= m - 1 & m divides z holds
z = 0
theorem :: EULER_2:3
canceled;
theorem :: EULER_2:4
canceled;
theorem Th5: :: EULER_2:5
theorem Th6: :: EULER_2:6
theorem Th7: :: EULER_2:7
theorem :: EULER_2:8
theorem Th9: :: EULER_2:9
theorem :: EULER_2:10
theorem Th11: :: EULER_2:11
theorem :: EULER_2:12
canceled;
theorem :: EULER_2:13
canceled;
theorem :: EULER_2:14
canceled;
theorem :: EULER_2:15
canceled;
theorem :: EULER_2:16
canceled;
theorem :: EULER_2:17
canceled;
theorem :: EULER_2:18
canceled;
theorem :: EULER_2:19
canceled;
theorem :: EULER_2:20
canceled;
theorem :: EULER_2:21
canceled;
theorem :: EULER_2:22
canceled;
theorem :: EULER_2:23
canceled;
theorem :: EULER_2:24
canceled;
theorem Th25: :: EULER_2:25
:: deftheorem Def1 defines mod EULER_2:def 1 :
theorem :: EULER_2:26
theorem Th27: :: EULER_2:27
theorem :: EULER_2:28
theorem :: EULER_2:29
theorem :: EULER_2:30
theorem :: EULER_2:31
theorem :: EULER_2:32
theorem Th33: :: EULER_2:33
theorem :: EULER_2:34