Metamath Proof Explorer

Theorem sticksstones10

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

Ref Expression
Hypotheses sticksstones10.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones10.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
sticksstones10.3 ⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) )
sticksstones10.4 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
sticksstones10.5 ⊢ 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
Assertion sticksstones10 ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )

Proof

Step Hyp Ref Expression
1 sticksstones10.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones10.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 sticksstones10.3 ⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) )
4 sticksstones10.4 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
5 sticksstones10.5 ⊢ 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
6 2 nnne0d ⊢ ( 𝜑 → 𝐾 ≠ 0 )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ≠ 0 )
8 7 neneqd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ¬ 𝐾 = 0 )
9 8 iffalsed ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) )
10 9 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) = if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) )
11 eleq1 ⊢ ( ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) = if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) → ( ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℕ0 ↔ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ∈ ℕ0 ) )
12 eleq1 ⊢ ( if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) = if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) → ( if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ∈ ℕ0 ↔ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ∈ ℕ0 ) )
13 1 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑁 ∈ ℤ )
15 2 nnzd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ∈ ℤ )
17 14 16 zaddcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑁 + 𝐾 ) ∈ ℤ )
18 5 eleq2i ⊢ ( 𝑏 ∈ 𝐵 ↔ 𝑏 ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
19 vex ⊢ 𝑏 ∈ V
20 feq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ↔ 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ) )
21 fveq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) )
22 fveq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑦 ) )
23 21 22 breq12d ⊢ ( 𝑓 = 𝑏 → ( ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) )
24 23 imbi2d ⊢ ( 𝑓 = 𝑏 → ( ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) ) )
25 24 2ralbidv ⊢ ( 𝑓 = 𝑏 → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) ) )
26 20 25 anbi12d ⊢ ( 𝑓 = 𝑏 → ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) ) ) )
27 19 26 elab ⊢ ( 𝑏 ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) ) )
28 18 27 bitri ⊢ ( 𝑏 ∈ 𝐵 ↔ ( 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) ) )
29 28 bilani ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) ) )
30 29 simpld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
31 1zzd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 1 ∈ ℤ )
32 2 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐾 )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 1 ≤ 𝐾 )
34 16 zred ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ∈ ℝ )
35 34 leidd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ≤ 𝐾 )
36 31 16 16 33 35 elfzd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ∈ ( 1 ... 𝐾 ) )
37 30 36 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝐾 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
38 elfznn ⊢ ( ( 𝑏 ‘ 𝐾 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝐾 ) ∈ ℕ )
39 37 38 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝐾 ) ∈ ℕ )
40 39 nnzd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝐾 ) ∈ ℤ )
41 17 40 zsubcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℤ )
42 39 nnred ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝐾 ) ∈ ℝ )
43 42 recnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝐾 ) ∈ ℂ )
44 43 addridd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 𝐾 ) + 0 ) = ( 𝑏 ‘ 𝐾 ) )
45 elfzle2 ⊢ ( ( 𝑏 ‘ 𝐾 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝐾 ) ≤ ( 𝑁 + 𝐾 ) )
46 37 45 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝐾 ) ≤ ( 𝑁 + 𝐾 ) )
47 44 46 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 𝐾 ) + 0 ) ≤ ( 𝑁 + 𝐾 ) )
48 0red ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 0 ∈ ℝ )
49 17 zred ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑁 + 𝐾 ) ∈ ℝ )
50 42 48 49 leaddsub2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝑏 ‘ 𝐾 ) + 0 ) ≤ ( 𝑁 + 𝐾 ) ↔ 0 ≤ ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) )
51 47 50 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 0 ≤ ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) )
52 41 51 jca ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℤ ∧ 0 ≤ ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) )
53 elnn0z ⊢ ( ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℕ0 ↔ ( ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℤ ∧ 0 ≤ ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) )
54 52 53 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℕ0 )
55 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℕ0 )
56 55 3impa ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℕ0 )
57 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑘 = ( 𝐾 + 1 ) ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℕ0 )
58 eleq1 ⊢ ( ( ( 𝑏 ‘ 1 ) − 1 ) = if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) → ( ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℕ0 ↔ if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ∈ ℕ0 ) )
59 eleq1 ⊢ ( ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) = if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) → ( ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ∈ ℕ0 ↔ if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ∈ ℕ0 ) )
60 1red ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 1 ∈ ℝ )
61 60 leidd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 1 ≤ 1 )
62 31 16 31 61 33 elfzd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 1 ∈ ( 1 ... 𝐾 ) )
63 30 62 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 1 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
64 elfznn ⊢ ( ( 𝑏 ‘ 1 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 1 ) ∈ ℕ )
65 64 nnzd ⊢ ( ( 𝑏 ‘ 1 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 1 ) ∈ ℤ )
66 63 65 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 1 ) ∈ ℤ )
67 66 31 zsubcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℤ )
68 1cnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 1 ∈ ℂ )
69 68 addridd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 1 + 0 ) = 1 )
70 elfzle1 ⊢ ( ( 𝑏 ‘ 1 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → 1 ≤ ( 𝑏 ‘ 1 ) )
71 63 70 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 1 ≤ ( 𝑏 ‘ 1 ) )
72 69 71 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 1 + 0 ) ≤ ( 𝑏 ‘ 1 ) )
73 66 zred ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 1 ) ∈ ℝ )
74 60 48 73 leaddsub2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 1 + 0 ) ≤ ( 𝑏 ‘ 1 ) ↔ 0 ≤ ( ( 𝑏 ‘ 1 ) − 1 ) ) )
75 72 74 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 0 ≤ ( ( 𝑏 ‘ 1 ) − 1 ) )
76 67 75 jca ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑏 ‘ 1 ) − 1 ) ) )
77 elnn0z ⊢ ( ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℕ0 ↔ ( ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑏 ‘ 1 ) − 1 ) ) )
78 76 77 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℕ0 )
79 78 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℕ0 )
80 79 3impa ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℕ0 )
81 80 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℕ0 )
82 81 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ 𝑘 = 1 ) → ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℕ0 )
83 30 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
84 83 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
85 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 1 ∈ ℤ )
86 16 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝐾 ∈ ℤ )
87 86 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝐾 ∈ ℤ )
88 simp3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) )
89 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) → 𝑘 ∈ ℕ )
90 88 89 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑘 ∈ ℕ )
91 90 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝑘 ∈ ℕ )
92 91 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝑘 ∈ ℤ )
93 91 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 1 ≤ 𝑘 )
94 elfzle2 ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) → 𝑘 ≤ ( 𝐾 + 1 ) )
95 88 94 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑘 ≤ ( 𝐾 + 1 ) )
96 95 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝑘 ≤ ( 𝐾 + 1 ) )
97 neqne ⊢ ( ¬ 𝑘 = ( 𝐾 + 1 ) → 𝑘 ≠ ( 𝐾 + 1 ) )
98 97 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝑘 ≠ ( 𝐾 + 1 ) )
99 98 necomd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ≠ 𝑘 )
100 96 99 jca ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ( 𝑘 ≤ ( 𝐾 + 1 ) ∧ ( 𝐾 + 1 ) ≠ 𝑘 ) )
101 91 nnred ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝑘 ∈ ℝ )
102 87 zred ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝐾 ∈ ℝ )
103 1red ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 1 ∈ ℝ )
104 102 103 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ∈ ℝ )
105 101 104 ltlend ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ( 𝑘 < ( 𝐾 + 1 ) ↔ ( 𝑘 ≤ ( 𝐾 + 1 ) ∧ ( 𝐾 + 1 ) ≠ 𝑘 ) ) )
106 100 105 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝑘 < ( 𝐾 + 1 ) )
107 90 nnzd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑘 ∈ ℤ )
108 zleltp1 ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 ≤ 𝐾 ↔ 𝑘 < ( 𝐾 + 1 ) ) )
109 107 86 108 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝑘 ≤ 𝐾 ↔ 𝑘 < ( 𝐾 + 1 ) ) )
110 109 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ( 𝑘 ≤ 𝐾 ↔ 𝑘 < ( 𝐾 + 1 ) ) )
111 106 110 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝑘 ≤ 𝐾 )
112 85 87 92 93 111 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → 𝑘 ∈ ( 1 ... 𝐾 ) )
113 84 112 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ( 𝑏 ‘ 𝑘 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
114 elfznn ⊢ ( ( 𝑏 ‘ 𝑘 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑘 ) ∈ ℕ )
115 113 114 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ( 𝑏 ‘ 𝑘 ) ∈ ℕ )
116 115 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ( 𝑏 ‘ 𝑘 ) ∈ ℤ )
117 116 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑏 ‘ 𝑘 ) ∈ ℤ )
118 84 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
119 1zzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 1 ∈ ℤ )
120 87 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 𝐾 ∈ ℤ )
121 92 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 𝑘 ∈ ℤ )
122 121 119 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑘 − 1 ) ∈ ℤ )
123 93 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 1 ≤ 𝑘 )
124 neqne ⊢ ( ¬ 𝑘 = 1 → 𝑘 ≠ 1 )
125 124 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 𝑘 ≠ 1 )
126 123 125 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 1 ≤ 𝑘 ∧ 𝑘 ≠ 1 ) )
127 103 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 1 ∈ ℝ )
128 101 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 𝑘 ∈ ℝ )
129 127 128 ltlend ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 1 < 𝑘 ↔ ( 1 ≤ 𝑘 ∧ 𝑘 ≠ 1 ) ) )
130 126 129 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 1 < 𝑘 )
131 119 121 zltlem1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 1 < 𝑘 ↔ 1 ≤ ( 𝑘 − 1 ) ) )
132 130 131 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 1 ≤ ( 𝑘 − 1 ) )
133 90 nnred ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑘 ∈ ℝ )
134 60 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 1 ∈ ℝ )
135 34 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝐾 ∈ ℝ )
136 lesubadd ⊢ ( ( 𝑘 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( 𝑘 − 1 ) ≤ 𝐾 ↔ 𝑘 ≤ ( 𝐾 + 1 ) ) )
137 133 134 135 136 syl3anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( ( 𝑘 − 1 ) ≤ 𝐾 ↔ 𝑘 ≤ ( 𝐾 + 1 ) ) )
138 95 137 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝑘 − 1 ) ≤ 𝐾 )
139 138 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ( 𝑘 − 1 ) ≤ 𝐾 )
140 139 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑘 − 1 ) ≤ 𝐾 )
141 119 120 122 132 140 elfzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑘 − 1 ) ∈ ( 1 ... 𝐾 ) )
142 118 141 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
143 elfznn ⊢ ( ( 𝑏 ‘ ( 𝑘 − 1 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) ∈ ℕ )
144 142 143 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) ∈ ℕ )
145 144 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) ∈ ℤ )
146 117 145 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ∈ ℤ )
147 146 119 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ∈ ℤ )
148 0p1e1 ⊢ ( 0 + 1 ) = 1
149 148 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 0 + 1 ) = 1 )
150 1cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 1 ∈ ℂ )
151 150 subidd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 1 − 1 ) = 0 )
152 145 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) ∈ ℝ )
153 152 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) ∈ ℂ )
154 153 addridd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( 𝑏 ‘ ( 𝑘 − 1 ) ) + 0 ) = ( 𝑏 ‘ ( 𝑘 − 1 ) ) )
155 128 ltm1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑘 − 1 ) < 𝑘 )
156 112 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 𝑘 ∈ ( 1 ... 𝐾 ) )
157 141 156 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( 𝑘 − 1 ) ∈ ( 1 ... 𝐾 ) ∧ 𝑘 ∈ ( 1 ... 𝐾 ) ) )
158 29 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) )
159 158 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) )
160 159 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) )
161 160 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) )
162 breq1 ⊢ ( 𝑥 = ( 𝑘 − 1 ) → ( 𝑥 < 𝑦 ↔ ( 𝑘 − 1 ) < 𝑦 ) )
163 fveq2 ⊢ ( 𝑥 = ( 𝑘 − 1 ) → ( 𝑏 ‘ 𝑥 ) = ( 𝑏 ‘ ( 𝑘 − 1 ) ) )
164 163 breq1d ⊢ ( 𝑥 = ( 𝑘 − 1 ) → ( ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ↔ ( 𝑏 ‘ ( 𝑘 − 1 ) ) < ( 𝑏 ‘ 𝑦 ) ) )
165 162 164 imbi12d ⊢ ( 𝑥 = ( 𝑘 − 1 ) → ( ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) ↔ ( ( 𝑘 − 1 ) < 𝑦 → ( 𝑏 ‘ ( 𝑘 − 1 ) ) < ( 𝑏 ‘ 𝑦 ) ) ) )
166 breq2 ⊢ ( 𝑦 = 𝑘 → ( ( 𝑘 − 1 ) < 𝑦 ↔ ( 𝑘 − 1 ) < 𝑘 ) )
167 fveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝑏 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑘 ) )
168 167 breq2d ⊢ ( 𝑦 = 𝑘 → ( ( 𝑏 ‘ ( 𝑘 − 1 ) ) < ( 𝑏 ‘ 𝑦 ) ↔ ( 𝑏 ‘ ( 𝑘 − 1 ) ) < ( 𝑏 ‘ 𝑘 ) ) )
169 166 168 imbi12d ⊢ ( 𝑦 = 𝑘 → ( ( ( 𝑘 − 1 ) < 𝑦 → ( 𝑏 ‘ ( 𝑘 − 1 ) ) < ( 𝑏 ‘ 𝑦 ) ) ↔ ( ( 𝑘 − 1 ) < 𝑘 → ( 𝑏 ‘ ( 𝑘 − 1 ) ) < ( 𝑏 ‘ 𝑘 ) ) ) )
170 165 169 rspc2va ⊢ ( ( ( ( 𝑘 − 1 ) ∈ ( 1 ... 𝐾 ) ∧ 𝑘 ∈ ( 1 ... 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑏 ‘ 𝑥 ) < ( 𝑏 ‘ 𝑦 ) ) ) → ( ( 𝑘 − 1 ) < 𝑘 → ( 𝑏 ‘ ( 𝑘 − 1 ) ) < ( 𝑏 ‘ 𝑘 ) ) )
171 157 161 170 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( 𝑘 − 1 ) < 𝑘 → ( 𝑏 ‘ ( 𝑘 − 1 ) ) < ( 𝑏 ‘ 𝑘 ) ) )
172 155 171 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) < ( 𝑏 ‘ 𝑘 ) )
173 154 172 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( 𝑏 ‘ ( 𝑘 − 1 ) ) + 0 ) < ( 𝑏 ‘ 𝑘 ) )
174 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 0 ∈ ℝ )
175 117 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 𝑏 ‘ 𝑘 ) ∈ ℝ )
176 152 174 175 ltaddsub2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( ( 𝑏 ‘ ( 𝑘 − 1 ) ) + 0 ) < ( 𝑏 ‘ 𝑘 ) ↔ 0 < ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ) )
177 173 176 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 0 < ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) )
178 151 177 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 1 − 1 ) < ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) )
179 zlem1lt ⊢ ( ( 1 ∈ ℤ ∧ ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ∈ ℤ ) → ( 1 ≤ ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ↔ ( 1 − 1 ) < ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ) )
180 119 146 179 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 1 ≤ ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ↔ ( 1 − 1 ) < ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ) )
181 178 180 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 1 ≤ ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) )
182 149 181 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( 0 + 1 ) ≤ ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) )
183 146 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ∈ ℝ )
184 leaddsub ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ∈ ℝ ) → ( ( 0 + 1 ) ≤ ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ↔ 0 ≤ ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) )
185 174 127 183 184 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( 0 + 1 ) ≤ ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) ↔ 0 ≤ ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) )
186 182 185 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → 0 ≤ ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) )
187 147 186 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ∈ ℤ ∧ 0 ≤ ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) )
188 elnn0z ⊢ ( ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ∈ ℕ0 ↔ ( ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ∈ ℤ ∧ 0 ≤ ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) )
189 187 188 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑘 = 1 ) → ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ∈ ℕ0 )
190 58 59 82 189 ifbothda ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑘 = ( 𝐾 + 1 ) ) → if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ∈ ℕ0 )
191 11 12 57 190 ifbothda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ∈ ℕ0 )
192 191 3expa ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ∈ ℕ0 )
193 192 fmpttd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
194 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) )
195 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → 𝑘 = 𝑖 )
196 195 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → ( 𝑘 = ( 𝐾 + 1 ) ↔ 𝑖 = ( 𝐾 + 1 ) ) )
197 195 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → ( 𝑘 = 1 ↔ 𝑖 = 1 ) )
198 195 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → ( 𝑏 ‘ 𝑘 ) = ( 𝑏 ‘ 𝑖 ) )
199 195 fvoveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → ( 𝑏 ‘ ( 𝑘 − 1 ) ) = ( 𝑏 ‘ ( 𝑖 − 1 ) ) )
200 198 199 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
201 200 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) = ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) )
202 197 201 ifbieq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) = if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) )
203 196 202 ifbieq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑘 = 𝑖 ) → if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) = if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) )
204 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) )
205 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ V )
206 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( ( 𝑏 ‘ 1 ) − 1 ) ∈ V )
207 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ∈ V )
208 206 207 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ∈ V )
209 205 208 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) ∈ V )
210 194 203 204 209 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) = if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) )
211 210 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) )
212 2 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ∈ ℕ )
213 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
214 212 213 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ∈ ( ℤ≥ ‘ 1 ) )
215 eleq1 ⊢ ( ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) = if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) → ( ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℤ ↔ if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) ∈ ℤ ) )
216 eleq1 ⊢ ( if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) = if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) → ( if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ∈ ℤ ↔ if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) ∈ ℤ ) )
217 14 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑁 ∈ ℤ )
218 217 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑖 = ( 𝐾 + 1 ) ) → 𝑁 ∈ ℤ )
219 16 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝐾 ∈ ℤ )
220 219 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑖 = ( 𝐾 + 1 ) ) → 𝐾 ∈ ℤ )
221 218 220 zaddcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑖 = ( 𝐾 + 1 ) ) → ( 𝑁 + 𝐾 ) ∈ ℤ )
222 39 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝑏 ‘ 𝐾 ) ∈ ℕ )
223 222 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑖 = ( 𝐾 + 1 ) ) → ( 𝑏 ‘ 𝐾 ) ∈ ℕ )
224 223 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑖 = ( 𝐾 + 1 ) ) → ( 𝑏 ‘ 𝐾 ) ∈ ℤ )
225 221 224 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ 𝑖 = ( 𝐾 + 1 ) ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℤ )
226 eleq1 ⊢ ( ( ( 𝑏 ‘ 1 ) − 1 ) = if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) → ( ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℤ ↔ if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ∈ ℤ ) )
227 eleq1 ⊢ ( ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) = if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) → ( ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ∈ ℤ ↔ if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ∈ ℤ ) )
228 66 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝑏 ‘ 1 ) ∈ ℤ )
229 228 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → ( 𝑏 ‘ 1 ) ∈ ℤ )
230 229 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ 𝑖 = 1 ) → ( 𝑏 ‘ 1 ) ∈ ℤ )
231 1zzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ 𝑖 = 1 ) → 1 ∈ ℤ )
232 230 231 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ 𝑖 = 1 ) → ( ( 𝑏 ‘ 1 ) − 1 ) ∈ ℤ )
233 30 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
234 233 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
235 234 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
236 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 1 ∈ ℤ )
237 219 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 𝐾 ∈ ℤ )
238 elfznn ⊢ ( 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) → 𝑖 ∈ ℕ )
239 238 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑖 ∈ ℕ )
240 239 3impa ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑖 ∈ ℕ )
241 240 nnzd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑖 ∈ ℤ )
242 241 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 𝑖 ∈ ℤ )
243 240 nnge1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 1 ≤ 𝑖 )
244 243 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 1 ≤ 𝑖 )
245 simp3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) )
246 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) → 𝑖 ≤ ( 𝐾 + 1 ) )
247 245 246 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑖 ≤ ( 𝐾 + 1 ) )
248 247 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 𝑖 ≤ ( 𝐾 + 1 ) )
249 neqne ⊢ ( ¬ 𝑖 = ( 𝐾 + 1 ) → 𝑖 ≠ ( 𝐾 + 1 ) )
250 249 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 𝑖 ≠ ( 𝐾 + 1 ) )
251 250 necomd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ≠ 𝑖 )
252 248 251 jca ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → ( 𝑖 ≤ ( 𝐾 + 1 ) ∧ ( 𝐾 + 1 ) ≠ 𝑖 ) )
253 242 zred ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 𝑖 ∈ ℝ )
254 237 zred ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 𝐾 ∈ ℝ )
255 1red ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 1 ∈ ℝ )
256 254 255 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ∈ ℝ )
257 253 256 ltlend ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → ( 𝑖 < ( 𝐾 + 1 ) ↔ ( 𝑖 ≤ ( 𝐾 + 1 ) ∧ ( 𝐾 + 1 ) ≠ 𝑖 ) ) )
258 252 257 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 𝑖 < ( 𝐾 + 1 ) )
259 zleltp1 ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑖 ≤ 𝐾 ↔ 𝑖 < ( 𝐾 + 1 ) ) )
260 242 237 259 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → ( 𝑖 ≤ 𝐾 ↔ 𝑖 < ( 𝐾 + 1 ) ) )
261 258 260 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 𝑖 ≤ 𝐾 )
262 236 237 242 244 261 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → 𝑖 ∈ ( 1 ... 𝐾 ) )
263 262 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ∈ ( 1 ... 𝐾 ) )
264 235 263 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ 𝑖 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
265 elfznn ⊢ ( ( 𝑏 ‘ 𝑖 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℕ )
266 264 265 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ 𝑖 ) ∈ ℕ )
267 266 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ 𝑖 ) ∈ ℤ )
268 1zzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ∈ ℤ )
269 237 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 𝐾 ∈ ℤ )
270 242 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ∈ ℤ )
271 270 268 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑖 − 1 ) ∈ ℤ )
272 244 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ≤ 𝑖 )
273 neqne ⊢ ( ¬ 𝑖 = 1 → 𝑖 ≠ 1 )
274 273 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ≠ 1 )
275 272 274 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 1 ≤ 𝑖 ∧ 𝑖 ≠ 1 ) )
276 1red ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ∈ ℝ )
277 270 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ∈ ℝ )
278 276 277 ltlend ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 1 < 𝑖 ↔ ( 1 ≤ 𝑖 ∧ 𝑖 ≠ 1 ) ) )
279 275 278 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 1 < 𝑖 )
280 zltp1le ⊢ ( ( 1 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 1 < 𝑖 ↔ ( 1 + 1 ) ≤ 𝑖 ) )
281 268 270 280 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 1 < 𝑖 ↔ ( 1 + 1 ) ≤ 𝑖 ) )
282 279 281 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 1 + 1 ) ≤ 𝑖 )
283 leaddsub ⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑖 ∈ ℝ ) → ( ( 1 + 1 ) ≤ 𝑖 ↔ 1 ≤ ( 𝑖 − 1 ) ) )
284 276 276 277 283 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( ( 1 + 1 ) ≤ 𝑖 ↔ 1 ≤ ( 𝑖 − 1 ) ) )
285 282 284 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ≤ ( 𝑖 − 1 ) )
286 248 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ≤ ( 𝐾 + 1 ) )
287 254 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → 𝐾 ∈ ℝ )
288 lesubadd ⊢ ( ( 𝑖 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( 𝑖 − 1 ) ≤ 𝐾 ↔ 𝑖 ≤ ( 𝐾 + 1 ) ) )
289 277 276 287 288 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( ( 𝑖 − 1 ) ≤ 𝐾 ↔ 𝑖 ≤ ( 𝐾 + 1 ) ) )
290 286 289 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑖 − 1 ) ≤ 𝐾 )
291 268 269 271 285 290 elfzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑖 − 1 ) ∈ ( 1 ... 𝐾 ) )
292 235 291 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
293 elfznn ⊢ ( ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ℕ )
294 292 293 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ℕ )
295 294 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ℤ )
296 267 295 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ℤ )
297 296 268 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) ∧ ¬ 𝑖 = 1 ) → ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ∈ ℤ )
298 226 227 232 297 ifbothda ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) ∧ ¬ 𝑖 = ( 𝐾 + 1 ) ) → if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ∈ ℤ )
299 215 216 225 298 ifbothda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) ∈ ℤ )
300 299 3expa ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) ∈ ℤ )
301 300 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) ∈ ℂ )
302 eqeq1 ⊢ ( 𝑖 = ( 𝐾 + 1 ) → ( 𝑖 = ( 𝐾 + 1 ) ↔ ( 𝐾 + 1 ) = ( 𝐾 + 1 ) ) )
303 eqeq1 ⊢ ( 𝑖 = ( 𝐾 + 1 ) → ( 𝑖 = 1 ↔ ( 𝐾 + 1 ) = 1 ) )
304 fveq2 ⊢ ( 𝑖 = ( 𝐾 + 1 ) → ( 𝑏 ‘ 𝑖 ) = ( 𝑏 ‘ ( 𝐾 + 1 ) ) )
305 fvoveq1 ⊢ ( 𝑖 = ( 𝐾 + 1 ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) = ( 𝑏 ‘ ( ( 𝐾 + 1 ) − 1 ) ) )
306 304 305 oveq12d ⊢ ( 𝑖 = ( 𝐾 + 1 ) → ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) = ( ( 𝑏 ‘ ( 𝐾 + 1 ) ) − ( 𝑏 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) )
307 306 oveq1d ⊢ ( 𝑖 = ( 𝐾 + 1 ) → ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) = ( ( ( 𝑏 ‘ ( 𝐾 + 1 ) ) − ( 𝑏 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) − 1 ) )
308 303 307 ifbieq2d ⊢ ( 𝑖 = ( 𝐾 + 1 ) → if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) = if ( ( 𝐾 + 1 ) = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ ( 𝐾 + 1 ) ) − ( 𝑏 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) − 1 ) ) )
309 302 308 ifbieq2d ⊢ ( 𝑖 = ( 𝐾 + 1 ) → if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) = if ( ( 𝐾 + 1 ) = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( ( 𝐾 + 1 ) = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ ( 𝐾 + 1 ) ) − ( 𝑏 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) − 1 ) ) ) )
310 214 301 309 fsump1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) + if ( ( 𝐾 + 1 ) = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( ( 𝐾 + 1 ) = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ ( 𝐾 + 1 ) ) − ( 𝑏 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) − 1 ) ) ) ) )
311 eqidd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐾 + 1 ) = ( 𝐾 + 1 ) )
312 311 iftrued ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → if ( ( 𝐾 + 1 ) = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( ( 𝐾 + 1 ) = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ ( 𝐾 + 1 ) ) − ( 𝑏 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) − 1 ) ) ) = ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) )
313 312 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) + if ( ( 𝐾 + 1 ) = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( ( 𝐾 + 1 ) = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ ( 𝐾 + 1 ) ) − ( 𝑏 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) − 1 ) ) ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) )
314 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝐾 ) → 𝑖 ∈ ℕ )
315 314 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑖 ∈ ℕ )
316 315 nnred ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑖 ∈ ℝ )
317 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝐾 ∈ ℝ )
318 1red ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 1 ∈ ℝ )
319 317 318 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝐾 + 1 ) ∈ ℝ )
320 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... 𝐾 ) → 𝑖 ≤ 𝐾 )
321 320 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑖 ≤ 𝐾 )
322 317 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝐾 < ( 𝐾 + 1 ) )
323 316 317 319 321 322 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑖 < ( 𝐾 + 1 ) )
324 316 323 ltned ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑖 ≠ ( 𝐾 + 1 ) )
325 324 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ¬ 𝑖 = ( 𝐾 + 1 ) )
326 325 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) = if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) )
327 326 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) = Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) )
328 327 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) )
329 eqeq1 ⊢ ( ( ( 𝑏 ‘ 1 ) − 1 ) = if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) → ( ( ( 𝑏 ‘ 1 ) − 1 ) = ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) ↔ if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) = ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) ) )
330 eqeq1 ⊢ ( ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) = if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) → ( ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) = ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) ↔ if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) = ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) ) )
331 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑖 = 1 ) → ( ( 𝑏 ‘ 1 ) − 1 ) = ( ( 𝑏 ‘ 1 ) − 1 ) )
332 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑖 = 1 ) → 𝑖 = 1 )
333 332 iftrued ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑖 = 1 ) → if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 1 ) )
334 333 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑖 = 1 ) → ( 𝑏 ‘ 1 ) = if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
335 334 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑖 = 1 ) → ( ( 𝑏 ‘ 1 ) − 1 ) = ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) )
336 331 335 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑖 = 1 ) → ( ( 𝑏 ‘ 1 ) − 1 ) = ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) )
337 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) = ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) )
338 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ¬ 𝑖 = 1 )
339 338 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
340 339 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) )
341 340 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) = ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) )
342 337 341 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) = ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) )
343 329 330 336 342 ifbothda ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) = ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) )
344 343 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) = Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) )
345 344 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) )
346 fzfid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 1 ... 𝐾 ) ∈ Fin )
347 eleq1 ⊢ ( ( 𝑏 ‘ 1 ) = if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) → ( ( 𝑏 ‘ 1 ) ∈ ℤ ↔ if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ℤ ) )
348 eleq1 ⊢ ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) = if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) → ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ℤ ↔ if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ℤ ) )
349 66 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑖 = 1 ) → ( 𝑏 ‘ 1 ) ∈ ℤ )
350 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
351 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑖 ∈ ( 1 ... 𝐾 ) )
352 350 351 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
353 265 nnzd ⊢ ( ( 𝑏 ‘ 𝑖 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℤ )
354 352 353 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℤ )
355 354 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ 𝑖 ) ∈ ℤ )
356 350 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
357 1zzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ∈ ℤ )
358 16 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 𝐾 ∈ ℤ )
359 315 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑖 ∈ ℤ )
360 359 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ∈ ℤ )
361 360 357 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑖 − 1 ) ∈ ℤ )
362 315 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 1 ≤ 𝑖 )
363 362 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ≤ 𝑖 )
364 338 273 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ≠ 1 )
365 363 364 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 1 ≤ 𝑖 ∧ 𝑖 ≠ 1 ) )
366 318 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ∈ ℝ )
367 316 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ∈ ℝ )
368 366 367 ltlend ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 1 < 𝑖 ↔ ( 1 ≤ 𝑖 ∧ 𝑖 ≠ 1 ) ) )
369 365 368 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 1 < 𝑖 )
370 zltlem1 ⊢ ( ( 1 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 1 < 𝑖 ↔ 1 ≤ ( 𝑖 − 1 ) ) )
371 357 360 370 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 1 < 𝑖 ↔ 1 ≤ ( 𝑖 − 1 ) ) )
372 369 371 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ≤ ( 𝑖 − 1 ) )
373 316 318 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑖 − 1 ) ∈ ℝ )
374 316 lem1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑖 − 1 ) ≤ 𝑖 )
375 373 316 317 374 321 letrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑖 − 1 ) ≤ 𝐾 )
376 375 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑖 − 1 ) ≤ 𝐾 )
377 357 358 361 372 376 elfzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑖 − 1 ) ∈ ( 1 ... 𝐾 ) )
378 356 377 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
379 378 293 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ℕ )
380 379 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ℤ )
381 355 380 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ℤ )
382 347 348 349 381 ifbothda ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ℤ )
383 382 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ℂ )
384 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 1 ∈ ℂ )
385 346 383 384 fsumsub ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... 𝐾 ) 1 ) )
386 id ⊢ ( 𝑖 = 1 → 𝑖 = 1 )
387 386 iftrued ⊢ ( 𝑖 = 1 → if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 1 ) )
388 214 383 387 fsum1p ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) )
389 60 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 1 ∈ ℝ )
390 elfzle1 ⊢ ( 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) → ( 1 + 1 ) ≤ 𝑖 )
391 390 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → ( 1 + 1 ) ≤ 𝑖 )
392 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 1 ∈ ℤ )
393 elfzelz ⊢ ( 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) → 𝑖 ∈ ℤ )
394 393 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 𝑖 ∈ ℤ )
395 392 394 280 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → ( 1 < 𝑖 ↔ ( 1 + 1 ) ≤ 𝑖 ) )
396 391 395 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 1 < 𝑖 )
397 389 396 ltned ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 1 ≠ 𝑖 )
398 397 necomd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 𝑖 ≠ 1 )
399 398 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → ¬ 𝑖 = 1 )
400 399 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
401 400 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
402 401 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
403 34 recnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ∈ ℂ )
404 403 68 npcand ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
405 404 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 = ( ( 𝐾 − 1 ) + 1 ) )
406 405 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 1 + 1 ) ... 𝐾 ) = ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) )
407 406 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) = Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
408 407 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
409 elfzelz ⊢ ( 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) → 𝑖 ∈ ℤ )
410 409 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑖 ∈ ℤ )
411 410 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑖 ∈ ℂ )
412 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 1 ∈ ℂ )
413 411 412 npcand ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( ( 𝑖 − 1 ) + 1 ) = 𝑖 )
414 413 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑖 = ( ( 𝑖 − 1 ) + 1 ) )
415 414 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( 𝑏 ‘ 𝑖 ) = ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) )
416 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) = ( 𝑏 ‘ ( 𝑖 − 1 ) ) )
417 415 416 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) = ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
418 417 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) = Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
419 418 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
420 16 31 zsubcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐾 − 1 ) ∈ ℤ )
421 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
422 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 1 ∈ ℤ )
423 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℤ )
424 elfznn ⊢ ( 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) → 𝑠 ∈ ℕ )
425 424 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ∈ ℕ )
426 425 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ∈ ℤ )
427 426 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑠 + 1 ) ∈ ℤ )
428 1red ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 1 ∈ ℝ )
429 425 nnred ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ∈ ℝ )
430 429 428 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑠 + 1 ) ∈ ℝ )
431 425 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 1 ≤ 𝑠 )
432 429 lep1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ≤ ( 𝑠 + 1 ) )
433 428 429 430 431 432 letrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 1 ≤ ( 𝑠 + 1 ) )
434 elfzle2 ⊢ ( 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) → 𝑠 ≤ ( 𝐾 − 1 ) )
435 434 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ≤ ( 𝐾 − 1 ) )
436 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℝ )
437 leaddsub ⊢ ( ( 𝑠 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( 𝑠 + 1 ) ≤ 𝐾 ↔ 𝑠 ≤ ( 𝐾 − 1 ) ) )
438 429 428 436 437 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑠 + 1 ) ≤ 𝐾 ↔ 𝑠 ≤ ( 𝐾 − 1 ) ) )
439 435 438 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑠 + 1 ) ≤ 𝐾 )
440 422 423 427 433 439 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑠 + 1 ) ∈ ( 1 ... 𝐾 ) )
441 421 440 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑏 ‘ ( 𝑠 + 1 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
442 elfznn ⊢ ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ ( 𝑠 + 1 ) ) ∈ ℕ )
443 441 442 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑏 ‘ ( 𝑠 + 1 ) ) ∈ ℕ )
444 443 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑏 ‘ ( 𝑠 + 1 ) ) ∈ ℤ )
445 436 428 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) ∈ ℝ )
446 436 lem1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) ≤ 𝐾 )
447 429 445 436 435 446 letrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ≤ 𝐾 )
448 422 423 426 431 447 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ∈ ( 1 ... 𝐾 ) )
449 421 448 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑏 ‘ 𝑠 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
450 elfznn ⊢ ( ( 𝑏 ‘ 𝑠 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑠 ) ∈ ℕ )
451 450 nnzd ⊢ ( ( 𝑏 ‘ 𝑠 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑠 ) ∈ ℤ )
452 449 451 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑏 ‘ 𝑠 ) ∈ ℤ )
453 444 452 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ∈ ℤ )
454 453 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ∈ ℂ )
455 fvoveq1 ⊢ ( 𝑠 = ( 𝑖 − 1 ) → ( 𝑏 ‘ ( 𝑠 + 1 ) ) = ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) )
456 fveq2 ⊢ ( 𝑠 = ( 𝑖 − 1 ) → ( 𝑏 ‘ 𝑠 ) = ( 𝑏 ‘ ( 𝑖 − 1 ) ) )
457 455 456 oveq12d ⊢ ( 𝑠 = ( 𝑖 − 1 ) → ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) = ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
458 31 31 420 454 457 fsumshft ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) = Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
459 458 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
460 459 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ) )
461 fvoveq1 ⊢ ( 𝑠 = 𝑖 → ( 𝑏 ‘ ( 𝑠 + 1 ) ) = ( 𝑏 ‘ ( 𝑖 + 1 ) ) )
462 fveq2 ⊢ ( 𝑠 = 𝑖 → ( 𝑏 ‘ 𝑠 ) = ( 𝑏 ‘ 𝑖 ) )
463 461 462 oveq12d ⊢ ( 𝑠 = 𝑖 → ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) = ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) )
464 nfcv ⊢ Ⅎ 𝑖 ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) )
465 nfcv ⊢ Ⅎ 𝑠 ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) )
466 463 464 465 cbvsum ⊢ Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) = Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) )
467 466 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) = Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) )
468 467 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) ) )
469 fveq2 ⊢ ( 𝑤 = 𝑖 → ( 𝑏 ‘ 𝑤 ) = ( 𝑏 ‘ 𝑖 ) )
470 fveq2 ⊢ ( 𝑤 = ( 𝑖 + 1 ) → ( 𝑏 ‘ 𝑤 ) = ( 𝑏 ‘ ( 𝑖 + 1 ) ) )
471 fveq2 ⊢ ( 𝑤 = 1 → ( 𝑏 ‘ 𝑤 ) = ( 𝑏 ‘ 1 ) )
472 fveq2 ⊢ ( 𝑤 = ( ( 𝐾 − 1 ) + 1 ) → ( 𝑏 ‘ 𝑤 ) = ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) )
473 404 214 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐾 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
474 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
475 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 1 ∈ ℤ )
476 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝐾 ∈ ℤ )
477 elfzelz ⊢ ( 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) → 𝑤 ∈ ℤ )
478 477 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑤 ∈ ℤ )
479 elfzle1 ⊢ ( 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) → 1 ≤ 𝑤 )
480 479 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 1 ≤ 𝑤 )
481 elfzle2 ⊢ ( 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) → 𝑤 ≤ ( ( 𝐾 − 1 ) + 1 ) )
482 481 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑤 ≤ ( ( 𝐾 − 1 ) + 1 ) )
483 404 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
484 482 483 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑤 ≤ 𝐾 )
485 475 476 478 480 484 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑤 ∈ ( 1 ... 𝐾 ) )
486 474 485 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( 𝑏 ‘ 𝑤 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
487 elfznn ⊢ ( ( 𝑏 ‘ 𝑤 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑤 ) ∈ ℕ )
488 487 nncnd ⊢ ( ( 𝑏 ‘ 𝑤 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑤 ) ∈ ℂ )
489 486 488 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( 𝑏 ‘ 𝑤 ) ∈ ℂ )
490 469 470 471 472 420 473 489 telfsum2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) = ( ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) − ( 𝑏 ‘ 1 ) ) )
491 490 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) ) = ( ( 𝑏 ‘ 1 ) + ( ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) − ( 𝑏 ‘ 1 ) ) ) )
492 73 recnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 1 ) ∈ ℂ )
493 39 nncnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝐾 ) ∈ ℂ )
494 404 fveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( 𝑏 ‘ 𝐾 ) )
495 494 eleq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) ∈ ℂ ↔ ( 𝑏 ‘ 𝐾 ) ∈ ℂ ) )
496 493 495 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) ∈ ℂ )
497 492 496 pncan3d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + ( ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) − ( 𝑏 ‘ 1 ) ) ) = ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) )
498 497 494 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + ( ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) − ( 𝑏 ‘ 1 ) ) ) = ( 𝑏 ‘ 𝐾 ) )
499 491 498 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑏 ‘ 𝐾 ) )
500 468 499 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ) = ( 𝑏 ‘ 𝐾 ) )
501 460 500 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 𝐾 ) )
502 419 501 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 𝐾 ) )
503 408 502 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 𝐾 ) )
504 402 503 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) = ( 𝑏 ‘ 𝐾 ) )
505 388 504 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 𝐾 ) )
506 fsumconst ⊢ ( ( ( 1 ... 𝐾 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) 1 = ( ( ♯ ‘ ( 1 ... 𝐾 ) ) · 1 ) )
507 346 68 506 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) 1 = ( ( ♯ ‘ ( 1 ... 𝐾 ) ) · 1 ) )
508 212 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ∈ ℕ0 )
509 hashfz1 ⊢ ( 𝐾 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝐾 ) ) = 𝐾 )
510 508 509 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ♯ ‘ ( 1 ... 𝐾 ) ) = 𝐾 )
511 510 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( ♯ ‘ ( 1 ... 𝐾 ) ) · 1 ) = ( 𝐾 · 1 ) )
512 403 mulridd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐾 · 1 ) = 𝐾 )
513 511 512 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( ♯ ‘ ( 1 ... 𝐾 ) ) · 1 ) = 𝐾 )
514 507 513 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) 1 = 𝐾 )
515 505 514 oveq12d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... 𝐾 ) 1 ) = ( ( 𝑏 ‘ 𝐾 ) − 𝐾 ) )
516 385 515 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( ( 𝑏 ‘ 𝐾 ) − 𝐾 ) )
517 43 addlidd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 0 + ( 𝑏 ‘ 𝐾 ) ) = ( 𝑏 ‘ 𝐾 ) )
518 517 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝐾 ) = ( 0 + ( 𝑏 ‘ 𝐾 ) ) )
519 518 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 𝐾 ) − 𝐾 ) = ( ( 0 + ( 𝑏 ‘ 𝐾 ) ) − 𝐾 ) )
520 516 519 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( ( 0 + ( 𝑏 ‘ 𝐾 ) ) − 𝐾 ) )
521 0cnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 0 ∈ ℂ )
522 521 403 43 subsub3d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 0 − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) = ( ( 0 + ( 𝑏 ‘ 𝐾 ) ) − 𝐾 ) )
523 522 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 0 + ( 𝑏 ‘ 𝐾 ) ) − 𝐾 ) = ( 0 − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) )
524 520 523 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( 0 − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) )
525 14 zcnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑁 ∈ ℂ )
526 525 subidd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑁 − 𝑁 ) = 0 )
527 526 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 0 = ( 𝑁 − 𝑁 ) )
528 527 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 0 − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) = ( ( 𝑁 − 𝑁 ) − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) )
529 524 528 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( ( 𝑁 − 𝑁 ) − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) )
530 403 43 subcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ∈ ℂ )
531 525 525 530 subsub4d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑁 − 𝑁 ) − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) = ( 𝑁 − ( 𝑁 + ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) ) )
532 529 531 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( 𝑁 − ( 𝑁 + ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) ) )
533 525 403 43 addsubassd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) = ( 𝑁 + ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) )
534 533 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑁 + ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) = ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) )
535 534 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑁 − ( 𝑁 + ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) ) = ( 𝑁 − ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) )
536 532 535 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( 𝑁 − ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) )
537 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 1 ∈ ℤ )
538 382 537 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) ∈ ℤ )
539 346 538 fsumzcl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) ∈ ℤ )
540 539 zcnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) ∈ ℂ )
541 54 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℂ )
542 540 541 525 addlsub ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) = 𝑁 ↔ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( 𝑁 − ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) ) )
543 536 542 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) = 𝑁 )
544 345 543 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) = 𝑁 )
545 328 544 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) = 𝑁 )
546 313 545 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) + if ( ( 𝐾 + 1 ) = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( ( 𝐾 + 1 ) = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ ( 𝐾 + 1 ) ) − ( 𝑏 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) − 1 ) ) ) ) = 𝑁 )
547 310 546 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) = 𝑁 )
548 211 547 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) = 𝑁 )
549 193 548 jca ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) = 𝑁 ) )
550 ovex ⊢ ( 1 ... ( 𝐾 + 1 ) ) ∈ V
551 550 mptex ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∈ V
552 feq1 ⊢ ( 𝑔 = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) → ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ↔ ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ) )
553 simpl ⊢ ( ( 𝑔 = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑔 = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) )
554 553 fveq1d ⊢ ( ( 𝑔 = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝑔 ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) )
555 554 sumeq2dv ⊢ ( 𝑔 = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) )
556 555 eqeq1d ⊢ ( 𝑔 = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) → ( Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) = 𝑁 ) )
557 552 556 anbi12d ⊢ ( 𝑔 = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) → ( ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) ↔ ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) = 𝑁 ) ) )
558 551 557 elab ⊢ ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) = 𝑁 ) )
559 549 558 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
560 4 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
561 559 560 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∈ 𝐴 )
562 10 561 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) ∈ 𝐴 )
563 562 3 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )