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

Theorem isummolem3 10770
Description: Lemma for isummo 10773. (Contributed by Mario Carneiro, 29-Mar-2014.)
Hypotheses
Ref Expression
isummo.1 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 0))
isummo.2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
isummolem3.5 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ))
isummolem3.6 (𝜑𝑓:(1...𝑀)–1-1-onto𝐴)
isummolem3.7 (𝜑𝐾:(1...𝑁)–1-1-onto𝐴)
isummolem3.g 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛𝑀, (𝑓𝑛) / 𝑘𝐵, 0))
isummolem3.4 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛𝑁, (𝐾𝑛) / 𝑘𝐵, 0))
Assertion
Ref Expression
isummolem3 (𝜑 → (seq1( + , 𝐺, ℂ)‘𝑀) = (seq1( + , 𝐻, ℂ)‘𝑁))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑛,𝐹   𝑘,𝑁,𝑛   𝜑,𝑘,𝑛   𝑘,𝑀,𝑛   𝐵,𝑛   𝑘,𝐾,𝑛   𝑓,𝑘,𝑛
Allowed substitution hints:   𝜑(𝑓)   𝐴(𝑓)   𝐵(𝑓,𝑘)   𝐹(𝑓,𝑘)   𝐺(𝑓,𝑘,𝑛)   𝐻(𝑓,𝑘,𝑛)   𝐾(𝑓)   𝑀(𝑓)   𝑁(𝑓)

Proof of Theorem isummolem3
Dummy variables 𝑖 𝑗 𝑚 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addcl 7467 . . . . 5 ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) ∈ ℂ)
21adantl 271 . . . 4 ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) ∈ ℂ)
3 addcom 7619 . . . . 5 ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) = (𝑗 + 𝑚))
43adantl 271 . . . 4 ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) = (𝑗 + 𝑚))
5 addass 7472 . . . . 5 ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦)))
65adantl 271 . . . 4 ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦)))
7 isummolem3.5 . . . . . 6 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ))
87simpld 110 . . . . 5 (𝜑𝑀 ∈ ℕ)
9 nnuz 9054 . . . . 5 ℕ = (ℤ‘1)
108, 9syl6eleq 2180 . . . 4 (𝜑𝑀 ∈ (ℤ‘1))
11 isummolem3.6 . . . . . . 7 (𝜑𝑓:(1...𝑀)–1-1-onto𝐴)
12 f1ocnv 5266 . . . . . . 7 (𝑓:(1...𝑀)–1-1-onto𝐴𝑓:𝐴1-1-onto→(1...𝑀))
1311, 12syl 14 . . . . . 6 (𝜑𝑓:𝐴1-1-onto→(1...𝑀))
14 isummolem3.7 . . . . . 6 (𝜑𝐾:(1...𝑁)–1-1-onto𝐴)
15 f1oco 5276 . . . . . 6 ((𝑓:𝐴1-1-onto→(1...𝑀) ∧ 𝐾:(1...𝑁)–1-1-onto𝐴) → (𝑓𝐾):(1...𝑁)–1-1-onto→(1...𝑀))
1613, 14, 15syl2anc 403 . . . . 5 (𝜑 → (𝑓𝐾):(1...𝑁)–1-1-onto→(1...𝑀))
17 isummo.1 . . . . . . . . 9 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 0))
18 isummo.2 . . . . . . . . 9 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
1917, 18, 7, 11, 14isummolemnm 10769 . . . . . . . 8 (𝜑𝑁 = 𝑀)
2019eqcomd 2093 . . . . . . 7 (𝜑𝑀 = 𝑁)
2120oveq2d 5668 . . . . . 6 (𝜑 → (1...𝑀) = (1...𝑁))
22 f1oeq2 5245 . . . . . 6 ((1...𝑀) = (1...𝑁) → ((𝑓𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (𝑓𝐾):(1...𝑁)–1-1-onto→(1...𝑀)))
2321, 22syl 14 . . . . 5 (𝜑 → ((𝑓𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (𝑓𝐾):(1...𝑁)–1-1-onto→(1...𝑀)))
2416, 23mpbird 165 . . . 4 (𝜑 → (𝑓𝐾):(1...𝑀)–1-1-onto→(1...𝑀))
25 elnnuz 9055 . . . . 5 (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ‘1))
26 simplr 497 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ∈ ℕ)
27 elfzle2 9442 . . . . . . . . . . 11 (𝑚 ∈ (1...𝑀) → 𝑚𝑀)
2827adantl 271 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → 𝑚𝑀)
2928iftrued 3400 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → if(𝑚𝑀, (𝑓𝑚) / 𝑘𝐵, 0) = (𝑓𝑚) / 𝑘𝐵)
30 f1of 5253 . . . . . . . . . . . . 13 (𝑓:(1...𝑀)–1-1-onto𝐴𝑓:(1...𝑀)⟶𝐴)
3111, 30syl 14 . . . . . . . . . . . 12 (𝜑𝑓:(1...𝑀)⟶𝐴)
3231ffvelrnda 5434 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (1...𝑀)) → (𝑓𝑚) ∈ 𝐴)
3318ralrimiva 2446 . . . . . . . . . . . 12 (𝜑 → ∀𝑘𝐴 𝐵 ∈ ℂ)
3433adantr 270 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (1...𝑀)) → ∀𝑘𝐴 𝐵 ∈ ℂ)
35 nfcsb1v 2963 . . . . . . . . . . . . 13 𝑘(𝑓𝑚) / 𝑘𝐵
3635nfel1 2239 . . . . . . . . . . . 12 𝑘(𝑓𝑚) / 𝑘𝐵 ∈ ℂ
37 csbeq1a 2941 . . . . . . . . . . . . 13 (𝑘 = (𝑓𝑚) → 𝐵 = (𝑓𝑚) / 𝑘𝐵)
3837eleq1d 2156 . . . . . . . . . . . 12 (𝑘 = (𝑓𝑚) → (𝐵 ∈ ℂ ↔ (𝑓𝑚) / 𝑘𝐵 ∈ ℂ))
3936, 38rspc 2716 . . . . . . . . . . 11 ((𝑓𝑚) ∈ 𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → (𝑓𝑚) / 𝑘𝐵 ∈ ℂ))
4032, 34, 39sylc 61 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1...𝑀)) → (𝑓𝑚) / 𝑘𝐵 ∈ ℂ)
4140adantlr 461 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → (𝑓𝑚) / 𝑘𝐵 ∈ ℂ)
4229, 41eqeltrd 2164 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → if(𝑚𝑀, (𝑓𝑚) / 𝑘𝐵, 0) ∈ ℂ)
43 breq1 3848 . . . . . . . . . 10 (𝑛 = 𝑚 → (𝑛𝑀𝑚𝑀))
44 fveq2 5305 . . . . . . . . . . 11 (𝑛 = 𝑚 → (𝑓𝑛) = (𝑓𝑚))
4544csbeq1d 2939 . . . . . . . . . 10 (𝑛 = 𝑚(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑚) / 𝑘𝐵)
4643, 45ifbieq1d 3413 . . . . . . . . 9 (𝑛 = 𝑚 → if(𝑛𝑀, (𝑓𝑛) / 𝑘𝐵, 0) = if(𝑚𝑀, (𝑓𝑚) / 𝑘𝐵, 0))
47 isummolem3.g . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛𝑀, (𝑓𝑛) / 𝑘𝐵, 0))
4846, 47fvmptg 5380 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ if(𝑚𝑀, (𝑓𝑚) / 𝑘𝐵, 0) ∈ ℂ) → (𝐺𝑚) = if(𝑚𝑀, (𝑓𝑚) / 𝑘𝐵, 0))
4926, 42, 48syl2anc 403 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → (𝐺𝑚) = if(𝑚𝑀, (𝑓𝑚) / 𝑘𝐵, 0))
5049, 42eqeltrd 2164 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → (𝐺𝑚) ∈ ℂ)
51 simplr 497 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → 𝑚 ∈ ℕ)
528ad2antrr 472 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → 𝑀 ∈ ℕ)
5352nnzd 8867 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → 𝑀 ∈ ℤ)
54 eluzp1l 9043 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → 𝑀 < 𝑚)
5553, 54sylancom 411 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → 𝑀 < 𝑚)
5651nnzd 8867 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → 𝑚 ∈ ℤ)
57 zltnle 8796 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 < 𝑚 ↔ ¬ 𝑚𝑀))
5853, 56, 57syl2anc 403 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → (𝑀 < 𝑚 ↔ ¬ 𝑚𝑀))
5955, 58mpbid 145 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → ¬ 𝑚𝑀)
6059iffalsed 3403 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → if(𝑚𝑀, (𝑓𝑚) / 𝑘𝐵, 0) = 0)
61 0cn 7480 . . . . . . . . 9 0 ∈ ℂ
6260, 61syl6eqel 2178 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → if(𝑚𝑀, (𝑓𝑚) / 𝑘𝐵, 0) ∈ ℂ)
6351, 62, 48syl2anc 403 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → (𝐺𝑚) = if(𝑚𝑀, (𝑓𝑚) / 𝑘𝐵, 0))
6463, 62eqeltrd 2164 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → (𝐺𝑚) ∈ ℂ)
65 nnsplit 9548 . . . . . . . . . 10 (𝑀 ∈ ℕ → ℕ = ((1...𝑀) ∪ (ℤ‘(𝑀 + 1))))
668, 65syl 14 . . . . . . . . 9 (𝜑 → ℕ = ((1...𝑀) ∪ (ℤ‘(𝑀 + 1))))
6766eleq2d 2157 . . . . . . . 8 (𝜑 → (𝑚 ∈ ℕ ↔ 𝑚 ∈ ((1...𝑀) ∪ (ℤ‘(𝑀 + 1)))))
6867biimpa 290 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ((1...𝑀) ∪ (ℤ‘(𝑀 + 1))))
69 elun 3141 . . . . . . 7 (𝑚 ∈ ((1...𝑀) ∪ (ℤ‘(𝑀 + 1))) ↔ (𝑚 ∈ (1...𝑀) ∨ 𝑚 ∈ (ℤ‘(𝑀 + 1))))
7068, 69sylib 120 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝑚 ∈ (1...𝑀) ∨ 𝑚 ∈ (ℤ‘(𝑀 + 1))))
7150, 64, 70mpjaodan 747 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) ∈ ℂ)
7225, 71sylan2br 282 . . . 4 ((𝜑𝑚 ∈ (ℤ‘1)) → (𝐺𝑚) ∈ ℂ)
7319oveq2d 5668 . . . . . . . . . 10 (𝜑 → (1...𝑁) = (1...𝑀))
7473eleq2d 2157 . . . . . . . . 9 (𝜑 → (𝑚 ∈ (1...𝑁) ↔ 𝑚 ∈ (1...𝑀)))
7574adantr 270 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ) → (𝑚 ∈ (1...𝑁) ↔ 𝑚 ∈ (1...𝑀)))
7675pm5.32i 442 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) ↔ ((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)))
77 simplr 497 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑚 ∈ ℕ)
78 elfzle2 9442 . . . . . . . . . . . 12 (𝑚 ∈ (1...𝑁) → 𝑚𝑁)
7978adantl 271 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑚𝑁)
8079iftrued 3400 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → if(𝑚𝑁, (𝐾𝑚) / 𝑘𝐵, 0) = (𝐾𝑚) / 𝑘𝐵)
81 f1of 5253 . . . . . . . . . . . . . 14 (𝐾:(1...𝑁)–1-1-onto𝐴𝐾:(1...𝑁)⟶𝐴)
8214, 81syl 14 . . . . . . . . . . . . 13 (𝜑𝐾:(1...𝑁)⟶𝐴)
8382ffvelrnda 5434 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (1...𝑁)) → (𝐾𝑚) ∈ 𝐴)
8433adantr 270 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (1...𝑁)) → ∀𝑘𝐴 𝐵 ∈ ℂ)
85 nfcsb1v 2963 . . . . . . . . . . . . . 14 𝑘(𝐾𝑚) / 𝑘𝐵
8685nfel1 2239 . . . . . . . . . . . . 13 𝑘(𝐾𝑚) / 𝑘𝐵 ∈ ℂ
87 csbeq1a 2941 . . . . . . . . . . . . . 14 (𝑘 = (𝐾𝑚) → 𝐵 = (𝐾𝑚) / 𝑘𝐵)
8887eleq1d 2156 . . . . . . . . . . . . 13 (𝑘 = (𝐾𝑚) → (𝐵 ∈ ℂ ↔ (𝐾𝑚) / 𝑘𝐵 ∈ ℂ))
8986, 88rspc 2716 . . . . . . . . . . . 12 ((𝐾𝑚) ∈ 𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → (𝐾𝑚) / 𝑘𝐵 ∈ ℂ))
9083, 84, 89sylc 61 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (1...𝑁)) → (𝐾𝑚) / 𝑘𝐵 ∈ ℂ)
9190adantlr 461 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐾𝑚) / 𝑘𝐵 ∈ ℂ)
9280, 91eqeltrd 2164 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → if(𝑚𝑁, (𝐾𝑚) / 𝑘𝐵, 0) ∈ ℂ)
93 breq1 3848 . . . . . . . . . . 11 (𝑛 = 𝑚 → (𝑛𝑁𝑚𝑁))
94 fveq2 5305 . . . . . . . . . . . 12 (𝑛 = 𝑚 → (𝐾𝑛) = (𝐾𝑚))
9594csbeq1d 2939 . . . . . . . . . . 11 (𝑛 = 𝑚(𝐾𝑛) / 𝑘𝐵 = (𝐾𝑚) / 𝑘𝐵)
9693, 95ifbieq1d 3413 . . . . . . . . . 10 (𝑛 = 𝑚 → if(𝑛𝑁, (𝐾𝑛) / 𝑘𝐵, 0) = if(𝑚𝑁, (𝐾𝑚) / 𝑘𝐵, 0))
97 isummolem3.4 . . . . . . . . . 10 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛𝑁, (𝐾𝑛) / 𝑘𝐵, 0))
9896, 97fvmptg 5380 . . . . . . . . 9 ((𝑚 ∈ ℕ ∧ if(𝑚𝑁, (𝐾𝑚) / 𝑘𝐵, 0) ∈ ℂ) → (𝐻𝑚) = if(𝑚𝑁, (𝐾𝑚) / 𝑘𝐵, 0))
9977, 92, 98syl2anc 403 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐻𝑚) = if(𝑚𝑁, (𝐾𝑚) / 𝑘𝐵, 0))
10099, 92eqeltrd 2164 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐻𝑚) ∈ ℂ)
10176, 100sylbir 133 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → (𝐻𝑚) ∈ ℂ)
10219breq2d 3857 . . . . . . . . . . . . 13 (𝜑 → (𝑚𝑁𝑚𝑀))
103102notbid 627 . . . . . . . . . . . 12 (𝜑 → (¬ 𝑚𝑁 ↔ ¬ 𝑚𝑀))
104103ad2antrr 472 . . . . . . . . . . 11 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → (¬ 𝑚𝑁 ↔ ¬ 𝑚𝑀))
10559, 104mpbird 165 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → ¬ 𝑚𝑁)
106105iffalsed 3403 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → if(𝑚𝑁, (𝐾𝑚) / 𝑘𝐵, 0) = 0)
107106, 61syl6eqel 2178 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → if(𝑚𝑁, (𝐾𝑚) / 𝑘𝐵, 0) ∈ ℂ)
10851, 107, 98syl2anc 403 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → (𝐻𝑚) = if(𝑚𝑁, (𝐾𝑚) / 𝑘𝐵, 0))
109108, 107eqeltrd 2164 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝑀 + 1))) → (𝐻𝑚) ∈ ℂ)
110101, 109, 70mpjaodan 747 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐻𝑚) ∈ ℂ)
11125, 110sylan2br 282 . . . 4 ((𝜑𝑚 ∈ (ℤ‘1)) → (𝐻𝑚) ∈ ℂ)
112 f1oeq2 5245 . . . . . . . . . . . 12 ((1...𝑀) = (1...𝑁) → (𝐾:(1...𝑀)–1-1-onto𝐴𝐾:(1...𝑁)–1-1-onto𝐴))
11321, 112syl 14 . . . . . . . . . . 11 (𝜑 → (𝐾:(1...𝑀)–1-1-onto𝐴𝐾:(1...𝑁)–1-1-onto𝐴))
11414, 113mpbird 165 . . . . . . . . . 10 (𝜑𝐾:(1...𝑀)–1-1-onto𝐴)
115 f1of 5253 . . . . . . . . . 10 (𝐾:(1...𝑀)–1-1-onto𝐴𝐾:(1...𝑀)⟶𝐴)
116114, 115syl 14 . . . . . . . . 9 (𝜑𝐾:(1...𝑀)⟶𝐴)
117 fvco3 5375 . . . . . . . . 9 ((𝐾:(1...𝑀)⟶𝐴𝑖 ∈ (1...𝑀)) → ((𝑓𝐾)‘𝑖) = (𝑓‘(𝐾𝑖)))
118116, 117sylan 277 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑓𝐾)‘𝑖) = (𝑓‘(𝐾𝑖)))
119118fveq2d 5309 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑓‘((𝑓𝐾)‘𝑖)) = (𝑓‘(𝑓‘(𝐾𝑖))))
12011adantr 270 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑓:(1...𝑀)–1-1-onto𝐴)
121116ffvelrnda 5434 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐾𝑖) ∈ 𝐴)
122 f1ocnvfv2 5557 . . . . . . . 8 ((𝑓:(1...𝑀)–1-1-onto𝐴 ∧ (𝐾𝑖) ∈ 𝐴) → (𝑓‘(𝑓‘(𝐾𝑖))) = (𝐾𝑖))
123120, 121, 122syl2anc 403 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑓‘(𝑓‘(𝐾𝑖))) = (𝐾𝑖))
124119, 123eqtr2d 2121 . . . . . 6 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐾𝑖) = (𝑓‘((𝑓𝐾)‘𝑖)))
125124csbeq1d 2939 . . . . 5 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐾𝑖) / 𝑘𝐵 = (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵)
126 elfznn 9468 . . . . . . 7 (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
127 elfzle2 9442 . . . . . . . . . . 11 (𝑖 ∈ (1...𝑀) → 𝑖𝑀)
128127adantl 271 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑖𝑀)
12920breq2d 3857 . . . . . . . . . . 11 (𝜑 → (𝑖𝑀𝑖𝑁))
130129adantr 270 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑖𝑀𝑖𝑁))
131128, 130mpbid 145 . . . . . . . . 9 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑖𝑁)
132131iftrued 3400 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑀)) → if(𝑖𝑁, (𝐾𝑖) / 𝑘𝐵, 0) = (𝐾𝑖) / 𝑘𝐵)
13333adantr 270 . . . . . . . . 9 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑘𝐴 𝐵 ∈ ℂ)
134 nfcsb1v 2963 . . . . . . . . . . 11 𝑘(𝐾𝑖) / 𝑘𝐵
135134nfel1 2239 . . . . . . . . . 10 𝑘(𝐾𝑖) / 𝑘𝐵 ∈ ℂ
136 csbeq1a 2941 . . . . . . . . . . 11 (𝑘 = (𝐾𝑖) → 𝐵 = (𝐾𝑖) / 𝑘𝐵)
137136eleq1d 2156 . . . . . . . . . 10 (𝑘 = (𝐾𝑖) → (𝐵 ∈ ℂ ↔ (𝐾𝑖) / 𝑘𝐵 ∈ ℂ))
138135, 137rspc 2716 . . . . . . . . 9 ((𝐾𝑖) ∈ 𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → (𝐾𝑖) / 𝑘𝐵 ∈ ℂ))
139121, 133, 138sylc 61 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐾𝑖) / 𝑘𝐵 ∈ ℂ)
140132, 139eqeltrd 2164 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑀)) → if(𝑖𝑁, (𝐾𝑖) / 𝑘𝐵, 0) ∈ ℂ)
141 breq1 3848 . . . . . . . . 9 (𝑛 = 𝑖 → (𝑛𝑁𝑖𝑁))
142 fveq2 5305 . . . . . . . . . 10 (𝑛 = 𝑖 → (𝐾𝑛) = (𝐾𝑖))
143142csbeq1d 2939 . . . . . . . . 9 (𝑛 = 𝑖(𝐾𝑛) / 𝑘𝐵 = (𝐾𝑖) / 𝑘𝐵)
144141, 143ifbieq1d 3413 . . . . . . . 8 (𝑛 = 𝑖 → if(𝑛𝑁, (𝐾𝑛) / 𝑘𝐵, 0) = if(𝑖𝑁, (𝐾𝑖) / 𝑘𝐵, 0))
145144, 97fvmptg 5380 . . . . . . 7 ((𝑖 ∈ ℕ ∧ if(𝑖𝑁, (𝐾𝑖) / 𝑘𝐵, 0) ∈ ℂ) → (𝐻𝑖) = if(𝑖𝑁, (𝐾𝑖) / 𝑘𝐵, 0))
146126, 140, 145syl2an2 561 . . . . . 6 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻𝑖) = if(𝑖𝑁, (𝐾𝑖) / 𝑘𝐵, 0))
147146, 132eqtrd 2120 . . . . 5 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻𝑖) = (𝐾𝑖) / 𝑘𝐵)
148 f1of 5253 . . . . . . . . . 10 ((𝑓𝐾):(1...𝑀)–1-1-onto→(1...𝑀) → (𝑓𝐾):(1...𝑀)⟶(1...𝑀))
14924, 148syl 14 . . . . . . . . 9 (𝜑 → (𝑓𝐾):(1...𝑀)⟶(1...𝑀))
150149ffvelrnda 5434 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑓𝐾)‘𝑖) ∈ (1...𝑀))
151 elfznn 9468 . . . . . . . 8 (((𝑓𝐾)‘𝑖) ∈ (1...𝑀) → ((𝑓𝐾)‘𝑖) ∈ ℕ)
152150, 151syl 14 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑓𝐾)‘𝑖) ∈ ℕ)
153 elfzle2 9442 . . . . . . . . . . 11 (((𝑓𝐾)‘𝑖) ∈ (1...𝑀) → ((𝑓𝐾)‘𝑖) ≤ 𝑀)
154150, 153syl 14 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑓𝐾)‘𝑖) ≤ 𝑀)
155154iftrued 3400 . . . . . . . . 9 ((𝜑𝑖 ∈ (1...𝑀)) → if(((𝑓𝐾)‘𝑖) ≤ 𝑀, (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵, 0) = (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵)
156155, 125eqtr4d 2123 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑀)) → if(((𝑓𝐾)‘𝑖) ≤ 𝑀, (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵, 0) = (𝐾𝑖) / 𝑘𝐵)
157156, 139eqeltrd 2164 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑀)) → if(((𝑓𝐾)‘𝑖) ≤ 𝑀, (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵, 0) ∈ ℂ)
158 breq1 3848 . . . . . . . . 9 (𝑛 = ((𝑓𝐾)‘𝑖) → (𝑛𝑀 ↔ ((𝑓𝐾)‘𝑖) ≤ 𝑀))
159 fveq2 5305 . . . . . . . . . 10 (𝑛 = ((𝑓𝐾)‘𝑖) → (𝑓𝑛) = (𝑓‘((𝑓𝐾)‘𝑖)))
160159csbeq1d 2939 . . . . . . . . 9 (𝑛 = ((𝑓𝐾)‘𝑖) → (𝑓𝑛) / 𝑘𝐵 = (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵)
161158, 160ifbieq1d 3413 . . . . . . . 8 (𝑛 = ((𝑓𝐾)‘𝑖) → if(𝑛𝑀, (𝑓𝑛) / 𝑘𝐵, 0) = if(((𝑓𝐾)‘𝑖) ≤ 𝑀, (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵, 0))
162161, 47fvmptg 5380 . . . . . . 7 ((((𝑓𝐾)‘𝑖) ∈ ℕ ∧ if(((𝑓𝐾)‘𝑖) ≤ 𝑀, (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵, 0) ∈ ℂ) → (𝐺‘((𝑓𝐾)‘𝑖)) = if(((𝑓𝐾)‘𝑖) ≤ 𝑀, (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵, 0))
163152, 157, 162syl2anc 403 . . . . . 6 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘((𝑓𝐾)‘𝑖)) = if(((𝑓𝐾)‘𝑖) ≤ 𝑀, (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵, 0))
164163, 155eqtrd 2120 . . . . 5 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘((𝑓𝐾)‘𝑖)) = (𝑓‘((𝑓𝐾)‘𝑖)) / 𝑘𝐵)
165125, 147, 1643eqtr4d 2130 . . . 4 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻𝑖) = (𝐺‘((𝑓𝐾)‘𝑖)))
1662, 4, 6, 10, 24, 72, 111, 165seq3f1o 9933 . . 3 (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐺)‘𝑀))
167 1zzd 8777 . . . . 5 (𝜑 → 1 ∈ ℤ)
168167, 111iseqseq3 9902 . . . 4 (𝜑 → seq1( + , 𝐻, ℂ) = seq1( + , 𝐻))
169168fveq1d 5307 . . 3 (𝜑 → (seq1( + , 𝐻, ℂ)‘𝑀) = (seq1( + , 𝐻)‘𝑀))
170167, 72iseqseq3 9902 . . . 4 (𝜑 → seq1( + , 𝐺, ℂ) = seq1( + , 𝐺))
171170fveq1d 5307 . . 3 (𝜑 → (seq1( + , 𝐺, ℂ)‘𝑀) = (seq1( + , 𝐺)‘𝑀))
172166, 169, 1713eqtr4d 2130 . 2 (𝜑 → (seq1( + , 𝐻, ℂ)‘𝑀) = (seq1( + , 𝐺, ℂ)‘𝑀))
17320fveq2d 5309 . 2 (𝜑 → (seq1( + , 𝐻, ℂ)‘𝑀) = (seq1( + , 𝐻, ℂ)‘𝑁))
174172, 173eqtr3d 2122 1 (𝜑 → (seq1( + , 𝐺, ℂ)‘𝑀) = (seq1( + , 𝐻, ℂ)‘𝑁))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 664  w3a 924   = wceq 1289  wcel 1438  wral 2359  csb 2933  cun 2997  ifcif 3393   class class class wbr 3845  cmpt 3899  ccnv 4437  ccom 4442  wf 5011  1-1-ontowf1o 5014  cfv 5015  (class class class)co 5652  cc 7348  0cc0 7350  1c1 7351   + caddc 7353   < clt 7522  cle 7523  cn 8422  cz 8750  cuz 9019  ...cfz 9424  seqcseq4 9851  seqcseq 9852
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3954  ax-sep 3957  ax-nul 3965  ax-pow 4009  ax-pr 4036  ax-un 4260  ax-setind 4353  ax-iinf 4403  ax-cnex 7436  ax-resscn 7437  ax-1cn 7438  ax-1re 7439  ax-icn 7440  ax-addcl 7441  ax-addrcl 7442  ax-mulcl 7443  ax-addcom 7445  ax-addass 7447  ax-distr 7449  ax-i2m1 7450  ax-0lt1 7451  ax-0id 7453  ax-rnegex 7454  ax-cnre 7456  ax-pre-ltirr 7457  ax-pre-ltwlin 7458  ax-pre-lttrn 7459  ax-pre-apti 7460  ax-pre-ltadd 7461
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-if 3394  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-int 3689  df-iun 3732  df-br 3846  df-opab 3900  df-mpt 3901  df-tr 3937  df-id 4120  df-iord 4193  df-on 4195  df-ilim 4196  df-suc 4198  df-iom 4406  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-res 4450  df-ima 4451  df-iota 4980  df-fun 5017  df-fn 5018  df-f 5019  df-f1 5020  df-fo 5021  df-f1o 5022  df-fv 5023  df-riota 5608  df-ov 5655  df-oprab 5656  df-mpt2 5657  df-1st 5911  df-2nd 5912  df-recs 6070  df-frec 6156  df-1o 6181  df-er 6292  df-en 6458  df-dom 6459  df-fin 6460  df-pnf 7524  df-mnf 7525  df-xr 7526  df-ltxr 7527  df-le 7528  df-sub 7655  df-neg 7656  df-inn 8423  df-n0 8674  df-z 8751  df-uz 9020  df-fz 9425  df-fzo 9554  df-iseq 9853  df-seq3 9854  df-ihash 10184
This theorem is referenced by:  isummolem2a  10771  isummo  10773
  Copyright terms: Public domain W3C validator