Metamath Proof Explorer

Theorem sticksstones12

Description: Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024)

Ref Expression
Hypotheses 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 sticksstones12 ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Proof

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