Metamath Proof Explorer

Theorem pockthg

Description: The generalized Pocklington's theorem. If N - 1 = A x. B where B < A , then N is prime if and only if for every prime factor p of A , there is an x such that x ^ ( N - 1 ) = 1 ( mod N ) and gcd ( x ^ ( ( N - 1 ) / p ) - 1 , N ) = 1 . (Contributed by Mario Carneiro, 2-Mar-2014)

Ref Expression
Hypotheses pockthg.1 
|- ( ph -> A e. NN )
pockthg.2 
|- ( ph -> B e. NN )
pockthg.3 
|- ( ph -> B < A )
pockthg.4 
|- ( ph -> N = ( ( A x. B ) + 1 ) )
pockthg.5 
|- ( ph -> A. p e. Prime ( p || A -> E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) )
Assertion pockthg 
|- ( ph -> N e. Prime )

Proof

Step Hyp Ref Expression
1 pockthg.1 
 |-  ( ph -> A e. NN )
2 pockthg.2 
 |-  ( ph -> B e. NN )
3 pockthg.3 
 |-  ( ph -> B < A )
4 pockthg.4 
 |-  ( ph -> N = ( ( A x. B ) + 1 ) )
5 pockthg.5 
 |-  ( ph -> A. p e. Prime ( p || A -> E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) )
6 1 2 nnmulcld 
 |-  ( ph -> ( A x. B ) e. NN )
7 nnuz 
 |-  NN = ( ZZ>= ` 1 )
8 6 7 eleqtrdi 
 |-  ( ph -> ( A x. B ) e. ( ZZ>= ` 1 ) )
9 eluzp1p1 
 |-  ( ( A x. B ) e. ( ZZ>= ` 1 ) -> ( ( A x. B ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
10 8 9 syl 
 |-  ( ph -> ( ( A x. B ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
11 df-2 
 |-  2 = ( 1 + 1 )
12 11 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
13 10 12 eleqtrrdi 
 |-  ( ph -> ( ( A x. B ) + 1 ) e. ( ZZ>= ` 2 ) )
14 4 13 eqeltrd 
 |-  ( ph -> N e. ( ZZ>= ` 2 ) )
15 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
16 14 15 syl 
 |-  ( ph -> N e. RR )
17 16 adantr 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> N e. RR )
18 1 nnred 
 |-  ( ph -> A e. RR )
19 18 resqcld 
 |-  ( ph -> ( A ^ 2 ) e. RR )
20 19 adantr 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( A ^ 2 ) e. RR )
21 prmnn 
 |-  ( q e. Prime -> q e. NN )
22 21 ad2antrl 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> q e. NN )
23 22 nnred 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> q e. RR )
24 23 resqcld 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( q ^ 2 ) e. RR )
25 2 nnred 
 |-  ( ph -> B e. RR )
26 1 nngt0d 
 |-  ( ph -> 0 < A )
27 ltmul2 
 |-  ( ( B e. RR /\ A e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( B < A <-> ( A x. B ) < ( A x. A ) ) )
28 25 18 18 26 27 syl112anc 
 |-  ( ph -> ( B < A <-> ( A x. B ) < ( A x. A ) ) )
29 3 28 mpbid 
 |-  ( ph -> ( A x. B ) < ( A x. A ) )
30 1 1 nnmulcld 
 |-  ( ph -> ( A x. A ) e. NN )
31 nnltp1le 
 |-  ( ( ( A x. B ) e. NN /\ ( A x. A ) e. NN ) -> ( ( A x. B ) < ( A x. A ) <-> ( ( A x. B ) + 1 ) <_ ( A x. A ) ) )
32 6 30 31 syl2anc 
 |-  ( ph -> ( ( A x. B ) < ( A x. A ) <-> ( ( A x. B ) + 1 ) <_ ( A x. A ) ) )
33 29 32 mpbid 
 |-  ( ph -> ( ( A x. B ) + 1 ) <_ ( A x. A ) )
34 1 nncnd 
 |-  ( ph -> A e. CC )
35 34 sqvald 
 |-  ( ph -> ( A ^ 2 ) = ( A x. A ) )
36 33 4 35 3brtr4d 
 |-  ( ph -> N <_ ( A ^ 2 ) )
37 36 adantr 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> N <_ ( A ^ 2 ) )
38 5 adantr 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> A. p e. Prime ( p || A -> E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) )
39 prmnn 
 |-  ( p e. Prime -> p e. NN )
40 39 ad2antrl 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> p e. NN )
41 40 nncnd 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> p e. CC )
42 41 exp1d 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> ( p ^ 1 ) = p )
43 nnge1 
 |-  ( ( p pCnt A ) e. NN -> 1 <_ ( p pCnt A ) )
44 43 ad2antll 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> 1 <_ ( p pCnt A ) )
45 simprl 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> p e. Prime )
46 1 nnzd 
 |-  ( ph -> A e. ZZ )
47 46 ad2antrr 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> A e. ZZ )
48 1nn0 
 |-  1 e. NN0
49 48 a1i 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> 1 e. NN0 )
50 pcdvdsb 
 |-  ( ( p e. Prime /\ A e. ZZ /\ 1 e. NN0 ) -> ( 1 <_ ( p pCnt A ) <-> ( p ^ 1 ) || A ) )
51 45 47 49 50 syl3anc 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> ( 1 <_ ( p pCnt A ) <-> ( p ^ 1 ) || A ) )
52 44 51 mpbid 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> ( p ^ 1 ) || A )
53 42 52 eqbrtrrd 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> p || A )
54 simpl1 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> ph )
55 54 1 syl 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> A e. NN )
56 54 2 syl 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> B e. NN )
57 54 3 syl 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> B < A )
58 54 4 syl 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> N = ( ( A x. B ) + 1 ) )
59 simpl2l 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> q e. Prime )
60 simpl2r 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> q || N )
61 simpl3l 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> p e. Prime )
62 simpl3r 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> ( p pCnt A ) e. NN )
63 simprl 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> x e. ZZ )
64 simprrl 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> ( ( x ^ ( N - 1 ) ) mod N ) = 1 )
65 simprrr 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 )
66 55 56 57 58 59 60 61 62 63 64 65 pockthlem 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) /\ ( x e. ZZ /\ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) ) -> ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) )
67 66 rexlimdvaa 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> ( E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) -> ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) ) )
68 67 3expa 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> ( E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) -> ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) ) )
69 53 68 embantd 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ ( p e. Prime /\ ( p pCnt A ) e. NN ) ) -> ( ( p || A -> E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) -> ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) ) )
70 69 expr 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ p e. Prime ) -> ( ( p pCnt A ) e. NN -> ( ( p || A -> E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) -> ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) ) ) )
71 id 
 |-  ( p e. Prime -> p e. Prime )
72 prmuz2 
 |-  ( q e. Prime -> q e. ( ZZ>= ` 2 ) )
73 uz2m1nn 
 |-  ( q e. ( ZZ>= ` 2 ) -> ( q - 1 ) e. NN )
74 72 73 syl 
 |-  ( q e. Prime -> ( q - 1 ) e. NN )
75 74 ad2antrl 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( q - 1 ) e. NN )
76 pccl 
 |-  ( ( p e. Prime /\ ( q - 1 ) e. NN ) -> ( p pCnt ( q - 1 ) ) e. NN0 )
77 71 75 76 syl2anr 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ p e. Prime ) -> ( p pCnt ( q - 1 ) ) e. NN0 )
78 77 nn0ge0d 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ p e. Prime ) -> 0 <_ ( p pCnt ( q - 1 ) ) )
79 breq1 
 |-  ( ( p pCnt A ) = 0 -> ( ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) <-> 0 <_ ( p pCnt ( q - 1 ) ) ) )
80 78 79 syl5ibrcom 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ p e. Prime ) -> ( ( p pCnt A ) = 0 -> ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) ) )
81 80 a1dd 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ p e. Prime ) -> ( ( p pCnt A ) = 0 -> ( ( p || A -> E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) -> ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) ) ) )
82 simpr 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ p e. Prime ) -> p e. Prime )
83 1 ad2antrr 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ p e. Prime ) -> A e. NN )
84 82 83 pccld 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ p e. Prime ) -> ( p pCnt A ) e. NN0 )
85 elnn0 
 |-  ( ( p pCnt A ) e. NN0 <-> ( ( p pCnt A ) e. NN \/ ( p pCnt A ) = 0 ) )
86 84 85 sylib 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ p e. Prime ) -> ( ( p pCnt A ) e. NN \/ ( p pCnt A ) = 0 ) )
87 70 81 86 mpjaod 
 |-  ( ( ( ph /\ ( q e. Prime /\ q || N ) ) /\ p e. Prime ) -> ( ( p || A -> E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) -> ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) ) )
88 87 ralimdva 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( A. p e. Prime ( p || A -> E. x e. ZZ ( ( ( x ^ ( N - 1 ) ) mod N ) = 1 /\ ( ( ( x ^ ( ( N - 1 ) / p ) ) - 1 ) gcd N ) = 1 ) ) -> A. p e. Prime ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) ) )
89 38 88 mpd 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> A. p e. Prime ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) )
90 75 nnzd 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( q - 1 ) e. ZZ )
91 pc2dvds 
 |-  ( ( A e. ZZ /\ ( q - 1 ) e. ZZ ) -> ( A || ( q - 1 ) <-> A. p e. Prime ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) ) )
92 46 90 91 syl2an2r 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( A || ( q - 1 ) <-> A. p e. Prime ( p pCnt A ) <_ ( p pCnt ( q - 1 ) ) ) )
93 89 92 mpbird 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> A || ( q - 1 ) )
94 dvdsle 
 |-  ( ( A e. ZZ /\ ( q - 1 ) e. NN ) -> ( A || ( q - 1 ) -> A <_ ( q - 1 ) ) )
95 46 75 94 syl2an2r 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( A || ( q - 1 ) -> A <_ ( q - 1 ) ) )
96 93 95 mpd 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> A <_ ( q - 1 ) )
97 1 nnnn0d 
 |-  ( ph -> A e. NN0 )
98 22 nnnn0d 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> q e. NN0 )
99 nn0ltlem1 
 |-  ( ( A e. NN0 /\ q e. NN0 ) -> ( A < q <-> A <_ ( q - 1 ) ) )
100 97 98 99 syl2an2r 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( A < q <-> A <_ ( q - 1 ) ) )
101 96 100 mpbird 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> A < q )
102 18 adantr 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> A e. RR )
103 97 nn0ge0d 
 |-  ( ph -> 0 <_ A )
104 103 adantr 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> 0 <_ A )
105 98 nn0ge0d 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> 0 <_ q )
106 102 23 104 105 lt2sqd 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( A < q <-> ( A ^ 2 ) < ( q ^ 2 ) ) )
107 101 106 mpbid 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( A ^ 2 ) < ( q ^ 2 ) )
108 17 20 24 37 107 lelttrd 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> N < ( q ^ 2 ) )
109 17 24 ltnled 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> ( N < ( q ^ 2 ) <-> -. ( q ^ 2 ) <_ N ) )
110 108 109 mpbid 
 |-  ( ( ph /\ ( q e. Prime /\ q || N ) ) -> -. ( q ^ 2 ) <_ N )
111 110 expr 
 |-  ( ( ph /\ q e. Prime ) -> ( q || N -> -. ( q ^ 2 ) <_ N ) )
112 111 con2d 
 |-  ( ( ph /\ q e. Prime ) -> ( ( q ^ 2 ) <_ N -> -. q || N ) )
113 112 ralrimiva 
 |-  ( ph -> A. q e. Prime ( ( q ^ 2 ) <_ N -> -. q || N ) )
114 isprm5 
 |-  ( N e. Prime <-> ( N e. ( ZZ>= ` 2 ) /\ A. q e. Prime ( ( q ^ 2 ) <_ N -> -. q || N ) ) )
115 14 113 114 sylanbrc 
 |-  ( ph -> N e. Prime )