ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  seqf1oglem2 GIF version

Theorem seqf1oglem2 10581
Description: Lemma for seqf1og 10582. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.)
Hypotheses
Ref Expression
seqf1o.1 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
seqf1o.2 ((𝜑 ∧ (𝑥𝐶𝑦𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
seqf1o.3 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
seqf1o.4 (𝜑𝑁 ∈ (ℤ𝑀))
seqf1o.5 (𝜑𝐶𝑆)
seqf1og.p (𝜑+𝑉)
seqf1olem.5 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
seqf1olem.6 (𝜑𝐺:(𝑀...(𝑁 + 1))⟶𝐶)
seqf1olem.7 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
seqf1olem.8 𝐾 = (𝐹‘(𝑁 + 1))
seqf1olem.9 (𝜑 → ∀𝑔𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)))
Assertion
Ref Expression
seqf1oglem2 (𝜑 → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = (seq𝑀( + , 𝐺)‘(𝑁 + 1)))
Distinct variable groups:   𝑓,𝑔,𝑘,𝑥,𝑦,𝑧,𝐹   𝑓,𝐺,𝑔,𝑘,𝑥,𝑦,𝑧   𝑓,𝑀,𝑔,𝑘,𝑥,𝑦,𝑧   + ,𝑓,𝑔,𝑘,𝑥,𝑦,𝑧   𝑓,𝐽,𝑔,𝑥,𝑦,𝑧   𝑓,𝑁,𝑔,𝑘,𝑥,𝑦,𝑧   𝑘,𝐾,𝑥,𝑦,𝑧   𝜑,𝑓,𝑔,𝑘,𝑥,𝑦,𝑧   𝑆,𝑘,𝑥,𝑦,𝑧   𝐶,𝑓,𝑔,𝑘,𝑥,𝑦,𝑧
Allowed substitution hints:   𝑆(𝑓,𝑔)   𝐽(𝑘)   𝐾(𝑓,𝑔)   𝑉(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘)

Proof of Theorem seqf1oglem2
StepHypRef Expression
1 seqf1olem.6 . . . . . . . . . 10 (𝜑𝐺:(𝑀...(𝑁 + 1))⟶𝐶)
21ffnd 5396 . . . . . . . . 9 (𝜑𝐺 Fn (𝑀...(𝑁 + 1)))
3 fzssp1 10123 . . . . . . . . 9 (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
4 fnssres 5359 . . . . . . . . 9 ((𝐺 Fn (𝑀...(𝑁 + 1)) ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁))
52, 3, 4sylancl 413 . . . . . . . 8 (𝜑 → (𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁))
6 seqf1o.4 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ𝑀))
7 eluzel2 9587 . . . . . . . . . 10 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
86, 7syl 14 . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
9 eluzelz 9591 . . . . . . . . . 10 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
106, 9syl 14 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
118, 10fzfigd 10492 . . . . . . . 8 (𝜑 → (𝑀...𝑁) ∈ Fin)
12 fnfi 6985 . . . . . . . 8 (((𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin) → (𝐺 ↾ (𝑀...𝑁)) ∈ Fin)
135, 11, 12syl2anc 411 . . . . . . 7 (𝜑 → (𝐺 ↾ (𝑀...𝑁)) ∈ Fin)
1413elexd 2773 . . . . . 6 (𝜑 → (𝐺 ↾ (𝑀...𝑁)) ∈ V)
15 seqf1o.1 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
16 seqf1o.2 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐶𝑦𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
17 seqf1o.3 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
18 seqf1o.5 . . . . . . . . 9 (𝜑𝐶𝑆)
19 seqf1og.p . . . . . . . . 9 (𝜑+𝑉)
20 seqf1olem.5 . . . . . . . . 9 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
21 seqf1olem.7 . . . . . . . . 9 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
22 seqf1olem.8 . . . . . . . . 9 𝐾 = (𝐹‘(𝑁 + 1))
2315, 16, 17, 6, 18, 19, 20, 1, 21, 22seqf1oglem1 10580 . . . . . . . 8 (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
24 f1of 5492 . . . . . . . 8 (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → 𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
2523, 24syl 14 . . . . . . 7 (𝜑𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
2625, 11fexd 5780 . . . . . 6 (𝜑𝐽 ∈ V)
2714, 26jca 306 . . . . 5 (𝜑 → ((𝐺 ↾ (𝑀...𝑁)) ∈ V ∧ 𝐽 ∈ V))
28 seqf1olem.9 . . . . 5 (𝜑 → ∀𝑔𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)))
29 fssres 5421 . . . . . . 7 ((𝐺:(𝑀...(𝑁 + 1))⟶𝐶 ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶)
301, 3, 29sylancl 413 . . . . . 6 (𝜑 → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶)
3123, 30jca 306 . . . . 5 (𝜑 → (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶))
32 f1oeq1 5480 . . . . . . . 8 (𝑓 = 𝐽 → (𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ↔ 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)))
33 feq1 5378 . . . . . . . 8 (𝑔 = (𝐺 ↾ (𝑀...𝑁)) → (𝑔:(𝑀...𝑁)⟶𝐶 ↔ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶))
3432, 33bi2anan9r 607 . . . . . . 7 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → ((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) ↔ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶)))
35 coeq1 4813 . . . . . . . . . . 11 (𝑔 = (𝐺 ↾ (𝑀...𝑁)) → (𝑔𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝑓))
36 coeq2 4814 . . . . . . . . . . 11 (𝑓 = 𝐽 → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))
3735, 36sylan9eq 2246 . . . . . . . . . 10 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (𝑔𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))
3837seqeq3d 10516 . . . . . . . . 9 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → seq𝑀( + , (𝑔𝑓)) = seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)))
3938fveq1d 5548 . . . . . . . 8 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))
40 simpl 109 . . . . . . . . . 10 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → 𝑔 = (𝐺 ↾ (𝑀...𝑁)))
4140seqeq3d 10516 . . . . . . . . 9 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → seq𝑀( + , 𝑔) = seq𝑀( + , (𝐺 ↾ (𝑀...𝑁))))
4241fveq1d 5548 . . . . . . . 8 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (seq𝑀( + , 𝑔)‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁))
4339, 42eqeq12d 2208 . . . . . . 7 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → ((seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁) ↔ (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁)))
4434, 43imbi12d 234 . . . . . 6 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)) ↔ ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁))))
4544spc2gv 2851 . . . . 5 (((𝐺 ↾ (𝑀...𝑁)) ∈ V ∧ 𝐽 ∈ V) → (∀𝑔𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)) → ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁))))
4627, 28, 31, 45syl3c 63 . . . 4 (𝜑 → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁))
47 fvres 5570 . . . . . 6 (𝑥 ∈ (𝑀...𝑁) → ((𝐺 ↾ (𝑀...𝑁))‘𝑥) = (𝐺𝑥))
4847adantl 277 . . . . 5 ((𝜑𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘𝑥) = (𝐺𝑥))
4910peano2zd 9432 . . . . . . . 8 (𝜑 → (𝑁 + 1) ∈ ℤ)
508, 49fzfigd 10492 . . . . . . 7 (𝜑 → (𝑀...(𝑁 + 1)) ∈ Fin)
511, 50fexd 5780 . . . . . 6 (𝜑𝐺 ∈ V)
52 resexg 4976 . . . . . 6 (𝐺 ∈ V → (𝐺 ↾ (𝑀...𝑁)) ∈ V)
5351, 52syl 14 . . . . 5 (𝜑 → (𝐺 ↾ (𝑀...𝑁)) ∈ V)
546, 48, 19, 53, 51seqfveqg 10539 . . . 4 (𝜑 → (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁))
5546, 54eqtrd 2226 . . 3 (𝜑 → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁))
5655oveq1d 5925 . 2 (𝜑 → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1))))
5715adantlr 477 . . . . 5 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
5817adantlr 477 . . . . 5 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
59 elfzuz3 10078 . . . . . . 7 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
6059adantl 277 . . . . . 6 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ𝐾))
61 eluzp1p1 9608 . . . . . 6 (𝑁 ∈ (ℤ𝐾) → (𝑁 + 1) ∈ (ℤ‘(𝐾 + 1)))
6260, 61syl 14 . . . . 5 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ (ℤ‘(𝐾 + 1)))
6319adantr 276 . . . . 5 ((𝜑𝐾 ∈ (𝑀...𝑁)) → +𝑉)
6451adantr 276 . . . . . 6 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝐺 ∈ V)
65 f1of 5492 . . . . . . . . 9 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
6620, 65syl 14 . . . . . . . 8 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
6766, 50fexd 5780 . . . . . . 7 (𝜑𝐹 ∈ V)
6867adantr 276 . . . . . 6 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝐹 ∈ V)
69 coexg 5202 . . . . . 6 ((𝐺 ∈ V ∧ 𝐹 ∈ V) → (𝐺𝐹) ∈ V)
7064, 68, 69syl2anc 411 . . . . 5 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝐺𝐹) ∈ V)
71 elfzuz 10077 . . . . . 6 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
7271adantl 277 . . . . 5 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝐾 ∈ (ℤ𝑀))
73 fco 5411 . . . . . . . . 9 ((𝐺:(𝑀...(𝑁 + 1))⟶𝐶𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) → (𝐺𝐹):(𝑀...(𝑁 + 1))⟶𝐶)
741, 66, 73syl2anc 411 . . . . . . . 8 (𝜑 → (𝐺𝐹):(𝑀...(𝑁 + 1))⟶𝐶)
7574, 18fssd 5408 . . . . . . 7 (𝜑 → (𝐺𝐹):(𝑀...(𝑁 + 1))⟶𝑆)
7675ffvelcdmda 5685 . . . . . 6 ((𝜑𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘𝑥) ∈ 𝑆)
7776adantlr 477 . . . . 5 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘𝑥) ∈ 𝑆)
7857, 58, 62, 63, 70, 72, 77seqsplitg 10550 . . . 4 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))))
79 elfzp12 10155 . . . . . . 7 (𝑁 ∈ (ℤ𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀𝐾 ∈ ((𝑀 + 1)...𝑁))))
8079biimpa 296 . . . . . 6 ((𝑁 ∈ (ℤ𝑀) ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐾 = 𝑀𝐾 ∈ ((𝑀 + 1)...𝑁)))
816, 80sylan 283 . . . . 5 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝐾 = 𝑀𝐾 ∈ ((𝑀 + 1)...𝑁)))
82 seqeq1 10511 . . . . . . . . . . 11 (𝐾 = 𝑀 → seq𝐾( + , (𝐺𝐹)) = seq𝑀( + , (𝐺𝐹)))
8382eqcomd 2199 . . . . . . . . . 10 (𝐾 = 𝑀 → seq𝑀( + , (𝐺𝐹)) = seq𝐾( + , (𝐺𝐹)))
8483fveq1d 5548 . . . . . . . . 9 (𝐾 = 𝑀 → (seq𝑀( + , (𝐺𝐹))‘𝐾) = (seq𝐾( + , (𝐺𝐹))‘𝐾))
85 f1ocnv 5505 . . . . . . . . . . . . . 14 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
86 f1of 5492 . . . . . . . . . . . . . 14 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
8720, 85, 863syl 17 . . . . . . . . . . . . 13 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
88 peano2uz 9638 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
89 eluzfz2 10088 . . . . . . . . . . . . . 14 ((𝑁 + 1) ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
906, 88, 893syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
9187, 90ffvelcdmd 5686 . . . . . . . . . . . 12 (𝜑 → (𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1)))
9222, 91eqeltrid 2280 . . . . . . . . . . 11 (𝜑𝐾 ∈ (𝑀...(𝑁 + 1)))
9392elfzelzd 10082 . . . . . . . . . 10 (𝜑𝐾 ∈ ℤ)
9451, 67, 69syl2anc 411 . . . . . . . . . 10 (𝜑 → (𝐺𝐹) ∈ V)
95 seq1g 10524 . . . . . . . . . 10 ((𝐾 ∈ ℤ ∧ (𝐺𝐹) ∈ V ∧ +𝑉) → (seq𝐾( + , (𝐺𝐹))‘𝐾) = ((𝐺𝐹)‘𝐾))
9693, 94, 19, 95syl3anc 1249 . . . . . . . . 9 (𝜑 → (seq𝐾( + , (𝐺𝐹))‘𝐾) = ((𝐺𝐹)‘𝐾))
9784, 96sylan9eqr 2248 . . . . . . . 8 ((𝜑𝐾 = 𝑀) → (seq𝑀( + , (𝐺𝐹))‘𝐾) = ((𝐺𝐹)‘𝐾))
9897oveq1d 5925 . . . . . . 7 ((𝜑𝐾 = 𝑀) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))))
99 simpr 110 . . . . . . . . 9 ((𝜑𝐾 = 𝑀) → 𝐾 = 𝑀)
100 eluzfz1 10087 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
1016, 100syl 14 . . . . . . . . . 10 (𝜑𝑀 ∈ (𝑀...𝑁))
102101adantr 276 . . . . . . . . 9 ((𝜑𝐾 = 𝑀) → 𝑀 ∈ (𝑀...𝑁))
10399, 102eqeltrd 2270 . . . . . . . 8 ((𝜑𝐾 = 𝑀) → 𝐾 ∈ (𝑀...𝑁))
10416adantlr 477 . . . . . . . . . 10 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥𝐶𝑦𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
10518adantr 276 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝐶𝑆)
10674adantr 276 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝐺𝐹):(𝑀...(𝑁 + 1))⟶𝐶)
10792adantr 276 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝐾 ∈ (𝑀...(𝑁 + 1)))
108 peano2uz 9638 . . . . . . . . . . 11 (𝐾 ∈ (ℤ𝑀) → (𝐾 + 1) ∈ (ℤ𝑀))
109 fzss1 10119 . . . . . . . . . . 11 ((𝐾 + 1) ∈ (ℤ𝑀) → ((𝐾 + 1)...(𝑁 + 1)) ⊆ (𝑀...(𝑁 + 1)))
11072, 108, 1093syl 17 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → ((𝐾 + 1)...(𝑁 + 1)) ⊆ (𝑀...(𝑁 + 1)))
11150adantr 276 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝑀...(𝑁 + 1)) ∈ Fin)
11257, 104, 58, 62, 105, 63, 106, 107, 110, 111seqf1oglem2a 10579 . . . . . . . . 9 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) + ((𝐺𝐹)‘𝐾)))
113 1zzd 9334 . . . . . . . . . . 11 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 1 ∈ ℤ)
114 elfzuz 10077 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ (ℤ𝑀))
115 fzss1 10119 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ (ℤ𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁))
11692, 114, 1153syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾...𝑁) ⊆ (𝑀...𝑁))
117116sselda 3179 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ (𝑀...𝑁))
11825ffvelcdmda 5685 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐽𝑥) ∈ (𝑀...𝑁))
119117, 118syldan 282 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐽𝑥) ∈ (𝑀...𝑁))
120119fvresd 5571 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐾...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)) = (𝐺‘(𝐽𝑥)))
121 breq1 4032 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑥 → (𝑘 < 𝐾𝑥 < 𝐾))
122 id 19 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑥𝑘 = 𝑥)
123 oveq1 5917 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑥 → (𝑘 + 1) = (𝑥 + 1))
124121, 122, 123ifbieq12d 3583 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑥 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))
125124fveq2d 5550 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))))
12666adantr 276 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
1273, 117sselid 3177 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
128 fzp1elp1 10131 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → (𝑥 + 1) ∈ (𝑀...(𝑁 + 1)))
129117, 128syl 14 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝑥 + 1) ∈ (𝑀...(𝑁 + 1)))
130117elfzelzd 10082 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ ℤ)
13193adantr 276 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝐾 ∈ ℤ)
132 zdclt 9384 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID 𝑥 < 𝐾)
133130, 131, 132syl2anc 411 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝐾...𝑁)) → DECID 𝑥 < 𝐾)
134127, 129, 133ifcldcd 3593 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐾...𝑁)) → if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)) ∈ (𝑀...(𝑁 + 1)))
135126, 134ffvelcdmd 5686 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) ∈ (𝑀...(𝑁 + 1)))
13621, 125, 117, 135fvmptd3 5643 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐽𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))))
13793zred 9429 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ ℝ)
138137adantr 276 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝐾 ∈ ℝ)
139 elfzelz 10081 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐾...𝑁) → 𝑥 ∈ ℤ)
140139adantl 277 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ ℤ)
141140zred 9429 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ ℝ)
142 elfzle1 10083 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐾...𝑁) → 𝐾𝑥)
143142adantl 277 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝐾𝑥)
144138, 141, 143lensymd 8131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐾...𝑁)) → ¬ 𝑥 < 𝐾)
145 iffalse 3565 . . . . . . . . . . . . . . . . . 18 𝑥 < 𝐾 → if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)) = (𝑥 + 1))
146145fveq2d 5550 . . . . . . . . . . . . . . . . 17 𝑥 < 𝐾 → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘(𝑥 + 1)))
147144, 146syl 14 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘(𝑥 + 1)))
148136, 147eqtrd 2226 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐽𝑥) = (𝐹‘(𝑥 + 1)))
149148fveq2d 5550 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐺‘(𝐽𝑥)) = (𝐺‘(𝐹‘(𝑥 + 1))))
150120, 149eqtrd 2226 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐾...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)) = (𝐺‘(𝐹‘(𝑥 + 1))))
151 fvco3 5620 . . . . . . . . . . . . . . 15 ((𝐽:(𝑀...𝑁)⟶(𝑀...𝑁) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
15225, 151sylan 283 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
153117, 152syldan 282 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
154 fvco3 5620 . . . . . . . . . . . . . . 15 ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1))))
15566, 154sylan 283 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1))))
156129, 155syldan 282 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐾...𝑁)) → ((𝐺𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1))))
157150, 153, 1563eqtr4d 2236 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺𝐹)‘(𝑥 + 1)))
158157adantlr 477 . . . . . . . . . . 11 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺𝐹)‘(𝑥 + 1)))
15964, 52syl 14 . . . . . . . . . . . 12 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝐺 ↾ (𝑀...𝑁)) ∈ V)
16026adantr 276 . . . . . . . . . . . 12 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝐽 ∈ V)
161 coexg 5202 . . . . . . . . . . . 12 (((𝐺 ↾ (𝑀...𝑁)) ∈ V ∧ 𝐽 ∈ V) → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽) ∈ V)
162159, 160, 161syl2anc 411 . . . . . . . . . . 11 ((𝜑𝐾 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽) ∈ V)
16360, 113, 158, 63, 162, 70seqshft2g 10543 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)))
164 fvco3 5620 . . . . . . . . . . . . 13 ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ 𝐾 ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘𝐾) = (𝐺‘(𝐹𝐾)))
16566, 92, 164syl2anc 411 . . . . . . . . . . . 12 (𝜑 → ((𝐺𝐹)‘𝐾) = (𝐺‘(𝐹𝐾)))
16622fveq2i 5549 . . . . . . . . . . . . . 14 (𝐹𝐾) = (𝐹‘(𝐹‘(𝑁 + 1)))
167 f1ocnvfv2 5813 . . . . . . . . . . . . . . 15 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(𝐹‘(𝑁 + 1))) = (𝑁 + 1))
16820, 90, 167syl2anc 411 . . . . . . . . . . . . . 14 (𝜑 → (𝐹‘(𝐹‘(𝑁 + 1))) = (𝑁 + 1))
169166, 168eqtrid 2238 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐾) = (𝑁 + 1))
170169fveq2d 5550 . . . . . . . . . . . 12 (𝜑 → (𝐺‘(𝐹𝐾)) = (𝐺‘(𝑁 + 1)))
171165, 170eqtr2d 2227 . . . . . . . . . . 11 (𝜑 → (𝐺‘(𝑁 + 1)) = ((𝐺𝐹)‘𝐾))
172171adantr 276 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝐺‘(𝑁 + 1)) = ((𝐺𝐹)‘𝐾))
173163, 172oveq12d 5928 . . . . . . . . 9 ((𝜑𝐾 ∈ (𝑀...𝑁)) → ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) + ((𝐺𝐹)‘𝐾)))
174112, 173eqtr4d 2229 . . . . . . . 8 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
175103, 174syldan 282 . . . . . . 7 ((𝜑𝐾 = 𝑀) → (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
17699seqeq1d 10514 . . . . . . . . 9 ((𝜑𝐾 = 𝑀) → seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) = seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)))
177176fveq1d 5548 . . . . . . . 8 ((𝜑𝐾 = 𝑀) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))
178177oveq1d 5925 . . . . . . 7 ((𝜑𝐾 = 𝑀) → ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
17998, 175, 1783eqtrd 2230 . . . . . 6 ((𝜑𝐾 = 𝑀) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
180 elfzuz 10077 . . . . . . . . . . 11 (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝐾 ∈ (ℤ‘(𝑀 + 1)))
181 eluzp1m1 9606 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (ℤ‘(𝑀 + 1))) → (𝐾 − 1) ∈ (ℤ𝑀))
1828, 180, 181syl2an 289 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (𝐾 − 1) ∈ (ℤ𝑀))
18310zcnd 9430 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
184 ax-1cn 7955 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
185 pncan 8215 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
186183, 184, 185sylancl 413 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
187 elfzelz 10081 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ ℤ)
188 peano2zm 9345 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
18992, 187, 1883syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐾 − 1) ∈ ℤ)
190 elfzuz3 10078 . . . . . . . . . . . . . . . . . . . . 21 (𝐾 ∈ (𝑀...(𝑁 + 1)) → (𝑁 + 1) ∈ (ℤ𝐾))
19192, 190syl 14 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑁 + 1) ∈ (ℤ𝐾))
19293zcnd 9430 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐾 ∈ ℂ)
193 npcan 8218 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
194192, 184, 193sylancl 413 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
195194fveq2d 5550 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℤ‘((𝐾 − 1) + 1)) = (ℤ𝐾))
196191, 195eleqtrrd 2273 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 + 1) ∈ (ℤ‘((𝐾 − 1) + 1)))
197 eluzp1m1 9606 . . . . . . . . . . . . . . . . . . 19 (((𝐾 − 1) ∈ ℤ ∧ (𝑁 + 1) ∈ (ℤ‘((𝐾 − 1) + 1))) → ((𝑁 + 1) − 1) ∈ (ℤ‘(𝐾 − 1)))
198189, 196, 197syl2anc 411 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 + 1) − 1) ∈ (ℤ‘(𝐾 − 1)))
199186, 198eqeltrrd 2271 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(𝐾 − 1)))
200 fzss2 10120 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝐾 − 1)) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁))
201199, 200syl 14 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁))
202201sselda 3179 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...𝑁))
203202, 118syldan 282 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽𝑥) ∈ (𝑀...𝑁))
204203fvresd 5571 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)) = (𝐺‘(𝐽𝑥)))
205 simpr 110 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ (𝑀...𝑁))
20666adantr 276 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
207 fzelp1 10130 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
208207adantl 277 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
209128adantl 277 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑥 + 1) ∈ (𝑀...(𝑁 + 1)))
210 elfzelz 10081 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
211210, 93, 132syl2anr 290 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → DECID 𝑥 < 𝐾)
212208, 209, 211ifcldcd 3593 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝑀...𝑁)) → if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)) ∈ (𝑀...(𝑁 + 1)))
213206, 212ffvelcdmd 5686 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) ∈ (𝑀...(𝑁 + 1)))
21421, 125, 205, 213fvmptd3 5643 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐽𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))))
215202, 214syldan 282 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))))
216 elfzm11 10147 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑥 ∈ (𝑀...(𝐾 − 1)) ↔ (𝑥 ∈ ℤ ∧ 𝑀𝑥𝑥 < 𝐾)))
2178, 93, 216syl2anc 411 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑥 ∈ (𝑀...(𝐾 − 1)) ↔ (𝑥 ∈ ℤ ∧ 𝑀𝑥𝑥 < 𝐾)))
218217biimpa 296 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝑥 ∈ ℤ ∧ 𝑀𝑥𝑥 < 𝐾))
219218simp3d 1013 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 < 𝐾)
220 iftrue 3562 . . . . . . . . . . . . . . . . 17 (𝑥 < 𝐾 → if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)) = 𝑥)
221220fveq2d 5550 . . . . . . . . . . . . . . . 16 (𝑥 < 𝐾 → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹𝑥))
222219, 221syl 14 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹𝑥))
223215, 222eqtrd 2226 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽𝑥) = (𝐹𝑥))
224223fveq2d 5550 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐺‘(𝐽𝑥)) = (𝐺‘(𝐹𝑥)))
225204, 224eqtr2d 2227 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐺‘(𝐹𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
226 peano2uz 9638 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘(𝐾 − 1)) → (𝑁 + 1) ∈ (ℤ‘(𝐾 − 1)))
227 fzss2 10120 . . . . . . . . . . . . . . 15 ((𝑁 + 1) ∈ (ℤ‘(𝐾 − 1)) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...(𝑁 + 1)))
228199, 226, 2273syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...(𝑁 + 1)))
229228sselda 3179 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
230 fvco3 5620 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
23166, 230sylan 283 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
232229, 231syldan 282 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
233202, 152syldan 282 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
234225, 232, 2333eqtr4d 2236 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥))
235234adantlr 477 . . . . . . . . . 10 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥))
23619adantr 276 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → +𝑉)
23794adantr 276 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (𝐺𝐹) ∈ V)
23827, 161syl 14 . . . . . . . . . . 11 (𝜑 → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽) ∈ V)
239238adantr 276 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽) ∈ V)
240182, 235, 236, 237, 239seqfveqg 10539 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)))
241 fzp1ss 10129 . . . . . . . . . . . 12 (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁))
2426, 7, 2413syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁))
243242sselda 3179 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ (𝑀...𝑁))
244243, 174syldan 282 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
245240, 244oveq12d 5928 . . . . . . . 8 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))))
246229, 76syldan 282 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺𝐹)‘𝑥) ∈ 𝑆)
247246adantlr 477 . . . . . . . . . . 11 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺𝐹)‘𝑥) ∈ 𝑆)
24815adantlr 477 . . . . . . . . . . 11 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
249182, 247, 248, 237, 236seqclg 10533 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) ∈ 𝑆)
25074, 92ffvelcdmd 5686 . . . . . . . . . . . 12 (𝜑 → ((𝐺𝐹)‘𝐾) ∈ 𝐶)
25118, 250sseldd 3180 . . . . . . . . . . 11 (𝜑 → ((𝐺𝐹)‘𝐾) ∈ 𝑆)
252251adantr 276 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((𝐺𝐹)‘𝐾) ∈ 𝑆)
253110sselda 3179 . . . . . . . . . . . . 13 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ ((𝐾 + 1)...(𝑁 + 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
254253, 77syldan 282 . . . . . . . . . . . 12 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ ((𝐾 + 1)...(𝑁 + 1))) → ((𝐺𝐹)‘𝑥) ∈ 𝑆)
25562, 254, 57, 70, 63seqclg 10533 . . . . . . . . . . 11 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) ∈ 𝑆)
256243, 255syldan 282 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) ∈ 𝑆)
257249, 252, 2563jca 1179 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) ∈ 𝑆 ∧ ((𝐺𝐹)‘𝐾) ∈ 𝑆 ∧ (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) ∈ 𝑆))
25817caovassg 6069 . . . . . . . . 9 ((𝜑 ∧ ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) ∈ 𝑆 ∧ ((𝐺𝐹)‘𝐾) ∈ 𝑆 ∧ (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) ∈ 𝑆)) → (((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)))))
259257, 258syldan 282 . . . . . . . 8 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)))))
2601, 18fssd 5408 . . . . . . . . . . . . . . . 16 (𝜑𝐺:(𝑀...(𝑁 + 1))⟶𝑆)
261 fssres 5421 . . . . . . . . . . . . . . . 16 ((𝐺:(𝑀...(𝑁 + 1))⟶𝑆 ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆)
262260, 3, 261sylancl 413 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆)
263 fco 5411 . . . . . . . . . . . . . . 15 (((𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽):(𝑀...𝑁)⟶𝑆)
264262, 25, 263syl2anc 411 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽):(𝑀...𝑁)⟶𝑆)
265264ffvelcdmda 5685 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
266202, 265syldan 282 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
267266adantlr 477 . . . . . . . . . . 11 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
268182, 267, 248, 239, 236seqclg 10533 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆)
269 elfzuz3 10078 . . . . . . . . . . . 12 (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝑁 ∈ (ℤ𝐾))
270269adantl 277 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝑁 ∈ (ℤ𝐾))
271117, 265syldan 282 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
272271adantlr 477 . . . . . . . . . . 11 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
273270, 272, 248, 239, 236seqclg 10533 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆)
274260, 90ffvelcdmd 5686 . . . . . . . . . . 11 (𝜑 → (𝐺‘(𝑁 + 1)) ∈ 𝑆)
275274adantr 276 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (𝐺‘(𝑁 + 1)) ∈ 𝑆)
276268, 273, 2753jca 1179 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆 ∧ (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆 ∧ (𝐺‘(𝑁 + 1)) ∈ 𝑆))
27717caovassg 6069 . . . . . . . . 9 ((𝜑 ∧ ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆 ∧ (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆 ∧ (𝐺‘(𝑁 + 1)) ∈ 𝑆)) → (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))))
278276, 277syldan 282 . . . . . . . 8 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))))
279245, 259, 2783eqtr4d 2236 . . . . . . 7 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))))
2808adantr 276 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ∈ ℤ)
281180adantl 277 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ (ℤ‘(𝑀 + 1)))
282280, 281, 236, 237seqm1g 10535 . . . . . . . 8 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺𝐹))‘𝐾) = ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)))
283282oveq1d 5925 . . . . . . 7 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = (((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))))
28417adantlr 477 . . . . . . . . . 10 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
285 elfzelz 10081 . . . . . . . . . . . . . . 15 (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝐾 ∈ ℤ)
286285adantl 277 . . . . . . . . . . . . . 14 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ ℤ)
287286zcnd 9430 . . . . . . . . . . . . 13 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ ℂ)
288287, 184, 193sylancl 413 . . . . . . . . . . . 12 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((𝐾 − 1) + 1) = 𝐾)
289288fveq2d 5550 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (ℤ‘((𝐾 − 1) + 1)) = (ℤ𝐾))
290270, 289eleqtrrd 2273 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝑁 ∈ (ℤ‘((𝐾 − 1) + 1)))
291265adantlr 477 . . . . . . . . . 10 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
292248, 284, 290, 236, 239, 182, 291seqsplitg 10550 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)))
293288seqeq1d 10514 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) = seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)))
294293fveq1d 5548 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))
295294oveq2d 5926 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)))
296292, 295eqtrd 2226 . . . . . . . 8 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)))
297296oveq1d 5925 . . . . . . 7 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))))
298279, 283, 2973eqtr4d 2236 . . . . . 6 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
299179, 298jaodan 798 . . . . 5 ((𝜑 ∧ (𝐾 = 𝑀𝐾 ∈ ((𝑀 + 1)...𝑁))) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
30081, 299syldan 282 . . . 4 ((𝜑𝐾 ∈ (𝑀...𝑁)) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
30178, 300eqtrd 2226 . . 3 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
3026adantr 276 . . . . 5 ((𝜑𝐾 = (𝑁 + 1)) → 𝑁 ∈ (ℤ𝑀))
30394adantr 276 . . . . 5 ((𝜑𝐾 = (𝑁 + 1)) → (𝐺𝐹) ∈ V)
30419adantr 276 . . . . 5 ((𝜑𝐾 = (𝑁 + 1)) → +𝑉)
305 seqp1g 10527 . . . . 5 ((𝑁 ∈ (ℤ𝑀) ∧ (𝐺𝐹) ∈ V ∧ +𝑉) → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺𝐹))‘𝑁) + ((𝐺𝐹)‘(𝑁 + 1))))
306302, 303, 304, 305syl3anc 1249 . . . 4 ((𝜑𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺𝐹))‘𝑁) + ((𝐺𝐹)‘(𝑁 + 1))))
307214adantlr 477 . . . . . . . . . 10 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐽𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))))
308210zred 9429 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℝ)
309308adantl 277 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
31010zred 9429 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℝ)
311310adantr 276 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ)
312 peano2re 8145 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
313311, 312syl 14 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ)
314 elfzle2 10084 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑀...𝑁) → 𝑥𝑁)
315314adantl 277 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥𝑁)
316311ltp1d 8939 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1))
317309, 311, 313, 315, 316lelttrd 8134 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
318317adantlr 477 . . . . . . . . . . . 12 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
319 simplr 528 . . . . . . . . . . . 12 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 = (𝑁 + 1))
320318, 319breqtrrd 4057 . . . . . . . . . . 11 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < 𝐾)
321320, 221syl 14 . . . . . . . . . 10 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹𝑥))
322307, 321eqtrd 2226 . . . . . . . . 9 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐽𝑥) = (𝐹𝑥))
323322fveq2d 5550 . . . . . . . 8 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐹𝑥)))
32466ad2antrr 488 . . . . . . . . . . . . 13 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
325207adantl 277 . . . . . . . . . . . . 13 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
326324, 325ffvelcdmd 5686 . . . . . . . . . . . 12 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) ∈ (𝑀...(𝑁 + 1)))
327326elfzelzd 10082 . . . . . . . . . . 11 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) ∈ ℤ)
3286ad2antrr 488 . . . . . . . . . . . 12 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ𝑀))
329328, 7syl 14 . . . . . . . . . . 11 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ)
330328, 9syl 14 . . . . . . . . . . 11 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℤ)
331 fzdcel 10096 . . . . . . . . . . 11 (((𝐹𝑥) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝐹𝑥) ∈ (𝑀...𝑁))
332327, 329, 330, 331syl3anc 1249 . . . . . . . . . 10 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → DECID (𝐹𝑥) ∈ (𝑀...𝑁))
333308adantl 277 . . . . . . . . . . 11 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
334333, 320gtned 8122 . . . . . . . . . 10 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾𝑥)
335 elfzp1 10128 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑥) ∈ (𝑀...𝑁) ∨ (𝐹𝑥) = (𝑁 + 1))))
336328, 335syl 14 . . . . . . . . . . . . . . 15 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑥) ∈ (𝑀...𝑁) ∨ (𝐹𝑥) = (𝑁 + 1))))
337326, 336mpbid 147 . . . . . . . . . . . . . 14 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹𝑥) ∈ (𝑀...𝑁) ∨ (𝐹𝑥) = (𝑁 + 1)))
338337ord 725 . . . . . . . . . . . . 13 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (¬ (𝐹𝑥) ∈ (𝑀...𝑁) → (𝐹𝑥) = (𝑁 + 1)))
33920ad2antrr 488 . . . . . . . . . . . . . . 15 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
340 f1ocnvfv 5814 . . . . . . . . . . . . . . 15 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐹𝑥) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑥))
341339, 325, 340syl2anc 411 . . . . . . . . . . . . . 14 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹𝑥) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑥))
34222eqeq1i 2201 . . . . . . . . . . . . . 14 (𝐾 = 𝑥 ↔ (𝐹‘(𝑁 + 1)) = 𝑥)
343341, 342imbitrrdi 162 . . . . . . . . . . . . 13 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹𝑥) = (𝑁 + 1) → 𝐾 = 𝑥))
344338, 343syld 45 . . . . . . . . . . . 12 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (¬ (𝐹𝑥) ∈ (𝑀...𝑁) → 𝐾 = 𝑥))
345344a1d 22 . . . . . . . . . . 11 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (DECID (𝐹𝑥) ∈ (𝑀...𝑁) → (¬ (𝐹𝑥) ∈ (𝑀...𝑁) → 𝐾 = 𝑥)))
346345necon1addc 2440 . . . . . . . . . 10 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (DECID (𝐹𝑥) ∈ (𝑀...𝑁) → (𝐾𝑥 → (𝐹𝑥) ∈ (𝑀...𝑁))))
347332, 334, 346mp2d 47 . . . . . . . . 9 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) ∈ (𝑀...𝑁))
348347fvresd 5571 . . . . . . . 8 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐹𝑥)) = (𝐺‘(𝐹𝑥)))
349323, 348eqtr2d 2227 . . . . . . 7 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘(𝐹𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
35066, 207, 230syl2an 289 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑀...𝑁)) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
351350adantlr 477 . . . . . . 7 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
352152adantlr 477 . . . . . . 7 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
353349, 351, 3523eqtr4d 2236 . . . . . 6 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥))
354238adantr 276 . . . . . 6 ((𝜑𝐾 = (𝑁 + 1)) → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽) ∈ V)
355302, 353, 304, 303, 354seqfveqg 10539 . . . . 5 ((𝜑𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺𝐹))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))
356 fvco3 5620 . . . . . . . 8 ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1))))
35766, 90, 356syl2anc 411 . . . . . . 7 (𝜑 → ((𝐺𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1))))
358357adantr 276 . . . . . 6 ((𝜑𝐾 = (𝑁 + 1)) → ((𝐺𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1))))
359 simpr 110 . . . . . . . . . 10 ((𝜑𝐾 = (𝑁 + 1)) → 𝐾 = (𝑁 + 1))
36022, 359eqtr3id 2240 . . . . . . . . 9 ((𝜑𝐾 = (𝑁 + 1)) → (𝐹‘(𝑁 + 1)) = (𝑁 + 1))
361360fveq2d 5550 . . . . . . . 8 ((𝜑𝐾 = (𝑁 + 1)) → (𝐹‘(𝐹‘(𝑁 + 1))) = (𝐹‘(𝑁 + 1)))
362168adantr 276 . . . . . . . 8 ((𝜑𝐾 = (𝑁 + 1)) → (𝐹‘(𝐹‘(𝑁 + 1))) = (𝑁 + 1))
363361, 362eqtr3d 2228 . . . . . . 7 ((𝜑𝐾 = (𝑁 + 1)) → (𝐹‘(𝑁 + 1)) = (𝑁 + 1))
364363fveq2d 5550 . . . . . 6 ((𝜑𝐾 = (𝑁 + 1)) → (𝐺‘(𝐹‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1)))
365358, 364eqtrd 2226 . . . . 5 ((𝜑𝐾 = (𝑁 + 1)) → ((𝐺𝐹)‘(𝑁 + 1)) = (𝐺‘(𝑁 + 1)))
366355, 365oveq12d 5928 . . . 4 ((𝜑𝐾 = (𝑁 + 1)) → ((seq𝑀( + , (𝐺𝐹))‘𝑁) + ((𝐺𝐹)‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
367306, 366eqtrd 2226 . . 3 ((𝜑𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
368 elfzp1 10128 . . . . 5 (𝑁 ∈ (ℤ𝑀) → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1))))
3696, 368syl 14 . . . 4 (𝜑 → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1))))
37092, 369mpbid 147 . . 3 (𝜑 → (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1)))
371301, 367, 370mpjaodan 799 . 2 (𝜑 → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
372 seqp1g 10527 . . 3 ((𝑁 ∈ (ℤ𝑀) ∧ 𝐺 ∈ V ∧ +𝑉) → (seq𝑀( + , 𝐺)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1))))
3736, 51, 19, 372syl3anc 1249 . 2 (𝜑 → (seq𝑀( + , 𝐺)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1))))
37456, 371, 3733eqtr4d 2236 1 (𝜑 → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = (seq𝑀( + , 𝐺)‘(𝑁 + 1)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  DECID wdc 835  w3a 980  wal 1362   = wceq 1364  wcel 2164  wne 2364  Vcvv 2760  wss 3153  ifcif 3557   class class class wbr 4029  cmpt 4090  ccnv 4654  cres 4657  ccom 4659   Fn wfn 5241  wf 5242  1-1-ontowf1o 5245  cfv 5246  (class class class)co 5910  Fincfn 6785  cc 7860  cr 7861  1c1 7863   + caddc 7865   < clt 8044  cle 8045  cmin 8180  cz 9307  cuz 9582  ...cfz 10064  seqcseq 10508
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4462  ax-setind 4565  ax-iinf 4616  ax-cnex 7953  ax-resscn 7954  ax-1cn 7955  ax-1re 7956  ax-icn 7957  ax-addcl 7958  ax-addrcl 7959  ax-mulcl 7960  ax-mulrcl 7961  ax-addcom 7962  ax-mulcom 7963  ax-addass 7964  ax-mulass 7965  ax-distr 7966  ax-i2m1 7967  ax-0lt1 7968  ax-1rid 7969  ax-0id 7970  ax-rnegex 7971  ax-precex 7972  ax-cnre 7973  ax-pre-ltirr 7974  ax-pre-ltwlin 7975  ax-pre-lttrn 7976  ax-pre-apti 7977  ax-pre-ltadd 7978  ax-pre-mulgt0 7979
This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-if 3558  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-id 4322  df-iord 4395  df-on 4397  df-ilim 4398  df-suc 4400  df-iom 4619  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-iota 5207  df-fun 5248  df-fn 5249  df-f 5250  df-f1 5251  df-fo 5252  df-f1o 5253  df-fv 5254  df-riota 5865  df-ov 5913  df-oprab 5914  df-mpo 5915  df-1st 6184  df-2nd 6185  df-recs 6349  df-frec 6435  df-1o 6460  df-er 6578  df-en 6786  df-fin 6788  df-pnf 8046  df-mnf 8047  df-xr 8048  df-ltxr 8049  df-le 8050  df-sub 8182  df-neg 8183  df-reap 8584  df-ap 8591  df-inn 8973  df-n0 9231  df-z 9308  df-uz 9583  df-fz 10065  df-fzo 10199  df-seqfrec 10509
This theorem is referenced by:  seqf1og  10582
  Copyright terms: Public domain W3C validator