Proof of Theorem sge0p1
| Step | Hyp | Ref
| Expression |
| 1 | | sge0p1.1 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 2 | | fzsuc 13611 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)})) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑀...(𝑁 + 1)) = ((𝑀...𝑁) ∪ {(𝑁 + 1)})) |
| 4 | 3 | mpteq1d 5237 |
. . 3
⊢ (𝜑 → (𝑘 ∈ (𝑀...(𝑁 + 1)) ↦ 𝐴) = (𝑘 ∈ ((𝑀...𝑁) ∪ {(𝑁 + 1)}) ↦ 𝐴)) |
| 5 | 4 | fveq2d 6910 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝑀...(𝑁 + 1)) ↦ 𝐴)) =
(Σ^‘(𝑘 ∈ ((𝑀...𝑁) ∪ {(𝑁 + 1)}) ↦ 𝐴))) |
| 6 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑘𝜑 |
| 7 | | ovex 7464 |
. . . 4
⊢ (𝑀...𝑁) ∈ V |
| 8 | 7 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑀...𝑁) ∈ V) |
| 9 | | snex 5436 |
. . . 4
⊢ {(𝑁 + 1)} ∈ V |
| 10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → {(𝑁 + 1)} ∈ V) |
| 11 | | fzp1disj 13623 |
. . . 4
⊢ ((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅ |
| 12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝑀...𝑁) ∩ {(𝑁 + 1)}) = ∅) |
| 13 | | 0xr 11308 |
. . . . 5
⊢ 0 ∈
ℝ* |
| 14 | 13 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 0 ∈
ℝ*) |
| 15 | | pnfxr 11315 |
. . . . 5
⊢ +∞
∈ ℝ* |
| 16 | 15 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → +∞ ∈
ℝ*) |
| 17 | | iccssxr 13470 |
. . . . 5
⊢
(0[,]+∞) ⊆ ℝ* |
| 18 | | simpl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝜑) |
| 19 | | fzelp1 13616 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (𝑀...(𝑁 + 1))) |
| 20 | 19 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ (𝑀...(𝑁 + 1))) |
| 21 | | sge0p1.2 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ (0[,]+∞)) |
| 22 | 18, 20, 21 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ (0[,]+∞)) |
| 23 | 17, 22 | sselid 3981 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈
ℝ*) |
| 24 | | iccgelb 13443 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐴 ∈ (0[,]+∞))
→ 0 ≤ 𝐴) |
| 25 | 14, 16, 22, 24 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 0 ≤ 𝐴) |
| 26 | | iccleub 13442 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝐴 ∈ (0[,]+∞))
→ 𝐴 ≤
+∞) |
| 27 | 14, 16, 22, 26 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ≤ +∞) |
| 28 | 14, 16, 23, 25, 27 | eliccxrd 45540 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ (0[,]+∞)) |
| 29 | | simpl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {(𝑁 + 1)}) → 𝜑) |
| 30 | | elsni 4643 |
. . . . . 6
⊢ (𝑘 ∈ {(𝑁 + 1)} → 𝑘 = (𝑁 + 1)) |
| 31 | 30 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {(𝑁 + 1)}) → 𝑘 = (𝑁 + 1)) |
| 32 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = (𝑁 + 1)) → 𝑘 = (𝑁 + 1)) |
| 33 | | peano2uz 12943 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
| 34 | | eluzfz2 13572 |
. . . . . . . 8
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
| 35 | 1, 33, 34 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
| 36 | 35 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = (𝑁 + 1)) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) |
| 37 | 32, 36 | eqeltrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = (𝑁 + 1)) → 𝑘 ∈ (𝑀...(𝑁 + 1))) |
| 38 | 29, 31, 37 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {(𝑁 + 1)}) → 𝑘 ∈ (𝑀...(𝑁 + 1))) |
| 39 | 29, 38, 21 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ {(𝑁 + 1)}) → 𝐴 ∈ (0[,]+∞)) |
| 40 | 6, 8, 10, 12, 28, 39 | sge0splitmpt 46426 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ ((𝑀...𝑁) ∪ {(𝑁 + 1)}) ↦ 𝐴)) =
((Σ^‘(𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)) +𝑒
(Σ^‘(𝑘 ∈ {(𝑁 + 1)} ↦ 𝐴)))) |
| 41 | | ovex 7464 |
. . . . 5
⊢ (𝑁 + 1) ∈ V |
| 42 | 41 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑁 + 1) ∈ V) |
| 43 | | id 22 |
. . . . 5
⊢ (𝜑 → 𝜑) |
| 44 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → (𝑘 ∈ (𝑀...(𝑁 + 1)) ↔ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))) |
| 45 | 44 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑘 = (𝑁 + 1) → ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) ↔ (𝜑 ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))))) |
| 46 | | sge0p1.3 |
. . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵) |
| 47 | 46 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑘 = (𝑁 + 1) → (𝐴 ∈ (0[,]+∞) ↔ 𝐵 ∈
(0[,]+∞))) |
| 48 | 45, 47 | imbi12d 344 |
. . . . . . 7
⊢ (𝑘 = (𝑁 + 1) → (((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → 𝐵 ∈ (0[,]+∞)))) |
| 49 | 48, 21 | vtoclg 3554 |
. . . . . 6
⊢ ((𝑁 + 1) ∈ V → ((𝜑 ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → 𝐵 ∈ (0[,]+∞))) |
| 50 | 41, 49 | ax-mp 5 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → 𝐵 ∈ (0[,]+∞)) |
| 51 | 43, 35, 50 | syl2anc 584 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) |
| 52 | 42, 51, 46 | sge0snmpt 46398 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ {(𝑁 + 1)} ↦ 𝐴)) = 𝐵) |
| 53 | 52 | oveq2d 7447 |
. 2
⊢ (𝜑 →
((Σ^‘(𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)) +𝑒
(Σ^‘(𝑘 ∈ {(𝑁 + 1)} ↦ 𝐴))) =
((Σ^‘(𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)) +𝑒 𝐵)) |
| 54 | 5, 40, 53 | 3eqtrd 2781 |
1
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ (𝑀...(𝑁 + 1)) ↦ 𝐴)) =
((Σ^‘(𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)) +𝑒 𝐵)) |