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