Proof of Theorem dvfsumge
Step | Hyp | Ref
| Expression |
1 | | dvfsumle.m |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | df-neg 10609 |
. . . . . 6
⊢ -𝐴 = (0 − 𝐴) |
3 | 2 | mpteq2i 4976 |
. . . . 5
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ -𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ (0 − 𝐴)) |
4 | | eqid 2778 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
5 | 4 | subcn 23077 |
. . . . . 6
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
6 | | 0red 10380 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
7 | | eluzel2 11997 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
8 | 1, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
9 | 8 | zred 11834 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) |
10 | | eluzelz 12002 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
11 | 1, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
12 | 11 | zred 11834 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
13 | | iccssre 12567 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀[,]𝑁) ⊆ ℝ) |
14 | 9, 12, 13 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) |
15 | | ax-resscn 10329 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
16 | 14, 15 | syl6ss 3833 |
. . . . . . 7
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℂ) |
17 | 15 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℂ) |
18 | | cncfmptc 23122 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ (𝑀[,]𝑁) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑥 ∈
(𝑀[,]𝑁) ↦ 0) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
19 | 6, 16, 17, 18 | syl3anc 1439 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 0) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
20 | | dvfsumle.a |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
21 | | resubcl 10687 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 − 𝐴) ∈ ℝ) |
22 | 4, 5, 19, 20, 15, 21 | cncfmpt2ss 23126 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ (0 − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
23 | 3, 22 | syl5eqel 2863 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ -𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) |
24 | | negex 10620 |
. . . . 5
⊢ -𝐵 ∈ V |
25 | 24 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → -𝐵 ∈ V) |
26 | | reelprrecn 10364 |
. . . . . 6
⊢ ℝ
∈ {ℝ, ℂ} |
27 | 26 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
28 | | ioossicc 12571 |
. . . . . . . 8
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) |
29 | 28 | sseli 3817 |
. . . . . . 7
⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁)) |
30 | | cncff 23104 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
31 | 20, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
32 | | eqid 2778 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) |
33 | 32 | fmpt 6644 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐴 ∈ ℝ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) |
34 | 31, 33 | sylibr 226 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ) |
35 | 34 | r19.21bi 3114 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ) |
36 | 29, 35 | sylan2 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ) |
37 | 36 | recnd 10405 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℂ) |
38 | | dvfsumle.v |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) |
39 | | dvfsumle.b |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
40 | 27, 37, 38, 39 | dvmptneg 24166 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ -𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ -𝐵)) |
41 | | dvfsumle.c |
. . . . 5
⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶) |
42 | 41 | negeqd 10616 |
. . . 4
⊢ (𝑥 = 𝑀 → -𝐴 = -𝐶) |
43 | | dvfsumle.d |
. . . . 5
⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷) |
44 | 43 | negeqd 10616 |
. . . 4
⊢ (𝑥 = 𝑁 → -𝐴 = -𝐷) |
45 | | dvfsumle.x |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ) |
46 | 45 | renegcld 10802 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → -𝑋 ∈ ℝ) |
47 | | dvfsumge.l |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝐵 ≤ 𝑋) |
48 | 9 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ) |
49 | 48 | rexrd 10426 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈
ℝ*) |
50 | | elfzole1 12797 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑘) |
51 | 50 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑘) |
52 | | iooss1 12522 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ*
∧ 𝑀 ≤ 𝑘) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) |
53 | 49, 51, 52 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) |
54 | 12 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ) |
55 | 54 | rexrd 10426 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈
ℝ*) |
56 | | fzofzp1 12884 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
57 | 56 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
58 | | elfzle2 12662 |
. . . . . . . . . . . 12
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ≤ 𝑁) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ≤ 𝑁) |
60 | | iooss2 12523 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ*
∧ (𝑘 + 1) ≤ 𝑁) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
61 | 55, 59, 60 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
62 | 53, 61 | sstrd 3831 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) |
63 | 62 | sselda 3821 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝑥 ∈ (𝑀(,)𝑁)) |
64 | 35 | adantlr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ) |
65 | 29, 64 | sylan2 586 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ) |
66 | 65 | fmpttd 6649 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ) |
67 | | ioossre 12547 |
. . . . . . . . . . . 12
⊢ (𝑀(,)𝑁) ⊆ ℝ |
68 | | dvfre 24151 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ ∧ (𝑀(,)𝑁) ⊆ ℝ) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) |
69 | 66, 67, 68 | sylancl 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) |
70 | 39 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
71 | 70 | dmeqd 5571 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) |
72 | 38 | adantlr 705 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) |
73 | 72 | ralrimiva 3148 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ 𝑉) |
74 | | dmmptg 5886 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐵 ∈ 𝑉 → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) |
76 | 71, 75 | eqtrd 2814 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑀(,)𝑁)) |
77 | 70, 76 | feq12d 6279 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ)) |
78 | 69, 77 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ) |
79 | | eqid 2778 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) |
80 | 79 | fmpt 6644 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐵 ∈ ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ) |
81 | 78, 80 | sylibr 226 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ) |
82 | 81 | r19.21bi 3114 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ ℝ) |
83 | 63, 82 | syldan 585 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝐵 ∈ ℝ) |
84 | 83 | anasss 460 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝐵 ∈ ℝ) |
85 | 45 | adantrr 707 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝑋 ∈ ℝ) |
86 | 84, 85 | lenegd 10954 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → (𝐵 ≤ 𝑋 ↔ -𝑋 ≤ -𝐵)) |
87 | 47, 86 | mpbid 224 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → -𝑋 ≤ -𝐵) |
88 | 1, 23, 25, 40, 42, 44, 46, 87 | dvfsumle 24221 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)-𝑋 ≤ (-𝐷 − -𝐶)) |
89 | | fzofi 13092 |
. . . . 5
⊢ (𝑀..^𝑁) ∈ Fin |
90 | 89 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin) |
91 | 45 | recnd 10405 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ) |
92 | 90, 91 | fsumneg 14923 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)-𝑋 = -Σ𝑘 ∈ (𝑀..^𝑁)𝑋) |
93 | 43 | eleq1d 2844 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐴 ∈ ℝ ↔ 𝐷 ∈ ℝ)) |
94 | 9 | rexrd 10426 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℝ*) |
95 | 12 | rexrd 10426 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
96 | | eluzle 12005 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
97 | 1, 96 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
98 | | ubicc2 12603 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → 𝑁 ∈ (𝑀[,]𝑁)) |
99 | 94, 95, 97, 98 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (𝑀[,]𝑁)) |
100 | 93, 34, 99 | rspcdva 3517 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℝ) |
101 | 100 | recnd 10405 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ℂ) |
102 | 41 | eleq1d 2844 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (𝐴 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
103 | | lbicc2 12602 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁)) |
104 | 94, 95, 97, 103 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁)) |
105 | 102, 34, 104 | rspcdva 3517 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
106 | 105 | recnd 10405 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) |
107 | 101, 106 | neg2subd 10751 |
. . . 4
⊢ (𝜑 → (-𝐷 − -𝐶) = (𝐶 − 𝐷)) |
108 | 101, 106 | negsubdi2d 10750 |
. . . 4
⊢ (𝜑 → -(𝐷 − 𝐶) = (𝐶 − 𝐷)) |
109 | 107, 108 | eqtr4d 2817 |
. . 3
⊢ (𝜑 → (-𝐷 − -𝐶) = -(𝐷 − 𝐶)) |
110 | 88, 92, 109 | 3brtr3d 4917 |
. 2
⊢ (𝜑 → -Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ -(𝐷 − 𝐶)) |
111 | 100, 105 | resubcld 10803 |
. . 3
⊢ (𝜑 → (𝐷 − 𝐶) ∈ ℝ) |
112 | 90, 45 | fsumrecl 14872 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ∈ ℝ) |
113 | 111, 112 | lenegd 10954 |
. 2
⊢ (𝜑 → ((𝐷 − 𝐶) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ↔ -Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ -(𝐷 − 𝐶))) |
114 | 110, 113 | mpbird 249 |
1
⊢ (𝜑 → (𝐷 − 𝐶) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑋) |