Step | Hyp | Ref
| Expression |
1 | | isprm4 16241 |
. 2
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈
(ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃))) |
2 | | prmuz2 16253 |
. . . . . . . 8
⊢ (𝑧 ∈ ℙ → 𝑧 ∈
(ℤ≥‘2)) |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑧 ∈ ℙ → 𝑧 ∈
(ℤ≥‘2))) |
4 | | eluz2gt1 12516 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈
(ℤ≥‘2) → 1 < 𝑃) |
5 | | eluzelre 12449 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℝ) |
6 | | eluz2nn 12480 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℕ) |
7 | 6 | nngt0d 11879 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → 0 < 𝑃) |
8 | | ltmulgt11 11692 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 0 <
𝑃) → (1 < 𝑃 ↔ 𝑃 < (𝑃 · 𝑃))) |
9 | 5, 5, 7, 8 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈
(ℤ≥‘2) → (1 < 𝑃 ↔ 𝑃 < (𝑃 · 𝑃))) |
10 | 4, 9 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 < (𝑃 · 𝑃)) |
11 | 5, 5 | remulcld 10863 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 · 𝑃) ∈ ℝ) |
12 | 5, 11 | ltnled 10979 |
. . . . . . . . . . 11
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 < (𝑃 · 𝑃) ↔ ¬ (𝑃 · 𝑃) ≤ 𝑃)) |
13 | 10, 12 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝑃 ∈
(ℤ≥‘2) → ¬ (𝑃 · 𝑃) ≤ 𝑃) |
14 | | oveq12 7222 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 𝑃 ∧ 𝑧 = 𝑃) → (𝑧 · 𝑧) = (𝑃 · 𝑃)) |
15 | 14 | anidms 570 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑃 → (𝑧 · 𝑧) = (𝑃 · 𝑃)) |
16 | 15 | breq1d 5063 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑃 → ((𝑧 · 𝑧) ≤ 𝑃 ↔ (𝑃 · 𝑃) ≤ 𝑃)) |
17 | 16 | notbid 321 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑃 → (¬ (𝑧 · 𝑧) ≤ 𝑃 ↔ ¬ (𝑃 · 𝑃) ≤ 𝑃)) |
18 | 13, 17 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑧 = 𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃)) |
19 | 18 | imim2d 57 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → (𝑧 ∥ 𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃))) |
20 | | con2 137 |
. . . . . . . 8
⊢ ((𝑧 ∥ 𝑃 → ¬ (𝑧 · 𝑧) ≤ 𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)) |
21 | 19, 20 | syl6 35 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
22 | 3, 21 | imim12d 81 |
. . . . . 6
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈ (ℤ≥‘2)
→ (𝑧 ∥ 𝑃 → 𝑧 = 𝑃)) → (𝑧 ∈ ℙ → ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))) |
23 | 22 | ralimdv2 3099 |
. . . . 5
⊢ (𝑃 ∈
(ℤ≥‘2) → (∀𝑧 ∈
(ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
24 | | annim 407 |
. . . . . . . . 9
⊢ ((𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃) ↔ ¬ (𝑧 ∥ 𝑃 → 𝑧 = 𝑃)) |
25 | | oveq12 7222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑧) → (𝑥 · 𝑥) = (𝑧 · 𝑧)) |
26 | 25 | anidms 570 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (𝑥 · 𝑥) = (𝑧 · 𝑧)) |
27 | 26 | breq1d 5063 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → ((𝑥 · 𝑥) ≤ 𝑃 ↔ (𝑧 · 𝑧) ≤ 𝑃)) |
28 | | breq1 5056 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝑥 ∥ 𝑃 ↔ 𝑧 ∥ 𝑃)) |
29 | 27, 28 | anbi12d 634 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃) ↔ ((𝑧 · 𝑧) ≤ 𝑃 ∧ 𝑧 ∥ 𝑃))) |
30 | 29 | rspcev 3537 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ ((𝑧 · 𝑧) ≤ 𝑃 ∧ 𝑧 ∥ 𝑃)) → ∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) |
31 | 30 | ancom2s 650 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ (𝑧 ∥ 𝑃 ∧ (𝑧 · 𝑧) ≤ 𝑃)) → ∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) |
32 | 31 | expr 460 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → ((𝑧 · 𝑧) ≤ 𝑃 → ∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃))) |
33 | 32 | ad2ant2lr 748 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) ≤ 𝑃 → ∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃))) |
34 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∥ 𝑃) |
35 | | eluzelz 12448 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℤ) |
36 | 35 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℤ) |
37 | | eluz2nn 12480 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℕ) |
38 | 37 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℕ) |
39 | 38 | nnne0d 11880 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ≠ 0) |
40 | | eluzelz 12448 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℤ) |
41 | 40 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℤ) |
42 | | dvdsval2 15818 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℤ ∧ 𝑧 ≠ 0 ∧ 𝑃 ∈ ℤ) → (𝑧 ∥ 𝑃 ↔ (𝑃 / 𝑧) ∈ ℤ)) |
43 | 36, 39, 41, 42 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 ∥ 𝑃 ↔ (𝑃 / 𝑧) ∈ ℤ)) |
44 | 34, 43 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∈ ℤ) |
45 | | eluzelre 12449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℝ) |
46 | 45 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℝ) |
47 | 46 | recnd 10861 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ∈ ℂ) |
48 | 47 | mulid2d 10851 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (1 · 𝑧) = 𝑧) |
49 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℝ) |
50 | 6 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℕ) |
51 | | dvdsle 15871 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑧 ∥ 𝑃 → 𝑧 ≤ 𝑃)) |
52 | 51 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) ∧ 𝑧 ∥ 𝑃) → 𝑧 ≤ 𝑃) |
53 | 36, 50, 34, 52 | syl21anc 838 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ≤ 𝑃) |
54 | | simprr 773 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ¬ 𝑧 = 𝑃) |
55 | 54 | neqned 2947 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 ≠ 𝑃) |
56 | 55 | necomd 2996 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ≠ 𝑧) |
57 | 46, 49, 53, 56 | leneltd 10986 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑧 < 𝑃) |
58 | 48, 57 | eqbrtrd 5075 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (1 · 𝑧) < 𝑃) |
59 | | 1red 10834 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 1 ∈ ℝ) |
60 | 41 | zred 12282 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℝ) |
61 | | nnre 11837 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
62 | | nngt0 11861 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℕ → 0 <
𝑧) |
63 | 61, 62 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ℕ → (𝑧 ∈ ℝ ∧ 0 <
𝑧)) |
64 | 38, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 ∈ ℝ ∧ 0 < 𝑧)) |
65 | | ltmuldiv 11705 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ 𝑃
∈ ℝ ∧ (𝑧
∈ ℝ ∧ 0 < 𝑧)) → ((1 · 𝑧) < 𝑃 ↔ 1 < (𝑃 / 𝑧))) |
66 | 59, 60, 64, 65 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((1 · 𝑧) < 𝑃 ↔ 1 < (𝑃 / 𝑧))) |
67 | 58, 66 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 1 < (𝑃 / 𝑧)) |
68 | | eluz2b1 12515 |
. . . . . . . . . . . . 13
⊢ ((𝑃 / 𝑧) ∈ (ℤ≥‘2)
↔ ((𝑃 / 𝑧) ∈ ℤ ∧ 1 <
(𝑃 / 𝑧))) |
69 | 44, 67, 68 | sylanbrc 586 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∈
(ℤ≥‘2)) |
70 | 46, 46 | remulcld 10863 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℝ) |
71 | 38, 38 | nnmulcld 11883 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℕ) |
72 | | nnrp 12597 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ+) |
73 | | nnrp 12597 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 · 𝑧) ∈ ℕ → (𝑧 · 𝑧) ∈
ℝ+) |
74 | | rpdivcl 12611 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℝ+
∧ (𝑧 · 𝑧) ∈ ℝ+)
→ (𝑃 / (𝑧 · 𝑧)) ∈
ℝ+) |
75 | 72, 73, 74 | syl2an 599 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℕ ∧ (𝑧 · 𝑧) ∈ ℕ) → (𝑃 / (𝑧 · 𝑧)) ∈
ℝ+) |
76 | 50, 71, 75 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / (𝑧 · 𝑧)) ∈
ℝ+) |
77 | 49, 70, 76 | lemul1d 12671 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) ↔ (𝑃 · (𝑃 / (𝑧 · 𝑧))) ≤ ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧))))) |
78 | 49 | recnd 10861 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 ∈ ℂ) |
79 | 78, 47, 78, 47, 39, 39 | divmuldivd 11649 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) = ((𝑃 · 𝑃) / (𝑧 · 𝑧))) |
80 | 71 | nncnd 11846 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ∈ ℂ) |
81 | 71 | nnne0d 11880 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · 𝑧) ≠ 0) |
82 | 78, 78, 80, 81 | divassd 11643 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 · 𝑃) / (𝑧 · 𝑧)) = (𝑃 · (𝑃 / (𝑧 · 𝑧)))) |
83 | 79, 82 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) = (𝑃 · (𝑃 / (𝑧 · 𝑧)))) |
84 | 78, 80, 81 | divcan2d 11610 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧))) = 𝑃) |
85 | 84 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → 𝑃 = ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧)))) |
86 | 83, 85 | breq12d 5066 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ↔ (𝑃 · (𝑃 / (𝑧 · 𝑧))) ≤ ((𝑧 · 𝑧) · (𝑃 / (𝑧 · 𝑧))))) |
87 | 77, 86 | bitr4d 285 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) ↔ ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃)) |
88 | 87 | biimpd 232 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃)) |
89 | 78, 47, 39 | divcan2d 11610 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑧 · (𝑃 / 𝑧)) = 𝑃) |
90 | | dvds0lem 15828 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ℤ ∧ (𝑃 / 𝑧) ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ (𝑧 · (𝑃 / 𝑧)) = 𝑃) → (𝑃 / 𝑧) ∥ 𝑃) |
91 | 36, 44, 41, 89, 90 | syl31anc 1375 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 / 𝑧) ∥ 𝑃) |
92 | 88, 91 | jctird 530 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃))) |
93 | | oveq12 7222 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = (𝑃 / 𝑧) ∧ 𝑥 = (𝑃 / 𝑧)) → (𝑥 · 𝑥) = ((𝑃 / 𝑧) · (𝑃 / 𝑧))) |
94 | 93 | anidms 570 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑃 / 𝑧) → (𝑥 · 𝑥) = ((𝑃 / 𝑧) · (𝑃 / 𝑧))) |
95 | 94 | breq1d 5063 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑃 / 𝑧) → ((𝑥 · 𝑥) ≤ 𝑃 ↔ ((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃)) |
96 | | breq1 5056 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑃 / 𝑧) → (𝑥 ∥ 𝑃 ↔ (𝑃 / 𝑧) ∥ 𝑃)) |
97 | 95, 96 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑃 / 𝑧) → (((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃) ↔ (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃))) |
98 | 97 | rspcev 3537 |
. . . . . . . . . . . 12
⊢ (((𝑃 / 𝑧) ∈ (ℤ≥‘2)
∧ (((𝑃 / 𝑧) · (𝑃 / 𝑧)) ≤ 𝑃 ∧ (𝑃 / 𝑧) ∥ 𝑃)) → ∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) |
99 | 69, 92, 98 | syl6an 684 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → (𝑃 ≤ (𝑧 · 𝑧) → ∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃))) |
100 | 70, 49 | letrid 10984 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ((𝑧 · 𝑧) ≤ 𝑃 ∨ 𝑃 ≤ (𝑧 · 𝑧))) |
101 | 33, 99, 100 | mpjaod 860 |
. . . . . . . . . 10
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
∧ (𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃)) → ∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) |
102 | 101 | ex 416 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((𝑧 ∥ 𝑃 ∧ ¬ 𝑧 = 𝑃) → ∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃))) |
103 | 24, 102 | syl5bir 246 |
. . . . . . . 8
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2))
→ (¬ (𝑧 ∥
𝑃 → 𝑧 = 𝑃) → ∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃))) |
104 | 103 | rexlimdva 3203 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → (∃𝑧 ∈ (ℤ≥‘2)
¬ (𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃))) |
105 | | prmz 16232 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℙ → 𝑧 ∈
ℤ) |
106 | 105 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑧 ∈ ℤ) |
107 | 106 | zred 12282 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑧 ∈ ℝ) |
108 | 107, 107 | remulcld 10863 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑧 · 𝑧) ∈ ℝ) |
109 | | eluzelz 12448 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
(ℤ≥‘2) → 𝑥 ∈ ℤ) |
110 | 109 | ad3antlr 731 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑥 ∈ ℤ) |
111 | 110 | zred 12282 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑥 ∈ ℝ) |
112 | 111, 111 | remulcld 10863 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑥 · 𝑥) ∈ ℝ) |
113 | 40 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑃 ∈ ℤ) |
114 | 113 | zred 12282 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑃 ∈ ℝ) |
115 | | eluz2nn 12480 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
(ℤ≥‘2) → 𝑥 ∈ ℕ) |
116 | 115 | ad3antlr 731 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑥 ∈ ℕ) |
117 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑧 ∥ 𝑥) |
118 | | dvdsle 15871 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑧 ∥ 𝑥 → 𝑧 ≤ 𝑥)) |
119 | 118 | imp 410 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ℤ ∧ 𝑥 ∈ ℕ) ∧ 𝑧 ∥ 𝑥) → 𝑧 ≤ 𝑥) |
120 | 106, 116,
117, 119 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑧 ≤ 𝑥) |
121 | | eluzge2nn0 12483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℕ0) |
122 | 121 | nn0ge0d 12153 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈
(ℤ≥‘2) → 0 ≤ 𝑧) |
123 | 2, 122 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℙ → 0 ≤
𝑧) |
124 | 123 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 0 ≤ 𝑧) |
125 | | nnnn0 12097 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ0) |
126 | 125 | nn0ge0d 12153 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℕ → 0 ≤
𝑥) |
127 | 116, 126 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 0 ≤ 𝑥) |
128 | | le2msq 11732 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) ∧ (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) → (𝑧 ≤ 𝑥 ↔ (𝑧 · 𝑧) ≤ (𝑥 · 𝑥))) |
129 | 107, 124,
111, 127, 128 | syl22anc 839 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑧 ≤ 𝑥 ↔ (𝑧 · 𝑧) ≤ (𝑥 · 𝑥))) |
130 | 120, 129 | mpbid 235 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑧 · 𝑧) ≤ (𝑥 · 𝑥)) |
131 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑥 · 𝑥) ≤ 𝑃) |
132 | 108, 112,
114, 130, 131 | letrd 10989 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → (𝑧 · 𝑧) ≤ 𝑃) |
133 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑥 ∥ 𝑃) |
134 | 106, 110,
113, 117, 133 | dvdstrd 15856 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → 𝑧 ∥ 𝑃) |
135 | 132, 134 | jc 164 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ∥ 𝑥)) → ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)) |
136 | | exprmfct 16261 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘2) → ∃𝑧 ∈ ℙ 𝑧 ∥ 𝑥) |
137 | 136 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) → ∃𝑧 ∈ ℙ 𝑧 ∥ 𝑥) |
138 | 135, 137 | reximddv 3194 |
. . . . . . . . 9
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
∧ ((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃)) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)) |
139 | 138 | ex 416 |
. . . . . . . 8
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑥 ∈ (ℤ≥‘2))
→ (((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
140 | 139 | rexlimdva 3203 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → (∃𝑥 ∈
(ℤ≥‘2)((𝑥 · 𝑥) ≤ 𝑃 ∧ 𝑥 ∥ 𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
141 | 104, 140 | syld 47 |
. . . . . 6
⊢ (𝑃 ∈
(ℤ≥‘2) → (∃𝑧 ∈ (ℤ≥‘2)
¬ (𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ∃𝑧 ∈ ℙ ¬ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
142 | | rexnal 3160 |
. . . . . 6
⊢
(∃𝑧 ∈
(ℤ≥‘2) ¬ (𝑧 ∥ 𝑃 → 𝑧 = 𝑃) ↔ ¬ ∀𝑧 ∈
(ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃)) |
143 | | rexnal 3160 |
. . . . . 6
⊢
(∃𝑧 ∈
ℙ ¬ ((𝑧 ·
𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃) ↔ ¬ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)) |
144 | 141, 142,
143 | 3imtr3g 298 |
. . . . 5
⊢ (𝑃 ∈
(ℤ≥‘2) → (¬ ∀𝑧 ∈
(ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃) → ¬ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
145 | 23, 144 | impcon4bid 230 |
. . . 4
⊢ (𝑃 ∈
(ℤ≥‘2) → (∀𝑧 ∈
(ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
146 | | prmnn 16231 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℙ → 𝑧 ∈
ℕ) |
147 | 146 | nncnd 11846 |
. . . . . . . 8
⊢ (𝑧 ∈ ℙ → 𝑧 ∈
ℂ) |
148 | 147 | sqvald 13713 |
. . . . . . 7
⊢ (𝑧 ∈ ℙ → (𝑧↑2) = (𝑧 · 𝑧)) |
149 | 148 | breq1d 5063 |
. . . . . 6
⊢ (𝑧 ∈ ℙ → ((𝑧↑2) ≤ 𝑃 ↔ (𝑧 · 𝑧) ≤ 𝑃)) |
150 | 149 | imbi1d 345 |
. . . . 5
⊢ (𝑧 ∈ ℙ → (((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃) ↔ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
151 | 150 | ralbiia 3087 |
. . . 4
⊢
(∀𝑧 ∈
ℙ ((𝑧↑2) ≤
𝑃 → ¬ 𝑧 ∥ 𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧 · 𝑧) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)) |
152 | 145, 151 | bitr4di 292 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) → (∀𝑧 ∈
(ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃) ↔ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
153 | 152 | pm5.32i 578 |
. 2
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈
(ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃)) ↔ (𝑃 ∈ (ℤ≥‘2)
∧ ∀𝑧 ∈
ℙ ((𝑧↑2) ≤
𝑃 → ¬ 𝑧 ∥ 𝑃))) |
154 | 1, 153 | bitri 278 |
1
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |