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 40566
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 12473 . . 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 40561 . 2 (𝜑𝐹:𝐴𝐵)
8 sticksstones12.4 . . 3 𝐺 = (𝑏𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
91, 2, 8, 5, 6sticksstones10 40563 . 2 (𝜑𝐺:𝐵𝐴)
108a1i 11 . . . . . . 7 (𝜑𝐺 = (𝑏𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))))
11 0red 11158 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
122nngt0d 12202 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝐾)
1311, 12ltned 11291 . . . . . . . . . . . 12 (𝜑 → 0 ≠ 𝐾)
1413necomd 2999 . . . . . . . . . . 11 (𝜑𝐾 ≠ 0)
1514neneqd 2948 . . . . . . . . . 10 (𝜑 → ¬ 𝐾 = 0)
1615iffalsed 4497 . . . . . . . . 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 481 . . . . . . . 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 5205 . . . . . . 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 2776 . . . . . 6 (𝜑𝐺 = (𝑏𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
2019adantr 481 . . . . 5 ((𝜑𝑐𝐴) → 𝐺 = (𝑏𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
21 fveq1 6841 . . . . . . . . . 10 (𝑏 = (𝐹𝑐) → (𝑏𝐾) = ((𝐹𝑐)‘𝐾))
2221oveq2d 7373 . . . . . . . . 9 (𝑏 = (𝐹𝑐) → ((𝑁 + 𝐾) − (𝑏𝐾)) = ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)))
23 fveq1 6841 . . . . . . . . . . 11 (𝑏 = (𝐹𝑐) → (𝑏‘1) = ((𝐹𝑐)‘1))
2423oveq1d 7372 . . . . . . . . . 10 (𝑏 = (𝐹𝑐) → ((𝑏‘1) − 1) = (((𝐹𝑐)‘1) − 1))
25 fveq1 6841 . . . . . . . . . . . 12 (𝑏 = (𝐹𝑐) → (𝑏𝑘) = ((𝐹𝑐)‘𝑘))
26 fveq1 6841 . . . . . . . . . . . 12 (𝑏 = (𝐹𝑐) → (𝑏‘(𝑘 − 1)) = ((𝐹𝑐)‘(𝑘 − 1)))
2725, 26oveq12d 7375 . . . . . . . . . . 11 (𝑏 = (𝐹𝑐) → ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) = (((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))))
2827oveq1d 7372 . . . . . . . . . 10 (𝑏 = (𝐹𝑐) → (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1) = ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1))
2924, 28ifeq12d 4507 . . . . . . . . 9 (𝑏 = (𝐹𝑐) → if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)) = if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))
3022, 29ifeq12d 4507 . . . . . . . 8 (𝑏 = (𝐹𝑐) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))) = if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1))))
3130adantr 481 . . . . . . 7 ((𝑏 = (𝐹𝑐) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))) = if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1))))
3231mpteq2dva 5205 . . . . . 6 (𝑏 = (𝐹𝑐) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))))
3332adantl 482 . . . . 5 (((𝜑𝑐𝐴) ∧ 𝑏 = (𝐹𝑐)) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))))
347ffvelcdmda 7035 . . . . 5 ((𝜑𝑐𝐴) → (𝐹𝑐) ∈ 𝐵)
35 fzfid 13878 . . . . . 6 ((𝜑𝑐𝐴) → (1...(𝐾 + 1)) ∈ Fin)
3635mptexd 7174 . . . . 5 ((𝜑𝑐𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))) ∈ V)
3720, 33, 34, 36fvmptd 6955 . . . 4 ((𝜑𝑐𝐴) → (𝐺‘(𝐹𝑐)) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))))
384a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → 𝐹 = (𝑎𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙)))))
39 simpllr 774 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑎 = 𝑐)
4039fveq1d 6844 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑎𝑙) = (𝑐𝑙))
4140sumeq2dv 15588 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → Σ𝑙 ∈ (1...𝑗)(𝑎𝑙) = Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))
4241oveq2d 7373 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙)) = (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))
4342mpteq2dva 5205 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐴) ∧ 𝑎 = 𝑐) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
44 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → 𝑐𝐴)
45 fzfid 13878 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → (1...𝐾) ∈ Fin)
4645mptexd 7174 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))) ∈ V)
4738, 43, 44, 46fvmptd 6955 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (𝐹𝑐) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
48 simpr 485 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐴) ∧ 𝑗 = 𝐾) → 𝑗 = 𝐾)
4948oveq2d 7373 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐴) ∧ 𝑗 = 𝐾) → (1...𝑗) = (1...𝐾))
5049sumeq1d 15586 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐴) ∧ 𝑗 = 𝐾) → Σ𝑙 ∈ (1...𝑗)(𝑐𝑙) = Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))
5148, 50oveq12d 7375 . . . . . . . . . . . . . 14 (((𝜑𝑐𝐴) ∧ 𝑗 = 𝐾) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)) = (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)))
52 1zzd 12534 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℤ)
533nn0zd 12525 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ ℤ)
542nnge1d 12201 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ≤ 𝐾)
552nnred 12168 . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ ℝ)
5655leidd 11721 . . . . . . . . . . . . . . . 16 (𝜑𝐾𝐾)
5752, 53, 53, 54, 56elfzd 13432 . . . . . . . . . . . . . . 15 (𝜑𝐾 ∈ (1...𝐾))
5857adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → 𝐾 ∈ (1...𝐾))
59 ovexd 7392 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)) ∈ V)
6047, 51, 58, 59fvmptd 6955 . . . . . . . . . . . . 13 ((𝜑𝑐𝐴) → ((𝐹𝑐)‘𝐾) = (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)))
6160oveq2d 7373 . . . . . . . . . . . 12 ((𝜑𝑐𝐴) → ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)) = ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))))
621nn0cnd 12475 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℂ)
6362adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → 𝑁 ∈ ℂ)
6455recnd 11183 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ ℂ)
6564adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → 𝐾 ∈ ℂ)
6663, 65addcomd 11357 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (𝑁 + 𝐾) = (𝐾 + 𝑁))
6766oveq1d 7372 . . . . . . . . . . . . 13 ((𝜑𝑐𝐴) → ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))) = ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))))
68 1zzd 12534 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 1 ∈ ℤ)
6953ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ∈ ℤ)
7069peano2zd 12610 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝐾 + 1) ∈ ℤ)
71 elfzelz 13441 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...𝐾) → 𝑙 ∈ ℤ)
7271adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ ℤ)
73 elfzle1 13444 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...𝐾) → 1 ≤ 𝑙)
7473adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 1 ≤ 𝑙)
7572zred 12607 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ ℝ)
7655ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ∈ ℝ)
7770zred 12607 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝐾 + 1) ∈ ℝ)
78 elfzle2 13445 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ (1...𝐾) → 𝑙𝐾)
7978adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙𝐾)
8076lep1d 12086 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ≤ (𝐾 + 1))
8175, 76, 77, 79, 80letrd 11312 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ≤ (𝐾 + 1))
8268, 70, 72, 74, 81elfzd 13432 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ (1...(𝐾 + 1)))
835eleq2i 2829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐𝐴𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)})
8483biimpi 215 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐𝐴𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)})
8584adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑐𝐴) → 𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)})
86 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑐 ∈ V
87 feq1 6649 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔 = 𝑐 → (𝑔:(1...(𝐾 + 1))⟶ℕ0𝑐:(1...(𝐾 + 1))⟶ℕ0))
88 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔 = 𝑐𝑖 ∈ (1...(𝐾 + 1))) → 𝑔 = 𝑐)
8988fveq1d 6844 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 = 𝑐𝑖 ∈ (1...(𝐾 + 1))) → (𝑔𝑖) = (𝑐𝑖))
9089sumeq2dv 15588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑔 = 𝑐 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖))
9190eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑔 = 𝑐 → (Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖) = 𝑁))
9287, 91anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑔 = 𝑐 → ((𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁) ↔ (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖) = 𝑁)))
9386, 92elab 3630 . . . . . . . . . . . . . . . . . . . . . . . 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 495 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
9897adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
9998ffvelcdmda 7035 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℕ0)
10082, 99mpdan 685 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝑐𝑙) ∈ ℕ0)
10145, 100fsumnn0cl 15621 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) ∈ ℕ0)
102101nn0cnd 12475 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) ∈ ℂ)
10365, 63, 102pnpcand 11549 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))) = (𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)))
104 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . 24 1 = 1
105 1p0e1 12277 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 0) = 1
106104, 105eqtr4i 2767 . . . . . . . . . . . . . . . . . . . . . . 23 1 = (1 + 0)
107106a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 = (1 + 0))
108 1red 11156 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 ∈ ℝ)
109 0le1 11678 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 1
110109a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ≤ 1)
111108, 11, 55, 108, 54, 110le2addd 11774 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1 + 0) ≤ (𝐾 + 1))
112107, 111eqbrtrd 5127 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ≤ (𝐾 + 1))
11353peano2zd 12610 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐾 + 1) ∈ ℤ)
114 eluz 12777 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ) → ((𝐾 + 1) ∈ (ℤ‘1) ↔ 1 ≤ (𝐾 + 1)))
11552, 113, 114syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐾 + 1) ∈ (ℤ‘1) ↔ 1 ≤ (𝐾 + 1)))
116112, 115mpbird 256 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 + 1) ∈ (ℤ‘1))
117116adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → (𝐾 + 1) ∈ (ℤ‘1))
11897ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℕ0)
119118nn0cnd 12475 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℂ)
120 fveq2 6842 . . . . . . . . . . . . . . . . . . 19 (𝑙 = (𝐾 + 1) → (𝑐𝑙) = (𝑐‘(𝐾 + 1)))
121117, 119, 120fsumm1 15636 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙) = (Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐𝑙) + (𝑐‘(𝐾 + 1))))
122 1cnd 11150 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑐𝐴) → 1 ∈ ℂ)
12365, 122pncand 11513 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → ((𝐾 + 1) − 1) = 𝐾)
124123oveq2d 7373 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → (1...((𝐾 + 1) − 1)) = (1...𝐾))
125124sumeq1d 15586 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐𝑙) = Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))
126125oveq1d 7372 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → (Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐𝑙) + (𝑐‘(𝐾 + 1))) = (Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) + (𝑐‘(𝐾 + 1))))
127121, 126eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙) = (Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) + (𝑐‘(𝐾 + 1))))
128127eqcomd 2742 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → (Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) + (𝑐‘(𝐾 + 1))) = Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙))
129 fveq2 6842 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (𝑐𝑙) = (𝑐𝑖))
130 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑖(1...(𝐾 + 1))
131 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑙(1...(𝐾 + 1))
132 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑖(𝑐𝑙)
133 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑙(𝑐𝑖)
134129, 130, 131, 132, 133cbvsum 15580 . . . . . . . . . . . . . . . . . 18 Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖)
135134a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖))
13696simprd 496 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐𝑖) = 𝑁)
137135, 136eqtrd 2776 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐𝑙) = 𝑁)
138128, 137eqtrd 2776 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → (Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) + (𝑐‘(𝐾 + 1))) = 𝑁)
139 1zzd 12534 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → 1 ∈ ℤ)
14053adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → 𝐾 ∈ ℤ)
141140peano2zd 12610 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → (𝐾 + 1) ∈ ℤ)
142 1e0p1 12660 . . . . . . . . . . . . . . . . . . . . 21 1 = (0 + 1)
143142a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → 1 = (0 + 1))
144 0red 11158 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → 0 ∈ ℝ)
14555adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → 𝐾 ∈ ℝ)
146 1red 11156 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → 1 ∈ ℝ)
14711, 55, 12ltled 11303 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 0 ≤ 𝐾)
148147adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴) → 0 ≤ 𝐾)
149144, 145, 146, 148leadd1dd 11769 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴) → (0 + 1) ≤ (𝐾 + 1))
150143, 149eqbrtrd 5127 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → 1 ≤ (𝐾 + 1))
15155, 55, 108, 56leadd1dd 11769 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐾 + 1) ≤ (𝐾 + 1))
152151adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → (𝐾 + 1) ≤ (𝐾 + 1))
153139, 141, 141, 150, 152elfzd 13432 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → (𝐾 + 1) ∈ (1...(𝐾 + 1)))
15497, 153ffvelcdmd 7036 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → (𝑐‘(𝐾 + 1)) ∈ ℕ0)
155154nn0cnd 12475 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → (𝑐‘(𝐾 + 1)) ∈ ℂ)
15663, 102, 155subaddd 11530 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → ((𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)) = (𝑐‘(𝐾 + 1)) ↔ (Σ𝑙 ∈ (1...𝐾)(𝑐𝑙) + (𝑐‘(𝐾 + 1))) = 𝑁))
157138, 156mpbird 256 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐𝑙)) = (𝑐‘(𝐾 + 1)))
158103, 157eqtrd 2776 . . . . . . . . . . . . 13 ((𝜑𝑐𝐴) → ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))) = (𝑐‘(𝐾 + 1)))
15967, 158eqtrd 2776 . . . . . . . . . . . 12 ((𝜑𝑐𝐴) → ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐𝑙))) = (𝑐‘(𝐾 + 1)))
16061, 159eqtrd 2776 . . . . . . . . . . 11 ((𝜑𝑐𝐴) → ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1)))
1611603adant3 1132 . . . . . . . . . 10 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1)))
162161adantr 481 . . . . . . . . 9 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1)))
163 simpr 485 . . . . . . . . . . 11 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → 𝑘 = (𝐾 + 1))
164163fveq2d 6846 . . . . . . . . . 10 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → (𝑐𝑘) = (𝑐‘(𝐾 + 1)))
165164eqcomd 2742 . . . . . . . . 9 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → (𝑐‘(𝐾 + 1)) = (𝑐𝑘))
166162, 165eqtrd 2776 . . . . . . . 8 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)) = (𝑐𝑘))
16747fveq1d 6844 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → ((𝐹𝑐)‘1) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘1))
168167oveq1d 7372 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (((𝐹𝑐)‘1) − 1) = (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘1) − 1))
169 eqidd 2737 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
170 simpr 485 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴) ∧ 𝑗 = 1) → 𝑗 = 1)
171170oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑗 = 1) → (1...𝑗) = (1...1))
172171sumeq1d 15586 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴) ∧ 𝑗 = 1) → Σ𝑙 ∈ (1...𝑗)(𝑐𝑙) = Σ𝑙 ∈ (1...1)(𝑐𝑙))
173170, 172oveq12d 7375 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴) ∧ 𝑗 = 1) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)) = (1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)))
174146leidd 11721 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → 1 ≤ 1)
17554adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → 1 ≤ 𝐾)
176139, 140, 139, 174, 175elfzd 13432 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → 1 ∈ (1...𝐾))
177 ovexd 7392 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → (1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)) ∈ V)
178169, 173, 176, 177fvmptd 6955 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘1) = (1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)))
179178oveq1d 7372 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘1) − 1) = ((1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)) − 1))
180 fzfid 13878 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → (1...1) ∈ Fin)
181 1zzd 12534 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ∈ ℤ)
182140adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝐾 ∈ ℤ)
183182peano2zd 12610 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → (𝐾 + 1) ∈ ℤ)
184 elfzelz 13441 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 ∈ (1...1) → 𝑙 ∈ ℤ)
185184adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ ℤ)
186 elfzle1 13444 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 ∈ (1...1) → 1 ≤ 𝑙)
187186adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ≤ 𝑙)
188185zred 12607 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ ℝ)
189 0red 11158 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 0 ∈ ℝ)
190 1red 11156 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ∈ ℝ)
191189, 190readdcld 11184 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → (0 + 1) ∈ ℝ)
192183zred 12607 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → (𝐾 + 1) ∈ ℝ)
193 elfzle2 13445 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 ∈ (1...1) → 𝑙 ≤ 1)
194193adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ 1)
195142a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 1 = (0 + 1))
196194, 195breqtrd 5131 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ (0 + 1))
197149adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → (0 + 1) ≤ (𝐾 + 1))
198188, 191, 192, 196, 197letrd 11312 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ (𝐾 + 1))
199181, 183, 185, 187, 198elfzd 13432 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ (1...(𝐾 + 1)))
200118adantlr 713 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℕ0)
201199, 200mpdan 685 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴) ∧ 𝑙 ∈ (1...1)) → (𝑐𝑙) ∈ ℕ0)
202180, 201fsumnn0cl 15621 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...1)(𝑐𝑙) ∈ ℕ0)
203202nn0cnd 12475 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...1)(𝑐𝑙) ∈ ℂ)
204122, 203pncan2d 11514 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → ((1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)) − 1) = Σ𝑙 ∈ (1...1)(𝑐𝑙))
205139, 141, 139, 174, 150elfzd 13432 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴) → 1 ∈ (1...(𝐾 + 1)))
20697, 205ffvelcdmd 7036 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴) → (𝑐‘1) ∈ ℕ0)
207206nn0cnd 12475 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴) → (𝑐‘1) ∈ ℂ)
208 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑙 = 1 → (𝑐𝑙) = (𝑐‘1))
209208fsum1 15632 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℤ ∧ (𝑐‘1) ∈ ℂ) → Σ𝑙 ∈ (1...1)(𝑐𝑙) = (𝑐‘1))
210139, 207, 209syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐴) → Σ𝑙 ∈ (1...1)(𝑐𝑙) = (𝑐‘1))
211204, 210eqtrd 2776 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐴) → ((1 + Σ𝑙 ∈ (1...1)(𝑐𝑙)) − 1) = (𝑐‘1))
212179, 211eqtrd 2776 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐴) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘1) − 1) = (𝑐‘1))
213168, 212eqtrd 2776 . . . . . . . . . . . . 13 ((𝜑𝑐𝐴) → (((𝐹𝑐)‘1) − 1) = (𝑐‘1))
2142133adant3 1132 . . . . . . . . . . . 12 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → (((𝐹𝑐)‘1) − 1) = (𝑐‘1))
215214adantr 481 . . . . . . . . . . 11 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (((𝐹𝑐)‘1) − 1) = (𝑐‘1))
216215adantr 481 . . . . . . . . . 10 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (((𝐹𝑐)‘1) − 1) = (𝑐‘1))
217 simpr 485 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → 𝑘 = 1)
218217fveq2d 6846 . . . . . . . . . . 11 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (𝑐𝑘) = (𝑐‘1))
219218eqcomd 2742 . . . . . . . . . 10 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (𝑐‘1) = (𝑐𝑘))
220216, 219eqtrd 2776 . . . . . . . . 9 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (((𝐹𝑐)‘1) − 1) = (𝑐𝑘))
2214a1i 11 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐹 = (𝑎𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙)))))
222 simpllr 774 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑎 = 𝑐)
223222fveq1d 6844 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑎𝑙) = (𝑐𝑙))
224223sumeq2dv 15588 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → Σ𝑙 ∈ (1...𝑗)(𝑎𝑙) = Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))
225224oveq2d 7373 . . . . . . . . . . . . . . 15 ((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙)) = (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))
226225mpteq2dva 5205 . . . . . . . . . . . . . 14 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
227 simpll2 1213 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑐𝐴)
228 fzfid 13878 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...𝐾) ∈ Fin)
229228mptexd 7174 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))) ∈ V)
230221, 226, 227, 229fvmptd 6955 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝐹𝑐) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
231230fveq1d 6844 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐹𝑐)‘𝑘) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘))
232230fveq1d 6844 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐹𝑐)‘(𝑘 − 1)) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1)))
233231, 232oveq12d 7375 . . . . . . . . . . 11 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) = (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1))))
234233oveq1d 7372 . . . . . . . . . 10 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1) = ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1))) − 1))
235 eqidd 2737 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙))))
236 simpr 485 . . . . . . . . . . . . . . 15 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘)
237236oveq2d 7373 . . . . . . . . . . . . . . . 16 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → (1...𝑗) = (1...𝑘))
238237sumeq1d 15586 . . . . . . . . . . . . . . 15 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → Σ𝑙 ∈ (1...𝑗)(𝑐𝑙) = Σ𝑙 ∈ (1...𝑘)(𝑐𝑙))
239236, 238oveq12d 7375 . . . . . . . . . . . . . 14 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)) = (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)))
240 1zzd 12534 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℤ)
2411403adant3 1132 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝐾 ∈ ℤ)
242241adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝐾 ∈ ℤ)
243242adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ)
244 elfznn 13470 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ∈ ℕ)
2452443ad2ant3 1135 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℕ)
246245nnzd 12526 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℤ)
247246adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℤ)
248247adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ)
249245nnge1d 12201 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 1 ≤ 𝑘)
250249adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ≤ 𝑘)
251250adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ 𝑘)
252 simpl3 1193 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ (1...(𝐾 + 1)))
253 1zzd 12534 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ∈ ℤ)
254242peano2zd 12610 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ∈ ℤ)
255 elfz 13430 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℤ ∧ 1 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ) → (𝑘 ∈ (1...(𝐾 + 1)) ↔ (1 ≤ 𝑘𝑘 ≤ (𝐾 + 1))))
256247, 253, 254, 255syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 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 496 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≤ (𝐾 + 1))
260 neqne 2951 . . . . . . . . . . . . . . . . . . . . 21 𝑘 = (𝐾 + 1) → 𝑘 ≠ (𝐾 + 1))
261260adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≠ (𝐾 + 1))
262261necomd 2999 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑘)
263259, 262jca 512 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑘))
264247zred 12607 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℝ)
265254zred 12607 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
266264, 265ltlend 11300 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 < (𝐾 + 1) ↔ (𝑘 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑘)))
267263, 266mpbird 256 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 < (𝐾 + 1))
268 zleltp1 12554 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘𝐾𝑘 < (𝐾 + 1)))
269247, 242, 268syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘𝐾𝑘 < (𝐾 + 1)))
270267, 269mpbird 256 . . . . . . . . . . . . . . . 16 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘𝐾)
271270adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘𝐾)
272240, 243, 248, 251, 271elfzd 13432 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (1...𝐾))
273 ovexd 7392 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) ∈ V)
274235, 239, 272, 273fvmptd 6955 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) = (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)))
275 simpr 485 . . . . . . . . . . . . . . 15 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → 𝑗 = (𝑘 − 1))
276275oveq2d 7373 . . . . . . . . . . . . . . . 16 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → (1...𝑗) = (1...(𝑘 − 1)))
277276sumeq1d 15586 . . . . . . . . . . . . . . 15 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → Σ𝑙 ∈ (1...𝑗)(𝑐𝑙) = Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))
278275, 277oveq12d 7375 . . . . . . . . . . . . . 14 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)) = ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)))
279 1zzd 12534 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℤ)
28053ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ)
2812803impa 1110 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ)
282244nnzd 12526 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ∈ ℤ)
283282adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℤ)
284283adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ)
2852843impa 1110 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ)
286285, 279zsubcld 12612 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℤ)
287 neqne 2951 . . . . . . . . . . . . . . . . . . . . . 22 𝑘 = 1 → 𝑘 ≠ 1)
2882873ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≠ 1)
2891083ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℝ)
290285zred 12607 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℝ)
291 simp2 1137 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (1...(𝐾 + 1)))
292 elfzle1 13444 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (1...(𝐾 + 1)) → 1 ≤ 𝑘)
293291, 292syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ 𝑘)
294289, 290, 293leltned 11308 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 < 𝑘𝑘 ≠ 1))
295288, 294mpbird 256 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 < 𝑘)
296279, 285zltp1led 40437 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 < 𝑘 ↔ (1 + 1) ≤ 𝑘))
297295, 296mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 + 1) ≤ 𝑘)
298 leaddsub 11631 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((1 + 1) ≤ 𝑘 ↔ 1 ≤ (𝑘 − 1)))
299289, 289, 290, 298syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + 1) ≤ 𝑘 ↔ 1 ≤ (𝑘 − 1)))
300297, 299mpbid 231 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ (𝑘 − 1))
301286zred 12607 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℝ)
302553ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℝ)
303 1red 11156 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℝ)
304302, 303readdcld 11184 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝐾 + 1) ∈ ℝ)
305304, 303resubcld 11583 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) ∈ ℝ)
306 elfzle2 13445 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ≤ (𝐾 + 1))
3073063ad2ant2 1134 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≤ (𝐾 + 1))
308290, 304, 303, 307lesub1dd 11771 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ≤ ((𝐾 + 1) − 1))
309643ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℂ)
310 1cnd 11150 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℂ)
311309, 310pncand 11513 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) = 𝐾)
312563ad2ant1 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾𝐾)
313311, 312eqbrtrd 5127 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) ≤ 𝐾)
314301, 305, 302, 308, 313letrd 11312 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ≤ 𝐾)
315279, 281, 286, 300, 314elfzd 13432 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
3163153expa 1118 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
3173163adantl2 1167 . . . . . . . . . . . . . . 15 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
318317adantlr 713 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
319 ovexd 7392 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)) ∈ V)
320235, 278, 318, 319fvmptd 6955 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1)) = ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)))
321274, 320oveq12d 7375 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1))) = ((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))))
322321oveq1d 7372 . . . . . . . . . . 11 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1))) − 1) = (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1))
323248zcnd 12608 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℂ)
324 fzfid 13878 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...𝑘) ∈ Fin)
325 1zzd 12534 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 1 ∈ ℤ)
326243adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝐾 ∈ ℤ)
327326peano2zd 12610 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝐾 + 1) ∈ ℤ)
328 elfznn 13470 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...𝑘) → 𝑙 ∈ ℕ)
329328adantl 482 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℕ)
330329nnzd 12526 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℤ)
331329nnge1d 12201 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 1 ≤ 𝑙)
332329nnred 12168 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℝ)
333264ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
334265ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝐾 + 1) ∈ ℝ)
335 elfzle2 13445 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...𝑘) → 𝑙𝑘)
336335adantl 482 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙𝑘)
337259ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑘 ≤ (𝐾 + 1))
338332, 333, 334, 336, 337letrd 11312 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ≤ (𝐾 + 1))
339325, 327, 330, 331, 338elfzd 13432 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ (1...(𝐾 + 1)))
340973adant3 1132 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
341340adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
342341adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
343342adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
344343ffvelcdmda 7035 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℕ0)
345339, 344mpdan 685 . . . . . . . . . . . . . . . 16 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝑐𝑙) ∈ ℕ0)
346324, 345fsumnn0cl 15621 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) ∈ ℕ0)
347346nn0cnd 12475 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) ∈ ℂ)
348 1cnd 11150 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℂ)
349323, 348subcld 11512 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℂ)
350 fzfid 13878 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...(𝑘 − 1)) ∈ Fin)
351 1zzd 12534 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ∈ ℤ)
352243adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝐾 ∈ ℤ)
353352peano2zd 12610 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝐾 + 1) ∈ ℤ)
354 elfznn 13470 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...(𝑘 − 1)) → 𝑙 ∈ ℕ)
355354adantl 482 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℕ)
356355nnzd 12526 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℤ)
357355nnge1d 12201 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ≤ 𝑙)
358355nnred 12168 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℝ)
359264ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑘 ∈ ℝ)
360 1red 11156 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ∈ ℝ)
361359, 360resubcld 11583 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ)
362265ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝐾 + 1) ∈ ℝ)
363 elfzle2 13445 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (1...(𝑘 − 1)) → 𝑙 ≤ (𝑘 − 1))
364363adantl 482 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ≤ (𝑘 − 1))
365359lem1d 12088 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ≤ 𝑘)
366259ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑘 ≤ (𝐾 + 1))
367361, 359, 362, 365, 366letrd 11312 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ≤ (𝐾 + 1))
368358, 361, 362, 364, 367letrd 11312 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ≤ (𝐾 + 1))
369351, 353, 356, 357, 368elfzd 13432 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ (1...(𝐾 + 1)))
370342adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
371370ffvelcdmda 7035 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐𝑙) ∈ ℕ0)
372369, 371mpdan 685 . . . . . . . . . . . . . . . 16 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑐𝑙) ∈ ℕ0)
373350, 372fsumnn0cl 15621 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙) ∈ ℕ0)
374373nn0cnd 12475 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙) ∈ ℂ)
375323, 347, 349, 374addsub4d 11559 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) = ((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))))
376375oveq1d 7372 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1))
377323, 348nncand 11517 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − (𝑘 − 1)) = 1)
378377oveq1d 7372 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) = (1 + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))))
379378oveq1d 7372 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1))
380347, 374subcld 11512 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)) ∈ ℂ)
381348, 380pncan2d 11514 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)))
3821393adant3 1132 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 1 ∈ ℤ)
383382, 246, 2493jca 1128 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → (1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
384 eluz2 12769 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
385383, 384sylibr 233 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ (ℤ‘1))
386385adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ (ℤ‘1))
387386adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (ℤ‘1))
388345nn0cnd 12475 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝑐𝑙) ∈ ℂ)
389 fveq2 6842 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → (𝑐𝑙) = (𝑐𝑘))
390387, 388, 389fsumm1 15636 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) = (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙) + (𝑐𝑘)))
391390eqcomd 2742 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙) + (𝑐𝑘)) = Σ𝑙 ∈ (1...𝑘)(𝑐𝑙))
392 simp3 1138 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ (1...(𝐾 + 1)))
393340, 392ffvelcdmd 7036 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → (𝑐𝑘) ∈ ℕ0)
394393nn0cnd 12475 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → (𝑐𝑘) ∈ ℂ)
395394adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑐𝑘) ∈ ℂ)
396395adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑐𝑘) ∈ ℂ)
397347, 374, 396subaddd 11530 . . . . . . . . . . . . . . 15 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)) = (𝑐𝑘) ↔ (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙) + (𝑐𝑘)) = Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)))
398391, 397mpbird 256 . . . . . . . . . . . . . 14 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙)) = (𝑐𝑘))
399381, 398eqtrd 2776 . . . . . . . . . . . . 13 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = (𝑐𝑘))
400379, 399eqtrd 2776 . . . . . . . . . . . 12 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = (𝑐𝑘))
401376, 400eqtrd 2776 . . . . . . . . . . 11 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐𝑙))) − 1) = (𝑐𝑘))
402322, 401eqtrd 2776 . . . . . . . . . 10 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐𝑙)))‘(𝑘 − 1))) − 1) = (𝑐𝑘))
403234, 402eqtrd 2776 . . . . . . . . 9 ((((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1) = (𝑐𝑘))
404220, 403ifeqda 4522 . . . . . . . 8 (((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)) = (𝑐𝑘))
405166, 404ifeqda 4522 . . . . . . 7 ((𝜑𝑐𝐴𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1))) = (𝑐𝑘))
4064053expa 1118 . . . . . 6 (((𝜑𝑐𝐴) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1))) = (𝑐𝑘))
407406mpteq2dva 5205 . . . . 5 ((𝜑𝑐𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐𝑘)))
40897ffnd 6669 . . . . . . 7 ((𝜑𝑐𝐴) → 𝑐 Fn (1...(𝐾 + 1)))
409 dffn5 6901 . . . . . . . 8 (𝑐 Fn (1...(𝐾 + 1)) ↔ 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐𝑘)))
410409biimpi 215 . . . . . . 7 (𝑐 Fn (1...(𝐾 + 1)) → 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐𝑘)))
411408, 410syl 17 . . . . . 6 ((𝜑𝑐𝐴) → 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐𝑘)))
412411eqcomd 2742 . . . . 5 ((𝜑𝑐𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐𝑘)) = 𝑐)
413407, 412eqtrd 2776 . . . 4 ((𝜑𝑐𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹𝑐)‘1) − 1), ((((𝐹𝑐)‘𝑘) − ((𝐹𝑐)‘(𝑘 − 1))) − 1)))) = 𝑐)
41437, 413eqtrd 2776 . . 3 ((𝜑𝑐𝐴) → (𝐺‘(𝐹𝑐)) = 𝑐)
415414ralrimiva 3143 . 2 (𝜑 → ∀𝑐𝐴 (𝐺‘(𝐹𝑐)) = 𝑐)
4161, 2, 4, 8, 5, 6sticksstones12a 40565 . 2 (𝜑 → ∀𝑑𝐵 (𝐹‘(𝐺𝑑)) = 𝑑)
4177, 9, 415, 4162fvidf1od 7244 1 (𝜑𝐹:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  {cab 2713  wne 2943  wral 3064  Vcvv 3445  ifcif 4486  {csn 4586  cop 4592   class class class wbr 5105  cmpt 5188   Fn wfn 6491  wf 6492  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  Fincfn 8883  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   < clt 11189  cle 11190  cmin 11385  cn 12153  0cn0 12413  cz 12499  cuz 12763  ...cfz 13424  Σcsu 15570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-ico 13270  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571
This theorem is referenced by:  sticksstones13  40567
  Copyright terms: Public domain W3C validator