Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → 𝑁 < 𝑀) |
2 | 1 | iftrued 3564 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)))‘𝑁)) = (0g‘𝐺)) |
3 | | gsummptfidmadd.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
4 | | eqid 2193 |
. . . . 5
⊢
(0g‘𝐺) = (0g‘𝐺) |
5 | | gsummptfidmadd.p |
. . . . 5
⊢ + =
(+g‘𝐺) |
6 | | gsummptfidmadd.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ CMnd) |
7 | | gsumfzmptfidmadd.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
8 | | gsumfzmptfidmadd.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
9 | 6 | cmnmndd 13367 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Mnd) |
10 | 9 | adantr 276 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐺 ∈ Mnd) |
11 | | gsumfzmptfidmadd.c |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐶 ∈ 𝐵) |
12 | | gsumfzmptfidmadd.d |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐷 ∈ 𝐵) |
13 | 3, 5 | mndcl 12994 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 + 𝐷) ∈ 𝐵) |
14 | 10, 11, 12, 13 | syl3anc 1249 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐶 + 𝐷) ∈ 𝐵) |
15 | 14 | fmpttd 5705 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)):(𝑀...𝑁)⟶𝐵) |
16 | 3, 4, 5, 6, 7, 8, 15 | gsumfzval 12964 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)))‘𝑁))) |
17 | 16 | adantr 276 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)))‘𝑁))) |
18 | | gsumfzmptfidmadd.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ (𝑀...𝑁) ↦ 𝐶) |
19 | 11, 18 | fmptd 5704 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵) |
20 | 3, 4, 5, 6, 7, 8, 19 | gsumfzval 12964 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , 𝐹)‘𝑁))) |
21 | 20 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , 𝐹)‘𝑁))) |
22 | 1 | iftrued 3564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , 𝐹)‘𝑁)) = (0g‘𝐺)) |
23 | 21, 22 | eqtrd 2226 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = (0g‘𝐺)) |
24 | | gsumfzmptfidmadd.h |
. . . . . . . . 9
⊢ 𝐻 = (𝑥 ∈ (𝑀...𝑁) ↦ 𝐷) |
25 | 12, 24 | fmptd 5704 |
. . . . . . . 8
⊢ (𝜑 → 𝐻:(𝑀...𝑁)⟶𝐵) |
26 | 3, 4, 5, 6, 7, 8, 25 | gsumfzval 12964 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg 𝐻) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , 𝐻)‘𝑁))) |
27 | 26 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐻) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , 𝐻)‘𝑁))) |
28 | 1 | iftrued 3564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , 𝐻)‘𝑁)) = (0g‘𝐺)) |
29 | 27, 28 | eqtrd 2226 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐻) = (0g‘𝐺)) |
30 | 23, 29 | oveq12d 5928 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((0g‘𝐺) + (0g‘𝐺))) |
31 | 3, 4 | mndidcl 13001 |
. . . . . 6
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) |
32 | 3, 5, 4 | mndlid 13006 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧
(0g‘𝐺)
∈ 𝐵) →
((0g‘𝐺)
+
(0g‘𝐺)) =
(0g‘𝐺)) |
33 | 9, 31, 32 | syl2anc2 412 |
. . . . 5
⊢ (𝜑 →
((0g‘𝐺)
+
(0g‘𝐺)) =
(0g‘𝐺)) |
34 | 33 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → ((0g‘𝐺) + (0g‘𝐺)) = (0g‘𝐺)) |
35 | 30, 34 | eqtrd 2226 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = (0g‘𝐺)) |
36 | 2, 17, 35 | 3eqtr4d 2236 |
. 2
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |
37 | 9 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝐺 ∈ Mnd) |
38 | | simprl 529 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑝 ∈ 𝐵) |
39 | | simprr 531 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝑞 ∈ 𝐵) |
40 | 3, 5 | mndcl 12994 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝑝 + 𝑞) ∈ 𝐵) |
41 | 37, 38, 39, 40 | syl3anc 1249 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (𝑝 + 𝑞) ∈ 𝐵) |
42 | 6 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → 𝐺 ∈ CMnd) |
43 | 3, 5 | cmncom 13361 |
. . . . 5
⊢ ((𝐺 ∈ CMnd ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝑝 + 𝑞) = (𝑞 + 𝑝)) |
44 | 42, 38, 39, 43 | syl3anc 1249 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (𝑝 + 𝑞) = (𝑞 + 𝑝)) |
45 | 9 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → 𝐺 ∈ Mnd) |
46 | 3, 5 | mndass 12995 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑝 + 𝑞) + 𝑟) = (𝑝 + (𝑞 + 𝑟))) |
47 | 45, 46 | sylancom 420 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵)) → ((𝑝 + 𝑞) + 𝑟) = (𝑝 + (𝑞 + 𝑟))) |
48 | 7 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ∈ ℤ) |
49 | 8 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ ℤ) |
50 | 48 | zred 9429 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ∈ ℝ) |
51 | 49 | zred 9429 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ ℝ) |
52 | | simpr 110 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → ¬ 𝑁 < 𝑀) |
53 | 50, 51, 52 | nltled 8130 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ≤ 𝑁) |
54 | | eluz2 9588 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
55 | 48, 49, 53, 54 | syl3anbrc 1183 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ (ℤ≥‘𝑀)) |
56 | 19 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐹:(𝑀...𝑁)⟶𝐵) |
57 | 56 | ffvelcdmda 5685 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝐵) |
58 | 25 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐻:(𝑀...𝑁)⟶𝐵) |
59 | 58 | ffvelcdmda 5685 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) ∈ 𝐵) |
60 | 7, 8 | fzfigd 10492 |
. . . . . . . 8
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
61 | 18 | a1i 9 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝑀...𝑁) ↦ 𝐶)) |
62 | 24 | a1i 9 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = (𝑥 ∈ (𝑀...𝑁) ↦ 𝐷)) |
63 | 60, 11, 12, 61, 62 | offval2 6138 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐻) = (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))) |
64 | 63 | fveq1d 5548 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐻)‘𝑘) = ((𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))‘𝑘)) |
65 | 64 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝐹 ∘𝑓 + 𝐻)‘𝑘) = ((𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))‘𝑘)) |
66 | 19 | ffnd 5396 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn (𝑀...𝑁)) |
67 | 25 | ffnd 5396 |
. . . . . . 7
⊢ (𝜑 → 𝐻 Fn (𝑀...𝑁)) |
68 | | inidm 3368 |
. . . . . . 7
⊢ ((𝑀...𝑁) ∩ (𝑀...𝑁)) = (𝑀...𝑁) |
69 | | eqidd 2194 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
70 | | eqidd 2194 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = (𝐻‘𝑘)) |
71 | 9 | adantr 276 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐺 ∈ Mnd) |
72 | 19 | ffvelcdmda 5685 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝐵) |
73 | 25 | ffvelcdmda 5685 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) ∈ 𝐵) |
74 | 3, 5 | mndcl 12994 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ (𝐹‘𝑘) ∈ 𝐵 ∧ (𝐻‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘) + (𝐻‘𝑘)) ∈ 𝐵) |
75 | 71, 72, 73, 74 | syl3anc 1249 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝐹‘𝑘) + (𝐻‘𝑘)) ∈ 𝐵) |
76 | 66, 67, 60, 60, 68, 69, 70, 75 | ofvalg 6132 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝐹 ∘𝑓 + 𝐻)‘𝑘) = ((𝐹‘𝑘) + (𝐻‘𝑘))) |
77 | 76 | adantlr 477 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝐹 ∘𝑓 + 𝐻)‘𝑘) = ((𝐹‘𝑘) + (𝐻‘𝑘))) |
78 | 65, 77 | eqtr3d 2228 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))‘𝑘) = ((𝐹‘𝑘) + (𝐻‘𝑘))) |
79 | | plusgslid 12720 |
. . . . . . . 8
⊢
(+g = Slot (+g‘ndx) ∧
(+g‘ndx) ∈ ℕ) |
80 | 79 | slotex 12635 |
. . . . . . 7
⊢ (𝐺 ∈ CMnd →
(+g‘𝐺)
∈ V) |
81 | 6, 80 | syl 14 |
. . . . . 6
⊢ (𝜑 → (+g‘𝐺) ∈ V) |
82 | 5, 81 | eqeltrid 2280 |
. . . . 5
⊢ (𝜑 → + ∈ V) |
83 | 82 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → + ∈ V) |
84 | 19, 60 | fexd 5780 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ V) |
85 | 84 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐹 ∈ V) |
86 | 25, 60 | fexd 5780 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ V) |
87 | 86 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐻 ∈ V) |
88 | 15, 60 | fexd 5780 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)) ∈ V) |
89 | 88 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)) ∈ V) |
90 | 41, 44, 47, 55, 57, 59, 78, 83, 85, 87, 89 | seqcaoprg 10557 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (seq𝑀( + , (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)))‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐻)‘𝑁))) |
91 | 16 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)))‘𝑁))) |
92 | 52 | iffalsed 3567 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)))‘𝑁)) = (seq𝑀( + , (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)))‘𝑁)) |
93 | 91, 92 | eqtrd 2226 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))) = (seq𝑀( + , (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷)))‘𝑁)) |
94 | 20 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , 𝐹)‘𝑁))) |
95 | 52 | iffalsed 3567 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀( + , 𝐹)‘𝑁)) |
96 | 94, 95 | eqtrd 2226 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁)) |
97 | 26 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐻) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , 𝐻)‘𝑁))) |
98 | 52 | iffalsed 3567 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀( + , 𝐻)‘𝑁)) = (seq𝑀( + , 𝐻)‘𝑁)) |
99 | 97, 98 | eqtrd 2226 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐻) = (seq𝑀( + , 𝐻)‘𝑁)) |
100 | 96, 99 | oveq12d 5928 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐻)‘𝑁))) |
101 | 90, 93, 100 | 3eqtr4d 2236 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |
102 | | zdclt 9384 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
DECID 𝑁 <
𝑀) |
103 | 8, 7, 102 | syl2anc 411 |
. . 3
⊢ (𝜑 → DECID 𝑁 < 𝑀) |
104 | | exmiddc 837 |
. . 3
⊢
(DECID 𝑁 < 𝑀 → (𝑁 < 𝑀 ∨ ¬ 𝑁 < 𝑀)) |
105 | 103, 104 | syl 14 |
. 2
⊢ (𝜑 → (𝑁 < 𝑀 ∨ ¬ 𝑁 < 𝑀)) |
106 | 36, 101, 105 | mpjaodan 799 |
1
⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) |