:: EULER_1 semantic presentation
begin
theorem
:: EULER_1:1
for
n
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) holds
(
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ,
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
are_relative_prime
iff
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
=
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: EULER_1:2
for
k
,
n
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
k
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
<>
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
k
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
<
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) &
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) is
prime
holds
k
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ,
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
are_relative_prime
;
theorem
:: EULER_1:3
for
n
,
k
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) holds
(
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) is
prime
&
k
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
in
{
kk
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) where
kk
is ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : (
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ,
kk
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
are_relative_prime
&
kk
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
>=
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
kk
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
<=
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) )
}
iff (
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) is
prime
&
k
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
in
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) & not
k
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
in
{
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
}
: ( ( ) ( non
empty
trivial
finite
V42
() 1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) ) ) ;
theorem
:: EULER_1:4
for
A
being ( (
finite
) (
finite
)
set
)
for
x
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
A
: ( (
finite
) (
finite
)
set
) holds
card
(
A
: ( (
finite
) (
finite
)
set
)
\
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
finite
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
)
: ( ( ) (
finite
)
Element
of
bool
b
1
: ( (
finite
) (
finite
)
set
) : ( ( ) ( non
empty
finite
V42
() )
set
) ) : ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
set
) )
=
(
card
A
: ( (
finite
) (
finite
)
set
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
set
) )
-
(
card
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
finite
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
)
: ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
set
) ) : ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
) ;
theorem
:: EULER_1:5
for
a
,
b
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
gcd
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
=
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
for
c
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) holds
(
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
*
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
gcd
(
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
*
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
) : ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
=
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ;
theorem
:: EULER_1:6
for
a
,
c
,
b
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
<>
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
<>
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
(
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
*
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
gcd
(
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
*
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
) : ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
=
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) holds
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ,
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
are_relative_prime
;
theorem
:: EULER_1:7
for
a
,
b
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
gcd
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
=
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
(
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
+
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
gcd
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
=
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: EULER_1:8
for
a
,
b
,
c
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) holds
(
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
+
(
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
*
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
gcd
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
=
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
gcd
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
) ;
theorem
:: EULER_1:9
for
m
,
n
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
m
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ,
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
are_relative_prime
holds
ex
k
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
( ex
i0
,
j0
being ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
) st
(
k
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
=
(
i0
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
*
m
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
+
(
j0
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
*
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
) : ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
) &
k
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
>
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) & ( for
l
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st ex
i
,
j
being ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
) st
(
l
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
=
(
i
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
*
m
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
)
+
(
j
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
*
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
) : ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
) &
l
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
>
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ) holds
k
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
<=
l
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ) ) ;
theorem
:: EULER_1:10
for
m
,
n
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
m
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ,
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
are_relative_prime
holds
for
k
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ex
i
,
j
being ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
) st
(
i
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
*
m
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
)
+
(
j
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
*
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
) : ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
)
=
k
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ;
theorem
:: EULER_1:11
for
A
being ( ( ) ( )
set
)
for
B
being ( ( non
empty
) ( non
empty
)
set
)
for
f
being ( (
Function-like
quasi_total
) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
b
2
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of
A
: ( ( ) ( )
set
) ,
B
: ( ( non
empty
) ( non
empty
)
set
) ) st
f
: ( (
Function-like
quasi_total
) (
Relation-like
b
1
: ( ( ) ( )
set
)
-defined
b
2
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of
b
1
: ( ( ) ( )
set
) ,
b
2
: ( ( non
empty
) ( non
empty
)
set
) ) is
bijective
holds
card
A
: ( ( ) ( )
set
) : ( (
cardinal
) (
V27
()
V28
()
V29
()
cardinal
)
set
)
=
card
B
: ( ( non
empty
) ( non
empty
)
set
) : ( (
cardinal
) ( non
empty
V27
()
V28
()
V29
()
cardinal
)
set
) ;
theorem
:: EULER_1:12
for
i
,
k
,
n
being ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
) holds
(
i
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
+
(
k
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
*
n
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
)
mod
n
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
) : ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
set
)
=
i
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
mod
n
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
) : ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
set
) ;
theorem
:: EULER_1:13
for
c
,
a
,
b
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
divides
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
*
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
) &
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ,
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
are_relative_prime
holds
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
divides
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ;
theorem
:: EULER_1:14
for
a
,
c
,
b
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
<>
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
<>
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ,
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
are_relative_prime
&
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ,
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
are_relative_prime
holds
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
*
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
) ,
c
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
are_relative_prime
;
theorem
:: EULER_1:15
for
x
,
i
,
y
being ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
) st
x
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
<>
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
i
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
>
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
(
i
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
*
x
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
)
gcd
(
i
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
*
y
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
) : ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
=
i
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
*
(
x
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
gcd
y
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
)
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
) : ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
) ;
theorem
:: EULER_1:16
for
a
,
b
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
for
x
being ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
) st
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
<>
0
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
(
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
+
(
x
: ( (
integer
) (
ext-real
V34
()
V35
()
integer
)
Integer
)
*
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
)
)
: ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
)
gcd
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
)
=
a
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
gcd
b
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
) ;
begin
definition
let
n
be ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ;
func
Euler
n
->
( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
equals
:: EULER_1:def 1
card
{
k
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) where
k
is ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : (
n
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ,
k
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
are_relative_prime
&
k
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
>=
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
k
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
<=
n
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) )
}
: ( (
cardinal
) (
V27
()
V28
()
V29
()
cardinal
)
set
) ;
end;
theorem
:: EULER_1:17
Euler
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
=
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: EULER_1:18
Euler
2 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
=
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: EULER_1:19
for
n
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
>
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
Euler
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
<=
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
-
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
) ;
theorem
:: EULER_1:20
for
n
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) is
prime
holds
Euler
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) : ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
=
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
-
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
ext-real
V34
()
V35
()
integer
)
set
) ;
theorem
:: EULER_1:21
for
m
,
n
being ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) st
m
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
>
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
>
1 : ( ( ) ( non
empty
ext-real
positive
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) &
m
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
) ,
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
are_relative_prime
holds
Euler
(
m
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
*
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
set
) : ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
=
(
Euler
m
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
*
(
Euler
n
: ( (
V33
() ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Nat
)
)
: ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( ( ) (
ext-real
non
negative
V27
()
V28
()
V29
()
V33
()
V34
()
V35
()
integer
finite
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
V27
()
V28
()
V29
() non
finite
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ;