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: 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
A4: p = n * k by NAT_D:def 3;
A5: n <= p

proof

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

now

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

case k = 0 ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

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

then k >= 1 + 0 by INT_1:20;
then k * p >= 1 * p by XREAL_1:66;
hence contradiction by A4, A6, A7, XREAL_1:70; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A8: k <= p

proof

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

now

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

case n = 0 ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

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

then n >= 1 + 0 by INT_1:20;
then n * p >= 1 * p by XREAL_1:66;
hence contradiction by A4, A9, A10, 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 A4;
hence ( n = 1 or n = p ) by XCMPLX_1:5; :: thesis: verum

end;

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

then A11: k < p by A8, 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 A4;
then k = 1 by XCMPLX_1:5;
hence ( n = 1 or n = p ) by A4; :: thesis: verum

end;

case n <> p ; :: thesis: contradiction

then n < p by A5, XXREAL_0:1;
then reconsider n2 = n as Element of Segm p by NAT_1:45;
0 in p by NAT_1:45;
then U: 0 = 0. (INT.Ring p) by FUNCT_7:def 1;
k <> 0 by A4;
then A12: k <> 0. (INT.Ring p) by U;
reconsider k2 = k as Element of Segm p by A11, NAT_1:45;
reconsider n9 = n2 as Element of (INT.Ring p) ;
reconsider k9 = k2 as Element of (INT.Ring p) ;
n <> 0 by A4;
then A13: n <> 0. (INT.Ring p) by U;
n9 * k9 = (n2 * k2) mod p by Def11
.= 0. (INT.Ring p) by U, A4, INT_1:89 ;
hence contradiction by A3, A13, A12, 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;

now

assume A14: 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

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

proof

let m be Nat; :: thesis: ( m divides a9 & m divides p implies m divides 1 )
assume that
A18: m divides a9 and
A19: m divides p ; :: thesis: m divides 1
consider k being Nat such that
A20: a9 = m * k by A18, NAT_D:def 3;
m <= a9

proof

assume A21: m > a9 ; :: thesis: contradiction

now

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

case k = 0 ; :: thesis: contradiction

hence contradiction by A16, A20, FUNCT_7:def 1; :: thesis: verum

end;

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

then k >= 1 + 0 by INT_1:20;
then k * a9 >= 1 * a9 by XREAL_1:66;
hence contradiction by A20, A21, A22, 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 A14, A19, INT_2:def 5; :: thesis: verum

end;

1 * a9 = a9 ;
then 1 divides a9 by NAT_D:def 3;
then a9 gcd p = 1 by A15, A17, NAT_D:def 5;
then consider s, t being Integer such that
A23: 1 = (s * a9) + (t * p) by Th16;
s mod p >= 0 by Th9;
then A24: s mod p is Element of NAT by INT_1:16;
s mod p < p by Th9;
then reconsider b9 = s mod p as Element of Segm p by A24, NAT_1:45;
reconsider b = b9 as Element of P ;
b * a = (a9 * b9) 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 A23, 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;

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