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;
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 )
proof
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
proof
assume A6: n > p ; :: thesis: contradiction
now :: thesis: ( ( k = 0 & contradiction ) or ( k <> 0 & contradiction ) )
end;
hence contradiction ; :: thesis: verum
end;
A8: k <= p
proof
assume A9: k > p ; :: thesis: contradiction
now :: thesis: ( ( n = 0 & contradiction ) or ( n <> 0 & contradiction ) )
end;
hence contradiction ; :: thesis: verum
end;
now :: thesis: ( ( k = p & ( n = 1 or n = p ) ) or ( k <> p & ( n = 1 or n = p ) ) )
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 :: thesis: ( ( n = p & ( n = 1 or n = p ) ) or ( n <> p & contradiction ) )
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: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;
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 4; :: thesis: verum
end;
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 )
assume 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
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 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
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
proof
assume A22: m > a9 ; :: thesis: contradiction
now :: thesis: ( ( k = 0 & contradiction ) or ( k <> 0 & contradiction ) )
end;
hence contradiction ; :: thesis: verum
end;
then m <> p by NAT_1:44;
hence m divides 1 by A15, A20, INT_2:def 4; :: thesis: verum
end;
1 * a9 = a9 ;
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;
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
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