let p be Nat; :: 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 Nat ;

reconsider P = INT.Ring p as Ring by A1, Th11;

reconsider p = p as non zero Element of NAT by ORDINAL1:def 12;

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 Nat ;

reconsider P = INT.Ring p as Ring by A1, Th11;

reconsider p = p as non zero Element of NAT by ORDINAL1:def 12;

A2: now :: 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 implies p is Prime )

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 Nat holds

( not n divides p or n = 1 or n = p )

end;for n being Nat holds

( not n divides p or n = 1 or n = p )

proof

hence
p is Prime
by A1, INT_2:def 4; :: thesis: verum
let n be Nat; :: 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

end;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

A8:
k <= p
assume A6:
n > p
; :: thesis: contradiction

end;now :: thesis: ( ( k = 0 & contradiction ) or ( k <> 0 & contradiction ) )

hence
contradiction
; :: thesis: verumend;

proof

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

end;now :: thesis: ( ( n = 0 & contradiction ) or ( n <> 0 & contradiction ) )

hence
contradiction
; :: thesis: verumend;

now :: thesis: ( ( k = p & ( n = 1 or n = p ) ) or ( k <> p & ( n = 1 or n = p ) ) )end;

hence
( n = 1 or n = p )
; :: thesis: verumper cases
( k = p or k <> p )
;

end;

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

then A11:
k < p
by A8, XXREAL_0:1;

end;now :: thesis: ( ( n = p & ( n = 1 or n = p ) ) or ( n <> p & contradiction ) )end;

hence
( n = 1 or n = p )
; :: thesis: verumper cases
( n = p or n <> p )
;

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:44;

0 in Segm p by NAT_1:44;

then A12: 0 = 0. (INT.Ring p) by SUBSET_1:def 8;

k <> 0 by A4;

then A13: k <> 0. (INT.Ring p) by A12;

reconsider k2 = k as Element of Segm p by A11, NAT_1:44;

reconsider n9 = n2 as Element of (INT.Ring p) ;

reconsider k9 = k2 as Element of (INT.Ring p) ;

n <> 0 by A4;

then A14: n <> 0. (INT.Ring p) by A12;

n9 * k9 = (n2 * k2) mod p by Def10

.= 0. (INT.Ring p) by A12, A4, INT_1:62 ;

hence contradiction by A3, A14, A13, VECTSP_1:12; :: thesis: verum

end;then reconsider n2 = n as Element of Segm p by NAT_1:44;

0 in Segm p by NAT_1:44;

then A12: 0 = 0. (INT.Ring p) by SUBSET_1:def 8;

k <> 0 by A4;

then A13: k <> 0. (INT.Ring p) by A12;

reconsider k2 = k as Element of Segm p by A11, NAT_1:44;

reconsider n9 = n2 as Element of (INT.Ring p) ;

reconsider k9 = k2 as Element of (INT.Ring p) ;

n <> 0 by A4;

then A14: n <> 0. (INT.Ring p) by A12;

n9 * k9 = (n2 * k2) mod p by Def10

.= 0. (INT.Ring p) by A12, A4, INT_1:62 ;

hence contradiction by A3, A14, A13, VECTSP_1:12; :: thesis: verum

now :: thesis: ( p is Prime 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 )

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: verumassume A15:
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

end;for a being Element of P st a <> 0. P holds

ex b being Element of P st b * a = 1. P

proof

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, Th11, VECTSP_1:def 9; :: thesis: verum
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 A16: 1 divides p by NAT_D:def 3;

assume A17: a <> 0. P ; :: thesis: ex b being Element of P st b * a = 1. P

A18: for m being Nat st m divides a9 & m divides p holds

m divides 1

then 1 divides a9 by NAT_D:def 3;

then a9 gcd p = 1 by A16, A18, NAT_D:def 5;

then consider s, t being Integer such that

A24: 1 = (s * a9) + (t * p) by NAT_D:68;

s mod p >= 0 by NAT_D:62;

then A25: s mod p is Element of NAT by INT_1:3;

s mod p < p by NAT_D:62;

then reconsider b9 = s mod p as Element of Segm p by A25, NAT_1:44;

reconsider b = b9 as Element of P ;

b * a = (a9 * b9) mod p by Def10

.= ((a2 mod p) * ((s mod p) mod p)) mod p by NAT_D:67

.= ((a2 mod p) * (s mod p)) mod p by NAT_D:65

.= (a2 * s) mod p by NAT_D:67

.= e mod p by A24, NAT_D:61

.= e by A1, NAT_D:63

.= 1. P by A1, Lm7 ;

hence ex b being Element of P st b * a = 1. P ; :: thesis: verum

end;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 A16: 1 divides p by NAT_D:def 3;

assume A17: a <> 0. P ; :: thesis: ex b being Element of P st b * a = 1. P

A18: for m being Nat st m divides a9 & m divides p holds

m divides 1

proof

1 * a9 = a9
;
let m be Nat; :: thesis: ( m divides a9 & m divides p implies m divides 1 )

assume that

A19: m divides a9 and

A20: m divides p ; :: thesis: m divides 1

consider k being Nat such that

A21: a9 = m * k by A19, NAT_D:def 3;

m <= a9

hence m divides 1 by A15, A20, INT_2:def 4; :: thesis: verum

end;assume that

A19: m divides a9 and

A20: m divides p ; :: thesis: m divides 1

consider k being Nat such that

A21: a9 = m * k by A19, NAT_D:def 3;

m <= a9

proof

then
m <> p
by NAT_1:44;
assume A22:
m > a9
; :: thesis: contradiction

end;now :: thesis: ( ( k = 0 & contradiction ) or ( k <> 0 & contradiction ) )

hence
contradiction
; :: thesis: verumend;

hence m divides 1 by A15, A20, INT_2:def 4; :: thesis: verum

then 1 divides a9 by NAT_D:def 3;

then a9 gcd p = 1 by A16, A18, NAT_D:def 5;

then consider s, t being Integer such that

A24: 1 = (s * a9) + (t * p) by NAT_D:68;

s mod p >= 0 by NAT_D:62;

then A25: s mod p is Element of NAT by INT_1:3;

s mod p < p by NAT_D:62;

then reconsider b9 = s mod p as Element of Segm p by A25, NAT_1:44;

reconsider b = b9 as Element of P ;

b * a = (a9 * b9) mod p by Def10

.= ((a2 mod p) * ((s mod p) mod p)) mod p by NAT_D:67

.= ((a2 mod p) * (s mod p)) mod p by NAT_D:65

.= (a2 * s) mod p by NAT_D:67

.= e mod p by A24, NAT_D:61

.= e by A1, NAT_D:63

.= 1. P by A1, Lm7 ;

hence ex b being Element of P st b * a = 1. P ; :: thesis: verum