Step | Hyp | Ref
| Expression |
1 | | seqf1o.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzfz2 10088 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
4 | | fveq2 5546 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (seq𝑀( + , 𝐺)‘𝑚) = (seq𝑀( + , 𝐺)‘𝑀)) |
5 | 4 | oveq2d 5926 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑀))) |
6 | 4 | oveq1d 5925 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾)) = ((seq𝑀( + , 𝐺)‘𝑀) + (𝐺‘𝐾))) |
7 | 5, 6 | eqeq12d 2208 |
. . . 4
⊢ (𝑚 = 𝑀 → (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾)) ↔ ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑀)) = ((seq𝑀( + , 𝐺)‘𝑀) + (𝐺‘𝐾)))) |
8 | 7 | imbi2d 230 |
. . 3
⊢ (𝑚 = 𝑀 → ((𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾))) ↔ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑀)) = ((seq𝑀( + , 𝐺)‘𝑀) + (𝐺‘𝐾))))) |
9 | | fveq2 5546 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (seq𝑀( + , 𝐺)‘𝑚) = (seq𝑀( + , 𝐺)‘𝑛)) |
10 | 9 | oveq2d 5926 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛))) |
11 | 9 | oveq1d 5925 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾))) |
12 | 10, 11 | eqeq12d 2208 |
. . . 4
⊢ (𝑚 = 𝑛 → (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾)) ↔ ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾)))) |
13 | 12 | imbi2d 230 |
. . 3
⊢ (𝑚 = 𝑛 → ((𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾))) ↔ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾))))) |
14 | | fveq2 5546 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → (seq𝑀( + , 𝐺)‘𝑚) = (seq𝑀( + , 𝐺)‘(𝑛 + 1))) |
15 | 14 | oveq2d 5926 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘(𝑛 + 1)))) |
16 | 14 | oveq1d 5925 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾)) = ((seq𝑀( + , 𝐺)‘(𝑛 + 1)) + (𝐺‘𝐾))) |
17 | 15, 16 | eqeq12d 2208 |
. . . 4
⊢ (𝑚 = (𝑛 + 1) → (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾)) ↔ ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘(𝑛 + 1))) = ((seq𝑀( + , 𝐺)‘(𝑛 + 1)) + (𝐺‘𝐾)))) |
18 | 17 | imbi2d 230 |
. . 3
⊢ (𝑚 = (𝑛 + 1) → ((𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾))) ↔ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘(𝑛 + 1))) = ((seq𝑀( + , 𝐺)‘(𝑛 + 1)) + (𝐺‘𝐾))))) |
19 | | fveq2 5546 |
. . . . . 6
⊢ (𝑚 = 𝑁 → (seq𝑀( + , 𝐺)‘𝑚) = (seq𝑀( + , 𝐺)‘𝑁)) |
20 | 19 | oveq2d 5926 |
. . . . 5
⊢ (𝑚 = 𝑁 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑁))) |
21 | 19 | oveq1d 5925 |
. . . . 5
⊢ (𝑚 = 𝑁 → ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘𝐾))) |
22 | 20, 21 | eqeq12d 2208 |
. . . 4
⊢ (𝑚 = 𝑁 → (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾)) ↔ ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑁)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘𝐾)))) |
23 | 22 | imbi2d 230 |
. . 3
⊢ (𝑚 = 𝑁 → ((𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑚)) = ((seq𝑀( + , 𝐺)‘𝑚) + (𝐺‘𝐾))) ↔ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑁)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘𝐾))))) |
24 | | seqf1o.2 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
25 | | seqf1olem2a.1 |
. . . . . 6
⊢ (𝜑 → 𝐺:𝐴⟶𝐶) |
26 | | seqf1olem2a.3 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ 𝐴) |
27 | 25, 26 | ffvelcdmd 5686 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝐾) ∈ 𝐶) |
28 | | eluzel2 9587 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
29 | 1, 28 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
30 | | seqf1oglem2a.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑊) |
31 | 25, 30 | fexd 5780 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ V) |
32 | | seqf1og.p |
. . . . . . 7
⊢ (𝜑 → + ∈ 𝑉) |
33 | | seq1g 10524 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐺 ∈ V ∧ + ∈ 𝑉) → (seq𝑀( + , 𝐺)‘𝑀) = (𝐺‘𝑀)) |
34 | 29, 31, 32, 33 | syl3anc 1249 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( + , 𝐺)‘𝑀) = (𝐺‘𝑀)) |
35 | | seqf1olem2a.4 |
. . . . . . . 8
⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐴) |
36 | | eluzfz1 10087 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
37 | 1, 36 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
38 | 35, 37 | sseldd 3180 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ 𝐴) |
39 | 25, 38 | ffvelcdmd 5686 |
. . . . . 6
⊢ (𝜑 → (𝐺‘𝑀) ∈ 𝐶) |
40 | 34, 39 | eqeltrd 2270 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐺)‘𝑀) ∈ 𝐶) |
41 | 24, 27, 40 | caovcomd 6067 |
. . . 4
⊢ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑀)) = ((seq𝑀( + , 𝐺)‘𝑀) + (𝐺‘𝐾))) |
42 | 41 | a1i 9 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑀)) = ((seq𝑀( + , 𝐺)‘𝑀) + (𝐺‘𝐾)))) |
43 | | oveq1 5917 |
. . . . . 6
⊢ (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾)) → (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛)) + (𝐺‘(𝑛 + 1))) = (((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾)) + (𝐺‘(𝑛 + 1)))) |
44 | | elfzouz 10207 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝑀..^𝑁) → 𝑛 ∈ (ℤ≥‘𝑀)) |
45 | 44 | adantl 277 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
46 | 31 | adantr 276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝐺 ∈ V) |
47 | 32 | adantr 276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → + ∈ 𝑉) |
48 | | seqp1g 10527 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ V ∧ + ∈ 𝑉) → (seq𝑀( + , 𝐺)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
49 | 45, 46, 47, 48 | syl3anc 1249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐺)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1)))) |
50 | 49 | oveq2d 5926 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘(𝑛 + 1))) = ((𝐺‘𝐾) + ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1))))) |
51 | | seqf1o.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
52 | 51 | adantlr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
53 | | seqf1o.5 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ⊆ 𝑆) |
54 | 53, 27 | sseldd 3180 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝐾) ∈ 𝑆) |
55 | 54 | adantr 276 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐺‘𝐾) ∈ 𝑆) |
56 | 53 | adantr 276 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝐶 ⊆ 𝑆) |
57 | 56 | adantr 276 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀...𝑛)) → 𝐶 ⊆ 𝑆) |
58 | 25 | adantr 276 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝐺:𝐴⟶𝐶) |
59 | 58 | adantr 276 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀...𝑛)) → 𝐺:𝐴⟶𝐶) |
60 | | elfzouz2 10218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (𝑀..^𝑁) → 𝑁 ∈ (ℤ≥‘𝑛)) |
61 | 60 | adantl 277 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝑁 ∈ (ℤ≥‘𝑛)) |
62 | | fzss2 10120 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘𝑛) → (𝑀...𝑛) ⊆ (𝑀...𝑁)) |
63 | 61, 62 | syl 14 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝑀...𝑛) ⊆ (𝑀...𝑁)) |
64 | 35 | adantr 276 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝑀...𝑁) ⊆ 𝐴) |
65 | 63, 64 | sstrd 3189 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝑀...𝑛) ⊆ 𝐴) |
66 | 65 | sselda 3179 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀...𝑛)) → 𝑥 ∈ 𝐴) |
67 | 59, 66 | ffvelcdmd 5686 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀...𝑛)) → (𝐺‘𝑥) ∈ 𝐶) |
68 | 57, 67 | sseldd 3180 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀...𝑛)) → (𝐺‘𝑥) ∈ 𝑆) |
69 | | seqf1o.1 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
70 | 69 | adantlr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
71 | 45, 68, 70, 46, 47 | seqclg 10533 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐺)‘𝑛) ∈ 𝑆) |
72 | | fzofzp1 10284 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
73 | 72 | adantl 277 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
74 | 64, 73 | sseldd 3180 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝑛 + 1) ∈ 𝐴) |
75 | 58, 74 | ffvelcdmd 5686 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑛 + 1)) ∈ 𝐶) |
76 | 56, 75 | sseldd 3180 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑛 + 1)) ∈ 𝑆) |
77 | 52, 55, 71, 76 | caovassd 6070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛)) + (𝐺‘(𝑛 + 1))) = ((𝐺‘𝐾) + ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1))))) |
78 | 50, 77 | eqtr4d 2229 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘(𝑛 + 1))) = (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛)) + (𝐺‘(𝑛 + 1)))) |
79 | 52, 71, 76, 55 | caovassd 6070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1))) + (𝐺‘𝐾)) = ((seq𝑀( + , 𝐺)‘𝑛) + ((𝐺‘(𝑛 + 1)) + (𝐺‘𝐾)))) |
80 | 49 | oveq1d 5925 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐺)‘(𝑛 + 1)) + (𝐺‘𝐾)) = (((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1))) + (𝐺‘𝐾))) |
81 | 52, 71, 55, 76 | caovassd 6070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾)) + (𝐺‘(𝑛 + 1))) = ((seq𝑀( + , 𝐺)‘𝑛) + ((𝐺‘𝐾) + (𝐺‘(𝑛 + 1))))) |
82 | 24 | adantlr 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
83 | 27 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐺‘𝐾) ∈ 𝐶) |
84 | 82, 75, 83 | caovcomd 6067 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑛 + 1)) + (𝐺‘𝐾)) = ((𝐺‘𝐾) + (𝐺‘(𝑛 + 1)))) |
85 | 84 | oveq2d 5926 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐺)‘𝑛) + ((𝐺‘(𝑛 + 1)) + (𝐺‘𝐾))) = ((seq𝑀( + , 𝐺)‘𝑛) + ((𝐺‘𝐾) + (𝐺‘(𝑛 + 1))))) |
86 | 81, 85 | eqtr4d 2229 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾)) + (𝐺‘(𝑛 + 1))) = ((seq𝑀( + , 𝐺)‘𝑛) + ((𝐺‘(𝑛 + 1)) + (𝐺‘𝐾)))) |
87 | 79, 80, 86 | 3eqtr4d 2236 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐺)‘(𝑛 + 1)) + (𝐺‘𝐾)) = (((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾)) + (𝐺‘(𝑛 + 1)))) |
88 | 78, 87 | eqeq12d 2208 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘(𝑛 + 1))) = ((seq𝑀( + , 𝐺)‘(𝑛 + 1)) + (𝐺‘𝐾)) ↔ (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛)) + (𝐺‘(𝑛 + 1))) = (((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾)) + (𝐺‘(𝑛 + 1))))) |
89 | 43, 88 | imbitrrid 156 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾)) → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘(𝑛 + 1))) = ((seq𝑀( + , 𝐺)‘(𝑛 + 1)) + (𝐺‘𝐾)))) |
90 | 89 | expcom 116 |
. . . 4
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝜑 → (((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾)) → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘(𝑛 + 1))) = ((seq𝑀( + , 𝐺)‘(𝑛 + 1)) + (𝐺‘𝐾))))) |
91 | 90 | a2d 26 |
. . 3
⊢ (𝑛 ∈ (𝑀..^𝑁) → ((𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑛)) = ((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘𝐾))) → (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘(𝑛 + 1))) = ((seq𝑀( + , 𝐺)‘(𝑛 + 1)) + (𝐺‘𝐾))))) |
92 | 8, 13, 18, 23, 42, 91 | fzind2 10296 |
. 2
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑁)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘𝐾)))) |
93 | 3, 92 | mpcom 36 |
1
⊢ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑁)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘𝐾))) |