Proof of Theorem isprm7
| Step | Hyp | Ref
| Expression |
| 1 | | isprm5 16744 |
. 2
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
| 2 | | prmz 16712 |
. . . . . . . 8
⊢ (𝑧 ∈ ℙ → 𝑧 ∈
ℤ) |
| 3 | 2 | zred 12722 |
. . . . . . 7
⊢ (𝑧 ∈ ℙ → 𝑧 ∈
ℝ) |
| 4 | | 0red 11264 |
. . . . . . . 8
⊢ (𝑧 ∈ ℙ → 0 ∈
ℝ) |
| 5 | | 1red 11262 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℙ → 1 ∈
ℝ) |
| 6 | | 0lt1 11785 |
. . . . . . . . . 10
⊢ 0 <
1 |
| 7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℙ → 0 <
1) |
| 8 | | prmgt1 16734 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℙ → 1 <
𝑧) |
| 9 | 4, 5, 3, 7, 8 | lttrd 11422 |
. . . . . . . 8
⊢ (𝑧 ∈ ℙ → 0 <
𝑧) |
| 10 | 4, 3, 9 | ltled 11409 |
. . . . . . 7
⊢ (𝑧 ∈ ℙ → 0 ≤
𝑧) |
| 11 | 3, 10 | jca 511 |
. . . . . 6
⊢ (𝑧 ∈ ℙ → (𝑧 ∈ ℝ ∧ 0 ≤
𝑧)) |
| 12 | | eluzelre 12889 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℝ) |
| 13 | | 0red 11264 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → 0 ∈ ℝ) |
| 14 | | 2re 12340 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
| 15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ∈ ℝ) |
| 16 | | 0le2 12368 |
. . . . . . . . 9
⊢ 0 ≤
2 |
| 17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → 0 ≤ 2) |
| 18 | | eluzle 12891 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) |
| 19 | 13, 15, 12, 17, 18 | letrd 11418 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → 0 ≤ 𝑃) |
| 20 | 12, 19 | jca 511 |
. . . . . 6
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 ∈ ℝ ∧ 0 ≤ 𝑃)) |
| 21 | | resqcl 14164 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ → (𝑧↑2) ∈
ℝ) |
| 22 | | sqge0 14176 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ → 0 ≤
(𝑧↑2)) |
| 23 | 21, 22 | jca 511 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℝ → ((𝑧↑2) ∈ ℝ ∧ 0
≤ (𝑧↑2))) |
| 24 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) → ((𝑧↑2) ∈ ℝ ∧ 0
≤ (𝑧↑2))) |
| 25 | | sqrtle 15299 |
. . . . . . . 8
⊢ ((((𝑧↑2) ∈ ℝ ∧ 0
≤ (𝑧↑2)) ∧
(𝑃 ∈ ℝ ∧ 0
≤ 𝑃)) → ((𝑧↑2) ≤ 𝑃 ↔ (√‘(𝑧↑2)) ≤ (√‘𝑃))) |
| 26 | 24, 25 | sylan 580 |
. . . . . . 7
⊢ (((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) ∧ (𝑃 ∈ ℝ ∧ 0 ≤ 𝑃)) → ((𝑧↑2) ≤ 𝑃 ↔ (√‘(𝑧↑2)) ≤ (√‘𝑃))) |
| 27 | | sqrtsq 15308 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) →
(√‘(𝑧↑2))
= 𝑧) |
| 28 | 27 | breq1d 5153 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) →
((√‘(𝑧↑2))
≤ (√‘𝑃)
↔ 𝑧 ≤
(√‘𝑃))) |
| 29 | 28 | adantr 480 |
. . . . . . 7
⊢ (((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) ∧ (𝑃 ∈ ℝ ∧ 0 ≤ 𝑃)) → ((√‘(𝑧↑2)) ≤
(√‘𝑃) ↔
𝑧 ≤ (√‘𝑃))) |
| 30 | 26, 29 | bitrd 279 |
. . . . . 6
⊢ (((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) ∧ (𝑃 ∈ ℝ ∧ 0 ≤ 𝑃)) → ((𝑧↑2) ≤ 𝑃 ↔ 𝑧 ≤ (√‘𝑃))) |
| 31 | 11, 20, 30 | syl2anr 597 |
. . . . 5
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) → ((𝑧↑2) ≤ 𝑃 ↔ 𝑧 ≤ (√‘𝑃))) |
| 32 | 31 | imbi1d 341 |
. . . 4
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) → (((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃) ↔ (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃))) |
| 33 | 32 | ralbidva 3176 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) → (∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃) ↔ ∀𝑧 ∈ ℙ (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃))) |
| 34 | 33 | pm5.32i 574 |
. 2
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)) ↔ (𝑃 ∈ (ℤ≥‘2)
∧ ∀𝑧 ∈
ℙ (𝑧 ≤
(√‘𝑃) →
¬ 𝑧 ∥ 𝑃))) |
| 35 | | impexp 450 |
. . . . 5
⊢ (((𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃)) → ¬ 𝑧 ∥ 𝑃) ↔ (𝑧 ∈ ℙ → (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃))) |
| 36 | 12, 19 | resqrtcld 15456 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) → (√‘𝑃) ∈ ℝ) |
| 37 | 36 | flcld 13838 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → (⌊‘(√‘𝑃)) ∈
ℤ) |
| 38 | 37, 2 | anim12i 613 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) →
((⌊‘(√‘𝑃)) ∈ ℤ ∧ 𝑧 ∈ ℤ)) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) ∧ 𝑧 ≤ (√‘𝑃)) →
((⌊‘(√‘𝑃)) ∈ ℤ ∧ 𝑧 ∈ ℤ)) |
| 40 | | prmuz2 16733 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℙ → 𝑧 ∈
(ℤ≥‘2)) |
| 41 | | eluzle 12891 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
(ℤ≥‘2) → 2 ≤ 𝑧) |
| 42 | 40, 41 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℙ → 2 ≤
𝑧) |
| 43 | 42 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) ∧ 𝑧 ≤ (√‘𝑃)) → 2 ≤ 𝑧) |
| 44 | | flge 13845 |
. . . . . . . . . . . . 13
⊢
(((√‘𝑃)
∈ ℝ ∧ 𝑧
∈ ℤ) → (𝑧
≤ (√‘𝑃)
↔ 𝑧 ≤
(⌊‘(√‘𝑃)))) |
| 45 | 36, 2, 44 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) → (𝑧 ≤ (√‘𝑃) ↔ 𝑧 ≤ (⌊‘(√‘𝑃)))) |
| 46 | 45 | biimpa 476 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) ∧ 𝑧 ≤ (√‘𝑃)) → 𝑧 ≤ (⌊‘(√‘𝑃))) |
| 47 | | 2z 12649 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
| 48 | | elfz4 13557 |
. . . . . . . . . . . 12
⊢ (((2
∈ ℤ ∧ (⌊‘(√‘𝑃)) ∈ ℤ ∧ 𝑧 ∈ ℤ) ∧ (2 ≤ 𝑧 ∧ 𝑧 ≤ (⌊‘(√‘𝑃)))) → 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) |
| 49 | 47, 48 | mp3anl1 1457 |
. . . . . . . . . . 11
⊢
((((⌊‘(√‘𝑃)) ∈ ℤ ∧ 𝑧 ∈ ℤ) ∧ (2 ≤ 𝑧 ∧ 𝑧 ≤ (⌊‘(√‘𝑃)))) → 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) |
| 50 | 39, 43, 46, 49 | syl12anc 837 |
. . . . . . . . . 10
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) ∧ 𝑧 ≤ (√‘𝑃)) → 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) |
| 51 | 50 | anasss 466 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃))) → 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) |
| 52 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃))) → 𝑧 ∈ ℙ) |
| 53 | 51, 52 | elind 4200 |
. . . . . . . 8
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃))) → 𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ)) |
| 54 | 53 | ex 412 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃)) → 𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ))) |
| 55 | | elin 3967 |
. . . . . . . . 9
⊢ (𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) ↔ (𝑧 ∈
(2...(⌊‘(√‘𝑃))) ∧ 𝑧 ∈ ℙ)) |
| 56 | | elfzelz 13564 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(2...(⌊‘(√‘𝑃))) → 𝑧 ∈ ℤ) |
| 57 | 56 | zred 12722 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
(2...(⌊‘(√‘𝑃))) → 𝑧 ∈ ℝ) |
| 58 | 57 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) → 𝑧 ∈ ℝ) |
| 59 | | reflcl 13836 |
. . . . . . . . . . . . . 14
⊢
((√‘𝑃)
∈ ℝ → (⌊‘(√‘𝑃)) ∈ ℝ) |
| 60 | 36, 59 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → (⌊‘(√‘𝑃)) ∈
ℝ) |
| 61 | 60 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) →
(⌊‘(√‘𝑃)) ∈ ℝ) |
| 62 | 36 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) → (√‘𝑃) ∈ ℝ) |
| 63 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
(2...(⌊‘(√‘𝑃))) → 𝑧 ≤ (⌊‘(√‘𝑃))) |
| 64 | 63 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) → 𝑧 ≤ (⌊‘(√‘𝑃))) |
| 65 | | flle 13839 |
. . . . . . . . . . . . . 14
⊢
((√‘𝑃)
∈ ℝ → (⌊‘(√‘𝑃)) ≤ (√‘𝑃)) |
| 66 | 36, 65 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → (⌊‘(√‘𝑃)) ≤ (√‘𝑃)) |
| 67 | 66 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) →
(⌊‘(√‘𝑃)) ≤ (√‘𝑃)) |
| 68 | 58, 61, 62, 64, 67 | letrd 11418 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) → 𝑧 ≤ (√‘𝑃)) |
| 69 | 68 | ex 412 |
. . . . . . . . . 10
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑧 ∈
(2...(⌊‘(√‘𝑃))) → 𝑧 ≤ (√‘𝑃))) |
| 70 | 69 | anim1d 611 |
. . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈
(2...(⌊‘(√‘𝑃))) ∧ 𝑧 ∈ ℙ) → (𝑧 ≤ (√‘𝑃) ∧ 𝑧 ∈ ℙ))) |
| 71 | 55, 70 | biimtrid 242 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) → (𝑧 ≤ (√‘𝑃) ∧ 𝑧 ∈ ℙ))) |
| 72 | | ancom 460 |
. . . . . . . 8
⊢ ((𝑧 ≤ (√‘𝑃) ∧ 𝑧 ∈ ℙ) ↔ (𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃))) |
| 73 | 71, 72 | imbitrdi 251 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) → (𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃)))) |
| 74 | 54, 73 | impbid 212 |
. . . . . 6
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃)) ↔ 𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ))) |
| 75 | 74 | imbi1d 341 |
. . . . 5
⊢ (𝑃 ∈
(ℤ≥‘2) → (((𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃)) → ¬ 𝑧 ∥ 𝑃) ↔ (𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) → ¬ 𝑧 ∥ 𝑃))) |
| 76 | 35, 75 | bitr3id 285 |
. . . 4
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈ ℙ → (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃)) ↔ (𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) → ¬ 𝑧 ∥ 𝑃))) |
| 77 | 76 | ralbidv2 3174 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) → (∀𝑧 ∈ ℙ (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃) ↔ ∀𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) ¬ 𝑧 ∥ 𝑃)) |
| 78 | 77 | pm5.32i 574 |
. 2
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃)) ↔ (𝑃 ∈ (ℤ≥‘2)
∧ ∀𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) ¬ 𝑧 ∥ 𝑃)) |
| 79 | 1, 34, 78 | 3bitri 297 |
1
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) ¬ 𝑧 ∥ 𝑃)) |