let k be Nat; :: thesis: ( 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 ; :: thesis: for m being Nat st m,2 |^ k are_coprime holds
not m is_primitive_root_of 2 |^ k
now :: thesis: 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 ) ; :: thesis: contradiction
then consider m being Nat such that
A2: ( m,2 |^ k are_coprime & m is_primitive_root_of 2 |^ k ) ;
now :: thesis: not m is even
assume m is even ; :: thesis: contradiction
then A3: 2 divides m by PEPIN:22;
2 |^ 1 divides 2 |^ k by A1, XXREAL_0:2, NEWTON:89;
then 2 divides 2 |^ k ;
hence contradiction by A2, A3, PYTHTRIP:def 1; :: thesis: verum
end;
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 ; :: thesis: verum
end;
hence for m being Nat st m,2 |^ k are_coprime holds
not m is_primitive_root_of 2 |^ k ; :: thesis: verum