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