set A = { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } ;
A2: i <> 0

proof

assume i = 0 ; :: thesis: contradiction
then i gcd p = p by NEWTON:65;
hence contradiction by A1, INT_2:def 4; :: thesis: verum

end;

A3: { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } is non empty set

proof

A4: (i |^ (Euler p)) mod p = 1 by A1, A2, EULER_2:33;
Euler p <> 0 by A1, Th45;
then Euler p > 0 ;
then Euler p in { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } by A4;
hence { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } is non empty set ; :: thesis: verum

end;

{ k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } c= NAT

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } or a in NAT )
assume a in { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } ; :: thesis: a in NAT
then consider k being Element of NAT such that
A5: ( k = a & k > 0 & (i |^ k) mod p = 1 ) ;
thus a in NAT by A5; :: thesis: verum

end;

then reconsider A = { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } as non empty Subset of NAT by A3;
consider a being Element of A;
defpred S₁[ set ] means $1 in A;
a is Element of NAT ;
then A6: ex kk being Nat st S₁[kk] ;
consider kk being Nat such that
A7: S₁[kk] and
A8: for n being Nat st S₁[n] holds
kk <= n from NAT_1:sch 5(A6);
consider k being Element of NAT such that
A9: ( k = kk & k > 0 & (i |^ k) mod p = 1 ) by A7;
take kk ; :: thesis: ( kk is Element of NAT & kk > 0 & (i |^ kk) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < kk & kk <= k ) ) )
for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
kk <= k

proof

let k be Nat; :: thesis: ( k > 0 & (i |^ k) mod p = 1 implies kk <= k )
A10: k in NAT by ORDINAL1:def 13;
assume ( k > 0 & (i |^ k) mod p = 1 ) ; :: thesis: kk <= k
then k in A by A10;
hence kk <= k by A8; :: thesis: verum

end;

hence ( kk is Element of NAT & kk > 0 & (i |^ kk) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < kk & kk <= k ) ) ) by A9; :: thesis: verum