# 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}\in ℙ↔\left({P}\in {ℤ}_{\ge 2}\wedge \forall {z}\in ℙ\phantom{\rule{.4em}{0ex}}\left({{z}}^{2}\le {P}\to ¬{z}\parallel {P}\right)\right)$

### Proof

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