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