Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sticksstones12 Structured version   Visualization version   GIF version

Theorem sticksstones12 40094
Description: Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
Hypotheses
Ref Expression
sticksstones12.1 (𝜑𝑁 ∈ ℕ0)
sticksstones12.2 (𝜑𝐾 ∈ ℕ)
sticksstones12.3 𝐹 = (𝑎𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙))))
sticksstones12.4 𝐺 = (𝑏𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
sticksstones12.5 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)}
sticksstones12.6 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)))}
Assertion
Ref Expression
sticksstones12 (𝜑𝐹:𝐴1-1-onto𝐵)
Distinct variable groups:   𝐴,𝑎,𝑗,𝑘,𝑙   𝐴,𝑏,𝑘,𝑥,𝑦   𝑥,𝑎,𝑦,𝑗,𝑘,𝑙   𝐵,𝑎,𝑖,𝑘,𝑙   𝐵,𝑏   𝐵,𝑗   𝐹,𝑏,𝑘   𝐾,𝑎,𝑓,𝑗,𝑙,𝑥,𝑦   𝐾,𝑏,𝑘,𝑔,𝑖   𝑔,𝑎,𝑖,𝑘,𝑁   𝑓,𝑁,𝑗,𝑙   𝑁,𝑏,𝑘,𝑔,𝑖   𝜑,𝑎,𝑖,𝑘,𝑙   𝜑,𝑏   𝜑,𝑗,𝑥,𝑦   𝑖,𝑏   𝑓,𝑏,𝑥,𝑦   𝑔,𝑏
Allowed substitution hints:   𝜑(𝑓,𝑔)   𝐴(𝑓,𝑔,𝑖)   𝐵(𝑥,𝑦,𝑓,𝑔)   𝐹(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑎,𝑙)   𝐺(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑎,𝑏,𝑙)   𝑁(𝑥,𝑦)

Proof of Theorem sticksstones12
Dummy variables 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sticksstones12.1 . . 3 (𝜑𝑁 ∈ ℕ0)
2 sticksstones12.2 . . . 4 (𝜑𝐾 ∈ ℕ)
32nnnn0d 12276 . . 3 (𝜑𝐾 ∈ ℕ0)
4 sticksstones12.3 . . 3 𝐹 = (𝑎𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙))))
5 sticksstones12.5 . . 3 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)}
6 sticksstones12.6 . . 3 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)))}
71, 3, 4, 5, 6sticksstones8 40089 . 2 (𝜑𝐹:𝐴𝐵)
8 sticksstones12.4 . . 3 𝐺 = (𝑏𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
91, 2, 8, 5, 6sticksstones10 40091 . 2 (𝜑𝐺:𝐵𝐴)
108a1i 11 . . . . . . 7 (𝜑𝐺 = (𝑏𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))))
11 0red 10962 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
122nngt0d 12005 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝐾)
1311, 12ltned 11094 . . . . . . . . . . . 12 (𝜑 → 0 ≠ 𝐾)
1413necomd 3000 . . . . . . . . . . 11 (𝜑𝐾 ≠ 0)
1514neneqd 2949 . . . . . . . . . 10 (𝜑 → ¬ 𝐾 = 0)
1615iffalsed 4475 . . . . . . . . 9 (𝜑 → if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))
1716adantr 480 . . . . . . . 8 ((𝜑𝑏𝐵) → if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))
1817mpteq2dva 5178 . . . . . . 7 (𝜑 → (𝑏𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))) = (𝑏𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
1910, 18eqtrd 2779 . . . . . 6 (𝜑𝐺 = (𝑏𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
2019adantr 480 . . . . 5 ((𝜑𝑐𝐴) → 𝐺 = (𝑏𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
21 fveq1 6767 . . . . . . . . . 10 (𝑏 = (𝐹𝑐) → (𝑏𝐾) = ((𝐹𝑐)‘𝐾))
2221oveq2d 7284 . . . . . . . . 9 (𝑏 = (𝐹𝑐) → ((𝑁 + 𝐾) − (𝑏𝐾)) = ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)))
23 fveq1 6767 . . . . . . . . . . 11 (𝑏 = (𝐹𝑐) → (𝑏‘1) = ((𝐹𝑐)‘1))
2423oveq1d 7283 . . . . . . . . . 10 (𝑏 = (𝐹𝑐) → ((𝑏‘1) − 1) = (((𝐹𝑐)‘1) − 1))
25 fveq1 6767 . . . . . . . . . . . 12 (𝑏 = (𝐹𝑐) → (𝑏𝑘) = ((𝐹𝑐)‘𝑘))
26 fveq1 6767 . . . . . . . . . . . 12 (𝑏 = (𝐹𝑐) → (𝑏‘(𝑘 − 1)) = ((𝐹𝑐)‘(𝑘 − 1)))
2725, 26oveq12d 7286 . . . . . . . . . . 11 (𝑏 = (𝐹𝑐) → ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) = (((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))))
2827oveq1d 7283 . . . . . . . . . 10 (𝑏 = (𝐹𝑐) → (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1) = ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1))
2924, 28ifeq12d 4485 . . . . . . . . 9 (𝑏 = (𝐹𝑐) → if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)) = if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))
3022, 29ifeq12d 4485 . . . . . . . 8 (𝑏 = (𝐹𝑐) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))) = if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1))))
3130adantr 480 . . . . . . 7 ((𝑏 = (𝐹𝑐) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))) = if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1))))
3231mpteq2dva 5178 . . . . . 6 (𝑏 = (𝐹𝑐) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))))
3332adantl 481 . . . . 5 (((𝜑𝑐𝐴) ∧ 𝑏 = (𝐹𝑐)) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))))
347ffvelrnda 6955 . . . . 5 ((𝜑𝑐𝐴) → (𝐹𝑐) ∈ 𝐵)
35 fzfid 13674 . . . . . 6 ((𝜑𝑐𝐴) → (1...(𝐾 + 1)) ∈ Fin)
3635mptexd 7094 . . . . 5 ((𝜑𝑐𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))) ∈ V)
3720, 33, 34, 36fvmptd 6876 . . . 4 ((𝜑𝑐𝐴) → (𝐺‘(𝐹𝑐)) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))))
384a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → 𝐹 = (𝑎𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙)))))
39 simpllr 772 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑎 = 𝑐)
4039fveq1d 6770 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑎𝑙) = (𝑐𝑙))
4140sumeq2dv 15396 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → Σ𝑙 ∈ (1...𝑗)(𝑎𝑙) = Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))
4241oveq2d 7284 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙)) = (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))
4342mpteq2dva 5178 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐴) ∧ 𝑎 = 𝑐) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
44 simpr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → 𝑐𝐴)
45 fzfid 13674 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → (1...𝐾) ∈ Fin)
4645mptexd 7094 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))) ∈ V)
4738, 43, 44, 46fvmptd 6876 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (𝐹𝑐) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
48 simpr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐴) ∧ 𝑗 = 𝐾) → 𝑗 = 𝐾)
4948oveq2d 7284 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐴) ∧ 𝑗 = 𝐾) → (1...𝑗) = (1...𝐾))
5049sumeq1d 15394 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐴) ∧ 𝑗 = 𝐾) → Σ𝑙 ∈ (1...𝑗)(𝑐𝑙) = Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))
5148, 50oveq12d 7286 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐴) ∧ 𝑗 = 𝐾) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)) = (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)))
52 1zzd 12334 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℤ)
533nn0zd 12406 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ ℤ)
542nnge1d 12004 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ≤ 𝐾)
552nnred 11971 . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ ℝ)
5655leidd 11524 . . . . . . . . . . . . . . . 16 (𝜑𝐾𝐾)
5752, 53, 53, 54, 56elfzd 13229 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ (1...𝐾))
5857adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → 𝐾 ∈ (1...𝐾))
59 ovexd 7303 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)) ∈ V)
6047, 51, 58, 59fvmptd 6876 . . . . . . . . . . . . 13 ((𝜑𝑐𝐴) → ((𝐹𝑐)‘𝐾) = (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)))
6160oveq2d 7284 . . . . . . . . . . . 12 ((𝜑𝑐𝐴) → ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)) = ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))))
621nn0cnd 12278 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℂ)
6362adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → 𝑁 ∈ ℂ)
6455recnd 10987 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ ℂ)
6564adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → 𝐾 ∈ ℂ)
6663, 65addcomd 11160 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (𝑁 + 𝐾) = (𝐾 + 𝑁))
6766oveq1d 7283 . . . . . . . . . . . . 13 ((𝜑𝑐𝐴) → ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))) = ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))))
68 1zzd 12334 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 1 ∈ ℤ)
6953ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ∈ ℤ)
7069peano2zd 12411 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝐾 + 1) ∈ ℤ)
71 elfzelz 13238 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...𝐾) → 𝑙 ∈ ℤ)
7271adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ ℤ)
73 elfzle1 13241 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...𝐾) → 1 ≤ 𝑙)
7473adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 1 ≤ 𝑙)
7572zred 12408 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ ℝ)
7655ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ∈ ℝ)
7770zred 12408 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝐾 + 1) ∈ ℝ)
78 elfzle2 13242 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ (1...𝐾) → 𝑙𝐾)
7978adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙𝐾)
8076lep1d 11889 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ≤ (𝐾 + 1))
8175, 76, 77, 79, 80letrd 11115 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ≤ (𝐾 + 1))
8268, 70, 72, 74, 81elfzd 13229 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ (1...(𝐾 + 1)))
835eleq2i 2831 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐𝐴𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)})
8483biimpi 215 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐𝐴𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)})
8584adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑐𝐴) → 𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)})
86 vex 3434 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑐 ∈ V
87 feq1 6577 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔 = 𝑐 → (𝑔:(1...(𝐾 + 1))⟶ℕ0𝑐:(1...(𝐾 + 1))⟶ℕ0))
88 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔 = 𝑐𝑖 ∈ (1...(𝐾 + 1))) → 𝑔 = 𝑐)
8988fveq1d 6770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 = 𝑐𝑖 ∈ (1...(𝐾 + 1))) → (𝑔𝑖) = (𝑐𝑖))
9089sumeq2dv 15396 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔 = 𝑐 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖))
9190eqeq1d 2741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔 = 𝑐 → (Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖) = 𝑁))
9287, 91anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 = 𝑐 → ((𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁) ↔ (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖) = 𝑁)))
9386, 92elab 3610 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)} ↔ (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖) = 𝑁))
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑐𝐴) → (𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)} ↔ (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖) = 𝑁)))
9594biimpd 228 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑐𝐴) → (𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)} → (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖) = 𝑁)))
9685, 95mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖) = 𝑁))
9796simpld 494 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
9897adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
9998ffvelrnda 6955 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℕ0)
10082, 99mpdan 683 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝑐𝑙) ∈ ℕ0)
10145, 100fsumnn0cl 15429 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) ∈ ℕ0)
102101nn0cnd 12278 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) ∈ ℂ)
10365, 63, 102pnpcand 11352 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))) = (𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)))
104 eqid 2739 . . . . . . . . . . . . . . . . . . . . . . . 24 1 = 1
105 1p0e1 12080 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 0) = 1
106104, 105eqtr4i 2770 . . . . . . . . . . . . . . . . . . . . . . 23 1 = (1 + 0)
107106a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 = (1 + 0))
108 1red 10960 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 ∈ ℝ)
109 0le1 11481 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 1
110109a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ≤ 1)
111108, 11, 55, 108, 54, 110le2addd 11577 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1 + 0) ≤ (𝐾 + 1))
112107, 111eqbrtrd 5100 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ≤ (𝐾 + 1))
11353peano2zd 12411 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾 + 1) ∈ ℤ)
114 eluz 12578 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ) → ((𝐾 + 1) ∈ (ℤ‘1) ↔ 1 ≤ (𝐾 + 1)))
11552, 113, 114syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐾 + 1) ∈ (ℤ‘1) ↔ 1 ≤ (𝐾 + 1)))
116112, 115mpbird 256 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 + 1) ∈ (ℤ‘1))
117116adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → (𝐾 + 1) ∈ (ℤ‘1))
11897ffvelrnda 6955 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℕ0)
119118nn0cnd 12278 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℂ)
120 fveq2 6768 . . . . . . . . . . . . . . . . . . 19 (𝑙 = (𝐾 + 1) → (𝑐𝑙) = (𝑐‘(𝐾 + 1)))
121117, 119, 120fsumm1 15444 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙) = (Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐𝑙) + (𝑐‘(𝐾 + 1))))
122 1cnd 10954 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑐𝐴) → 1 ∈ ℂ)
12365, 122pncand 11316 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → ((𝐾 + 1) − 1) = 𝐾)
124123oveq2d 7284 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → (1...((𝐾 + 1) − 1)) = (1...𝐾))
125124sumeq1d 15394 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐𝑙) = Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))
126125oveq1d 7283 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → (Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐𝑙) + (𝑐‘(𝐾 + 1))) = (Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) + (𝑐‘(𝐾 + 1))))
127121, 126eqtrd 2779 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙) = (Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) + (𝑐‘(𝐾 + 1))))
128127eqcomd 2745 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → (Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) + (𝑐‘(𝐾 + 1))) = Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙))
129 fveq2 6768 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (𝑐𝑙) = (𝑐𝑖))
130 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 𝑖(1...(𝐾 + 1))
131 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 𝑙(1...(𝐾 + 1))
132 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 𝑖(𝑐𝑙)
133 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 𝑙(𝑐𝑖)
134129, 130, 131, 132, 133cbvsum 15388 . . . . . . . . . . . . . . . . . 18 Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖)
135134a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖))
13696simprd 495 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖) = 𝑁)
137135, 136eqtrd 2779 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙) = 𝑁)
138128, 137eqtrd 2779 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → (Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) + (𝑐‘(𝐾 + 1))) = 𝑁)
139 1zzd 12334 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → 1 ∈ ℤ)
14053adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → 𝐾 ∈ ℤ)
141140peano2zd 12411 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → (𝐾 + 1) ∈ ℤ)
142 1e0p1 12461 . . . . . . . . . . . . . . . . . . . . 21 1 = (0 + 1)
143142a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → 1 = (0 + 1))
144 0red 10962 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → 0 ∈ ℝ)
14555adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → 𝐾 ∈ ℝ)
146 1red 10960 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → 1 ∈ ℝ)
14711, 55, 12ltled 11106 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 0 ≤ 𝐾)
148147adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → 0 ≤ 𝐾)
149144, 145, 146, 148leadd1dd 11572 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → (0 + 1) ≤ (𝐾 + 1))
150143, 149eqbrtrd 5100 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → 1 ≤ (𝐾 + 1))
15155, 55, 108, 56leadd1dd 11572 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 + 1) ≤ (𝐾 + 1))
152151adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → (𝐾 + 1) ≤ (𝐾 + 1))
153139, 141, 141, 150, 152elfzd 13229 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → (𝐾 + 1) ∈ (1...(𝐾 + 1)))
15497, 153ffvelrnd 6956 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → (𝑐‘(𝐾 + 1)) ∈ ℕ0)
155154nn0cnd 12278 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → (𝑐‘(𝐾 + 1)) ∈ ℂ)
15663, 102, 155subaddd 11333 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → ((𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)) = (𝑐‘(𝐾 + 1)) ↔ (Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) + (𝑐‘(𝐾 + 1))) = 𝑁))
157138, 156mpbird 256 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)) = (𝑐‘(𝐾 + 1)))
158103, 157eqtrd 2779 . . . . . . . . . . . . 13 ((𝜑𝑐𝐴) → ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))) = (𝑐‘(𝐾 + 1)))
15967, 158eqtrd 2779 . . . . . . . . . . . 12 ((𝜑𝑐𝐴) → ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))) = (𝑐‘(𝐾 + 1)))
16061, 159eqtrd 2779 . . . . . . . . . . 11 ((𝜑𝑐𝐴) → ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1)))
1611603adant3 1130 . . . . . . . . . 10 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1)))
162161adantr 480 . . . . . . . . 9 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1)))
163 simpr 484 . . . . . . . . . . 11 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → 𝑘 = (𝐾 + 1))
164163fveq2d 6772 . . . . . . . . . 10 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → (𝑐𝑘) = (𝑐‘(𝐾 + 1)))
165164eqcomd 2745 . . . . . . . . 9 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → (𝑐‘(𝐾 + 1)) = (𝑐𝑘))
166162, 165eqtrd 2779 . . . . . . . 8 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)) = (𝑐𝑘))
16747fveq1d 6770 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → ((𝐹𝑐)‘1) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘1))
168167oveq1d 7283 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (((𝐹𝑐)‘1) − 1) = (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘1) − 1))
169 eqidd 2740 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
170 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴) ∧ 𝑗 = 1) → 𝑗 = 1)
171170oveq2d 7284 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑗 = 1) → (1...𝑗) = (1...1))
172171sumeq1d 15394 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴) ∧ 𝑗 = 1) → Σ𝑙 ∈ (1...𝑗)(𝑐𝑙) = Σ𝑙 ∈ (1...1)(𝑐𝑙))
173170, 172oveq12d 7286 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴) ∧ 𝑗 = 1) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)) = (1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)))
174146leidd 11524 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → 1 ≤ 1)
17554adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → 1 ≤ 𝐾)
176139, 140, 139, 174, 175elfzd 13229 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → 1 ∈ (1...𝐾))
177 ovexd 7303 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → (1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)) ∈ V)
178169, 173, 176, 177fvmptd 6876 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘1) = (1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)))
179178oveq1d 7283 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘1) − 1) = ((1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)) − 1))
180 fzfid 13674 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → (1...1) ∈ Fin)
181 1zzd 12334 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ∈ ℤ)
182140adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝐾 ∈ ℤ)
183182peano2zd 12411 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → (𝐾 + 1) ∈ ℤ)
184 elfzelz 13238 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 ∈ (1...1) → 𝑙 ∈ ℤ)
185184adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ ℤ)
186 elfzle1 13241 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 ∈ (1...1) → 1 ≤ 𝑙)
187186adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ≤ 𝑙)
188185zred 12408 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ ℝ)
189 0red 10962 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 0 ∈ ℝ)
190 1red 10960 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ∈ ℝ)
191189, 190readdcld 10988 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → (0 + 1) ∈ ℝ)
192183zred 12408 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → (𝐾 + 1) ∈ ℝ)
193 elfzle2 13242 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 ∈ (1...1) → 𝑙 ≤ 1)
194193adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ 1)
195142a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 1 = (0 + 1))
196194, 195breqtrd 5104 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ (0 + 1))
197149adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → (0 + 1) ≤ (𝐾 + 1))
198188, 191, 192, 196, 197letrd 11115 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ (𝐾 + 1))
199181, 183, 185, 187, 198elfzd 13229 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ (1...(𝐾 + 1)))
200118adantlr 711 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℕ0)
201199, 200mpdan 683 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → (𝑐𝑙) ∈ ℕ0)
202180, 201fsumnn0cl 15429 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...1)(𝑐𝑙) ∈ ℕ0)
203202nn0cnd 12278 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...1)(𝑐𝑙) ∈ ℂ)
204122, 203pncan2d 11317 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → ((1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)) − 1) = Σ𝑙 ∈ (1...1)(𝑐𝑙))
205139, 141, 139, 174, 150elfzd 13229 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → 1 ∈ (1...(𝐾 + 1)))
20697, 205ffvelrnd 6956 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → (𝑐‘1) ∈ ℕ0)
207206nn0cnd 12278 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → (𝑐‘1) ∈ ℂ)
208 fveq2 6768 . . . . . . . . . . . . . . . . . 18 (𝑙 = 1 → (𝑐𝑙) = (𝑐‘1))
209208fsum1 15440 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℤ ∧ (𝑐‘1) ∈ ℂ) → Σ𝑙 ∈ (1...1)(𝑐𝑙) = (𝑐‘1))
210139, 207, 209syl2anc 583 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...1)(𝑐𝑙) = (𝑐‘1))
211204, 210eqtrd 2779 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → ((1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)) − 1) = (𝑐‘1))
212179, 211eqtrd 2779 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘1) − 1) = (𝑐‘1))
213168, 212eqtrd 2779 . . . . . . . . . . . . 13 ((𝜑𝑐𝐴) → (((𝐹𝑐)‘1) − 1) = (𝑐‘1))
2142133adant3 1130 . . . . . . . . . . . 12 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → (((𝐹𝑐)‘1) − 1) = (𝑐‘1))
215214adantr 480 . . . . . . . . . . 11 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (((𝐹𝑐)‘1) − 1) = (𝑐‘1))
216215adantr 480 . . . . . . . . . 10 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (((𝐹𝑐)‘1) − 1) = (𝑐‘1))
217 simpr 484 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → 𝑘 = 1)
218217fveq2d 6772 . . . . . . . . . . 11 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (𝑐𝑘) = (𝑐‘1))
219218eqcomd 2745 . . . . . . . . . 10 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (𝑐‘1) = (𝑐𝑘))
220216, 219eqtrd 2779 . . . . . . . . 9 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (((𝐹𝑐)‘1) − 1) = (𝑐𝑘))
2214a1i 11 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐹 = (𝑎𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙)))))
222 simpllr 772 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑎 = 𝑐)
223222fveq1d 6770 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑎𝑙) = (𝑐𝑙))
224223sumeq2dv 15396 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → Σ𝑙 ∈ (1...𝑗)(𝑎𝑙) = Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))
225224oveq2d 7284 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙)) = (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))
226225mpteq2dva 5178 . . . . . . . . . . . . . 14 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
227 simpll2 1211 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑐𝐴)
228 fzfid 13674 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...𝐾) ∈ Fin)
229228mptexd 7094 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))) ∈ V)
230221, 226, 227, 229fvmptd 6876 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝐹𝑐) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
231230fveq1d 6770 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐹𝑐)‘𝑘) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘))
232230fveq1d 6770 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐹𝑐)‘(𝑘 − 1)) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1)))
233231, 232oveq12d 7286 . . . . . . . . . . 11 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) = (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1))))
234233oveq1d 7283 . . . . . . . . . 10 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1) = ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1))) − 1))
235 eqidd 2740 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
236 simpr 484 . . . . . . . . . . . . . . 15 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘)
237236oveq2d 7284 . . . . . . . . . . . . . . . 16 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → (1...𝑗) = (1...𝑘))
238237sumeq1d 15394 . . . . . . . . . . . . . . 15 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → Σ𝑙 ∈ (1...𝑗)(𝑐𝑙) = Σ𝑙 ∈ (1...𝑘)(𝑐𝑙))
239236, 238oveq12d 7286 . . . . . . . . . . . . . 14 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)) = (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)))
240 1zzd 12334 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℤ)
2411403adant3 1130 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝐾 ∈ ℤ)
242241adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝐾 ∈ ℤ)
243242adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ)
244 elfznn 13267 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ∈ ℕ)
2452443ad2ant3 1133 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℕ)
246245nnzd 12407 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℤ)
247246adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℤ)
248247adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ)
249245nnge1d 12004 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 1 ≤ 𝑘)
250249adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ≤ 𝑘)
251250adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ 𝑘)
252 simpl3 1191 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ (1...(𝐾 + 1)))
253 1zzd 12334 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ∈ ℤ)
254242peano2zd 12411 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ∈ ℤ)
255 elfz 13227 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℤ ∧ 1 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ) → (𝑘 ∈ (1...(𝐾 + 1)) ↔ (1 ≤ 𝑘𝑘 ≤ (𝐾 + 1))))
256247, 253, 254, 255syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ∈ (1...(𝐾 + 1)) ↔ (1 ≤ 𝑘𝑘 ≤ (𝐾 + 1))))
257256biimpd 228 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ∈ (1...(𝐾 + 1)) → (1 ≤ 𝑘𝑘 ≤ (𝐾 + 1))))
258252, 257mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (1 ≤ 𝑘𝑘 ≤ (𝐾 + 1)))
259258simprd 495 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≤ (𝐾 + 1))
260 neqne 2952 . . . . . . . . . . . . . . . . . . . . 21 𝑘 = (𝐾 + 1) → 𝑘 ≠ (𝐾 + 1))
261260adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≠ (𝐾 + 1))
262261necomd 3000 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑘)
263259, 262jca 511 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑘))
264247zred 12408 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℝ)
265254zred 12408 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
266264, 265ltlend 11103 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 < (𝐾 + 1) ↔ (𝑘 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑘)))
267263, 266mpbird 256 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 < (𝐾 + 1))
268 zleltp1 12354 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘𝐾𝑘 < (𝐾 + 1)))
269247, 242, 268syl2anc 583 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘𝐾𝑘 < (𝐾 + 1)))
270267, 269mpbird 256 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘𝐾)
271270adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘𝐾)
272240, 243, 248, 251, 271elfzd 13229 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (1...𝐾))
273 ovexd 7303 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) ∈ V)
274235, 239, 272, 273fvmptd 6876 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) = (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)))
275 simpr 484 . . . . . . . . . . . . . . 15 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → 𝑗 = (𝑘 − 1))
276275oveq2d 7284 . . . . . . . . . . . . . . . 16 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → (1...𝑗) = (1...(𝑘 − 1)))
277276sumeq1d 15394 . . . . . . . . . . . . . . 15 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → Σ𝑙 ∈ (1...𝑗)(𝑐𝑙) = Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))
278275, 277oveq12d 7286 . . . . . . . . . . . . . 14 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)) = ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)))
279 1zzd 12334 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℤ)
28053ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ)
2812803impa 1108 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ)
282244nnzd 12407 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ∈ ℤ)
283282adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℤ)
284283adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ)
2852843impa 1108 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ)
286285, 279zsubcld 12413 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℤ)
287 neqne 2952 . . . . . . . . . . . . . . . . . . . . . 22 𝑘 = 1 → 𝑘 ≠ 1)
2882873ad2ant3 1133 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≠ 1)
2891083ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℝ)
290285zred 12408 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℝ)
291 simp2 1135 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (1...(𝐾 + 1)))
292 elfzle1 13241 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (1...(𝐾 + 1)) → 1 ≤ 𝑘)
293291, 292syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ 𝑘)
294289, 290, 293leltned 11111 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 < 𝑘𝑘 ≠ 1))
295288, 294mpbird 256 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 < 𝑘)
296279, 285zltp1led 39968 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 < 𝑘 ↔ (1 + 1) ≤ 𝑘))
297295, 296mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 + 1) ≤ 𝑘)
298 leaddsub 11434 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((1 + 1) ≤ 𝑘 ↔ 1 ≤ (𝑘 − 1)))
299289, 289, 290, 298syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + 1) ≤ 𝑘 ↔ 1 ≤ (𝑘 − 1)))
300297, 299mpbid 231 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ (𝑘 − 1))
301286zred 12408 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℝ)
302553ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℝ)
303 1red 10960 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℝ)
304302, 303readdcld 10988 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝐾 + 1) ∈ ℝ)
305304, 303resubcld 11386 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) ∈ ℝ)
306 elfzle2 13242 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ≤ (𝐾 + 1))
3073063ad2ant2 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≤ (𝐾 + 1))
308290, 304, 303, 307lesub1dd 11574 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ≤ ((𝐾 + 1) − 1))
309643ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℂ)
310 1cnd 10954 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℂ)
311309, 310pncand 11316 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) = 𝐾)
312563ad2ant1 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾𝐾)
313311, 312eqbrtrd 5100 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) ≤ 𝐾)
314301, 305, 302, 308, 313letrd 11115 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ≤ 𝐾)
315279, 281, 286, 300, 314elfzd 13229 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
3163153expa 1116 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
3173163adantl2 1165 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
318317adantlr 711 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
319 ovexd 7303 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)) ∈ V)
320235, 278, 318, 319fvmptd 6876 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1)) = ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)))
321274, 320oveq12d 7286 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1))) = ((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))))
322321oveq1d 7283 . . . . . . . . . . 11 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1))) − 1) = (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1))
323248zcnd 12409 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℂ)
324 fzfid 13674 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...𝑘) ∈ Fin)
325 1zzd 12334 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 1 ∈ ℤ)
326243adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝐾 ∈ ℤ)
327326peano2zd 12411 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝐾 + 1) ∈ ℤ)
328 elfznn 13267 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...𝑘) → 𝑙 ∈ ℕ)
329328adantl 481 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℕ)
330329nnzd 12407 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℤ)
331329nnge1d 12004 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 1 ≤ 𝑙)
332329nnred 11971 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℝ)
333264ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
334265ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝐾 + 1) ∈ ℝ)
335 elfzle2 13242 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...𝑘) → 𝑙𝑘)
336335adantl 481 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙𝑘)
337259ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑘 ≤ (𝐾 + 1))
338332, 333, 334, 336, 337letrd 11115 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ≤ (𝐾 + 1))
339325, 327, 330, 331, 338elfzd 13229 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ (1...(𝐾 + 1)))
340973adant3 1130 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
341340adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
342341adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
343342adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
344343ffvelrnda 6955 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℕ0)
345339, 344mpdan 683 . . . . . . . . . . . . . . . 16 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝑐𝑙) ∈ ℕ0)
346324, 345fsumnn0cl 15429 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) ∈ ℕ0)
347346nn0cnd 12278 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) ∈ ℂ)
348 1cnd 10954 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℂ)
349323, 348subcld 11315 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℂ)
350 fzfid 13674 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...(𝑘 − 1)) ∈ Fin)
351 1zzd 12334 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ∈ ℤ)
352243adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝐾 ∈ ℤ)
353352peano2zd 12411 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝐾 + 1) ∈ ℤ)
354 elfznn 13267 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...(𝑘 − 1)) → 𝑙 ∈ ℕ)
355354adantl 481 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℕ)
356355nnzd 12407 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℤ)
357355nnge1d 12004 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ≤ 𝑙)
358355nnred 11971 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℝ)
359264ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑘 ∈ ℝ)
360 1red 10960 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ∈ ℝ)
361359, 360resubcld 11386 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ)
362265ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝐾 + 1) ∈ ℝ)
363 elfzle2 13242 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...(𝑘 − 1)) → 𝑙 ≤ (𝑘 − 1))
364363adantl 481 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ≤ (𝑘 − 1))
365359lem1d 11891 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ≤ 𝑘)
366259ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑘 ≤ (𝐾 + 1))
367361, 359, 362, 365, 366letrd 11115 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ≤ (𝐾 + 1))
368358, 361, 362, 364, 367letrd 11115 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ≤ (𝐾 + 1))
369351, 353, 356, 357, 368elfzd 13229 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ (1...(𝐾 + 1)))
370342adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
371370ffvelrnda 6955 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℕ0)
372369, 371mpdan 683 . . . . . . . . . . . . . . . 16 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑐𝑙) ∈ ℕ0)
373350, 372fsumnn0cl 15429 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙) ∈ ℕ0)
374373nn0cnd 12278 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙) ∈ ℂ)
375323, 347, 349, 374addsub4d 11362 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) = ((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))))
376375oveq1d 7283 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1))
377323, 348nncand 11320 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − (𝑘 − 1)) = 1)
378377oveq1d 7283 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) = (1 + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))))
379378oveq1d 7283 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1))
380347, 374subcld 11315 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)) ∈ ℂ)
381348, 380pncan2d 11317 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)))
3821393adant3 1130 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 1 ∈ ℤ)
383382, 246, 2493jca 1126 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → (1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
384 eluz2 12570 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
385383, 384sylibr 233 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ (ℤ‘1))
386385adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ (ℤ‘1))
387386adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (ℤ‘1))
388345nn0cnd 12278 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝑐𝑙) ∈ ℂ)
389 fveq2 6768 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → (𝑐𝑙) = (𝑐𝑘))
390387, 388, 389fsumm1 15444 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) = (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙) + (𝑐𝑘)))
391390eqcomd 2745 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙) + (𝑐𝑘)) = Σ𝑙 ∈ (1...𝑘)(𝑐𝑙))
392 simp3 1136 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ (1...(𝐾 + 1)))
393340, 392ffvelrnd 6956 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → (𝑐𝑘) ∈ ℕ0)
394393nn0cnd 12278 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → (𝑐𝑘) ∈ ℂ)
395394adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑐𝑘) ∈ ℂ)
396395adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑐𝑘) ∈ ℂ)
397347, 374, 396subaddd 11333 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)) = (𝑐𝑘) ↔ (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙) + (𝑐𝑘)) = Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)))
398391, 397mpbird 256 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)) = (𝑐𝑘))
399381, 398eqtrd 2779 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = (𝑐𝑘))
400379, 399eqtrd 2779 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = (𝑐𝑘))
401376, 400eqtrd 2779 . . . . . . . . . . 11 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = (𝑐𝑘))
402322, 401eqtrd 2779 . . . . . . . . . 10 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1))) − 1) = (𝑐𝑘))
403234, 402eqtrd 2779 . . . . . . . . 9 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1) = (𝑐𝑘))
404220, 403ifeqda 4500 . . . . . . . 8 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)) = (𝑐𝑘))
405166, 404ifeqda 4500 . . . . . . 7 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1))) = (𝑐𝑘))
4064053expa 1116 . . . . . 6 (((𝜑𝑐𝐴) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1))) = (𝑐𝑘))
407406mpteq2dva 5178 . . . . 5 ((𝜑𝑐𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐𝑘)))
40897ffnd 6597 . . . . . . 7 ((𝜑𝑐𝐴) → 𝑐 Fn (1...(𝐾 + 1)))
409 dffn5 6822 . . . . . . . 8 (𝑐 Fn (1...(𝐾 + 1)) ↔ 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐𝑘)))
410409biimpi 215 . . . . . . 7 (𝑐 Fn (1...(𝐾 + 1)) → 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐𝑘)))
411408, 410syl 17 . . . . . 6 ((𝜑𝑐𝐴) → 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐𝑘)))
412411eqcomd 2745 . . . . 5 ((𝜑𝑐𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐𝑘)) = 𝑐)
413407, 412eqtrd 2779 . . . 4 ((𝜑𝑐𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))) = 𝑐)
41437, 413eqtrd 2779 . . 3 ((𝜑𝑐𝐴) → (𝐺‘(𝐹𝑐)) = 𝑐)
415414ralrimiva 3109 . 2 (𝜑 → ∀𝑐𝐴 (𝐺‘(𝐹𝑐)) = 𝑐)
4161, 2, 4, 8, 5, 6sticksstones12a 40093 . 2 (𝜑 → ∀𝑑𝐵 (𝐹‘(𝐺𝑑)) = 𝑑)
4177, 9, 415, 4162fvidf1od 7163 1 (𝜑𝐹:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1085   = wceq 1541  wcel 2109  {cab 2716  wne 2944  wral 3065  Vcvv 3430  ifcif 4464  {csn 4566  cop 4572   class class class wbr 5078  cmpt 5161   Fn wfn 6425  wf 6426  1-1-ontowf1o 6429  cfv 6430  (class class class)co 7268  Fincfn 8707  cc 10853  cr 10854  0cc0 10855  1c1 10856   + caddc 10858   < clt 10993  cle 10994  cmin 11188  cn 11956  0cn0 12216  cz 12302  cuz 12564  ...cfz 13221  Σcsu 15378
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-rep 5213  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-inf2 9360  ax-cnex 10911  ax-resscn 10912  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-mulcom 10919  ax-addass 10920  ax-mulass 10921  ax-distr 10922  ax-i2m1 10923  ax-1ne0 10924  ax-1rid 10925  ax-rnegex 10926  ax-rrecex 10927  ax-cnre 10928  ax-pre-lttri 10929  ax-pre-lttrn 10930  ax-pre-ltadd 10931  ax-pre-mulgt0 10932  ax-pre-sup 10933
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3072  df-rmo 3073  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-int 4885  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-se 5544  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-isom 6439  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-om 7701  df-1st 7817  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-1o 8281  df-er 8472  df-en 8708  df-dom 8709  df-sdom 8710  df-fin 8711  df-sup 9162  df-oi 9230  df-card 9681  df-pnf 10995  df-mnf 10996  df-xr 10997  df-ltxr 10998  df-le 10999  df-sub 11190  df-neg 11191  df-div 11616  df-nn 11957  df-2 12019  df-3 12020  df-n0 12217  df-z 12303  df-uz 12565  df-rp 12713  df-ico 13067  df-fz 13222  df-fzo 13365  df-seq 13703  df-exp 13764  df-hash 14026  df-cj 14791  df-re 14792  df-im 14793  df-sqrt 14927  df-abs 14928  df-clim 15178  df-sum 15379
This theorem is referenced by:  sticksstones13  40095
  Copyright terms: Public domain W3C validator