Proof of Theorem dvfsumge
Step | Hyp | Ref
| Expression |
1 | | dvfsumle.m |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | df-neg 10269 |
. . . . . 6
⊢ -𝐴 = (0 − 𝐴) |
3 | 2 | mpteq2i 4741 |
. . . . 5
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ -𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ (0 − 𝐴)) |
4 | | eqid 2622 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
5 | 4 | subcn 22669 |
. . . . . 6
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
6 | | 0red 10041 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
7 | | eluzel2 11692 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
8 | 1, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
9 | 8 | zred 11482 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) |
10 | | eluzelz 11697 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
11 | 1, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
12 | 11 | zred 11482 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
13 | | iccssre 12255 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀[,]𝑁) ⊆ ℝ) |
14 | 9, 12, 13 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) |
15 | | ax-resscn 9993 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
16 | 14, 15 | syl6ss 3615 |
. . . . . . 7
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℂ) |
17 | 15 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℂ) |
18 | | cncfmptc 22714 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ (𝑀[,]𝑁) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑥 ∈
(𝑀[,]𝑁) ↦ 0) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
19 | 6, 16, 17, 18 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 0) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
20 | | dvfsumle.a |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
21 | | resubcl 10345 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 − 𝐴) ∈ ℝ) |
22 | 4, 5, 19, 20, 15, 21 | cncfmpt2ss 22718 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ (0 − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
23 | 3, 22 | syl5eqel 2705 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ -𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
24 | | negex 10279 |
. . . . 5
⊢ -𝐵 ∈ V |
25 | 24 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → -𝐵 ∈ V) |
26 | | reelprrecn 10028 |
. . . . . 6
⊢ ℝ
∈ {ℝ, ℂ} |
27 | 26 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
28 | | ioossicc 12259 |
. . . . . . . 8
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
29 | 28 | sseli 3599 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁)) |
30 | | cncff 22696 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
31 | 20, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
32 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) |
33 | 32 | fmpt 6381 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐴 ∈ ℝ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
34 | 31, 33 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ) |
35 | 34 | r19.21bi 2932 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ) |
36 | 29, 35 | sylan2 491 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ) |
37 | 36 | recnd 10068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℂ) |
38 | | dvfsumle.v |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) |
39 | | dvfsumle.b |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
40 | 27, 37, 38, 39 | dvmptneg 23729 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ -𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ -𝐵)) |
41 | | dvfsumle.c |
. . . . 5
⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶) |
42 | 41 | negeqd 10275 |
. . . 4
⊢ (𝑥 = 𝑀 → -𝐴 = -𝐶) |
43 | | dvfsumle.d |
. . . . 5
⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷) |
44 | 43 | negeqd 10275 |
. . . 4
⊢ (𝑥 = 𝑁 → -𝐴 = -𝐷) |
45 | | dvfsumle.x |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ) |
46 | 45 | renegcld 10457 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → -𝑋 ∈ ℝ) |
47 | | dvfsumge.l |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝐵 ≤ 𝑋) |
48 | 9 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ) |
49 | 48 | rexrd 10089 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈
ℝ*) |
50 | | elfzole1 12478 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑘) |
51 | 50 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑘) |
52 | | iooss1 12210 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ*
∧ 𝑀 ≤ 𝑘) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) |
53 | 49, 51, 52 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) |
54 | 12 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ) |
55 | 54 | rexrd 10089 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈
ℝ*) |
56 | | fzofzp1 12565 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
57 | 56 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
58 | | elfzle2 12345 |
. . . . . . . . . . . 12
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ≤ 𝑁) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ≤ 𝑁) |
60 | | iooss2 12211 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ*
∧ (𝑘 + 1) ≤ 𝑁) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
61 | 55, 59, 60 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
62 | 53, 61 | sstrd 3613 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
63 | 62 | sselda 3603 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝑥 ∈ (𝑀(,)𝑁)) |
64 | 35 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ) |
65 | 29, 64 | sylan2 491 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ) |
66 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴) |
67 | 65, 66 | fmptd 6385 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ) |
68 | | ioossre 12235 |
. . . . . . . . . . . 12
⊢ (𝑀(,)𝑁) ⊆ ℝ |
69 | | dvfre 23714 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ ∧ (𝑀(,)𝑁) ⊆ ℝ) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) |
70 | 67, 68, 69 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) |
71 | 39 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
72 | 71 | dmeqd 5326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
73 | 38 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) |
74 | 73 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ 𝑉) |
75 | | dmmptg 5632 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐵 ∈ 𝑉 → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) |
77 | 72, 76 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑀(,)𝑁)) |
78 | 71, 77 | feq12d 6033 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ)) |
79 | 70, 78 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ) |
80 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) |
81 | 80 | fmpt 6381 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐵 ∈ ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ) |
82 | 79, 81 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ) |
83 | 82 | r19.21bi 2932 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ ℝ) |
84 | 63, 83 | syldan 487 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝐵 ∈ ℝ) |
85 | 84 | anasss 679 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝐵 ∈ ℝ) |
86 | 45 | adantrr 753 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝑋 ∈ ℝ) |
87 | 85, 86 | lenegd 10606 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → (𝐵 ≤ 𝑋 ↔ -𝑋 ≤ -𝐵)) |
88 | 47, 87 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → -𝑋 ≤ -𝐵) |
89 | 1, 23, 25, 40, 42, 44, 46, 88 | dvfsumle 23784 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)-𝑋 ≤ (-𝐷 − -𝐶)) |
90 | | fzofi 12773 |
. . . . 5
⊢ (𝑀..^𝑁) ∈ Fin |
91 | 90 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin) |
92 | 45 | recnd 10068 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ) |
93 | 91, 92 | fsumneg 14519 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)-𝑋 = -Σ𝑘 ∈ (𝑀..^𝑁)𝑋) |
94 | 9 | rexrd 10089 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
95 | 12 | rexrd 10089 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
96 | | eluzle 11700 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
97 | 1, 96 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
98 | | ubicc2 12289 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → 𝑁 ∈ (𝑀[,]𝑁)) |
99 | 94, 95, 97, 98 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (𝑀[,]𝑁)) |
100 | 43 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝐴 ∈ ℝ ↔ 𝐷 ∈ ℝ)) |
101 | 100 | rspcv 3305 |
. . . . . . 7
⊢ (𝑁 ∈ (𝑀[,]𝑁) → (∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ → 𝐷 ∈ ℝ)) |
102 | 99, 34, 101 | sylc 65 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℝ) |
103 | 102 | recnd 10068 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ℂ) |
104 | | lbicc2 12288 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁)) |
105 | 94, 95, 97, 104 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁)) |
106 | 41 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → (𝐴 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
107 | 106 | rspcv 3305 |
. . . . . . 7
⊢ (𝑀 ∈ (𝑀[,]𝑁) → (∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ → 𝐶 ∈ ℝ)) |
108 | 105, 34, 107 | sylc 65 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
109 | 108 | recnd 10068 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) |
110 | 103, 109 | neg2subd 10409 |
. . . 4
⊢ (𝜑 → (-𝐷 − -𝐶) = (𝐶 − 𝐷)) |
111 | 103, 109 | negsubdi2d 10408 |
. . . 4
⊢ (𝜑 → -(𝐷 − 𝐶) = (𝐶 − 𝐷)) |
112 | 110, 111 | eqtr4d 2659 |
. . 3
⊢ (𝜑 → (-𝐷 − -𝐶) = -(𝐷 − 𝐶)) |
113 | 89, 93, 112 | 3brtr3d 4684 |
. 2
⊢ (𝜑 → -Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ -(𝐷 − 𝐶)) |
114 | 102, 108 | resubcld 10458 |
. . 3
⊢ (𝜑 → (𝐷 − 𝐶) ∈ ℝ) |
115 | 91, 45 | fsumrecl 14465 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ∈ ℝ) |
116 | 114, 115 | lenegd 10606 |
. 2
⊢ (𝜑 → ((𝐷 − 𝐶) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ↔ -Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ -(𝐷 − 𝐶))) |
117 | 113, 116 | mpbird 247 |
1
⊢ (𝜑 → (𝐷 − 𝐶) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑋) |