This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℙ ( ( 𝑧 ↑ 2 ) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃 ) ) )

Proof

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