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