Proof of Theorem rpnnen2lem9
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
| 2 | | nnz 12634 |
. . 3
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
| 3 | | eqidd 2738 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑀)) → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘)) |
| 4 | | eluznn 12960 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑀)) → 𝑘 ∈ ℕ) |
| 5 | | difss 4136 |
. . . . . . 7
⊢ (ℕ
∖ {𝑀}) ⊆
ℕ |
| 6 | | rpnnen2.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) |
| 7 | 6 | rpnnen2lem2 16251 |
. . . . . . 7
⊢ ((ℕ
∖ {𝑀}) ⊆
ℕ → (𝐹‘(ℕ ∖ {𝑀})):ℕ⟶ℝ) |
| 8 | 5, 7 | ax-mp 5 |
. . . . . 6
⊢ (𝐹‘(ℕ ∖ {𝑀})):ℕ⟶ℝ |
| 9 | 8 | ffvelcdmi 7103 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) ∈ ℝ) |
| 10 | 9 | recnd 11289 |
. . . 4
⊢ (𝑘 ∈ ℕ → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) ∈ ℂ) |
| 11 | 4, 10 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑀)) → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) ∈ ℂ) |
| 12 | 6 | rpnnen2lem5 16254 |
. . . 4
⊢
(((ℕ ∖ {𝑀}) ⊆ ℕ ∧ 𝑀 ∈ ℕ) → seq𝑀( + , (𝐹‘(ℕ ∖ {𝑀}))) ∈ dom ⇝ ) |
| 13 | 5, 12 | mpan 690 |
. . 3
⊢ (𝑀 ∈ ℕ → seq𝑀( + , (𝐹‘(ℕ ∖ {𝑀}))) ∈ dom ⇝ ) |
| 14 | 1, 2, 3, 11, 13 | isum1p 15877 |
. 2
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈
(ℤ≥‘𝑀)((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = (((𝐹‘(ℕ ∖ {𝑀}))‘𝑀) + Σ𝑘 ∈ (ℤ≥‘(𝑀 + 1))((𝐹‘(ℕ ∖ {𝑀}))‘𝑘))) |
| 15 | 6 | rpnnen2lem1 16250 |
. . . . 5
⊢
(((ℕ ∖ {𝑀}) ⊆ ℕ ∧ 𝑀 ∈ ℕ) → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑀) = if(𝑀 ∈ (ℕ ∖ {𝑀}), ((1 / 3)↑𝑀), 0)) |
| 16 | 5, 15 | mpan 690 |
. . . 4
⊢ (𝑀 ∈ ℕ → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑀) = if(𝑀 ∈ (ℕ ∖ {𝑀}), ((1 / 3)↑𝑀), 0)) |
| 17 | | neldifsnd 4793 |
. . . . 5
⊢ (𝑀 ∈ ℕ → ¬
𝑀 ∈ (ℕ ∖
{𝑀})) |
| 18 | 17 | iffalsed 4536 |
. . . 4
⊢ (𝑀 ∈ ℕ → if(𝑀 ∈ (ℕ ∖ {𝑀}), ((1 / 3)↑𝑀), 0) = 0) |
| 19 | 16, 18 | eqtrd 2777 |
. . 3
⊢ (𝑀 ∈ ℕ → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑀) = 0) |
| 20 | | eqid 2737 |
. . . 4
⊢
(ℤ≥‘(𝑀 + 1)) =
(ℤ≥‘(𝑀 + 1)) |
| 21 | | peano2nn 12278 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑀 + 1) ∈
ℕ) |
| 22 | 21 | nnzd 12640 |
. . . 4
⊢ (𝑀 ∈ ℕ → (𝑀 + 1) ∈
ℤ) |
| 23 | | eqidd 2738 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘)) |
| 24 | | eluznn 12960 |
. . . . . 6
⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑘 ∈ ℕ) |
| 25 | 21, 24 | sylan 580 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑘 ∈ ℕ) |
| 26 | 25, 10 | syl 17 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) ∈ ℂ) |
| 27 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 28 | | 3nn 12345 |
. . . . . . . 8
⊢ 3 ∈
ℕ |
| 29 | | nndivre 12307 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 3 ∈ ℕ) → (1 / 3) ∈
ℝ) |
| 30 | 27, 28, 29 | mp2an 692 |
. . . . . . 7
⊢ (1 / 3)
∈ ℝ |
| 31 | 30 | recni 11275 |
. . . . . 6
⊢ (1 / 3)
∈ ℂ |
| 32 | 31 | a1i 11 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (1 / 3)
∈ ℂ) |
| 33 | | 0re 11263 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
| 34 | | 3re 12346 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
| 35 | | 3pos 12371 |
. . . . . . . . . 10
⊢ 0 <
3 |
| 36 | 34, 35 | recgt0ii 12174 |
. . . . . . . . 9
⊢ 0 < (1
/ 3) |
| 37 | 33, 30, 36 | ltleii 11384 |
. . . . . . . 8
⊢ 0 ≤ (1
/ 3) |
| 38 | | absid 15335 |
. . . . . . . 8
⊢ (((1 / 3)
∈ ℝ ∧ 0 ≤ (1 / 3)) → (abs‘(1 / 3)) = (1 /
3)) |
| 39 | 30, 37, 38 | mp2an 692 |
. . . . . . 7
⊢
(abs‘(1 / 3)) = (1 / 3) |
| 40 | | 1lt3 12439 |
. . . . . . . 8
⊢ 1 <
3 |
| 41 | | recgt1 12164 |
. . . . . . . . 9
⊢ ((3
∈ ℝ ∧ 0 < 3) → (1 < 3 ↔ (1 / 3) <
1)) |
| 42 | 34, 35, 41 | mp2an 692 |
. . . . . . . 8
⊢ (1 < 3
↔ (1 / 3) < 1) |
| 43 | 40, 42 | mpbi 230 |
. . . . . . 7
⊢ (1 / 3)
< 1 |
| 44 | 39, 43 | eqbrtri 5164 |
. . . . . 6
⊢
(abs‘(1 / 3)) < 1 |
| 45 | 44 | a1i 11 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
(abs‘(1 / 3)) < 1) |
| 46 | 21 | nnnn0d 12587 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑀 + 1) ∈
ℕ0) |
| 47 | 6 | rpnnen2lem1 16250 |
. . . . . . . 8
⊢
(((ℕ ∖ {𝑀}) ⊆ ℕ ∧ 𝑘 ∈ ℕ) → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = if(𝑘 ∈ (ℕ ∖ {𝑀}), ((1 / 3)↑𝑘), 0)) |
| 48 | 5, 47 | mpan 690 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = if(𝑘 ∈ (ℕ ∖ {𝑀}), ((1 / 3)↑𝑘), 0)) |
| 49 | 25, 48 | syl 17 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = if(𝑘 ∈ (ℕ ∖ {𝑀}), ((1 / 3)↑𝑘), 0)) |
| 50 | | nnre 12273 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
| 51 | 50 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℝ) |
| 52 | | eluzle 12891 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑘) |
| 53 | 52 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑀 + 1) ≤ 𝑘) |
| 54 | | nnltp1le 12674 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑀 < 𝑘 ↔ (𝑀 + 1) ≤ 𝑘)) |
| 55 | 25, 54 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑀 < 𝑘 ↔ (𝑀 + 1) ≤ 𝑘)) |
| 56 | 53, 55 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑘) |
| 57 | 51, 56 | gtned 11396 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑘 ≠ 𝑀) |
| 58 | | eldifsn 4786 |
. . . . . . . 8
⊢ (𝑘 ∈ (ℕ ∖ {𝑀}) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≠ 𝑀)) |
| 59 | 25, 57, 58 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑘 ∈ (ℕ ∖ {𝑀})) |
| 60 | 59 | iftrued 4533 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → if(𝑘 ∈ (ℕ ∖ {𝑀}), ((1 / 3)↑𝑘), 0) = ((1 / 3)↑𝑘)) |
| 61 | 49, 60 | eqtrd 2777 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → ((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = ((1 / 3)↑𝑘)) |
| 62 | 32, 45, 46, 61 | geolim2 15907 |
. . . 4
⊢ (𝑀 ∈ ℕ → seq(𝑀 + 1)( + , (𝐹‘(ℕ ∖ {𝑀}))) ⇝ (((1 / 3)↑(𝑀 + 1)) / (1 − (1 /
3)))) |
| 63 | 20, 22, 23, 26, 62 | isumclim 15793 |
. . 3
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈
(ℤ≥‘(𝑀 + 1))((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = (((1 / 3)↑(𝑀 + 1)) / (1 − (1 /
3)))) |
| 64 | 19, 63 | oveq12d 7449 |
. 2
⊢ (𝑀 ∈ ℕ → (((𝐹‘(ℕ ∖ {𝑀}))‘𝑀) + Σ𝑘 ∈ (ℤ≥‘(𝑀 + 1))((𝐹‘(ℕ ∖ {𝑀}))‘𝑘)) = (0 + (((1 / 3)↑(𝑀 + 1)) / (1 − (1 /
3))))) |
| 65 | 14, 64 | eqtrd 2777 |
1
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈
(ℤ≥‘𝑀)((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = (0 + (((1 / 3)↑(𝑀 + 1)) / (1 − (1 /
3))))) |