Proof of Theorem isprm7
Step | Hyp | Ref
| Expression |
1 | | isprm5 16149 |
. 2
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))) |
2 | | prmz 16117 |
. . . . . . . 8
⊢ (𝑧 ∈ ℙ → 𝑧 ∈
ℤ) |
3 | 2 | zred 12169 |
. . . . . . 7
⊢ (𝑧 ∈ ℙ → 𝑧 ∈
ℝ) |
4 | | 0red 10723 |
. . . . . . . 8
⊢ (𝑧 ∈ ℙ → 0 ∈
ℝ) |
5 | | 1red 10721 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℙ → 1 ∈
ℝ) |
6 | | 0lt1 11241 |
. . . . . . . . . 10
⊢ 0 <
1 |
7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℙ → 0 <
1) |
8 | | prmgt1 16139 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℙ → 1 <
𝑧) |
9 | 4, 5, 3, 7, 8 | lttrd 10880 |
. . . . . . . 8
⊢ (𝑧 ∈ ℙ → 0 <
𝑧) |
10 | 4, 3, 9 | ltled 10867 |
. . . . . . 7
⊢ (𝑧 ∈ ℙ → 0 ≤
𝑧) |
11 | 3, 10 | jca 515 |
. . . . . 6
⊢ (𝑧 ∈ ℙ → (𝑧 ∈ ℝ ∧ 0 ≤
𝑧)) |
12 | | eluzelre 12336 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℝ) |
13 | | 0red 10723 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → 0 ∈ ℝ) |
14 | | 2re 11791 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ∈ ℝ) |
16 | | 0le2 11819 |
. . . . . . . . 9
⊢ 0 ≤
2 |
17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → 0 ≤ 2) |
18 | | eluzle 12338 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) |
19 | 13, 15, 12, 17, 18 | letrd 10876 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → 0 ≤ 𝑃) |
20 | 12, 19 | jca 515 |
. . . . . 6
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 ∈ ℝ ∧ 0 ≤ 𝑃)) |
21 | | resqcl 13583 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ → (𝑧↑2) ∈
ℝ) |
22 | | sqge0 13594 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ → 0 ≤
(𝑧↑2)) |
23 | 21, 22 | jca 515 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℝ → ((𝑧↑2) ∈ ℝ ∧ 0
≤ (𝑧↑2))) |
24 | 23 | adantr 484 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) → ((𝑧↑2) ∈ ℝ ∧ 0
≤ (𝑧↑2))) |
25 | | sqrtle 14711 |
. . . . . . . 8
⊢ ((((𝑧↑2) ∈ ℝ ∧ 0
≤ (𝑧↑2)) ∧
(𝑃 ∈ ℝ ∧ 0
≤ 𝑃)) → ((𝑧↑2) ≤ 𝑃 ↔ (√‘(𝑧↑2)) ≤ (√‘𝑃))) |
26 | 24, 25 | sylan 583 |
. . . . . . 7
⊢ (((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) ∧ (𝑃 ∈ ℝ ∧ 0 ≤ 𝑃)) → ((𝑧↑2) ≤ 𝑃 ↔ (√‘(𝑧↑2)) ≤ (√‘𝑃))) |
27 | | sqrtsq 14720 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) →
(√‘(𝑧↑2))
= 𝑧) |
28 | 27 | breq1d 5041 |
. . . . . . . 8
⊢ ((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) →
((√‘(𝑧↑2))
≤ (√‘𝑃)
↔ 𝑧 ≤
(√‘𝑃))) |
29 | 28 | adantr 484 |
. . . . . . 7
⊢ (((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) ∧ (𝑃 ∈ ℝ ∧ 0 ≤ 𝑃)) → ((√‘(𝑧↑2)) ≤
(√‘𝑃) ↔
𝑧 ≤ (√‘𝑃))) |
30 | 26, 29 | bitrd 282 |
. . . . . 6
⊢ (((𝑧 ∈ ℝ ∧ 0 ≤
𝑧) ∧ (𝑃 ∈ ℝ ∧ 0 ≤ 𝑃)) → ((𝑧↑2) ≤ 𝑃 ↔ 𝑧 ≤ (√‘𝑃))) |
31 | 11, 20, 30 | syl2anr 600 |
. . . . 5
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) → ((𝑧↑2) ≤ 𝑃 ↔ 𝑧 ≤ (√‘𝑃))) |
32 | 31 | imbi1d 345 |
. . . 4
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) → (((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃) ↔ (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃))) |
33 | 32 | ralbidva 3108 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) → (∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃) ↔ ∀𝑧 ∈ ℙ (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃))) |
34 | 33 | pm5.32i 578 |
. 2
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)) ↔ (𝑃 ∈ (ℤ≥‘2)
∧ ∀𝑧 ∈
ℙ (𝑧 ≤
(√‘𝑃) →
¬ 𝑧 ∥ 𝑃))) |
35 | | impexp 454 |
. . . . 5
⊢ (((𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃)) → ¬ 𝑧 ∥ 𝑃) ↔ (𝑧 ∈ ℙ → (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃))) |
36 | 12, 19 | resqrtcld 14868 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) → (√‘𝑃) ∈ ℝ) |
37 | 36 | flcld 13260 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → (⌊‘(√‘𝑃)) ∈
ℤ) |
38 | 37, 2 | anim12i 616 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) →
((⌊‘(√‘𝑃)) ∈ ℤ ∧ 𝑧 ∈ ℤ)) |
39 | 38 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) ∧ 𝑧 ≤ (√‘𝑃)) →
((⌊‘(√‘𝑃)) ∈ ℤ ∧ 𝑧 ∈ ℤ)) |
40 | | prmuz2 16138 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℙ → 𝑧 ∈
(ℤ≥‘2)) |
41 | | eluzle 12338 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
(ℤ≥‘2) → 2 ≤ 𝑧) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℙ → 2 ≤
𝑧) |
43 | 42 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) ∧ 𝑧 ≤ (√‘𝑃)) → 2 ≤ 𝑧) |
44 | | flge 13267 |
. . . . . . . . . . . . 13
⊢
(((√‘𝑃)
∈ ℝ ∧ 𝑧
∈ ℤ) → (𝑧
≤ (√‘𝑃)
↔ 𝑧 ≤
(⌊‘(√‘𝑃)))) |
45 | 36, 2, 44 | syl2an 599 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) → (𝑧 ≤ (√‘𝑃) ↔ 𝑧 ≤ (⌊‘(√‘𝑃)))) |
46 | 45 | biimpa 480 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) ∧ 𝑧 ≤ (√‘𝑃)) → 𝑧 ≤ (⌊‘(√‘𝑃))) |
47 | | 2z 12096 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
48 | | elfz4 12992 |
. . . . . . . . . . . 12
⊢ (((2
∈ ℤ ∧ (⌊‘(√‘𝑃)) ∈ ℤ ∧ 𝑧 ∈ ℤ) ∧ (2 ≤ 𝑧 ∧ 𝑧 ≤ (⌊‘(√‘𝑃)))) → 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) |
49 | 47, 48 | mp3anl1 1456 |
. . . . . . . . . . 11
⊢
((((⌊‘(√‘𝑃)) ∈ ℤ ∧ 𝑧 ∈ ℤ) ∧ (2 ≤ 𝑧 ∧ 𝑧 ≤ (⌊‘(√‘𝑃)))) → 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) |
50 | 39, 43, 46, 49 | syl12anc 836 |
. . . . . . . . . 10
⊢ (((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈ ℙ) ∧ 𝑧 ≤ (√‘𝑃)) → 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) |
51 | 50 | anasss 470 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃))) → 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) |
52 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃))) → 𝑧 ∈ ℙ) |
53 | 51, 52 | elind 4085 |
. . . . . . . 8
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃))) → 𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ)) |
54 | 53 | ex 416 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃)) → 𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ))) |
55 | | elin 3860 |
. . . . . . . . 9
⊢ (𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) ↔ (𝑧 ∈
(2...(⌊‘(√‘𝑃))) ∧ 𝑧 ∈ ℙ)) |
56 | | elfzelz 12999 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(2...(⌊‘(√‘𝑃))) → 𝑧 ∈ ℤ) |
57 | 56 | zred 12169 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
(2...(⌊‘(√‘𝑃))) → 𝑧 ∈ ℝ) |
58 | 57 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) → 𝑧 ∈ ℝ) |
59 | | reflcl 13258 |
. . . . . . . . . . . . . 14
⊢
((√‘𝑃)
∈ ℝ → (⌊‘(√‘𝑃)) ∈ ℝ) |
60 | 36, 59 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → (⌊‘(√‘𝑃)) ∈
ℝ) |
61 | 60 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) →
(⌊‘(√‘𝑃)) ∈ ℝ) |
62 | 36 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) → (√‘𝑃) ∈ ℝ) |
63 | | elfzle2 13003 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
(2...(⌊‘(√‘𝑃))) → 𝑧 ≤ (⌊‘(√‘𝑃))) |
64 | 63 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) → 𝑧 ≤ (⌊‘(√‘𝑃))) |
65 | | flle 13261 |
. . . . . . . . . . . . . 14
⊢
((√‘𝑃)
∈ ℝ → (⌊‘(√‘𝑃)) ≤ (√‘𝑃)) |
66 | 36, 65 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
(ℤ≥‘2) → (⌊‘(√‘𝑃)) ≤ (√‘𝑃)) |
67 | 66 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) →
(⌊‘(√‘𝑃)) ≤ (√‘𝑃)) |
68 | 58, 61, 62, 64, 67 | letrd 10876 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∈
(2...(⌊‘(√‘𝑃)))) → 𝑧 ≤ (√‘𝑃)) |
69 | 68 | ex 416 |
. . . . . . . . . 10
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑧 ∈
(2...(⌊‘(√‘𝑃))) → 𝑧 ≤ (√‘𝑃))) |
70 | 69 | anim1d 614 |
. . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈
(2...(⌊‘(√‘𝑃))) ∧ 𝑧 ∈ ℙ) → (𝑧 ≤ (√‘𝑃) ∧ 𝑧 ∈ ℙ))) |
71 | 55, 70 | syl5bi 245 |
. . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) → (𝑧 ≤ (√‘𝑃) ∧ 𝑧 ∈ ℙ))) |
72 | | ancom 464 |
. . . . . . . 8
⊢ ((𝑧 ≤ (√‘𝑃) ∧ 𝑧 ∈ ℙ) ↔ (𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃))) |
73 | 71, 72 | syl6ib 254 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) → (𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃)))) |
74 | 54, 73 | impbid 215 |
. . . . . 6
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃)) ↔ 𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ))) |
75 | 74 | imbi1d 345 |
. . . . 5
⊢ (𝑃 ∈
(ℤ≥‘2) → (((𝑧 ∈ ℙ ∧ 𝑧 ≤ (√‘𝑃)) → ¬ 𝑧 ∥ 𝑃) ↔ (𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) → ¬ 𝑧 ∥ 𝑃))) |
76 | 35, 75 | bitr3id 288 |
. . . 4
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈ ℙ → (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃)) ↔ (𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) → ¬ 𝑧 ∥ 𝑃))) |
77 | 76 | ralbidv2 3107 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) → (∀𝑧 ∈ ℙ (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃) ↔ ∀𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) ¬ 𝑧 ∥ 𝑃)) |
78 | 77 | pm5.32i 578 |
. 2
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ (𝑧 ≤ (√‘𝑃) → ¬ 𝑧 ∥ 𝑃)) ↔ (𝑃 ∈ (ℤ≥‘2)
∧ ∀𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) ¬ 𝑧 ∥ 𝑃)) |
79 | 1, 34, 78 | 3bitri 300 |
1
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈
((2...(⌊‘(√‘𝑃))) ∩ ℙ) ¬ 𝑧 ∥ 𝑃)) |