let k be Nat; ( k >= 3 implies for m being Nat st m,2 |^ k are_coprime holds
not m is_primitive_root_of 2 |^ k )
assume A1:
k >= 3
; for m being Nat st m,2 |^ k are_coprime holds
not m is_primitive_root_of 2 |^ k
now for m being Nat holds
( not m,2 |^ k are_coprime or not m is_primitive_root_of 2 |^ k )assume
ex
m being
Nat st
(
m,2
|^ k are_coprime &
m is_primitive_root_of 2
|^ k )
;
contradictionthen consider m being
Nat such that A2:
(
m,2
|^ k are_coprime &
m is_primitive_root_of 2
|^ k )
;
then A4:
(m |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1
by A1, Th7;
A5:
2
|^ k > 1
by A1, PEPIN:25;
order (
m,
(2 |^ k))
<= 2
|^ (k -' 2)
by A2, A4, A5, PEPIN:def 2;
then A6:
Euler (2 |^ k) <= 2
|^ (k -' 2)
by A2;
A7:
k > 1
by XXREAL_0:2, A1;
k = (k -' 1) + 1
by A7, XREAL_1:235;
then A8:
Euler (2 |^ k) =
(2 |^ ((k -' 1) + 1)) - (2 |^ (k -' 1))
by A1, XXREAL_0:2, Th8, INT_2:28
.=
((2 |^ (k -' 1)) * 2) - ((2 |^ (k -' 1)) * 1)
by NEWTON:6
.=
2
|^ (k -' 1)
;
k -' 1 =
((k - 1) - 1) + 1
by A7, XREAL_1:233
.=
(k - 2) + 1
.=
(k -' 2) + 1
by A1, XXREAL_0:2, XREAL_1:233
;
then
(2 |^ (k -' 2)) * 2
<= 2
|^ (k -' 2)
by A6, A8, NEWTON:6;
then
((2 |^ (k -' 2)) * 2) / (2 |^ (k -' 2)) <= (2 |^ (k -' 2)) / (2 |^ (k -' 2))
by XREAL_1:72;
then
2
<= (2 |^ (k -' 2)) / (2 |^ (k -' 2))
by XCMPLX_1:89;
then
2
<= 1
by XCMPLX_1:60;
hence
contradiction
;
verum end;
hence
for m being Nat st m,2 |^ k are_coprime holds
not m is_primitive_root_of 2 |^ k
; verum