let p be Nat; :: thesis: ( p > 1 implies order 1,p = 1 )
assume A1: p > 1 ; :: thesis: order 1,p = 1
assume A2: order 1,p <> 1 ; :: thesis: contradiction
p gcd 1 = 1 by NEWTON:64;
then A3: 1,p are_relative_prime by INT_2:def 4;
(1 |^ 1) mod p = 1 mod p by NEWTON:10
.= 1 by A1, NAT_D:24 ;
then order 1,p <= 1 by A1, A3, Def2;
then ( order 1,p < 1 or order 1,p = 1 ) by XXREAL_0:1;
then ( order 1,p = 0 or order 1,p = 1 ) by NAT_1:14;
hence contradiction by A1, A2, A3, Def2; :: thesis: verum