let a be Nat; :: thesis: for b, m, n being non zero Nat st m >= n & a mod (b |^ m) = 1 holds
a mod (b |^ n) = 1
let b be non zero Nat; :: thesis: for m, n being non zero Nat st m >= n & a mod (b |^ m) = 1 holds
a mod (b |^ n) = 1
let m, n be non zero Nat; :: thesis: ( m >= n & a mod (b |^ m) = 1 implies a mod (b |^ n) = 1 )
assume A1: m >= n ; :: thesis: ( not a mod (b |^ m) = 1 or a mod (b |^ n) = 1 )
assume A2: a mod (b |^ m) = 1 ; :: thesis: a mod (b |^ n) = 1
m - n >= n - n by A1, XREAL_1:9;
then m - n in NAT by INT_1:3;
then reconsider k = m - n as Nat ;
reconsider b = b as non trivial Nat by A2;
1 = a mod (b |^ (n + k)) by A2
.= a mod ((b |^ n) * (b |^ k)) by NEWTON:8 ;
hence a mod (b |^ n) = 1 by MT; :: thesis: verum