let p be natural number ; :: thesis: ( p > 1 implies ( INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr iff p is Prime ) )
assume A1: p > 1 ; :: thesis: ( INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr iff p is Prime )
then reconsider p = p as non zero natural number ;
reconsider P = INT.Ring p as Ring by A1, Th21;
reconsider p = p as non zero Element of NAT by ORDINAL1:def 13;

A2: now

assume A3: p is Prime ; :: thesis: INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for a being Element of P st a <> 0. P holds
ex b being Element of P st b * a = 1. P

proof

let a be Element of P; :: thesis: ( a <> 0. P implies ex b being Element of P st b * a = 1. P )
assume A4: a <> 0. P ; :: thesis: ex b being Element of P st b * a = 1. P
reconsider a' = a as Element of Segm p ;
reconsider a' = a' as Element of NAT ;
( 1 * a' = a' & 1 * p = p ) ;
then A5: ( 1 divides a' & 1 divides p ) by NAT_D:def 3;
for m being Nat st m divides a' & m divides p holds
m divides 1

proof

let m be Nat; :: thesis: ( m divides a' & m divides p implies m divides 1 )
assume A6: ( m divides a' & m divides p ) ; :: thesis: m divides 1
then consider k being Nat such that
A7: a' = m * k by NAT_D:def 3;
m <= a'

proof

assume A8: m > a' ; :: thesis: contradiction

now

per cases ( k = 0 or k <> 0 ) ;

case k = 0 ; :: thesis: contradiction

hence contradiction by A4, A7, FUNCT_7:def 1; :: thesis: verum

end;

case A9: k <> 0 ; :: thesis: contradiction

k >= 1 + 0 by A9, INT_1:20;
then k * a' >= 1 * a' by XREAL_1:66;
hence contradiction by A7, A8, A9, XREAL_1:70; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then m <> p by NAT_1:45;
hence m divides 1 by A3, A6, INT_2:def 5; :: thesis: verum

end;

then a' gcd p = 1 by A5, NAT_D:def 5;
then consider s, t being Integer such that
A11: 1 = (s * a') + (t * p) by Th16;
A12: ( s mod p >= 0 & s mod p < p ) by Th9;
then s mod p is Element of NAT by INT_1:16;
then reconsider b' = s mod p as Element of Segm p by A12, NAT_1:45;
reconsider b = b' as Element of P ;
reconsider a2 = a' as Integer ;
reconsider e = 1 as Integer ;
b * a = (a' * b') mod p by Def11
.= ((a2 mod p) * ((s mod p) mod p)) mod p by Th15
.= ((a2 mod p) * (s mod p)) mod p by Th13
.= (a2 * s) mod p by Th15
.= e mod p by A11, Th8
.= e by A1, Th10
.= 1. P by A1, Lm12 ;
hence ex b being Element of P st b * a = 1. P ; :: thesis: verum

end;

hence INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr by A1, Th21, VECTSP_1:def 20; :: thesis: verum

end;

now

assume A13: INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: p is Prime
for n being natural number holds
( not n divides p or n = 1 or n = p )

proof

let n be natural number ; :: thesis: ( not n divides p or n = 1 or n = p )
assume n divides p ; :: thesis: ( n = 1 or n = p )
then consider k being Nat such that
A14: p = n * k by NAT_D:def 3;
A15: k <= p

proof

assume A16: k > p ; :: thesis: contradiction

now

per cases ( n = 0 or n <> 0 ) ;

case n = 0 ; :: thesis: contradiction

hence contradiction by A14; :: thesis: verum

end;

case A17: n <> 0 ; :: thesis: contradiction

n >= 1 + 0 by A17, INT_1:20;
then n * p >= 1 * p by XREAL_1:66;
hence contradiction by A14, A16, A17, XREAL_1:70; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A19: n <= p

proof

assume A20: n > p ; :: thesis: contradiction

now

per cases ( k = 0 or k <> 0 ) ;

case k = 0 ; :: thesis: contradiction

hence contradiction by A14; :: thesis: verum

end;

case A21: k <> 0 ; :: thesis: contradiction

k >= 1 + 0 by A21, INT_1:20;
then k * p >= 1 * p by XREAL_1:66;
hence contradiction by A14, A20, A21, XREAL_1:70; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

now

per cases ( k = p or k <> p ) ;

case k = p ; :: thesis: ( n = 1 or n = p )

then 1 * p = p * n by A14;
hence ( n = 1 or n = p ) by XCMPLX_1:5; :: thesis: verum

end;

case k <> p ; :: thesis: ( n = 1 or n = p )

then A23: k < p by A15, XXREAL_0:1;

now

per cases ( n = p or n <> p ) ;

case n = p ; :: thesis: ( n = 1 or n = p )

then 1 * p = k * p by A14;
then k = 1 by XCMPLX_1:5;
hence ( n = 1 or n = p ) by A14; :: thesis: verum

end;

case n <> p ; :: thesis: contradiction

then n < p by A19, XXREAL_0:1;
then reconsider n2 = n as Element of Segm p by NAT_1:45;
reconsider n' = n2 as Element of (INT.Ring p) ;
reconsider k2 = k as Element of Segm p by A23, NAT_1:45;
reconsider k' = k2 as Element of (INT.Ring p) ;
( n <> 0 & k <> 0 ) by A14;
then A24: ( n <> 0. (INT.Ring p) & k <> 0. (INT.Ring p) ) by FUNCT_7:def 1, GR_CY_1:12;
n' * k' = (n2 * k2) mod p by Def11
.= 0 by A14, INT_1:89
.= 0. (INT.Ring p) by FUNCT_7:def 1, GR_CY_1:12 ;
hence contradiction by A13, A24, VECTSP_1:44; :: thesis: verum

end;

end;

end;

hence ( n = 1 or n = p ) ; :: thesis: verum

end;

end;

end;

hence ( n = 1 or n = p ) ; :: thesis: verum

end;

hence p is Prime by A1, INT_2:def 5; :: thesis: verum

end;

hence ( INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr iff p is Prime ) by A2; :: thesis: verum