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 mulid2d ( ( ( 𝑃 ∈ ( ℤ ‘ 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 syl5bir ( ( 𝑃 ∈ ( ℤ ‘ 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 ) ≤ 𝑃 → ¬ 𝑧𝑃 ) ) )