Proof of Theorem fsumle
Step | Hyp | Ref
| Expression |
1 | | fsumle.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
2 | | fsumle.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) |
3 | | fsumle.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
4 | 2, 3 | resubcld 10337 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐶 − 𝐵) ∈ ℝ) |
5 | | fsumle.4 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶) |
6 | 2, 3 | subge0d 10496 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (0 ≤ (𝐶 − 𝐵) ↔ 𝐵 ≤ 𝐶)) |
7 | 5, 6 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ (𝐶 − 𝐵)) |
8 | 1, 4, 7 | fsumge0 14368 |
. . 3
⊢ (𝜑 → 0 ≤ Σ𝑘 ∈ 𝐴 (𝐶 − 𝐵)) |
9 | 2 | recnd 9947 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
10 | 3 | recnd 9947 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
11 | 1, 9, 10 | fsumsub 14362 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐶 − 𝐵) = (Σ𝑘 ∈ 𝐴 𝐶 − Σ𝑘 ∈ 𝐴 𝐵)) |
12 | 8, 11 | breqtrd 4609 |
. 2
⊢ (𝜑 → 0 ≤ (Σ𝑘 ∈ 𝐴 𝐶 − Σ𝑘 ∈ 𝐴 𝐵)) |
13 | 1, 2 | fsumrecl 14312 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 ∈ ℝ) |
14 | 1, 3 | fsumrecl 14312 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ) |
15 | 13, 14 | subge0d 10496 |
. 2
⊢ (𝜑 → (0 ≤ (Σ𝑘 ∈ 𝐴 𝐶 − Σ𝑘 ∈ 𝐴 𝐵) ↔ Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐶)) |
16 | 12, 15 | mpbid 221 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝐴 𝐶) |