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 14 zcnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑁 ∈ ℂ )
347 54 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ∈ ℂ )
348 fzfid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 1 ... 𝐾 ) ∈ Fin )
349 eleq1 ⊢ ( ( 𝑏 ‘ 1 ) = if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) → ( ( 𝑏 ‘ 1 ) ∈ ℤ ↔ if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ℤ ) )
350 eleq1 ⊢ ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) = if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) → ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ℤ ↔ if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ℤ ) )
351 66 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑖 = 1 ) → ( 𝑏 ‘ 1 ) ∈ ℤ )
352 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
353 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑖 ∈ ( 1 ... 𝐾 ) )
354 352 353 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
355 265 nnzd ⊢ ( ( 𝑏 ‘ 𝑖 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℤ )
356 354 355 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℤ )
357 356 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ 𝑖 ) ∈ ℤ )
358 352 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
359 1zzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ∈ ℤ )
360 16 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 𝐾 ∈ ℤ )
361 315 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑖 ∈ ℤ )
362 361 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ∈ ℤ )
363 362 359 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑖 − 1 ) ∈ ℤ )
364 315 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 1 ≤ 𝑖 )
365 364 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ≤ 𝑖 )
366 338 273 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ≠ 1 )
367 365 366 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 1 ≤ 𝑖 ∧ 𝑖 ≠ 1 ) )
368 318 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ∈ ℝ )
369 316 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 𝑖 ∈ ℝ )
370 368 369 ltlend ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 1 < 𝑖 ↔ ( 1 ≤ 𝑖 ∧ 𝑖 ≠ 1 ) ) )
371 367 370 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 1 < 𝑖 )
372 zltlem1 ⊢ ( ( 1 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 1 < 𝑖 ↔ 1 ≤ ( 𝑖 − 1 ) ) )
373 359 362 372 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 1 < 𝑖 ↔ 1 ≤ ( 𝑖 − 1 ) ) )
374 371 373 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → 1 ≤ ( 𝑖 − 1 ) )
375 316 318 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑖 − 1 ) ∈ ℝ )
376 316 lem1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑖 − 1 ) ≤ 𝑖 )
377 375 316 317 376 321 letrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑖 − 1 ) ≤ 𝐾 )
378 377 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑖 − 1 ) ≤ 𝐾 )
379 359 360 363 374 378 elfzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑖 − 1 ) ∈ ( 1 ... 𝐾 ) )
380 358 379 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
381 380 293 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ℕ )
382 381 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) ∈ ℤ )
383 357 382 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ ¬ 𝑖 = 1 ) → ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ∈ ℤ )
384 349 350 351 383 ifbothda ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ℤ )
385 384 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ∈ ℂ )
386 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 1 ∈ ℂ )
387 348 385 386 fsumsub ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... 𝐾 ) 1 ) )
388 id ⊢ ( 𝑖 = 1 → 𝑖 = 1 )
389 388 iftrued ⊢ ( 𝑖 = 1 → if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 1 ) )
390 214 385 389 fsum1p ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) )
391 60 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 1 ∈ ℝ )
392 elfzle1 ⊢ ( 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) → ( 1 + 1 ) ≤ 𝑖 )
393 392 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → ( 1 + 1 ) ≤ 𝑖 )
394 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 1 ∈ ℤ )
395 elfzelz ⊢ ( 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) → 𝑖 ∈ ℤ )
396 395 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 𝑖 ∈ ℤ )
397 394 396 280 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → ( 1 < 𝑖 ↔ ( 1 + 1 ) ≤ 𝑖 ) )
398 393 397 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 1 < 𝑖 )
399 391 398 ltned ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 1 ≠ 𝑖 )
400 399 necomd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → 𝑖 ≠ 1 )
401 400 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → ¬ 𝑖 = 1 )
402 401 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ) → if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
403 402 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
404 403 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
405 34 recnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ∈ ℂ )
406 405 68 npcand ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
407 406 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 = ( ( 𝐾 − 1 ) + 1 ) )
408 407 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 1 + 1 ) ... 𝐾 ) = ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) )
409 408 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) = Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
410 409 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
411 elfzelz ⊢ ( 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) → 𝑖 ∈ ℤ )
412 411 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑖 ∈ ℤ )
413 412 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑖 ∈ ℂ )
414 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 1 ∈ ℂ )
415 413 414 npcand ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( ( 𝑖 − 1 ) + 1 ) = 𝑖 )
416 415 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑖 = ( ( 𝑖 − 1 ) + 1 ) )
417 416 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( 𝑏 ‘ 𝑖 ) = ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) )
418 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( 𝑏 ‘ ( 𝑖 − 1 ) ) = ( 𝑏 ‘ ( 𝑖 − 1 ) ) )
419 417 418 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) = ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
420 419 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) = Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
421 420 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
422 16 31 zsubcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐾 − 1 ) ∈ ℤ )
423 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
424 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 1 ∈ ℤ )
425 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℤ )
426 elfznn ⊢ ( 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) → 𝑠 ∈ ℕ )
427 426 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ∈ ℕ )
428 427 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ∈ ℤ )
429 428 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑠 + 1 ) ∈ ℤ )
430 1red ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 1 ∈ ℝ )
431 427 nnred ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ∈ ℝ )
432 431 430 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑠 + 1 ) ∈ ℝ )
433 427 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 1 ≤ 𝑠 )
434 431 lep1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ≤ ( 𝑠 + 1 ) )
435 430 431 432 433 434 letrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 1 ≤ ( 𝑠 + 1 ) )
436 elfzle2 ⊢ ( 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) → 𝑠 ≤ ( 𝐾 − 1 ) )
437 436 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ≤ ( 𝐾 − 1 ) )
438 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℝ )
439 leaddsub ⊢ ( ( 𝑠 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( 𝑠 + 1 ) ≤ 𝐾 ↔ 𝑠 ≤ ( 𝐾 − 1 ) ) )
440 431 430 438 439 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑠 + 1 ) ≤ 𝐾 ↔ 𝑠 ≤ ( 𝐾 − 1 ) ) )
441 437 440 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑠 + 1 ) ≤ 𝐾 )
442 424 425 429 435 441 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑠 + 1 ) ∈ ( 1 ... 𝐾 ) )
443 423 442 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑏 ‘ ( 𝑠 + 1 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
444 elfznn ⊢ ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ ( 𝑠 + 1 ) ) ∈ ℕ )
445 443 444 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑏 ‘ ( 𝑠 + 1 ) ) ∈ ℕ )
446 445 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑏 ‘ ( 𝑠 + 1 ) ) ∈ ℤ )
447 438 430 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) ∈ ℝ )
448 438 lem1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) ≤ 𝐾 )
449 431 447 438 437 448 letrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ≤ 𝐾 )
450 424 425 428 433 449 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → 𝑠 ∈ ( 1 ... 𝐾 ) )
451 423 450 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑏 ‘ 𝑠 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
452 elfznn ⊢ ( ( 𝑏 ‘ 𝑠 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑠 ) ∈ ℕ )
453 452 nnzd ⊢ ( ( 𝑏 ‘ 𝑠 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑠 ) ∈ ℤ )
454 451 453 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( 𝑏 ‘ 𝑠 ) ∈ ℤ )
455 446 454 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ∈ ℤ )
456 455 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ) → ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ∈ ℂ )
457 fvoveq1 ⊢ ( 𝑠 = ( 𝑖 − 1 ) → ( 𝑏 ‘ ( 𝑠 + 1 ) ) = ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) )
458 fveq2 ⊢ ( 𝑠 = ( 𝑖 − 1 ) → ( 𝑏 ‘ 𝑠 ) = ( 𝑏 ‘ ( 𝑖 − 1 ) ) )
459 457 458 oveq12d ⊢ ( 𝑠 = ( 𝑖 − 1 ) → ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) = ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
460 31 31 422 456 459 fsumshft ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) = Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) )
461 460 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) )
462 461 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ) )
463 fvoveq1 ⊢ ( 𝑠 = 𝑖 → ( 𝑏 ‘ ( 𝑠 + 1 ) ) = ( 𝑏 ‘ ( 𝑖 + 1 ) ) )
464 fveq2 ⊢ ( 𝑠 = 𝑖 → ( 𝑏 ‘ 𝑠 ) = ( 𝑏 ‘ 𝑖 ) )
465 463 464 oveq12d ⊢ ( 𝑠 = 𝑖 → ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) = ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) )
466 nfcv ⊢ Ⅎ 𝑖 ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) )
467 nfcv ⊢ Ⅎ 𝑠 ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) )
468 465 466 467 cbvsum ⊢ Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) = Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) )
469 468 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) = Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) )
470 469 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ) = ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) ) )
471 fveq2 ⊢ ( 𝑤 = 𝑖 → ( 𝑏 ‘ 𝑤 ) = ( 𝑏 ‘ 𝑖 ) )
472 fveq2 ⊢ ( 𝑤 = ( 𝑖 + 1 ) → ( 𝑏 ‘ 𝑤 ) = ( 𝑏 ‘ ( 𝑖 + 1 ) ) )
473 fveq2 ⊢ ( 𝑤 = 1 → ( 𝑏 ‘ 𝑤 ) = ( 𝑏 ‘ 1 ) )
474 fveq2 ⊢ ( 𝑤 = ( ( 𝐾 − 1 ) + 1 ) → ( 𝑏 ‘ 𝑤 ) = ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) )
475 406 214 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐾 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
476 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑏 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
477 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 1 ∈ ℤ )
478 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝐾 ∈ ℤ )
479 elfzelz ⊢ ( 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) → 𝑤 ∈ ℤ )
480 479 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑤 ∈ ℤ )
481 elfzle1 ⊢ ( 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) → 1 ≤ 𝑤 )
482 481 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 1 ≤ 𝑤 )
483 elfzle2 ⊢ ( 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) → 𝑤 ≤ ( ( 𝐾 − 1 ) + 1 ) )
484 483 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑤 ≤ ( ( 𝐾 − 1 ) + 1 ) )
485 406 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
486 484 485 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑤 ≤ 𝐾 )
487 477 478 480 482 486 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑤 ∈ ( 1 ... 𝐾 ) )
488 476 487 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( 𝑏 ‘ 𝑤 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
489 elfznn ⊢ ( ( 𝑏 ‘ 𝑤 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑤 ) ∈ ℕ )
490 489 nncnd ⊢ ( ( 𝑏 ‘ 𝑤 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) → ( 𝑏 ‘ 𝑤 ) ∈ ℂ )
491 488 490 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑤 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ) → ( 𝑏 ‘ 𝑤 ) ∈ ℂ )
492 471 472 473 474 422 475 491 telfsum2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) = ( ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) − ( 𝑏 ‘ 1 ) ) )
493 492 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) ) = ( ( 𝑏 ‘ 1 ) + ( ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) − ( 𝑏 ‘ 1 ) ) ) )
494 73 recnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 1 ) ∈ ℂ )
495 39 nncnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝐾 ) ∈ ℂ )
496 406 fveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( 𝑏 ‘ 𝐾 ) )
497 496 eleq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) ∈ ℂ ↔ ( 𝑏 ‘ 𝐾 ) ∈ ℂ ) )
498 495 497 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) ∈ ℂ )
499 494 498 pncan3d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + ( ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) − ( 𝑏 ‘ 1 ) ) ) = ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) )
500 499 496 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + ( ( 𝑏 ‘ ( ( 𝐾 − 1 ) + 1 ) ) − ( 𝑏 ‘ 1 ) ) ) = ( 𝑏 ‘ 𝐾 ) )
501 493 500 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑖 + 1 ) ) − ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑏 ‘ 𝐾 ) )
502 470 501 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑠 ∈ ( 1 ... ( 𝐾 − 1 ) ) ( ( 𝑏 ‘ ( 𝑠 + 1 ) ) − ( 𝑏 ‘ 𝑠 ) ) ) = ( 𝑏 ‘ 𝐾 ) )
503 462 502 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ ( ( 𝑖 − 1 ) + 1 ) ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 𝐾 ) )
504 421 503 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... ( ( 𝐾 − 1 ) + 1 ) ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 𝐾 ) )
505 410 504 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 𝐾 ) )
506 404 505 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 1 ) + Σ 𝑖 ∈ ( ( 1 + 1 ) ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) ) = ( 𝑏 ‘ 𝐾 ) )
507 390 506 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) = ( 𝑏 ‘ 𝐾 ) )
508 fsumconst ⊢ ( ( ( 1 ... 𝐾 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) 1 = ( ( ♯ ‘ ( 1 ... 𝐾 ) ) · 1 ) )
509 348 68 508 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) 1 = ( ( ♯ ‘ ( 1 ... 𝐾 ) ) · 1 ) )
510 212 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐾 ∈ ℕ0 )
511 hashfz1 ⊢ ( 𝐾 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝐾 ) ) = 𝐾 )
512 510 511 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ♯ ‘ ( 1 ... 𝐾 ) ) = 𝐾 )
513 512 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( ♯ ‘ ( 1 ... 𝐾 ) ) · 1 ) = ( 𝐾 · 1 ) )
514 405 mulridd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐾 · 1 ) = 𝐾 )
515 513 514 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( ♯ ‘ ( 1 ... 𝐾 ) ) · 1 ) = 𝐾 )
516 509 515 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) 1 = 𝐾 )
517 507 516 oveq12d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − Σ 𝑖 ∈ ( 1 ... 𝐾 ) 1 ) = ( ( 𝑏 ‘ 𝐾 ) − 𝐾 ) )
518 387 517 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( ( 𝑏 ‘ 𝐾 ) − 𝐾 ) )
519 43 addlidd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 0 + ( 𝑏 ‘ 𝐾 ) ) = ( 𝑏 ‘ 𝐾 ) )
520 519 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ‘ 𝐾 ) = ( 0 + ( 𝑏 ‘ 𝐾 ) ) )
521 520 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑏 ‘ 𝐾 ) − 𝐾 ) = ( ( 0 + ( 𝑏 ‘ 𝐾 ) ) − 𝐾 ) )
522 518 521 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( ( 0 + ( 𝑏 ‘ 𝐾 ) ) − 𝐾 ) )
523 0cnd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 0 ∈ ℂ )
524 523 405 43 subsub3d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 0 − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) = ( ( 0 + ( 𝑏 ‘ 𝐾 ) ) − 𝐾 ) )
525 524 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 0 + ( 𝑏 ‘ 𝐾 ) ) − 𝐾 ) = ( 0 − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) )
526 522 525 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( 0 − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) )
527 346 subidd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑁 − 𝑁 ) = 0 )
528 527 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 0 = ( 𝑁 − 𝑁 ) )
529 528 oveq1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 0 − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) = ( ( 𝑁 − 𝑁 ) − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) )
530 526 529 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( ( 𝑁 − 𝑁 ) − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) )
531 405 43 subcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ∈ ℂ )
532 346 346 531 subsub4d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑁 − 𝑁 ) − ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) = ( 𝑁 − ( 𝑁 + ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) ) )
533 530 532 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( 𝑁 − ( 𝑁 + ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) ) )
534 346 405 43 addsubassd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) = ( 𝑁 + ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) )
535 534 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑁 + ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) = ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) )
536 535 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑁 − ( 𝑁 + ( 𝐾 − ( 𝑏 ‘ 𝐾 ) ) ) ) = ( 𝑁 − ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) )
537 533 536 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) = ( 𝑁 − ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) )
538 346 347 537 mvrrsubd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( if ( 𝑖 = 1 , ( 𝑏 ‘ 1 ) , ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) ) − 1 ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) = 𝑁 )
539 345 538 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) = 𝑁 )
540 328 539 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) + ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) ) = 𝑁 )
541 313 540 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) + if ( ( 𝐾 + 1 ) = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( ( 𝐾 + 1 ) = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ ( 𝐾 + 1 ) ) − ( 𝑏 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) − 1 ) ) ) ) = 𝑁 )
542 310 541 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) if ( 𝑖 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑖 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ ( 𝑖 − 1 ) ) ) − 1 ) ) ) = 𝑁 )
543 211 542 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) = 𝑁 )
544 193 543 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 ) ) ) ) ‘ 𝑖 ) = 𝑁 ) )
545 ovex ⊢ ( 1 ... ( 𝐾 + 1 ) ) ∈ V
546 545 mptex ⊢ ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∈ V
547 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 ) )
548 simpl ⊢ ( ( 𝑔 = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑔 = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) )
549 548 fveq1d ⊢ ( ( 𝑔 = ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝑔 ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ‘ 𝑖 ) )
550 549 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 ) ) ) ) ‘ 𝑖 ) )
551 550 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 ) ) ) ) ‘ 𝑖 ) = 𝑁 ) )
552 547 551 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 ) ) ) ) ‘ 𝑖 ) = 𝑁 ) ) )
553 546 552 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 ) ) ) ) ‘ 𝑖 ) = 𝑁 ) )
554 544 553 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
555 4 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
556 554 555 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ∈ 𝐴 )
557 10 556 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) ∈ 𝐴 )
558 557 3 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )