Proof of Theorem ppiltx
| Step | Hyp | Ref
| Expression |
| 1 | | rpre 13043 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
| 2 | | ppicl 27174 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(π‘𝐴)
∈ ℕ0) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (π‘𝐴) ∈
ℕ0) |
| 4 | 3 | nn0red 12588 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (π‘𝐴) ∈ ℝ) |
| 5 | 4 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (π‘𝐴) ∈ ℝ) |
| 6 | | reflcl 13836 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
| 7 | 1, 6 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℝ) |
| 8 | 7 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (⌊‘𝐴) ∈ ℝ) |
| 9 | 1 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → 𝐴
∈ ℝ) |
| 10 | | fzfi 14013 |
. . . . . 6
⊢
(1...(⌊‘𝐴)) ∈ Fin |
| 11 | | inss1 4237 |
. . . . . . 7
⊢
((2...(⌊‘𝐴)) ∩ ℙ) ⊆
(2...(⌊‘𝐴)) |
| 12 | | 2eluzge1 12936 |
. . . . . . . . 9
⊢ 2 ∈
(ℤ≥‘1) |
| 13 | | fzss1 13603 |
. . . . . . . . 9
⊢ (2 ∈
(ℤ≥‘1) → (2...(⌊‘𝐴)) ⊆ (1...(⌊‘𝐴))) |
| 14 | 12, 13 | mp1i 13 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (2...(⌊‘𝐴)) ⊆ (1...(⌊‘𝐴))) |
| 15 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (⌊‘𝐴) ∈ ℕ) |
| 16 | | nnuz 12921 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
| 17 | 15, 16 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (⌊‘𝐴) ∈
(ℤ≥‘1)) |
| 18 | | eluzfz1 13571 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ (ℤ≥‘1) → 1 ∈
(1...(⌊‘𝐴))) |
| 19 | 17, 18 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → 1 ∈ (1...(⌊‘𝐴))) |
| 20 | | 1lt2 12437 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
| 21 | | 1re 11261 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
| 22 | | 2re 12340 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
| 23 | 21, 22 | ltnlei 11382 |
. . . . . . . . . . . 12
⊢ (1 < 2
↔ ¬ 2 ≤ 1) |
| 24 | 20, 23 | mpbi 230 |
. . . . . . . . . . 11
⊢ ¬ 2
≤ 1 |
| 25 | | elfzle1 13567 |
. . . . . . . . . . 11
⊢ (1 ∈
(2...(⌊‘𝐴))
→ 2 ≤ 1) |
| 26 | 24, 25 | mto 197 |
. . . . . . . . . 10
⊢ ¬ 1
∈ (2...(⌊‘𝐴)) |
| 27 | | nelne1 3039 |
. . . . . . . . . 10
⊢ ((1
∈ (1...(⌊‘𝐴)) ∧ ¬ 1 ∈
(2...(⌊‘𝐴)))
→ (1...(⌊‘𝐴)) ≠ (2...(⌊‘𝐴))) |
| 28 | 19, 26, 27 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (1...(⌊‘𝐴)) ≠ (2...(⌊‘𝐴))) |
| 29 | 28 | necomd 2996 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (2...(⌊‘𝐴)) ≠ (1...(⌊‘𝐴))) |
| 30 | | df-pss 3971 |
. . . . . . . 8
⊢
((2...(⌊‘𝐴)) ⊊ (1...(⌊‘𝐴)) ↔
((2...(⌊‘𝐴))
⊆ (1...(⌊‘𝐴)) ∧ (2...(⌊‘𝐴)) ≠
(1...(⌊‘𝐴)))) |
| 31 | 14, 29, 30 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (2...(⌊‘𝐴)) ⊊ (1...(⌊‘𝐴))) |
| 32 | | sspsstr 4108 |
. . . . . . 7
⊢
((((2...(⌊‘𝐴)) ∩ ℙ) ⊆
(2...(⌊‘𝐴))
∧ (2...(⌊‘𝐴)) ⊊ (1...(⌊‘𝐴))) →
((2...(⌊‘𝐴))
∩ ℙ) ⊊ (1...(⌊‘𝐴))) |
| 33 | 11, 31, 32 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → ((2...(⌊‘𝐴)) ∩ ℙ) ⊊
(1...(⌊‘𝐴))) |
| 34 | | php3 9249 |
. . . . . 6
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧
((2...(⌊‘𝐴))
∩ ℙ) ⊊ (1...(⌊‘𝐴))) → ((2...(⌊‘𝐴)) ∩ ℙ) ≺
(1...(⌊‘𝐴))) |
| 35 | 10, 33, 34 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → ((2...(⌊‘𝐴)) ∩ ℙ) ≺
(1...(⌊‘𝐴))) |
| 36 | | fzfi 14013 |
. . . . . . 7
⊢
(2...(⌊‘𝐴)) ∈ Fin |
| 37 | | ssfi 9213 |
. . . . . . 7
⊢
(((2...(⌊‘𝐴)) ∈ Fin ∧
((2...(⌊‘𝐴))
∩ ℙ) ⊆ (2...(⌊‘𝐴))) → ((2...(⌊‘𝐴)) ∩ ℙ) ∈
Fin) |
| 38 | 36, 11, 37 | mp2an 692 |
. . . . . 6
⊢
((2...(⌊‘𝐴)) ∩ ℙ) ∈
Fin |
| 39 | | hashsdom 14420 |
. . . . . 6
⊢
((((2...(⌊‘𝐴)) ∩ ℙ) ∈ Fin ∧
(1...(⌊‘𝐴))
∈ Fin) → ((♯‘((2...(⌊‘𝐴)) ∩ ℙ)) <
(♯‘(1...(⌊‘𝐴))) ↔ ((2...(⌊‘𝐴)) ∩ ℙ) ≺
(1...(⌊‘𝐴)))) |
| 40 | 38, 10, 39 | mp2an 692 |
. . . . 5
⊢
((♯‘((2...(⌊‘𝐴)) ∩ ℙ)) <
(♯‘(1...(⌊‘𝐴))) ↔ ((2...(⌊‘𝐴)) ∩ ℙ) ≺
(1...(⌊‘𝐴))) |
| 41 | 35, 40 | sylibr 234 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (♯‘((2...(⌊‘𝐴)) ∩ ℙ)) <
(♯‘(1...(⌊‘𝐴)))) |
| 42 | 1 | flcld 13838 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℤ) |
| 43 | | ppival2 27171 |
. . . . . . 7
⊢
((⌊‘𝐴)
∈ ℤ → (π‘(⌊‘𝐴)) =
(♯‘((2...(⌊‘𝐴)) ∩ ℙ))) |
| 44 | 42, 43 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (π‘(⌊‘𝐴)) =
(♯‘((2...(⌊‘𝐴)) ∩ ℙ))) |
| 45 | | ppifl 27203 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(π‘(⌊‘𝐴)) = (π‘𝐴)) |
| 46 | 1, 45 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (π‘(⌊‘𝐴)) = (π‘𝐴)) |
| 47 | 44, 46 | eqtr3d 2779 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (♯‘((2...(⌊‘𝐴)) ∩ ℙ)) =
(π‘𝐴)) |
| 48 | 47 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (♯‘((2...(⌊‘𝐴)) ∩ ℙ)) =
(π‘𝐴)) |
| 49 | | rpge0 13048 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ 0 ≤ 𝐴) |
| 50 | | flge0nn0 13860 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
| 51 | 1, 49, 50 | syl2anc 584 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℕ0) |
| 52 | | hashfz1 14385 |
. . . . . 6
⊢
((⌊‘𝐴)
∈ ℕ0 → (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
| 53 | 51, 52 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
| 54 | 53 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
| 55 | 41, 48, 54 | 3brtr3d 5174 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (π‘𝐴) < (⌊‘𝐴)) |
| 56 | | flle 13839 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
| 57 | 9, 56 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (⌊‘𝐴) ≤ 𝐴) |
| 58 | 5, 8, 9, 55, 57 | ltletrd 11421 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (π‘𝐴) < 𝐴) |
| 59 | 46 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (π‘(⌊‘𝐴)) = (π‘𝐴)) |
| 60 | | simpr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (⌊‘𝐴)
= 0) |
| 61 | 60 | fveq2d 6910 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (π‘(⌊‘𝐴)) = (π‘0)) |
| 62 | | 2pos 12369 |
. . . . . 6
⊢ 0 <
2 |
| 63 | | 0re 11263 |
. . . . . . 7
⊢ 0 ∈
ℝ |
| 64 | | ppieq0 27219 |
. . . . . . 7
⊢ (0 ∈
ℝ → ((π‘0) = 0 ↔ 0 < 2)) |
| 65 | 63, 64 | ax-mp 5 |
. . . . . 6
⊢
((π‘0) = 0 ↔ 0 < 2) |
| 66 | 62, 65 | mpbir 231 |
. . . . 5
⊢
(π‘0) = 0 |
| 67 | 61, 66 | eqtrdi 2793 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (π‘(⌊‘𝐴)) = 0) |
| 68 | 59, 67 | eqtr3d 2779 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (π‘𝐴) = 0) |
| 69 | | rpgt0 13047 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ 0 < 𝐴) |
| 70 | 69 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → 0 < 𝐴) |
| 71 | 68, 70 | eqbrtrd 5165 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (π‘𝐴) < 𝐴) |
| 72 | | elnn0 12528 |
. . 3
⊢
((⌊‘𝐴)
∈ ℕ0 ↔ ((⌊‘𝐴) ∈ ℕ ∨ (⌊‘𝐴) = 0)) |
| 73 | 51, 72 | sylib 218 |
. 2
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴)
∈ ℕ ∨ (⌊‘𝐴) = 0)) |
| 74 | 58, 71, 73 | mpjaodan 961 |
1
⊢ (𝐴 ∈ ℝ+
→ (π‘𝐴) < 𝐴) |