Metamath Proof Explorer


Theorem isprm5

Description: One need only check prime divisors of P up to sqrt P in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Assertion isprm5 P P 2 z z 2 P ¬ z P

Proof

Step Hyp Ref Expression
1 isprm4 P P 2 z 2 z P z = P
2 prmuz2 z z 2
3 2 a1i P 2 z z 2
4 eluz2gt1 P 2 1 < P
5 eluzelre P 2 P
6 eluz2nn P 2 P
7 6 nngt0d P 2 0 < P
8 ltmulgt11 P P 0 < P 1 < P P < P P
9 5 5 7 8 syl3anc P 2 1 < P P < P P
10 4 9 mpbid P 2 P < P P
11 5 5 remulcld P 2 P P
12 5 11 ltnled P 2 P < P P ¬ P P P
13 10 12 mpbid P 2 ¬ P P P
14 oveq12 z = P z = P z z = P P
15 14 anidms z = P z z = P P
16 15 breq1d z = P z z P P P P
17 16 notbid z = P ¬ z z P ¬ P P P
18 13 17 syl5ibrcom P 2 z = P ¬ z z P
19 18 imim2d P 2 z P z = P z P ¬ z z P
20 con2 z P ¬ z z P z z P ¬ z P
21 19 20 syl6 P 2 z P z = P z z P ¬ z P
22 3 21 imim12d P 2 z 2 z P z = P z z z P ¬ z P
23 22 ralimdv2 P 2 z 2 z P z = P z z z P ¬ z P
24 annim z P ¬ z = P ¬ z P z = P
25 oveq12 x = z x = z x x = z z
26 25 anidms x = z x x = z z
27 26 breq1d x = z x x P z z P
28 breq1 x = z x P z P
29 27 28 anbi12d x = z x x P x P z z P z P
30 29 rspcev z 2 z z P z P x 2 x x P x P
31 30 ancom2s z 2 z P z z P x 2 x x P x P
32 31 expr z 2 z P z z P x 2 x x P x P
33 32 ad2ant2lr P 2 z 2 z P ¬ z = P z z P x 2 x x P x P
34 simprl P 2 z 2 z P ¬ z = P z P
35 eluzelz z 2 z
36 35 ad2antlr P 2 z 2 z P ¬ z = P z
37 eluz2nn z 2 z
38 37 ad2antlr P 2 z 2 z P ¬ z = P z
39 38 nnne0d P 2 z 2 z P ¬ z = P z 0
40 eluzelz P 2 P
41 40 ad2antrr P 2 z 2 z P ¬ z = P P
42 dvdsval2 z z 0 P z P P z
43 36 39 41 42 syl3anc P 2 z 2 z P ¬ z = P z P P z
44 34 43 mpbid P 2 z 2 z P ¬ z = P P z
45 eluzelre z 2 z
46 45 ad2antlr P 2 z 2 z P ¬ z = P z
47 46 recnd P 2 z 2 z P ¬ z = P z
48 47 mulid2d P 2 z 2 z P ¬ z = P 1 z = z
49 5 ad2antrr P 2 z 2 z P ¬ z = P P
50 6 ad2antrr P 2 z 2 z P ¬ z = P P
51 dvdsle z P z P z P
52 51 imp z P z P z P
53 36 50 34 52 syl21anc P 2 z 2 z P ¬ z = P z P
54 simprr P 2 z 2 z P ¬ z = P ¬ z = P
55 54 neqned P 2 z 2 z P ¬ z = P z P
56 55 necomd P 2 z 2 z P ¬ z = P P z
57 46 49 53 56 leneltd P 2 z 2 z P ¬ z = P z < P
58 48 57 eqbrtrd P 2 z 2 z P ¬ z = P 1 z < P
59 1red P 2 z 2 z P ¬ z = P 1
60 41 zred P 2 z 2 z P ¬ z = P P
61 nnre z z
62 nngt0 z 0 < z
63 61 62 jca z z 0 < z
64 38 63 syl P 2 z 2 z P ¬ z = P z 0 < z
65 ltmuldiv 1 P z 0 < z 1 z < P 1 < P z
66 59 60 64 65 syl3anc P 2 z 2 z P ¬ z = P 1 z < P 1 < P z
67 58 66 mpbid P 2 z 2 z P ¬ z = P 1 < P z
68 eluz2b1 P z 2 P z 1 < P z
69 44 67 68 sylanbrc P 2 z 2 z P ¬ z = P P z 2
70 46 46 remulcld P 2 z 2 z P ¬ z = P z z
71 38 38 nnmulcld P 2 z 2 z P ¬ z = P z z
72 nnrp P P +
73 nnrp z z z z +
74 rpdivcl P + z z + P z z +
75 72 73 74 syl2an P z z P z z +
76 50 71 75 syl2anc P 2 z 2 z P ¬ z = P P z z +
77 49 70 76 lemul1d P 2 z 2 z P ¬ z = P P z z P P z z z z P z z
78 49 recnd P 2 z 2 z P ¬ z = P P
79 78 47 78 47 39 39 divmuldivd P 2 z 2 z P ¬ z = P P z P z = P P z z
80 71 nncnd P 2 z 2 z P ¬ z = P z z
81 71 nnne0d P 2 z 2 z P ¬ z = P z z 0
82 78 78 80 81 divassd P 2 z 2 z P ¬ z = P P P z z = P P z z
83 79 82 eqtrd P 2 z 2 z P ¬ z = P P z P z = P P z z
84 78 80 81 divcan2d P 2 z 2 z P ¬ z = P z z P z z = P
85 84 eqcomd P 2 z 2 z P ¬ z = P P = z z P z z
86 83 85 breq12d P 2 z 2 z P ¬ z = P P z P z P P P z z z z P z z
87 77 86 bitr4d P 2 z 2 z P ¬ z = P P z z P z P z P
88 87 biimpd P 2 z 2 z P ¬ z = P P z z P z P z P
89 78 47 39 divcan2d P 2 z 2 z P ¬ z = P z P z = P
90 dvds0lem z P z P z P z = P P z P
91 36 44 41 89 90 syl31anc P 2 z 2 z P ¬ z = P P z P
92 88 91 jctird P 2 z 2 z P ¬ z = P P z z P z P z P P z P
93 oveq12 x = P z x = P z x x = P z P z
94 93 anidms x = P z x x = P z P z
95 94 breq1d x = P z x x P P z P z P
96 breq1 x = P z x P P z P
97 95 96 anbi12d x = P z x x P x P P z P z P P z P
98 97 rspcev P z 2 P z P z P P z P x 2 x x P x P
99 69 92 98 syl6an P 2 z 2 z P ¬ z = P P z z x 2 x x P x P
100 70 49 letrid P 2 z 2 z P ¬ z = P z z P P z z
101 33 99 100 mpjaod P 2 z 2 z P ¬ z = P x 2 x x P x P
102 101 ex P 2 z 2 z P ¬ z = P x 2 x x P x P
103 24 102 syl5bir P 2 z 2 ¬ z P z = P x 2 x x P x P
104 103 rexlimdva P 2 z 2 ¬ z P z = P x 2 x x P x P
105 prmz z z
106 105 ad2antrl P 2 x 2 x x P x P z z x z
107 106 zred P 2 x 2 x x P x P z z x z
108 107 107 remulcld P 2 x 2 x x P x P z z x z z
109 eluzelz x 2 x
110 109 ad3antlr P 2 x 2 x x P x P z z x x
111 110 zred P 2 x 2 x x P x P z z x x
112 111 111 remulcld P 2 x 2 x x P x P z z x x x
113 40 ad3antrrr P 2 x 2 x x P x P z z x P
114 113 zred P 2 x 2 x x P x P z z x P
115 eluz2nn x 2 x
116 115 ad3antlr P 2 x 2 x x P x P z z x x
117 simprr P 2 x 2 x x P x P z z x z x
118 dvdsle z x z x z x
119 118 imp z x z x z x
120 106 116 117 119 syl21anc P 2 x 2 x x P x P z z x z x
121 eluzge2nn0 z 2 z 0
122 121 nn0ge0d z 2 0 z
123 2 122 syl z 0 z
124 123 ad2antrl P 2 x 2 x x P x P z z x 0 z
125 nnnn0 x x 0
126 125 nn0ge0d x 0 x
127 116 126 syl P 2 x 2 x x P x P z z x 0 x
128 le2msq z 0 z x 0 x z x z z x x
129 107 124 111 127 128 syl22anc P 2 x 2 x x P x P z z x z x z z x x
130 120 129 mpbid P 2 x 2 x x P x P z z x z z x x
131 simplrl P 2 x 2 x x P x P z z x x x P
132 108 112 114 130 131 letrd P 2 x 2 x x P x P z z x z z P
133 simplrr P 2 x 2 x x P x P z z x x P
134 106 110 113 117 133 dvdstrd P 2 x 2 x x P x P z z x z P
135 132 134 jc P 2 x 2 x x P x P z z x ¬ z z P ¬ z P
136 exprmfct x 2 z z x
137 136 ad2antlr P 2 x 2 x x P x P z z x
138 135 137 reximddv P 2 x 2 x x P x P z ¬ z z P ¬ z P
139 138 ex P 2 x 2 x x P x P z ¬ z z P ¬ z P
140 139 rexlimdva P 2 x 2 x x P x P z ¬ z z P ¬ z P
141 104 140 syld P 2 z 2 ¬ z P z = P z ¬ z z P ¬ z P
142 rexnal z 2 ¬ z P z = P ¬ z 2 z P z = P
143 rexnal z ¬ z z P ¬ z P ¬ z z z P ¬ z P
144 141 142 143 3imtr3g P 2 ¬ z 2 z P z = P ¬ z z z P ¬ z P
145 23 144 impcon4bid P 2 z 2 z P z = P z z z P ¬ z P
146 prmnn z z
147 146 nncnd z z
148 147 sqvald z z 2 = z z
149 148 breq1d z z 2 P z z P
150 149 imbi1d z z 2 P ¬ z P z z P ¬ z P
151 150 ralbiia z z 2 P ¬ z P z z z P ¬ z P
152 145 151 bitr4di P 2 z 2 z P z = P z z 2 P ¬ z P
153 152 pm5.32i P 2 z 2 z P z = P P 2 z z 2 P ¬ z P
154 1 153 bitri P P 2 z z 2 P ¬ z P