Theorem sticksstones12 41562

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.

Step	Hyp	Ref	Expression
1		sticksstones12.1	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
2		sticksstones12.2	. . . 4 ⊢ (𝜑 → 𝐾 ∈ ℕ)
3	2	nnnn0d 12554	. . 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...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}
7	1, 3, 4, 5, 6	sticksstones8 41557	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
8		sticksstones12.4	. . 3 ⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
9	1, 2, 8, 5, 6	sticksstones10 41559	. 2 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
10	8	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))))
11		0red 11239	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
12	2	nngt0d 12283	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝐾)
13	11, 12	ltned 11372	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ 𝐾)
14	13	necomd 2991	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ≠ 0)
15	14	neneqd 2940	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝐾 = 0)
16	15	iffalsed 4535	. . . . . . . . 9 ⊢ (𝜑 → if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))
17	16	adantr 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)))))
18	17	mpteq2dva 5242	. . . . . . 7 ⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))) = (𝑏 ∈ 𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
19	10, 18	eqtrd 2767	. . . . . 6 ⊢ (𝜑 → 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
20	19	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
21		fveq1 6890	. . . . . . . . . 10 ⊢ (𝑏 = (𝐹‘𝑐) → (𝑏‘𝐾) = ((𝐹‘𝑐)‘𝐾))
22	21	oveq2d 7430	. . . . . . . . 9 ⊢ (𝑏 = (𝐹‘𝑐) → ((𝑁 + 𝐾) − (𝑏‘𝐾)) = ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)))
23		fveq1 6890	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐹‘𝑐) → (𝑏‘1) = ((𝐹‘𝑐)‘1))
24	23	oveq1d 7429	. . . . . . . . . 10 ⊢ (𝑏 = (𝐹‘𝑐) → ((𝑏‘1) − 1) = (((𝐹‘𝑐)‘1) − 1))
25		fveq1 6890	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝐹‘𝑐) → (𝑏‘𝑘) = ((𝐹‘𝑐)‘𝑘))
26		fveq1 6890	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝐹‘𝑐) → (𝑏‘(𝑘 − 1)) = ((𝐹‘𝑐)‘(𝑘 − 1)))
27	25, 26	oveq12d 7432	. . . . . . . . . . 11 ⊢ (𝑏 = (𝐹‘𝑐) → ((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) = (((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))))
28	27	oveq1d 7429	. . . . . . . . . 10 ⊢ (𝑏 = (𝐹‘𝑐) → (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1) = ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))
29	24, 28	ifeq12d 4545	. . . . . . . . 9 ⊢ (𝑏 = (𝐹‘𝑐) → if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)) = if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))
30	22, 29	ifeq12d 4545	. . . . . . . 8 ⊢ (𝑏 = (𝐹‘𝑐) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))) = if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))))
31	30	adantr 480	. . . . . . 7 ⊢ ((𝑏 = (𝐹‘𝑐) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))) = if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))))
32	31	mpteq2dva 5242	. . . . . 6 ⊢ (𝑏 = (𝐹‘𝑐) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))))
33	32	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑏 = (𝐹‘𝑐)) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))))
34	7	ffvelcdmda 7088	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐹‘𝑐) ∈ 𝐵)
35		fzfid 13962	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1...(𝐾 + 1)) ∈ Fin)
36	35	mptexd 7230	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))) ∈ V)
37	20, 33, 34, 36	fvmptd 7006	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐺‘(𝐹‘𝑐)) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))))
38	4	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))))
39		simpllr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑎 = 𝑐)
40	39	fveq1d 6893	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑎‘𝑙) = (𝑐‘𝑙))
41	40	sumeq2dv 15673	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙) = Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))
42	41	oveq2d 7430	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)) = (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))
43	42	mpteq2dva 5242	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑎 = 𝑐) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))))
44		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ 𝐴)
45		fzfid 13962	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1...𝐾) ∈ Fin)
46	45	mptexd 7230	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))) ∈ V)
47	38, 43, 44, 46	fvmptd 7006	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐹‘𝑐) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))))
48		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 𝐾) → 𝑗 = 𝐾)
49	48	oveq2d 7430	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 𝐾) → (1...𝑗) = (1...𝐾))
50	49	sumeq1d 15671	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 𝐾) → Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙) = Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))
51	48, 50	oveq12d 7432	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 𝐾) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)) = (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)))
52		1zzd 12615	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℤ)
53	3	nn0zd 12606	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℤ)
54	2	nnge1d 12282	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ 𝐾)
55	2	nnred 12249	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℝ)
56	55	leidd 11802	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ≤ 𝐾)
57	52, 53, 53, 54, 56	elfzd 13516	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ (1...𝐾))
58	57	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐾 ∈ (1...𝐾))
59		ovexd 7449	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)) ∈ V)
60	47, 51, 58, 59	fvmptd 7006	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝐹‘𝑐)‘𝐾) = (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)))
61	60	oveq2d 7430	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)) = ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))))
62	1	nn0cnd 12556	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℂ)
63	62	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℂ)
64	55	recnd 11264	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℂ)
65	64	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐾 ∈ ℂ)
66	63, 65	addcomd 11438	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑁 + 𝐾) = (𝐾 + 𝑁))
67	66	oveq1d 7429	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) = ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))))
68		1zzd 12615	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 1 ∈ ℤ)
69	53	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ∈ ℤ)
70	69	peano2zd 12691	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝐾 + 1) ∈ ℤ)
71		elfzelz 13525	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ (1...𝐾) → 𝑙 ∈ ℤ)
72	71	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ ℤ)
73		elfzle1 13528	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ (1...𝐾) → 1 ≤ 𝑙)
74	73	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 1 ≤ 𝑙)
75	72	zred 12688	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ ℝ)
76	55	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ∈ ℝ)
77	70	zred 12688	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝐾 + 1) ∈ ℝ)
78		elfzle2 13529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑙 ∈ (1...𝐾) → 𝑙 ≤ 𝐾)
79	78	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ≤ 𝐾)
80	76	lep1d 12167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ≤ (𝐾 + 1))
81	75, 76, 77, 79, 80	letrd 11393	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ≤ (𝐾 + 1))
82	68, 70, 72, 74, 81	elfzd 13516	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ (1...(𝐾 + 1)))
83	5	eleq2i 2820	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝐴 ↔ 𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)})
84	83	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ 𝐴 → 𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)})
85	84	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)})
86		vex 3473	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑐 ∈ V
87		feq1 6697	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔 = 𝑐 → (𝑔:(1...(𝐾 + 1))⟶ℕ0 ↔ 𝑐:(1...(𝐾 + 1))⟶ℕ0))
88		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑔 = 𝑐 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → 𝑔 = 𝑐)
89	88	fveq1d 6893	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔 = 𝑐 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝑔‘𝑖) = (𝑐‘𝑖))
90	89	sumeq2dv 15673	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 = 𝑐 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖))
91	90	eqeq1d 2729	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔 = 𝑐 → (Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁))
92	87, 91	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔 = 𝑐 → ((𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁) ↔ (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁)))
93	86, 92	elab 3665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁))
94	93	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁)))
95	94	biimpd 228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} → (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁)))
96	85, 95	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁))
97	96	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
98	97	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
99	98	ffvelcdmda 7088	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈ ℕ0)
100	82, 99	mpdan 686	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝑐‘𝑙) ∈ ℕ0)
101	45, 100	fsumnn0cl 15706	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) ∈ ℕ0)
102	101	nn0cnd 12556	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) ∈ ℂ)
103	65, 63, 102	pnpcand 11630	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) = (𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)))
104		eqid 2727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 = 1
105		1p0e1 12358	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 + 0) = 1
106	104, 105	eqtr4i 2758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 = (1 + 0)
107	106	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 1 = (1 + 0))
108		1red 11237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 1 ∈ ℝ)
109		0le1 11759	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≤ 1
110	109	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 0 ≤ 1)
111	108, 11, 55, 108, 54, 110	le2addd 11855	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1 + 0) ≤ (𝐾 + 1))
112	107, 111	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ (𝐾 + 1))
113	53	peano2zd 12691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐾 + 1) ∈ ℤ)
114		eluz 12858	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ) → ((𝐾 + 1) ∈ (ℤ≥‘1) ↔ 1 ≤ (𝐾 + 1)))
115	52, 113, 114	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐾 + 1) ∈ (ℤ≥‘1) ↔ 1 ≤ (𝐾 + 1)))
116	112, 115	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 + 1) ∈ (ℤ≥‘1))
117	116	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐾 + 1) ∈ (ℤ≥‘1))
118	97	ffvelcdmda 7088	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈ ℕ0)
119	118	nn0cnd 12556	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈ ℂ)
120		fveq2 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑙 = (𝐾 + 1) → (𝑐‘𝑙) = (𝑐‘(𝐾 + 1)))
121	117, 119, 120	fsumm1 15721	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙) = (Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))))
122		1cnd 11231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ ℂ)
123	65, 122	pncand 11594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝐾 + 1) − 1) = 𝐾)
124	123	oveq2d 7430	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1...((𝐾 + 1) − 1)) = (1...𝐾))
125	124	sumeq1d 15671	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐‘𝑙) = Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))
126	125	oveq1d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))) = (Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))))
127	121, 126	eqtrd 2767	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙) = (Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))))
128	127	eqcomd 2733	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))) = Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙))
129		fveq2 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑙 = 𝑖 → (𝑐‘𝑙) = (𝑐‘𝑖))
130		nfcv 2898	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖(1...(𝐾 + 1))
131		nfcv 2898	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑙(1...(𝐾 + 1))
132		nfcv 2898	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑖(𝑐‘𝑙)
133		nfcv 2898	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑙(𝑐‘𝑖)
134	129, 130, 131, 132, 133	cbvsum 15665	. . . . . . . . . . . . . . . . . 18 ⊢ Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖)
135	134	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖))
136	96	simprd 495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁)
137	135, 136	eqtrd 2767	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙) = 𝑁)
138	128, 137	eqtrd 2767	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))) = 𝑁)
139		1zzd 12615	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ ℤ)
140	53	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐾 ∈ ℤ)
141	140	peano2zd 12691	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐾 + 1) ∈ ℤ)
142		1e0p1 12741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 = (0 + 1)
143	142	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 = (0 + 1))
144		0red 11239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 0 ∈ ℝ)
145	55	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐾 ∈ ℝ)
146		1red 11237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ ℝ)
147	11, 55, 12	ltled 11384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 0 ≤ 𝐾)
148	147	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 0 ≤ 𝐾)
149	144, 145, 146, 148	leadd1dd 11850	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (0 + 1) ≤ (𝐾 + 1))
150	143, 149	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ≤ (𝐾 + 1))
151	55, 55, 108, 56	leadd1dd 11850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 + 1) ≤ (𝐾 + 1))
152	151	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐾 + 1) ≤ (𝐾 + 1))
153	139, 141, 141, 150, 152	elfzd 13516	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐾 + 1) ∈ (1...(𝐾 + 1)))
154	97, 153	ffvelcdmd 7089	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘(𝐾 + 1)) ∈ ℕ0)
155	154	nn0cnd 12556	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘(𝐾 + 1)) ∈ ℂ)
156	63, 102, 155	subaddd 11611	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)) = (𝑐‘(𝐾 + 1)) ↔ (Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))) = 𝑁))
157	138, 156	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)) = (𝑐‘(𝐾 + 1)))
158	103, 157	eqtrd 2767	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) = (𝑐‘(𝐾 + 1)))
159	67, 158	eqtrd 2767	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) = (𝑐‘(𝐾 + 1)))
160	61, 159	eqtrd 2767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1)))
161	160	3adant3 1130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1)))
162	161	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1)))
163		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → 𝑘 = (𝐾 + 1))
164	163	fveq2d 6895	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → (𝑐‘𝑘) = (𝑐‘(𝐾 + 1)))
165	164	eqcomd 2733	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → (𝑐‘(𝐾 + 1)) = (𝑐‘𝑘))
166	162, 165	eqtrd 2767	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)) = (𝑐‘𝑘))
167	47	fveq1d 6893	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝐹‘𝑐)‘1) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘1))
168	167	oveq1d 7429	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (((𝐹‘𝑐)‘1) − 1) = (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘1) − 1))
169		eqidd 2728	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))))
170		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 1) → 𝑗 = 1)
171	170	oveq2d 7430	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 1) → (1...𝑗) = (1...1))
172	171	sumeq1d 15671	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 1) → Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙) = Σ𝑙 ∈ (1...1)(𝑐‘𝑙))
173	170, 172	oveq12d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 1) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)) = (1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙)))
174	146	leidd 11802	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ≤ 1)
175	54	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ≤ 𝐾)
176	139, 140, 139, 174, 175	elfzd 13516	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ (1...𝐾))
177		ovexd 7449	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙)) ∈ V)
178	169, 173, 176, 177	fvmptd 7006	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘1) = (1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙)))
179	178	oveq1d 7429	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘1) − 1) = ((1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙)) − 1))
180		fzfid 13962	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1...1) ∈ Fin)
181		1zzd 12615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ∈ ℤ)
182	140	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝐾 ∈ ℤ)
183	182	peano2zd 12691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → (𝐾 + 1) ∈ ℤ)
184		elfzelz 13525	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑙 ∈ (1...1) → 𝑙 ∈ ℤ)
185	184	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ ℤ)
186		elfzle1 13528	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑙 ∈ (1...1) → 1 ≤ 𝑙)
187	186	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ≤ 𝑙)
188	185	zred 12688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ ℝ)
189		0red 11239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 0 ∈ ℝ)
190		1red 11237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ∈ ℝ)
191	189, 190	readdcld 11265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → (0 + 1) ∈ ℝ)
192	183	zred 12688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → (𝐾 + 1) ∈ ℝ)
193		elfzle2 13529	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 ∈ (1...1) → 𝑙 ≤ 1)
194	193	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ 1)
195	142	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 1 = (0 + 1))
196	194, 195	breqtrd 5168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ (0 + 1))
197	149	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → (0 + 1) ≤ (𝐾 + 1))
198	188, 191, 192, 196, 197	letrd 11393	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ (𝐾 + 1))
199	181, 183, 185, 187, 198	elfzd 13516	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ (1...(𝐾 + 1)))
200	118	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈ ℕ0)
201	199, 200	mpdan 686	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → (𝑐‘𝑙) ∈ ℕ0)
202	180, 201	fsumnn0cl 15706	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...1)(𝑐‘𝑙) ∈ ℕ0)
203	202	nn0cnd 12556	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...1)(𝑐‘𝑙) ∈ ℂ)
204	122, 203	pncan2d 11595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙)) − 1) = Σ𝑙 ∈ (1...1)(𝑐‘𝑙))
205	139, 141, 139, 174, 150	elfzd 13516	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ (1...(𝐾 + 1)))
206	97, 205	ffvelcdmd 7089	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℕ0)
207	206	nn0cnd 12556	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℂ)
208		fveq2 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = 1 → (𝑐‘𝑙) = (𝑐‘1))
209	208	fsum1 15717	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℤ ∧ (𝑐‘1) ∈ ℂ) → Σ𝑙 ∈ (1...1)(𝑐‘𝑙) = (𝑐‘1))
210	139, 207, 209	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...1)(𝑐‘𝑙) = (𝑐‘1))
211	204, 210	eqtrd 2767	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙)) − 1) = (𝑐‘1))
212	179, 211	eqtrd 2767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘1) − 1) = (𝑐‘1))
213	168, 212	eqtrd 2767	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (((𝐹‘𝑐)‘1) − 1) = (𝑐‘1))
214	213	3adant3 1130	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → (((𝐹‘𝑐)‘1) − 1) = (𝑐‘1))
215	214	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (((𝐹‘𝑐)‘1) − 1) = (𝑐‘1))
216	215	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (((𝐹‘𝑐)‘1) − 1) = (𝑐‘1))
217		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → 𝑘 = 1)
218	217	fveq2d 6895	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (𝑐‘𝑘) = (𝑐‘1))
219	218	eqcomd 2733	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (𝑐‘1) = (𝑐‘𝑘))
220	216, 219	eqtrd 2767	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (((𝐹‘𝑐)‘1) − 1) = (𝑐‘𝑘))
221	4	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))))
222		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑎 = 𝑐)
223	222	fveq1d 6893	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑎‘𝑙) = (𝑐‘𝑙))
224	223	sumeq2dv 15673	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙) = Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))
225	224	oveq2d 7430	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)) = (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))
226	225	mpteq2dva 5242	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))))
227		simpll2 1211	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑐 ∈ 𝐴)
228		fzfid 13962	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...𝐾) ∈ Fin)
229	228	mptexd 7230	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))) ∈ V)
230	221, 226, 227, 229	fvmptd 7006	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝐹‘𝑐) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))))
231	230	fveq1d 6893	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐹‘𝑐)‘𝑘) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘))
232	230	fveq1d 6893	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐹‘𝑐)‘(𝑘 − 1)) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1)))
233	231, 232	oveq12d 7432	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) = (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1))))
234	233	oveq1d 7429	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1) = ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1))) − 1))
235		eqidd 2728	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))))
236		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘)
237	236	oveq2d 7430	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → (1...𝑗) = (1...𝑘))
238	237	sumeq1d 15671	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙) = Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙))
239	236, 238	oveq12d 7432	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)) = (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)))
240		1zzd 12615	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℤ)
241	140	3adant3 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝐾 ∈ ℤ)
242	241	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝐾 ∈ ℤ)
243	242	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ)
244		elfznn 13554	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ∈ ℕ)
245	244	3ad2ant3 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℕ)
246	245	nnzd 12607	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℤ)
247	246	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℤ)
248	247	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ)
249	245	nnge1d 12282	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 1 ≤ 𝑘)
250	249	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ≤ 𝑘)
251	250	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ 𝑘)
252		simpl3 1191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ (1...(𝐾 + 1)))
253		1zzd 12615	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ∈ ℤ)
254	242	peano2zd 12691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ∈ ℤ)
255		elfz 13514	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℤ ∧ 1 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ) → (𝑘 ∈ (1...(𝐾 + 1)) ↔ (1 ≤ 𝑘 ∧ 𝑘 ≤ (𝐾 + 1))))
256	247, 253, 254, 255	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ∈ (1...(𝐾 + 1)) ↔ (1 ≤ 𝑘 ∧ 𝑘 ≤ (𝐾 + 1))))
257	256	biimpd 228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ∈ (1...(𝐾 + 1)) → (1 ≤ 𝑘 ∧ 𝑘 ≤ (𝐾 + 1))))
258	252, 257	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (1 ≤ 𝑘 ∧ 𝑘 ≤ (𝐾 + 1)))
259	258	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≤ (𝐾 + 1))
260		neqne 2943	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑘 = (𝐾 + 1) → 𝑘 ≠ (𝐾 + 1))
261	260	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≠ (𝐾 + 1))
262	261	necomd 2991	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑘)
263	259, 262	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑘))
264	247	zred 12688	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℝ)
265	254	zred 12688	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
266	264, 265	ltlend 11381	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 < (𝐾 + 1) ↔ (𝑘 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑘)))
267	263, 266	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 < (𝐾 + 1))
268		zleltp1 12635	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ≤ 𝐾 ↔ 𝑘 < (𝐾 + 1)))
269	247, 242, 268	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ≤ 𝐾 ↔ 𝑘 < (𝐾 + 1)))
270	267, 269	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≤ 𝐾)
271	270	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≤ 𝐾)
272	240, 243, 248, 251, 271	elfzd 13516	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (1...𝐾))
273		ovexd 7449	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) ∈ V)
274	235, 239, 272, 273	fvmptd 7006	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) = (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)))
275		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → 𝑗 = (𝑘 − 1))
276	275	oveq2d 7430	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → (1...𝑗) = (1...(𝑘 − 1)))
277	276	sumeq1d 15671	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙) = Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))
278	275, 277	oveq12d 7432	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)) = ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)))
279		1zzd 12615	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℤ)
280	53	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ)
281	280	3impa 1108	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ)
282	244	nnzd 12607	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ∈ ℤ)
283	282	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℤ)
284	283	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ)
285	284	3impa 1108	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ)
286	285, 279	zsubcld 12693	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℤ)
287		neqne 2943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑘 = 1 → 𝑘 ≠ 1)
288	287	3ad2ant3 1133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≠ 1)
289	108	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℝ)
290	285	zred 12688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℝ)
291		simp2 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (1...(𝐾 + 1)))
292		elfzle1 13528	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (1...(𝐾 + 1)) → 1 ≤ 𝑘)
293	291, 292	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ 𝑘)
294	289, 290, 293	leltned 11389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 < 𝑘 ↔ 𝑘 ≠ 1))
295	288, 294	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 < 𝑘)
296	279, 285	zltp1led 41387	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 < 𝑘 ↔ (1 + 1) ≤ 𝑘))
297	295, 296	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 + 1) ≤ 𝑘)
298		leaddsub 11712	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((1 + 1) ≤ 𝑘 ↔ 1 ≤ (𝑘 − 1)))
299	289, 289, 290, 298	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + 1) ≤ 𝑘 ↔ 1 ≤ (𝑘 − 1)))
300	297, 299	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ (𝑘 − 1))
301	286	zred 12688	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℝ)
302	55	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℝ)
303		1red 11237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℝ)
304	302, 303	readdcld 11265	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝐾 + 1) ∈ ℝ)
305	304, 303	resubcld 11664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) ∈ ℝ)
306		elfzle2 13529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ≤ (𝐾 + 1))
307	306	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≤ (𝐾 + 1))
308	290, 304, 303, 307	lesub1dd 11852	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ≤ ((𝐾 + 1) − 1))
309	64	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℂ)
310		1cnd 11231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℂ)
311	309, 310	pncand 11594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) = 𝐾)
312	56	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ≤ 𝐾)
313	311, 312	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) ≤ 𝐾)
314	301, 305, 302, 308, 313	letrd 11393	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ≤ 𝐾)
315	279, 281, 286, 300, 314	elfzd 13516	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
316	315	3expa 1116	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
317	316	3adantl2 1165	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
318	317	adantlr 714	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
319		ovexd 7449	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)) ∈ V)
320	235, 278, 318, 319	fvmptd 7006	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1)) = ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)))
321	274, 320	oveq12d 7432	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1))) = ((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))))
322	321	oveq1d 7429	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1))) − 1) = (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1))
323	248	zcnd 12689	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℂ)
324		fzfid 13962	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...𝑘) ∈ Fin)
325		1zzd 12615	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 1 ∈ ℤ)
326	243	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝐾 ∈ ℤ)
327	326	peano2zd 12691	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝐾 + 1) ∈ ℤ)
328		elfznn 13554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ (1...𝑘) → 𝑙 ∈ ℕ)
329	328	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℕ)
330	329	nnzd 12607	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℤ)
331	329	nnge1d 12282	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 1 ≤ 𝑙)
332	329	nnred 12249	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℝ)
333	264	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑘 ∈ ℝ)
334	265	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝐾 + 1) ∈ ℝ)
335		elfzle2 13529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ (1...𝑘) → 𝑙 ≤ 𝑘)
336	335	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ≤ 𝑘)
337	259	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑘 ≤ (𝐾 + 1))
338	332, 333, 334, 336, 337	letrd 11393	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ≤ (𝐾 + 1))
339	325, 327, 330, 331, 338	elfzd 13516	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ (1...(𝐾 + 1)))
340	97	3adant3 1130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
341	340	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
342	341	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
343	342	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
344	343	ffvelcdmda 7088	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈ ℕ0)
345	339, 344	mpdan 686	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝑐‘𝑙) ∈ ℕ0)
346	324, 345	fsumnn0cl 15706	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) ∈ ℕ0)
347	346	nn0cnd 12556	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) ∈ ℂ)
348		1cnd 11231	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℂ)
349	323, 348	subcld 11593	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℂ)
350		fzfid 13962	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...(𝑘 − 1)) ∈ Fin)
351		1zzd 12615	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ∈ ℤ)
352	243	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝐾 ∈ ℤ)
353	352	peano2zd 12691	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝐾 + 1) ∈ ℤ)
354		elfznn 13554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ (1...(𝑘 − 1)) → 𝑙 ∈ ℕ)
355	354	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℕ)
356	355	nnzd 12607	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℤ)
357	355	nnge1d 12282	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ≤ 𝑙)
358	355	nnred 12249	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℝ)
359	264	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑘 ∈ ℝ)
360		1red 11237	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ∈ ℝ)
361	359, 360	resubcld 11664	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ)
362	265	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝐾 + 1) ∈ ℝ)
363		elfzle2 13529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ (1...(𝑘 − 1)) → 𝑙 ≤ (𝑘 − 1))
364	363	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ≤ (𝑘 − 1))
365	359	lem1d 12169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ≤ 𝑘)
366	259	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑘 ≤ (𝐾 + 1))
367	361, 359, 362, 365, 366	letrd 11393	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ≤ (𝐾 + 1))
368	358, 361, 362, 364, 367	letrd 11393	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ≤ (𝐾 + 1))
369	351, 353, 356, 357, 368	elfzd 13516	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ (1...(𝐾 + 1)))
370	342	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑐:(1...(𝐾 + 1))⟶ℕ0)
371	370	ffvelcdmda 7088	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈ ℕ0)
372	369, 371	mpdan 686	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑐‘𝑙) ∈ ℕ0)
373	350, 372	fsumnn0cl 15706	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙) ∈ ℕ0)
374	373	nn0cnd 12556	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙) ∈ ℂ)
375	323, 347, 349, 374	addsub4d 11640	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) = ((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))))
376	375	oveq1d 7429	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1))
377	323, 348	nncand 11598	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − (𝑘 − 1)) = 1)
378	377	oveq1d 7429	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) = (1 + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))))
379	378	oveq1d 7429	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1))
380	347, 374	subcld 11593	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)) ∈ ℂ)
381	348, 380	pncan2d 11595	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)))
382	139	3adant3 1130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 1 ∈ ℤ)
383	382, 246, 249	3jca 1126	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → (1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
384		eluz2 12850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
385	383, 384	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ (ℤ≥‘1))
386	385	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ (ℤ≥‘1))
387	386	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (ℤ≥‘1))
388	345	nn0cnd 12556	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝑐‘𝑙) ∈ ℂ)
389		fveq2 6891	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 𝑘 → (𝑐‘𝑙) = (𝑐‘𝑘))
390	387, 388, 389	fsumm1 15721	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) = (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙) + (𝑐‘𝑘)))
391	390	eqcomd 2733	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙) + (𝑐‘𝑘)) = Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙))
392		simp3 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ (1...(𝐾 + 1)))
393	340, 392	ffvelcdmd 7089	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑘) ∈ ℕ0)
394	393	nn0cnd 12556	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑘) ∈ ℂ)
395	394	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑐‘𝑘) ∈ ℂ)
396	395	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑐‘𝑘) ∈ ℂ)
397	347, 374, 396	subaddd 11611	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)) = (𝑐‘𝑘) ↔ (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙) + (𝑐‘𝑘)) = Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)))
398	391, 397	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)) = (𝑐‘𝑘))
399	381, 398	eqtrd 2767	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = (𝑐‘𝑘))
400	379, 399	eqtrd 2767	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = (𝑐‘𝑘))
401	376, 400	eqtrd 2767	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = (𝑐‘𝑘))
402	322, 401	eqtrd 2767	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1))) − 1) = (𝑐‘𝑘))
403	234, 402	eqtrd 2767	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1) = (𝑐‘𝑘))
404	220, 403	ifeqda 4560	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)) = (𝑐‘𝑘))
405	166, 404	ifeqda 4560	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))) = (𝑐‘𝑘))
406	405	3expa 1116	. . . . . 6 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))) = (𝑐‘𝑘))
407	406	mpteq2dva 5242	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐‘𝑘)))
408	97	ffnd 6717	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 Fn (1...(𝐾 + 1)))
409		dffn5 6951	. . . . . . . 8 ⊢ (𝑐 Fn (1...(𝐾 + 1)) ↔ 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐‘𝑘)))
410	409	biimpi 215	. . . . . . 7 ⊢ (𝑐 Fn (1...(𝐾 + 1)) → 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐‘𝑘)))
411	408, 410	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐‘𝑘)))
412	411	eqcomd 2733	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐‘𝑘)) = 𝑐)
413	407, 412	eqtrd 2767	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))) = 𝑐)
414	37, 413	eqtrd 2767	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐺‘(𝐹‘𝑐)) = 𝑐)
415	414	ralrimiva 3141	. 2 ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝐺‘(𝐹‘𝑐)) = 𝑐)
416	1, 2, 4, 8, 5, 6	sticksstones12a 41561	. 2 ⊢ (𝜑 → ∀𝑑 ∈ 𝐵 (𝐹‘(𝐺‘𝑑)) = 𝑑)
417	7, 9, 415, 416	2fvidf1od 7301	1 ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  {cab 2704   ≠ wne 2935  ∀wral 3056  Vcvv 3469  ifcif 4524  {csn 4624  ⟨cop 4630   class class class wbr 5142   ↦ cmpt 5225   Fn wfn 6537  ⟶wf 6538  –1-1-onto→wf1o 6541  ‘cfv 6542  (class class class)co 7414  Fincfn 8955  ℂcc 11128  ℝcr 11129  0cc0 11130  1c1 11131   + caddc 11133   < clt 11270   ≤ cle 11271   − cmin 11466  ℕcn 12234  ℕ₀cn0 12494  ℤcz 12580  ℤ_≥cuz 12844  ...cfz 13508  Σcsu 15656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9457  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-z 12581  df-uz 12845  df-rp 12999  df-ico 13354  df-fz 13509  df-fzo 13652  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-clim 15456  df-sum 15657

This theorem is referenced by:  sticksstones13  41563