Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sticksstones10 Structured version   Visualization version   GIF version

Theorem sticksstones10 40100
Description: Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024.)
Hypotheses
Ref Expression
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
Ref Expression
sticksstones10 (𝜑𝐺:𝐵𝐴)
Distinct variable groups:   𝐴,𝑏   𝐵,𝑏,𝑖,𝑘   𝑓,𝐾,𝑥,𝑦   𝑔,𝐾,𝑖,𝑘   𝑓,𝑁   𝑔,𝑁,𝑖,𝑘   𝑓,𝑏,𝑥,𝑦   𝑔,𝑏   𝜑,𝑏,𝑖,𝑘   𝑥,𝑘,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑔)   𝐴(𝑥,𝑦,𝑓,𝑔,𝑖,𝑘)   𝐵(𝑥,𝑦,𝑓,𝑔)   𝐺(𝑥,𝑦,𝑓,𝑔,𝑖,𝑘,𝑏)   𝐾(𝑏)   𝑁(𝑥,𝑦,𝑏)

Proof of Theorem sticksstones10
Dummy variables 𝑠 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sticksstones10.2 . . . . . . . 8 (𝜑𝐾 ∈ ℕ)
21nnne0d 12015 . . . . . . 7 (𝜑𝐾 ≠ 0)
32adantr 481 . . . . . 6 ((𝜑𝑏𝐵) → 𝐾 ≠ 0)
43neneqd 2950 . . . . 5 ((𝜑𝑏𝐵) → ¬ 𝐾 = 0)
54iffalsed 4476 . . . 4 ((𝜑𝑏𝐵) → if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))
65eqcomd 2746 . . 3 ((𝜑𝑏𝐵) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) = if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
7 eleq1 2828 . . . . . . . . 9 (((𝑁 + 𝐾) − (𝑏𝐾)) = if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))) → (((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℕ0 ↔ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))) ∈ ℕ0))
8 eleq1 2828 . . . . . . . . 9 (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))
9 sticksstones10.1 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℕ0)
109nn0zd 12415 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℤ)
1110adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → 𝑁 ∈ ℤ)
121nnzd 12416 . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ ℤ)
1312adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → 𝐾 ∈ ℤ)
1411, 13zaddcld 12421 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝑁 + 𝐾) ∈ ℤ)
15 sticksstones10.5 . . . . . . . . . . . . . . . . . . . . . . 23 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)))}
1615eleq2i 2832 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏𝐵𝑏 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)))})
17 vex 3435 . . . . . . . . . . . . . . . . . . . . . . 23 𝑏 ∈ V
18 feq1 6578 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑏 → (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾))))
19 fveq1 6768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑏 → (𝑓𝑥) = (𝑏𝑥))
20 fveq1 6768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑏 → (𝑓𝑦) = (𝑏𝑦))
2119, 20breq12d 5092 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑏 → ((𝑓𝑥) < (𝑓𝑦) ↔ (𝑏𝑥) < (𝑏𝑦)))
2221imbi2d 341 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑏 → ((𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)) ↔ (𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦))))
23222ralbidv 3125 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑏 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦))))
2418, 23anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑏 → ((𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦))) ↔ (𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦)))))
2517, 24elab 3611 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓𝑥) < (𝑓𝑦)))} ↔ (𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦))))
2616, 25bitri 274 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝐵 ↔ (𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦))))
2726biimpi 215 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐵 → (𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦))))
2827adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵) → (𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦))))
2928simpld 495 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
30 1zzd 12343 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵) → 1 ∈ ℤ)
311nnge1d 12013 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 1 ≤ 𝐾)
3231adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵) → 1 ≤ 𝐾)
3313zred 12417 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑏𝐵) → 𝐾 ∈ ℝ)
3433leidd 11533 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵) → 𝐾𝐾)
3530, 13, 13, 32, 34elfzd 13238 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → 𝐾 ∈ (1...𝐾))
3629, 35ffvelrnd 6957 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → (𝑏𝐾) ∈ (1...(𝑁 + 𝐾)))
37 elfznn 13276 . . . . . . . . . . . . . . . . 17 ((𝑏𝐾) ∈ (1...(𝑁 + 𝐾)) → (𝑏𝐾) ∈ ℕ)
3836, 37syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → (𝑏𝐾) ∈ ℕ)
3938nnzd 12416 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝑏𝐾) ∈ ℤ)
4014, 39zsubcld 12422 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → ((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℤ)
4138nnred 11980 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → (𝑏𝐾) ∈ ℝ)
4241recnd 10996 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → (𝑏𝐾) ∈ ℂ)
4342addid1d 11167 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → ((𝑏𝐾) + 0) = (𝑏𝐾))
44 elfzle2 13251 . . . . . . . . . . . . . . . . 17 ((𝑏𝐾) ∈ (1...(𝑁 + 𝐾)) → (𝑏𝐾) ≤ (𝑁 + 𝐾))
4536, 44syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → (𝑏𝐾) ≤ (𝑁 + 𝐾))
4643, 45eqbrtrd 5101 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → ((𝑏𝐾) + 0) ≤ (𝑁 + 𝐾))
47 0red 10971 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → 0 ∈ ℝ)
4814zred 12417 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → (𝑁 + 𝐾) ∈ ℝ)
4941, 47, 48leaddsub2d 11569 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (((𝑏𝐾) + 0) ≤ (𝑁 + 𝐾) ↔ 0 ≤ ((𝑁 + 𝐾) − (𝑏𝐾))))
5046, 49mpbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → 0 ≤ ((𝑁 + 𝐾) − (𝑏𝐾)))
5140, 50jca 512 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℤ ∧ 0 ≤ ((𝑁 + 𝐾) − (𝑏𝐾))))
52 elnn0z 12324 . . . . . . . . . . . . 13 (((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℕ0 ↔ (((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℤ ∧ 0 ≤ ((𝑁 + 𝐾) − (𝑏𝐾))))
5351, 52sylibr 233 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℕ0)
5453adantr 481 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → ((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℕ0)
55543impa 1109 . . . . . . . . . 10 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → ((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℕ0)
5655adantr 481 . . . . . . . . 9 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → ((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℕ0)
57 eleq1 2828 . . . . . . . . . 10 (((𝑏‘1) − 1) = if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)) → (((𝑏‘1) − 1) ∈ ℕ0 ↔ if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)) ∈ ℕ0))
58 eleq1 2828 . . . . . . . . . 10 ((((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1) = if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)) → ((((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1) ∈ ℕ0 ↔ if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)) ∈ ℕ0))
59 1red 10969 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑏𝐵) → 1 ∈ ℝ)
6059leidd 11533 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑏𝐵) → 1 ≤ 1)
6130, 13, 30, 60, 32elfzd 13238 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵) → 1 ∈ (1...𝐾))
6229, 61ffvelrnd 6957 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → (𝑏‘1) ∈ (1...(𝑁 + 𝐾)))
63 elfznn 13276 . . . . . . . . . . . . . . . . . . 19 ((𝑏‘1) ∈ (1...(𝑁 + 𝐾)) → (𝑏‘1) ∈ ℕ)
6463nnzd 12416 . . . . . . . . . . . . . . . . . 18 ((𝑏‘1) ∈ (1...(𝑁 + 𝐾)) → (𝑏‘1) ∈ ℤ)
6562, 64syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → (𝑏‘1) ∈ ℤ)
6665, 30zsubcld 12422 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → ((𝑏‘1) − 1) ∈ ℤ)
67 1cnd 10963 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵) → 1 ∈ ℂ)
6867addid1d 11167 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → (1 + 0) = 1)
69 elfzle1 13250 . . . . . . . . . . . . . . . . . . 19 ((𝑏‘1) ∈ (1...(𝑁 + 𝐾)) → 1 ≤ (𝑏‘1))
7062, 69syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → 1 ≤ (𝑏‘1))
7168, 70eqbrtrd 5101 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → (1 + 0) ≤ (𝑏‘1))
7265zred 12417 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → (𝑏‘1) ∈ ℝ)
7359, 47, 72leaddsub2d 11569 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → ((1 + 0) ≤ (𝑏‘1) ↔ 0 ≤ ((𝑏‘1) − 1)))
7471, 73mpbid 231 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → 0 ≤ ((𝑏‘1) − 1))
7566, 74jca 512 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (((𝑏‘1) − 1) ∈ ℤ ∧ 0 ≤ ((𝑏‘1) − 1)))
76 elnn0z 12324 . . . . . . . . . . . . . . 15 (((𝑏‘1) − 1) ∈ ℕ0 ↔ (((𝑏‘1) − 1) ∈ ℤ ∧ 0 ≤ ((𝑏‘1) − 1)))
7775, 76sylibr 233 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → ((𝑏‘1) − 1) ∈ ℕ0)
7877adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → ((𝑏‘1) − 1) ∈ ℕ0)
79783impa 1109 . . . . . . . . . . . 12 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → ((𝑏‘1) − 1) ∈ ℕ0)
8079adantr 481 . . . . . . . . . . 11 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → ((𝑏‘1) − 1) ∈ ℕ0)
8180adantr 481 . . . . . . . . . 10 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → ((𝑏‘1) − 1) ∈ ℕ0)
82293adant3 1131 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
8382adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
84 1zzd 12343 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ∈ ℤ)
85133adant3 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → 𝐾 ∈ ℤ)
8685adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝐾 ∈ ℤ)
87 simp3 1137 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ (1...(𝐾 + 1)))
88 elfznn 13276 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ∈ ℕ)
8987, 88syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℕ)
9089adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℕ)
9190nnzd 12416 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℤ)
9290nnge1d 12013 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ≤ 𝑘)
93 elfzle2 13251 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ≤ (𝐾 + 1))
9487, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ≤ (𝐾 + 1))
9594adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≤ (𝐾 + 1))
96 neqne 2953 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = (𝐾 + 1) → 𝑘 ≠ (𝐾 + 1))
9796adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≠ (𝐾 + 1))
9897necomd 3001 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑘)
9995, 98jca 512 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑘))
10090nnred 11980 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℝ)
10186zred 12417 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝐾 ∈ ℝ)
102 1red 10969 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ∈ ℝ)
103101, 102readdcld 10997 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
104100, 103ltlend 11112 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 < (𝐾 + 1) ↔ (𝑘 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑘)))
10599, 104mpbird 256 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 < (𝐾 + 1))
10689nnzd 12416 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℤ)
107 zleltp1 12363 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘𝐾𝑘 < (𝐾 + 1)))
108106, 85, 107syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → (𝑘𝐾𝑘 < (𝐾 + 1)))
109108adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘𝐾𝑘 < (𝐾 + 1)))
110105, 109mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘𝐾)
11184, 86, 91, 92, 110elfzd 13238 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ (1...𝐾))
11283, 111ffvelrnd 6957 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑏𝑘) ∈ (1...(𝑁 + 𝐾)))
113 elfznn 13276 . . . . . . . . . . . . . . . . 17 ((𝑏𝑘) ∈ (1...(𝑁 + 𝐾)) → (𝑏𝑘) ∈ ℕ)
114112, 113syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑏𝑘) ∈ ℕ)
115114nnzd 12416 . . . . . . . . . . . . . . 15 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑏𝑘) ∈ ℤ)
116115adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑏𝑘) ∈ ℤ)
11783adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
118 1zzd 12343 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℤ)
11986adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ)
12091adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ)
121120, 118zsubcld 12422 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℤ)
12292adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ 𝑘)
123 neqne 2953 . . . . . . . . . . . . . . . . . . . . . 22 𝑘 = 1 → 𝑘 ≠ 1)
124123adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≠ 1)
125122, 124jca 512 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 ≤ 𝑘𝑘 ≠ 1))
126102adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℝ)
127100adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℝ)
128126, 127ltlend 11112 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 < 𝑘 ↔ (1 ≤ 𝑘𝑘 ≠ 1)))
129125, 128mpbird 256 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 < 𝑘)
130118, 120zltlem1d 39976 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 < 𝑘 ↔ 1 ≤ (𝑘 − 1)))
131129, 130mpbid 231 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ (𝑘 − 1))
13289nnred 11980 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℝ)
133593adant3 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → 1 ∈ ℝ)
134333adant3 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → 𝐾 ∈ ℝ)
135 lesubadd 11439 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 − 1) ≤ 𝐾𝑘 ≤ (𝐾 + 1)))
136132, 133, 134, 135syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → ((𝑘 − 1) ≤ 𝐾𝑘 ≤ (𝐾 + 1)))
13794, 136mpbird 256 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → (𝑘 − 1) ≤ 𝐾)
138137adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 − 1) ≤ 𝐾)
139138adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ≤ 𝐾)
140118, 119, 121, 131, 139elfzd 13238 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾))
141117, 140ffvelrnd 6957 . . . . . . . . . . . . . . . 16 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑏‘(𝑘 − 1)) ∈ (1...(𝑁 + 𝐾)))
142 elfznn 13276 . . . . . . . . . . . . . . . 16 ((𝑏‘(𝑘 − 1)) ∈ (1...(𝑁 + 𝐾)) → (𝑏‘(𝑘 − 1)) ∈ ℕ)
143141, 142syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑏‘(𝑘 − 1)) ∈ ℕ)
144143nnzd 12416 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑏‘(𝑘 − 1)) ∈ ℤ)
145116, 144zsubcld 12422 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) ∈ ℤ)
146145, 118zsubcld 12422 . . . . . . . . . . . 12 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1) ∈ ℤ)
147 0p1e1 12087 . . . . . . . . . . . . . . 15 (0 + 1) = 1
148147a1i 11 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (0 + 1) = 1)
149 1cnd 10963 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈ ℂ)
150149subidd 11312 . . . . . . . . . . . . . . . 16 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 − 1) = 0)
151144zred 12417 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑏‘(𝑘 − 1)) ∈ ℝ)
152151recnd 10996 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑏‘(𝑘 − 1)) ∈ ℂ)
153152addid1d 11167 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑏‘(𝑘 − 1)) + 0) = (𝑏‘(𝑘 − 1)))
154127ltm1d 11899 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) < 𝑘)
155111adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (1...𝐾))
156140, 155jca 512 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 − 1) ∈ (1...𝐾) ∧ 𝑘 ∈ (1...𝐾)))
15728simprd 496 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑏𝐵) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦)))
1581573adant3 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦)))
159158adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦)))
160159adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦)))
161 breq1 5082 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑘 − 1) → (𝑥 < 𝑦 ↔ (𝑘 − 1) < 𝑦))
162 fveq2 6769 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑘 − 1) → (𝑏𝑥) = (𝑏‘(𝑘 − 1)))
163162breq1d 5089 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑘 − 1) → ((𝑏𝑥) < (𝑏𝑦) ↔ (𝑏‘(𝑘 − 1)) < (𝑏𝑦)))
164161, 163imbi12d 345 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑘 − 1) → ((𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦)) ↔ ((𝑘 − 1) < 𝑦 → (𝑏‘(𝑘 − 1)) < (𝑏𝑦))))
165 breq2 5083 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑘 → ((𝑘 − 1) < 𝑦 ↔ (𝑘 − 1) < 𝑘))
166 fveq2 6769 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑘 → (𝑏𝑦) = (𝑏𝑘))
167166breq2d 5091 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑘 → ((𝑏‘(𝑘 − 1)) < (𝑏𝑦) ↔ (𝑏‘(𝑘 − 1)) < (𝑏𝑘)))
168165, 167imbi12d 345 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑘 → (((𝑘 − 1) < 𝑦 → (𝑏‘(𝑘 − 1)) < (𝑏𝑦)) ↔ ((𝑘 − 1) < 𝑘 → (𝑏‘(𝑘 − 1)) < (𝑏𝑘))))
169164, 168rspc2va 3572 . . . . . . . . . . . . . . . . . . . 20 ((((𝑘 − 1) ∈ (1...𝐾) ∧ 𝑘 ∈ (1...𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑏𝑥) < (𝑏𝑦))) → ((𝑘 − 1) < 𝑘 → (𝑏‘(𝑘 − 1)) < (𝑏𝑘)))
170156, 160, 169syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 − 1) < 𝑘 → (𝑏‘(𝑘 − 1)) < (𝑏𝑘)))
171154, 170mpd 15 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑏‘(𝑘 − 1)) < (𝑏𝑘))
172153, 171eqbrtrd 5101 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑏‘(𝑘 − 1)) + 0) < (𝑏𝑘))
173 0red 10971 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 0 ∈ ℝ)
174116zred 12417 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑏𝑘) ∈ ℝ)
175151, 173, 174ltaddsub2d 11568 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑏‘(𝑘 − 1)) + 0) < (𝑏𝑘) ↔ 0 < ((𝑏𝑘) − (𝑏‘(𝑘 − 1)))))
176172, 175mpbid 231 . . . . . . . . . . . . . . . 16 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 0 < ((𝑏𝑘) − (𝑏‘(𝑘 − 1))))
177150, 176eqbrtrd 5101 . . . . . . . . . . . . . . 15 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 − 1) < ((𝑏𝑘) − (𝑏‘(𝑘 − 1))))
178 zlem1lt 12364 . . . . . . . . . . . . . . . 16 ((1 ∈ ℤ ∧ ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) ∈ ℤ) → (1 ≤ ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) ↔ (1 − 1) < ((𝑏𝑘) − (𝑏‘(𝑘 − 1)))))
179118, 145, 178syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 ≤ ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) ↔ (1 − 1) < ((𝑏𝑘) − (𝑏‘(𝑘 − 1)))))
180177, 179mpbird 256 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ ((𝑏𝑘) − (𝑏‘(𝑘 − 1))))
181148, 180eqbrtrd 5101 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (0 + 1) ≤ ((𝑏𝑘) − (𝑏‘(𝑘 − 1))))
182145zred 12417 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) ∈ ℝ)
183 leaddsub 11443 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) ∈ ℝ) → ((0 + 1) ≤ ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) ↔ 0 ≤ (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))
184173, 126, 182, 183syl3anc 1370 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((0 + 1) ≤ ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) ↔ 0 ≤ (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))
185181, 184mpbid 231 . . . . . . . . . . . 12 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 0 ≤ (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))
186146, 185jca 512 . . . . . . . . . . 11 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1) ∈ ℤ ∧ 0 ≤ (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))
187 elnn0z 12324 . . . . . . . . . . 11 ((((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1) ∈ ℕ0 ↔ ((((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1) ∈ ℤ ∧ 0 ≤ (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))
188186, 187sylibr 233 . . . . . . . . . 10 ((((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1) ∈ ℕ0)
18957, 58, 81, 188ifbothda 4503 . . . . . . . . 9 (((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)) ∈ ℕ0)
1907, 8, 56, 189ifbothda 4503 . . . . . . . 8 ((𝜑𝑏𝐵𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))) ∈ ℕ0)
1911903expa 1117 . . . . . . 7 (((𝜑𝑏𝐵) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))) ∈ ℕ0)
192191fmpttd 6984 . . . . . 6 ((𝜑𝑏𝐵) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))):(1...(𝐾 + 1))⟶ℕ0)
193 eqidd 2741 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))
194 simpr 485 . . . . . . . . . . 11 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = 𝑖) → 𝑘 = 𝑖)
195194eqeq1d 2742 . . . . . . . . . 10 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = 𝑖) → (𝑘 = (𝐾 + 1) ↔ 𝑖 = (𝐾 + 1)))
196194eqeq1d 2742 . . . . . . . . . . 11 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = 𝑖) → (𝑘 = 1 ↔ 𝑖 = 1))
197194fveq2d 6773 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = 𝑖) → (𝑏𝑘) = (𝑏𝑖))
198194fvoveq1d 7291 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = 𝑖) → (𝑏‘(𝑘 − 1)) = (𝑏‘(𝑖 − 1)))
199197, 198oveq12d 7287 . . . . . . . . . . . 12 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = 𝑖) → ((𝑏𝑘) − (𝑏‘(𝑘 − 1))) = ((𝑏𝑖) − (𝑏‘(𝑖 − 1))))
200199oveq1d 7284 . . . . . . . . . . 11 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = 𝑖) → (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1) = (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))
201196, 200ifbieq2d 4491 . . . . . . . . . 10 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = 𝑖) → if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)) = if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)))
202195, 201ifbieq2d 4491 . . . . . . . . 9 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = 𝑖) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))) = if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))))
203 simpr 485 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → 𝑖 ∈ (1...(𝐾 + 1)))
204 ovexd 7304 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → ((𝑁 + 𝐾) − (𝑏𝐾)) ∈ V)
205 ovexd 7304 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → ((𝑏‘1) − 1) ∈ V)
206 ovexd 7304 . . . . . . . . . . 11 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1) ∈ V)
207205, 206ifcld 4511 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) ∈ V)
208204, 207ifcld 4511 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) ∈ V)
209193, 202, 203, 208fvmptd 6877 . . . . . . . 8 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → ((𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))‘𝑖) = if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))))
210209sumeq2dv 15405 . . . . . . 7 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...(𝐾 + 1))((𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))‘𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))))
2111adantr 481 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝐾 ∈ ℕ)
212 nnuz 12612 . . . . . . . . . 10 ℕ = (ℤ‘1)
213211, 212eleqtrdi 2851 . . . . . . . . 9 ((𝜑𝑏𝐵) → 𝐾 ∈ (ℤ‘1))
214 eleq1 2828 . . . . . . . . . . . 12 (((𝑁 + 𝐾) − (𝑏𝐾)) = if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) → (((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℤ ↔ if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) ∈ ℤ))
215 eleq1 2828 . . . . . . . . . . . 12 (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))) ∈ ℤ))
216113adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → 𝑁 ∈ ℤ)
217216adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑖 = (𝐾 + 1)) → 𝑁 ∈ ℤ)
218133adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → 𝐾 ∈ ℤ)
219218adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑖 = (𝐾 + 1)) → 𝐾 ∈ ℤ)
220217, 219zaddcld 12421 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑖 = (𝐾 + 1)) → (𝑁 + 𝐾) ∈ ℤ)
221383adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → (𝑏𝐾) ∈ ℕ)
222221adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑖 = (𝐾 + 1)) → (𝑏𝐾) ∈ ℕ)
223222nnzd 12416 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑖 = (𝐾 + 1)) → (𝑏𝐾) ∈ ℤ)
224220, 223zsubcld 12422 . . . . . . . . . . . 12 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ 𝑖 = (𝐾 + 1)) → ((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℤ)
225 eleq1 2828 . . . . . . . . . . . . 13 (((𝑏‘1) − 1) = if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) → (((𝑏‘1) − 1) ∈ ℤ ↔ if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) ∈ ℤ))
226 eleq1 2828 . . . . . . . . . . . . 13 ((((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1) = if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) → ((((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1) ∈ ℤ ↔ if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) ∈ ℤ))
227653adant3 1131 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → (𝑏‘1) ∈ ℤ)
228227adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → (𝑏‘1) ∈ ℤ)
229228adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ 𝑖 = 1) → (𝑏‘1) ∈ ℤ)
230 1zzd 12343 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ 𝑖 = 1) → 1 ∈ ℤ)
231229, 230zsubcld 12422 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ 𝑖 = 1) → ((𝑏‘1) − 1) ∈ ℤ)
232293adant3 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
233232adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
234233adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
235 1zzd 12343 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 1 ∈ ℤ)
236218adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 𝐾 ∈ ℤ)
237 elfznn 13276 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (1...(𝐾 + 1)) → 𝑖 ∈ ℕ)
238237adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → 𝑖 ∈ ℕ)
2392383impa 1109 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → 𝑖 ∈ ℕ)
240239nnzd 12416 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → 𝑖 ∈ ℤ)
241240adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 𝑖 ∈ ℤ)
242239nnge1d 12013 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → 1 ≤ 𝑖)
243242adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 1 ≤ 𝑖)
244 simp3 1137 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → 𝑖 ∈ (1...(𝐾 + 1)))
245 elfzle2 13251 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (1...(𝐾 + 1)) → 𝑖 ≤ (𝐾 + 1))
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → 𝑖 ≤ (𝐾 + 1))
247246adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 𝑖 ≤ (𝐾 + 1))
248 neqne 2953 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖 = (𝐾 + 1) → 𝑖 ≠ (𝐾 + 1))
249248adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 𝑖 ≠ (𝐾 + 1))
250249necomd 3001 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑖)
251247, 250jca 512 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → (𝑖 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑖))
252241zred 12417 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 𝑖 ∈ ℝ)
253236zred 12417 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 𝐾 ∈ ℝ)
254 1red 10969 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 1 ∈ ℝ)
255253, 254readdcld 10997 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
256252, 255ltlend 11112 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → (𝑖 < (𝐾 + 1) ↔ (𝑖 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑖)))
257251, 256mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 𝑖 < (𝐾 + 1))
258 zleltp1 12363 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑖𝐾𝑖 < (𝐾 + 1)))
259241, 236, 258syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → (𝑖𝐾𝑖 < (𝐾 + 1)))
260257, 259mpbird 256 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 𝑖𝐾)
261235, 236, 241, 243, 260elfzd 13238 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → 𝑖 ∈ (1...𝐾))
262261adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ (1...𝐾))
263234, 262ffvelrnd 6957 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (𝑏𝑖) ∈ (1...(𝑁 + 𝐾)))
264 elfznn 13276 . . . . . . . . . . . . . . . . 17 ((𝑏𝑖) ∈ (1...(𝑁 + 𝐾)) → (𝑏𝑖) ∈ ℕ)
265263, 264syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (𝑏𝑖) ∈ ℕ)
266265nnzd 12416 . . . . . . . . . . . . . . 15 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (𝑏𝑖) ∈ ℤ)
267 1zzd 12343 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 1 ∈ ℤ)
268236adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 𝐾 ∈ ℤ)
269241adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ℤ)
270269, 267zsubcld 12422 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (𝑖 − 1) ∈ ℤ)
271243adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 1 ≤ 𝑖)
272 neqne 2953 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑖 = 1 → 𝑖 ≠ 1)
273272adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 𝑖 ≠ 1)
274271, 273jca 512 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (1 ≤ 𝑖𝑖 ≠ 1))
275 1red 10969 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 1 ∈ ℝ)
276269zred 12417 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ℝ)
277275, 276ltlend 11112 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (1 < 𝑖 ↔ (1 ≤ 𝑖𝑖 ≠ 1)))
278274, 277mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 1 < 𝑖)
279 zltp1le 12362 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (1 < 𝑖 ↔ (1 + 1) ≤ 𝑖))
280267, 269, 279syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (1 < 𝑖 ↔ (1 + 1) ≤ 𝑖))
281278, 280mpbid 231 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (1 + 1) ≤ 𝑖)
282 leaddsub 11443 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑖 ∈ ℝ) → ((1 + 1) ≤ 𝑖 ↔ 1 ≤ (𝑖 − 1)))
283275, 275, 276, 282syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → ((1 + 1) ≤ 𝑖 ↔ 1 ≤ (𝑖 − 1)))
284281, 283mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 1 ≤ (𝑖 − 1))
285247adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 𝑖 ≤ (𝐾 + 1))
286253adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → 𝐾 ∈ ℝ)
287 lesubadd 11439 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑖 − 1) ≤ 𝐾𝑖 ≤ (𝐾 + 1)))
288276, 275, 286, 287syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → ((𝑖 − 1) ≤ 𝐾𝑖 ≤ (𝐾 + 1)))
289285, 288mpbird 256 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (𝑖 − 1) ≤ 𝐾)
290267, 268, 270, 284, 289elfzd 13238 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (𝑖 − 1) ∈ (1...𝐾))
291234, 290ffvelrnd 6957 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (𝑏‘(𝑖 − 1)) ∈ (1...(𝑁 + 𝐾)))
292 elfznn 13276 . . . . . . . . . . . . . . . . 17 ((𝑏‘(𝑖 − 1)) ∈ (1...(𝑁 + 𝐾)) → (𝑏‘(𝑖 − 1)) ∈ ℕ)
293291, 292syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (𝑏‘(𝑖 − 1)) ∈ ℕ)
294293nnzd 12416 . . . . . . . . . . . . . . 15 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (𝑏‘(𝑖 − 1)) ∈ ℤ)
295266, 294zsubcld 12422 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → ((𝑏𝑖) − (𝑏‘(𝑖 − 1))) ∈ ℤ)
296295, 267zsubcld 12422 . . . . . . . . . . . . 13 ((((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) ∧ ¬ 𝑖 = 1) → (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1) ∈ ℤ)
297225, 226, 231, 296ifbothda 4503 . . . . . . . . . . . 12 (((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑖 = (𝐾 + 1)) → if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) ∈ ℤ)
298214, 215, 224, 297ifbothda 4503 . . . . . . . . . . 11 ((𝜑𝑏𝐵𝑖 ∈ (1...(𝐾 + 1))) → if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) ∈ ℤ)
2992983expa 1117 . . . . . . . . . 10 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) ∈ ℤ)
300299zcnd 12418 . . . . . . . . 9 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) ∈ ℂ)
301 eqeq1 2744 . . . . . . . . . 10 (𝑖 = (𝐾 + 1) → (𝑖 = (𝐾 + 1) ↔ (𝐾 + 1) = (𝐾 + 1)))
302 eqeq1 2744 . . . . . . . . . . 11 (𝑖 = (𝐾 + 1) → (𝑖 = 1 ↔ (𝐾 + 1) = 1))
303 fveq2 6769 . . . . . . . . . . . . 13 (𝑖 = (𝐾 + 1) → (𝑏𝑖) = (𝑏‘(𝐾 + 1)))
304 fvoveq1 7292 . . . . . . . . . . . . 13 (𝑖 = (𝐾 + 1) → (𝑏‘(𝑖 − 1)) = (𝑏‘((𝐾 + 1) − 1)))
305303, 304oveq12d 7287 . . . . . . . . . . . 12 (𝑖 = (𝐾 + 1) → ((𝑏𝑖) − (𝑏‘(𝑖 − 1))) = ((𝑏‘(𝐾 + 1)) − (𝑏‘((𝐾 + 1) − 1))))
306305oveq1d 7284 . . . . . . . . . . 11 (𝑖 = (𝐾 + 1) → (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1) = (((𝑏‘(𝐾 + 1)) − (𝑏‘((𝐾 + 1) − 1))) − 1))
307302, 306ifbieq2d 4491 . . . . . . . . . 10 (𝑖 = (𝐾 + 1) → if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) = if((𝐾 + 1) = 1, ((𝑏‘1) − 1), (((𝑏‘(𝐾 + 1)) − (𝑏‘((𝐾 + 1) − 1))) − 1)))
308301, 307ifbieq2d 4491 . . . . . . . . 9 (𝑖 = (𝐾 + 1) → if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) = if((𝐾 + 1) = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if((𝐾 + 1) = 1, ((𝑏‘1) − 1), (((𝑏‘(𝐾 + 1)) − (𝑏‘((𝐾 + 1) − 1))) − 1))))
309213, 300, 308fsump1 15458 . . . . . . . 8 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (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)))))
310 eqidd 2741 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → (𝐾 + 1) = (𝐾 + 1))
311310iftrued 4473 . . . . . . . . . 10 ((𝜑𝑏𝐵) → if((𝐾 + 1) = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if((𝐾 + 1) = 1, ((𝑏‘1) − 1), (((𝑏‘(𝐾 + 1)) − (𝑏‘((𝐾 + 1) − 1))) − 1))) = ((𝑁 + 𝐾) − (𝑏𝐾)))
312311oveq2d 7285 . . . . . . . . 9 ((𝜑𝑏𝐵) → (Σ𝑖 ∈ (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))) + ((𝑁 + 𝐾) − (𝑏𝐾))))
313 elfznn 13276 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝐾) → 𝑖 ∈ ℕ)
314313adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 𝑖 ∈ ℕ)
315314nnred 11980 . . . . . . . . . . . . . . 15 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 𝑖 ∈ ℝ)
31633adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 𝐾 ∈ ℝ)
317 1red 10969 . . . . . . . . . . . . . . . . 17 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 1 ∈ ℝ)
318316, 317readdcld 10997 . . . . . . . . . . . . . . . 16 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → (𝐾 + 1) ∈ ℝ)
319 elfzle2 13251 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...𝐾) → 𝑖𝐾)
320319adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 𝑖𝐾)
321316ltp1d 11897 . . . . . . . . . . . . . . . 16 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 𝐾 < (𝐾 + 1))
322315, 316, 318, 320, 321lelttrd 11125 . . . . . . . . . . . . . . 15 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 𝑖 < (𝐾 + 1))
323315, 322ltned 11103 . . . . . . . . . . . . . 14 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 𝑖 ≠ (𝐾 + 1))
324323neneqd 2950 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → ¬ 𝑖 = (𝐾 + 1))
325324iffalsed 4476 . . . . . . . . . . . 12 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) = if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)))
326325sumeq2dv 15405 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) = Σ𝑖 ∈ (1...𝐾)if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)))
327326oveq1d 7284 . . . . . . . . . 10 ((𝜑𝑏𝐵) → (Σ𝑖 ∈ (1...𝐾)if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) + ((𝑁 + 𝐾) − (𝑏𝐾))) = (Σ𝑖 ∈ (1...𝐾)if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) + ((𝑁 + 𝐾) − (𝑏𝐾))))
328 eqeq1 2744 . . . . . . . . . . . . . 14 (((𝑏‘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)))
329 eqeq1 2744 . . . . . . . . . . . . . 14 ((((𝑏𝑖) − (𝑏‘(𝑖 − 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 eqidd 2741 . . . . . . . . . . . . . . 15 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ 𝑖 = 1) → ((𝑏‘1) − 1) = ((𝑏‘1) − 1))
331 simpr 485 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ 𝑖 = 1) → 𝑖 = 1)
332331iftrued 4473 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ 𝑖 = 1) → if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = (𝑏‘1))
333332eqcomd 2746 . . . . . . . . . . . . . . . 16 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ 𝑖 = 1) → (𝑏‘1) = if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))))
334333oveq1d 7284 . . . . . . . . . . . . . . 15 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ 𝑖 = 1) → ((𝑏‘1) − 1) = (if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1))
335330, 334eqtrd 2780 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ 𝑖 = 1) → ((𝑏‘1) − 1) = (if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1))
336 eqidd 2741 . . . . . . . . . . . . . . 15 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1) = (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))
337 simpr 485 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → ¬ 𝑖 = 1)
338337iffalsed 4476 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = ((𝑏𝑖) − (𝑏‘(𝑖 − 1))))
339338oveq1d 7284 . . . . . . . . . . . . . . . 16 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) = (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))
340339eqcomd 2746 . . . . . . . . . . . . . . 15 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1) = (if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1))
341336, 340eqtrd 2780 . . . . . . . . . . . . . 14 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1) = (if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1))
342328, 329, 335, 341ifbothda 4503 . . . . . . . . . . . . 13 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) = (if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1))
343342sumeq2dv 15405 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) = Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1))
344343oveq1d 7284 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → (Σ𝑖 ∈ (1...𝐾)if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) + ((𝑁 + 𝐾) − (𝑏𝐾))) = (Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) + ((𝑁 + 𝐾) − (𝑏𝐾))))
345 fzfid 13683 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵) → (1...𝐾) ∈ Fin)
346 eleq1 2828 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏‘1) = if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) → ((𝑏‘1) ∈ ℤ ↔ if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) ∈ ℤ))
347 eleq1 2828 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) = if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) → (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) ∈ ℤ ↔ if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) ∈ ℤ))
34865ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ 𝑖 = 1) → (𝑏‘1) ∈ ℤ)
34929adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
350 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 𝑖 ∈ (1...𝐾))
351349, 350ffvelrnd 6957 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → (𝑏𝑖) ∈ (1...(𝑁 + 𝐾)))
352264nnzd 12416 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏𝑖) ∈ (1...(𝑁 + 𝐾)) → (𝑏𝑖) ∈ ℤ)
353351, 352syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → (𝑏𝑖) ∈ ℤ)
354353adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (𝑏𝑖) ∈ ℤ)
355349adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
356 1zzd 12343 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → 1 ∈ ℤ)
35713ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → 𝐾 ∈ ℤ)
358314nnzd 12416 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 𝑖 ∈ ℤ)
359358adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ℤ)
360359, 356zsubcld 12422 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (𝑖 − 1) ∈ ℤ)
361314nnge1d 12013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 1 ≤ 𝑖)
362361adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → 1 ≤ 𝑖)
363337, 272syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → 𝑖 ≠ 1)
364362, 363jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (1 ≤ 𝑖𝑖 ≠ 1))
365317adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → 1 ∈ ℝ)
366315adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ℝ)
367365, 366ltlend 11112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (1 < 𝑖 ↔ (1 ≤ 𝑖𝑖 ≠ 1)))
368364, 367mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → 1 < 𝑖)
369 zltlem1 12365 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (1 < 𝑖 ↔ 1 ≤ (𝑖 − 1)))
370356, 359, 369syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (1 < 𝑖 ↔ 1 ≤ (𝑖 − 1)))
371368, 370mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → 1 ≤ (𝑖 − 1))
372315, 317resubcld 11395 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → (𝑖 − 1) ∈ ℝ)
373315lem1d 11900 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → (𝑖 − 1) ≤ 𝑖)
374372, 315, 316, 373, 320letrd 11124 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → (𝑖 − 1) ≤ 𝐾)
375374adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (𝑖 − 1) ≤ 𝐾)
376356, 357, 360, 371, 375elfzd 13238 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (𝑖 − 1) ∈ (1...𝐾))
377355, 376ffvelrnd 6957 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (𝑏‘(𝑖 − 1)) ∈ (1...(𝑁 + 𝐾)))
378377, 292syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (𝑏‘(𝑖 − 1)) ∈ ℕ)
379378nnzd 12416 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → (𝑏‘(𝑖 − 1)) ∈ ℤ)
380354, 379zsubcld 12422 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) ∧ ¬ 𝑖 = 1) → ((𝑏𝑖) − (𝑏‘(𝑖 − 1))) ∈ ℤ)
381346, 347, 348, 380ifbothda 4503 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) ∈ ℤ)
382381zcnd 12418 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) ∈ ℂ)
38367adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 1 ∈ ℂ)
384345, 382, 383fsumsub 15490 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) = (Σ𝑖 ∈ (1...𝐾)if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − Σ𝑖 ∈ (1...𝐾)1))
385 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 1 → 𝑖 = 1)
386385iftrued 4473 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 1 → if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = (𝑏‘1))
387213, 382, 386fsum1p 15455 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...𝐾)if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1))))))
38859adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...𝐾)) → 1 ∈ ℝ)
389 elfzle1 13250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ ((1 + 1)...𝐾) → (1 + 1) ≤ 𝑖)
390389adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...𝐾)) → (1 + 1) ≤ 𝑖)
39130adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...𝐾)) → 1 ∈ ℤ)
392 elfzelz 13247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ ((1 + 1)...𝐾) → 𝑖 ∈ ℤ)
393392adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...𝐾)) → 𝑖 ∈ ℤ)
394391, 393, 279syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...𝐾)) → (1 < 𝑖 ↔ (1 + 1) ≤ 𝑖))
395390, 394mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...𝐾)) → 1 < 𝑖)
396388, 395ltned 11103 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...𝐾)) → 1 ≠ 𝑖)
397396necomd 3001 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...𝐾)) → 𝑖 ≠ 1)
398397neneqd 2950 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...𝐾)) → ¬ 𝑖 = 1)
399398iffalsed 4476 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...𝐾)) → if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = ((𝑏𝑖) − (𝑏‘(𝑖 − 1))))
400399sumeq2dv 15405 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵) → Σ𝑖 ∈ ((1 + 1)...𝐾)if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = Σ𝑖 ∈ ((1 + 1)...𝐾)((𝑏𝑖) − (𝑏‘(𝑖 − 1))))
401400oveq2d 7285 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...𝐾)if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1))))) = ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...𝐾)((𝑏𝑖) − (𝑏‘(𝑖 − 1)))))
40233recnd 10996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑏𝐵) → 𝐾 ∈ ℂ)
403402, 67npcand 11328 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑏𝐵) → ((𝐾 − 1) + 1) = 𝐾)
404403eqcomd 2746 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑏𝐵) → 𝐾 = ((𝐾 − 1) + 1))
405404oveq2d 7285 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑏𝐵) → ((1 + 1)...𝐾) = ((1 + 1)...((𝐾 − 1) + 1)))
406405sumeq1d 15403 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑏𝐵) → Σ𝑖 ∈ ((1 + 1)...𝐾)((𝑏𝑖) − (𝑏‘(𝑖 − 1))) = Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏𝑖) − (𝑏‘(𝑖 − 1))))
407406oveq2d 7285 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...𝐾)((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏𝑖) − (𝑏‘(𝑖 − 1)))))
408 elfzelz 13247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1)) → 𝑖 ∈ ℤ)
409408adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))) → 𝑖 ∈ ℤ)
410409zcnd 12418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))) → 𝑖 ∈ ℂ)
411 1cnd 10963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))) → 1 ∈ ℂ)
412410, 411npcand 11328 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))) → ((𝑖 − 1) + 1) = 𝑖)
413412eqcomd 2746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))) → 𝑖 = ((𝑖 − 1) + 1))
414413fveq2d 6773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))) → (𝑏𝑖) = (𝑏‘((𝑖 − 1) + 1)))
415 eqidd 2741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))) → (𝑏‘(𝑖 − 1)) = (𝑏‘(𝑖 − 1)))
416414, 415oveq12d 7287 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))) → ((𝑏𝑖) − (𝑏‘(𝑖 − 1))) = ((𝑏‘((𝑖 − 1) + 1)) − (𝑏‘(𝑖 − 1))))
417416sumeq2dv 15405 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑏𝐵) → Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏𝑖) − (𝑏‘(𝑖 − 1))) = Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏‘((𝑖 − 1) + 1)) − (𝑏‘(𝑖 − 1))))
418417oveq2d 7285 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏‘((𝑖 − 1) + 1)) − (𝑏‘(𝑖 − 1)))))
41913, 30zsubcld 12422 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑏𝐵) → (𝐾 − 1) ∈ ℤ)
42029adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
421 1zzd 12343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 1 ∈ ℤ)
42213adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℤ)
423 elfznn 13276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑠 ∈ (1...(𝐾 − 1)) → 𝑠 ∈ ℕ)
424423adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 𝑠 ∈ ℕ)
425424nnzd 12416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 𝑠 ∈ ℤ)
426425peano2zd 12420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝑠 + 1) ∈ ℤ)
427 1red 10969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 1 ∈ ℝ)
428424nnred 11980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 𝑠 ∈ ℝ)
429428, 427readdcld 10997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝑠 + 1) ∈ ℝ)
430424nnge1d 12013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 1 ≤ 𝑠)
431428lep1d 11898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 𝑠 ≤ (𝑠 + 1))
432427, 428, 429, 430, 431letrd 11124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 1 ≤ (𝑠 + 1))
433 elfzle2 13251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∈ (1...(𝐾 − 1)) → 𝑠 ≤ (𝐾 − 1))
434433adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 𝑠 ≤ (𝐾 − 1))
43533adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 𝐾 ∈ ℝ)
436 leaddsub 11443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑠 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑠 + 1) ≤ 𝐾𝑠 ≤ (𝐾 − 1)))
437428, 427, 435, 436syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → ((𝑠 + 1) ≤ 𝐾𝑠 ≤ (𝐾 − 1)))
438434, 437mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝑠 + 1) ≤ 𝐾)
439421, 422, 426, 432, 438elfzd 13238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝑠 + 1) ∈ (1...𝐾))
440420, 439ffvelrnd 6957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝑏‘(𝑠 + 1)) ∈ (1...(𝑁 + 𝐾)))
441 elfznn 13276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏‘(𝑠 + 1)) ∈ (1...(𝑁 + 𝐾)) → (𝑏‘(𝑠 + 1)) ∈ ℕ)
442440, 441syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝑏‘(𝑠 + 1)) ∈ ℕ)
443442nnzd 12416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝑏‘(𝑠 + 1)) ∈ ℤ)
444435, 427resubcld 11395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ∈ ℝ)
445435lem1d 11900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝐾 − 1) ≤ 𝐾)
446428, 444, 435, 434, 445letrd 11124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 𝑠𝐾)
447421, 422, 425, 430, 446elfzd 13238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → 𝑠 ∈ (1...𝐾))
448420, 447ffvelrnd 6957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝑏𝑠) ∈ (1...(𝑁 + 𝐾)))
449 elfznn 13276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑏𝑠) ∈ (1...(𝑁 + 𝐾)) → (𝑏𝑠) ∈ ℕ)
450449nnzd 12416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏𝑠) ∈ (1...(𝑁 + 𝐾)) → (𝑏𝑠) ∈ ℤ)
451448, 450syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → (𝑏𝑠) ∈ ℤ)
452443, 451zsubcld 12422 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → ((𝑏‘(𝑠 + 1)) − (𝑏𝑠)) ∈ ℤ)
453452zcnd 12418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑏𝐵) ∧ 𝑠 ∈ (1...(𝐾 − 1))) → ((𝑏‘(𝑠 + 1)) − (𝑏𝑠)) ∈ ℂ)
454 fvoveq1 7292 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 = (𝑖 − 1) → (𝑏‘(𝑠 + 1)) = (𝑏‘((𝑖 − 1) + 1)))
455 fveq2 6769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 = (𝑖 − 1) → (𝑏𝑠) = (𝑏‘(𝑖 − 1)))
456454, 455oveq12d 7287 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = (𝑖 − 1) → ((𝑏‘(𝑠 + 1)) − (𝑏𝑠)) = ((𝑏‘((𝑖 − 1) + 1)) − (𝑏‘(𝑖 − 1))))
45730, 30, 419, 453, 456fsumshft 15482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑏𝐵) → Σ𝑠 ∈ (1...(𝐾 − 1))((𝑏‘(𝑠 + 1)) − (𝑏𝑠)) = Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏‘((𝑖 − 1) + 1)) − (𝑏‘(𝑖 − 1))))
458457oveq2d 7285 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑠 ∈ (1...(𝐾 − 1))((𝑏‘(𝑠 + 1)) − (𝑏𝑠))) = ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏‘((𝑖 − 1) + 1)) − (𝑏‘(𝑖 − 1)))))
459458eqcomd 2746 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏‘((𝑖 − 1) + 1)) − (𝑏‘(𝑖 − 1)))) = ((𝑏‘1) + Σ𝑠 ∈ (1...(𝐾 − 1))((𝑏‘(𝑠 + 1)) − (𝑏𝑠))))
460 fvoveq1 7292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = 𝑖 → (𝑏‘(𝑠 + 1)) = (𝑏‘(𝑖 + 1)))
461 fveq2 6769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = 𝑖 → (𝑏𝑠) = (𝑏𝑖))
462460, 461oveq12d 7287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 = 𝑖 → ((𝑏‘(𝑠 + 1)) − (𝑏𝑠)) = ((𝑏‘(𝑖 + 1)) − (𝑏𝑖)))
463 nfcv 2909 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑖(1...(𝐾 − 1))
464 nfcv 2909 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑠(1...(𝐾 − 1))
465 nfcv 2909 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑖((𝑏‘(𝑠 + 1)) − (𝑏𝑠))
466 nfcv 2909 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑠((𝑏‘(𝑖 + 1)) − (𝑏𝑖))
467462, 463, 464, 465, 466cbvsum 15397 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Σ𝑠 ∈ (1...(𝐾 − 1))((𝑏‘(𝑠 + 1)) − (𝑏𝑠)) = Σ𝑖 ∈ (1...(𝐾 − 1))((𝑏‘(𝑖 + 1)) − (𝑏𝑖))
468467a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑏𝐵) → Σ𝑠 ∈ (1...(𝐾 − 1))((𝑏‘(𝑠 + 1)) − (𝑏𝑠)) = Σ𝑖 ∈ (1...(𝐾 − 1))((𝑏‘(𝑖 + 1)) − (𝑏𝑖)))
469468oveq2d 7285 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑠 ∈ (1...(𝐾 − 1))((𝑏‘(𝑠 + 1)) − (𝑏𝑠))) = ((𝑏‘1) + Σ𝑖 ∈ (1...(𝐾 − 1))((𝑏‘(𝑖 + 1)) − (𝑏𝑖))))
470 fveq2 6769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑖 → (𝑏𝑤) = (𝑏𝑖))
471 fveq2 6769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = (𝑖 + 1) → (𝑏𝑤) = (𝑏‘(𝑖 + 1)))
472 fveq2 6769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 1 → (𝑏𝑤) = (𝑏‘1))
473 fveq2 6769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = ((𝐾 − 1) + 1) → (𝑏𝑤) = (𝑏‘((𝐾 − 1) + 1)))
474403, 213eqeltrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑏𝐵) → ((𝐾 − 1) + 1) ∈ (ℤ‘1))
47529adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → 𝑏:(1...𝐾)⟶(1...(𝑁 + 𝐾)))
476 1zzd 12343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → 1 ∈ ℤ)
47713adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → 𝐾 ∈ ℤ)
478 elfzelz 13247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 ∈ (1...((𝐾 − 1) + 1)) → 𝑤 ∈ ℤ)
479478adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → 𝑤 ∈ ℤ)
480 elfzle1 13250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 ∈ (1...((𝐾 − 1) + 1)) → 1 ≤ 𝑤)
481480adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → 1 ≤ 𝑤)
482 elfzle2 13251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤 ∈ (1...((𝐾 − 1) + 1)) → 𝑤 ≤ ((𝐾 − 1) + 1))
483482adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → 𝑤 ≤ ((𝐾 − 1) + 1))
484403adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → ((𝐾 − 1) + 1) = 𝐾)
485483, 484breqtrd 5105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → 𝑤𝐾)
486476, 477, 479, 481, 485elfzd 13238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → 𝑤 ∈ (1...𝐾))
487475, 486ffvelrnd 6957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → (𝑏𝑤) ∈ (1...(𝑁 + 𝐾)))
488 elfznn 13276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑏𝑤) ∈ (1...(𝑁 + 𝐾)) → (𝑏𝑤) ∈ ℕ)
489488nncnd 11981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏𝑤) ∈ (1...(𝑁 + 𝐾)) → (𝑏𝑤) ∈ ℂ)
490487, 489syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑏𝐵) ∧ 𝑤 ∈ (1...((𝐾 − 1) + 1))) → (𝑏𝑤) ∈ ℂ)
491470, 471, 472, 473, 419, 474, 490telfsum2 15507 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...(𝐾 − 1))((𝑏‘(𝑖 + 1)) − (𝑏𝑖)) = ((𝑏‘((𝐾 − 1) + 1)) − (𝑏‘1)))
492491oveq2d 7285 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑖 ∈ (1...(𝐾 − 1))((𝑏‘(𝑖 + 1)) − (𝑏𝑖))) = ((𝑏‘1) + ((𝑏‘((𝐾 − 1) + 1)) − (𝑏‘1))))
49372recnd 10996 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑏𝐵) → (𝑏‘1) ∈ ℂ)
49438nncnd 11981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑏𝐵) → (𝑏𝐾) ∈ ℂ)
495403fveq2d 6773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑏𝐵) → (𝑏‘((𝐾 − 1) + 1)) = (𝑏𝐾))
496495eleq1d 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑏𝐵) → ((𝑏‘((𝐾 − 1) + 1)) ∈ ℂ ↔ (𝑏𝐾) ∈ ℂ))
497494, 496mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑏𝐵) → (𝑏‘((𝐾 − 1) + 1)) ∈ ℂ)
498493, 497pncan3d 11327 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑏𝐵) → ((𝑏‘1) + ((𝑏‘((𝐾 − 1) + 1)) − (𝑏‘1))) = (𝑏‘((𝐾 − 1) + 1)))
499498, 495eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑏𝐵) → ((𝑏‘1) + ((𝑏‘((𝐾 − 1) + 1)) − (𝑏‘1))) = (𝑏𝐾))
500492, 499eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑖 ∈ (1...(𝐾 − 1))((𝑏‘(𝑖 + 1)) − (𝑏𝑖))) = (𝑏𝐾))
501469, 500eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑠 ∈ (1...(𝐾 − 1))((𝑏‘(𝑠 + 1)) − (𝑏𝑠))) = (𝑏𝐾))
502459, 501eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏‘((𝑖 − 1) + 1)) − (𝑏‘(𝑖 − 1)))) = (𝑏𝐾))
503418, 502eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...((𝐾 − 1) + 1))((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = (𝑏𝐾))
504407, 503eqtrd 2780 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...𝐾)((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = (𝑏𝐾))
505401, 504eqtrd 2780 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑏𝐵) → ((𝑏‘1) + Σ𝑖 ∈ ((1 + 1)...𝐾)if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1))))) = (𝑏𝐾))
506387, 505eqtrd 2780 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) = (𝑏𝐾))
507 fsumconst 15492 . . . . . . . . . . . . . . . . . . . . 21 (((1...𝐾) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑖 ∈ (1...𝐾)1 = ((♯‘(1...𝐾)) · 1))
508345, 67, 507syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)1 = ((♯‘(1...𝐾)) · 1))
509211nnnn0d 12285 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑏𝐵) → 𝐾 ∈ ℕ0)
510 hashfz1 14050 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐾 ∈ ℕ0 → (♯‘(1...𝐾)) = 𝐾)
511509, 510syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑏𝐵) → (♯‘(1...𝐾)) = 𝐾)
512511oveq1d 7284 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑏𝐵) → ((♯‘(1...𝐾)) · 1) = (𝐾 · 1))
513402mulid1d 10985 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑏𝐵) → (𝐾 · 1) = 𝐾)
514512, 513eqtrd 2780 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑏𝐵) → ((♯‘(1...𝐾)) · 1) = 𝐾)
515508, 514eqtrd 2780 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)1 = 𝐾)
516506, 515oveq12d 7287 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → (Σ𝑖 ∈ (1...𝐾)if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − Σ𝑖 ∈ (1...𝐾)1) = ((𝑏𝐾) − 𝐾))
517384, 516eqtrd 2780 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) = ((𝑏𝐾) − 𝐾))
51842addid2d 11168 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑏𝐵) → (0 + (𝑏𝐾)) = (𝑏𝐾))
519518eqcomd 2746 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → (𝑏𝐾) = (0 + (𝑏𝐾)))
520519oveq1d 7284 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → ((𝑏𝐾) − 𝐾) = ((0 + (𝑏𝐾)) − 𝐾))
521517, 520eqtrd 2780 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) = ((0 + (𝑏𝐾)) − 𝐾))
522 0cnd 10961 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → 0 ∈ ℂ)
523522, 402, 42subsub3d 11354 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → (0 − (𝐾 − (𝑏𝐾))) = ((0 + (𝑏𝐾)) − 𝐾))
524523eqcomd 2746 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → ((0 + (𝑏𝐾)) − 𝐾) = (0 − (𝐾 − (𝑏𝐾))))
525521, 524eqtrd 2780 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) = (0 − (𝐾 − (𝑏𝐾))))
52611zcnd 12418 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑏𝐵) → 𝑁 ∈ ℂ)
527526subidd 11312 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏𝐵) → (𝑁𝑁) = 0)
528527eqcomd 2746 . . . . . . . . . . . . . . . 16 ((𝜑𝑏𝐵) → 0 = (𝑁𝑁))
529528oveq1d 7284 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (0 − (𝐾 − (𝑏𝐾))) = ((𝑁𝑁) − (𝐾 − (𝑏𝐾))))
530525, 529eqtrd 2780 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) = ((𝑁𝑁) − (𝐾 − (𝑏𝐾))))
531402, 42subcld 11324 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → (𝐾 − (𝑏𝐾)) ∈ ℂ)
532526, 526, 531subsub4d 11355 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → ((𝑁𝑁) − (𝐾 − (𝑏𝐾))) = (𝑁 − (𝑁 + (𝐾 − (𝑏𝐾)))))
533530, 532eqtrd 2780 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) = (𝑁 − (𝑁 + (𝐾 − (𝑏𝐾)))))
534526, 402, 42addsubassd 11344 . . . . . . . . . . . . . . 15 ((𝜑𝑏𝐵) → ((𝑁 + 𝐾) − (𝑏𝐾)) = (𝑁 + (𝐾 − (𝑏𝐾))))
535534eqcomd 2746 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → (𝑁 + (𝐾 − (𝑏𝐾))) = ((𝑁 + 𝐾) − (𝑏𝐾)))
536535oveq2d 7285 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → (𝑁 − (𝑁 + (𝐾 − (𝑏𝐾)))) = (𝑁 − ((𝑁 + 𝐾) − (𝑏𝐾))))
537533, 536eqtrd 2780 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) = (𝑁 − ((𝑁 + 𝐾) − (𝑏𝐾))))
538 1zzd 12343 . . . . . . . . . . . . . . . 16 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → 1 ∈ ℤ)
539381, 538zsubcld 12422 . . . . . . . . . . . . . . 15 (((𝜑𝑏𝐵) ∧ 𝑖 ∈ (1...𝐾)) → (if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) ∈ ℤ)
540345, 539fsumzcl 15437 . . . . . . . . . . . . . 14 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) ∈ ℤ)
541540zcnd 12418 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) ∈ ℂ)
54253nn0cnd 12287 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → ((𝑁 + 𝐾) − (𝑏𝐾)) ∈ ℂ)
543541, 542, 526addlsub 11383 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ((Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) + ((𝑁 + 𝐾) − (𝑏𝐾))) = 𝑁 ↔ Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) = (𝑁 − ((𝑁 + 𝐾) − (𝑏𝐾)))))
544537, 543mpbird 256 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → (Σ𝑖 ∈ (1...𝐾)(if(𝑖 = 1, (𝑏‘1), ((𝑏𝑖) − (𝑏‘(𝑖 − 1)))) − 1) + ((𝑁 + 𝐾) − (𝑏𝐾))) = 𝑁)
545344, 544eqtrd 2780 . . . . . . . . . 10 ((𝜑𝑏𝐵) → (Σ𝑖 ∈ (1...𝐾)if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1)) + ((𝑁 + 𝐾) − (𝑏𝐾))) = 𝑁)
546327, 545eqtrd 2780 . . . . . . . . 9 ((𝜑𝑏𝐵) → (Σ𝑖 ∈ (1...𝐾)if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) + ((𝑁 + 𝐾) − (𝑏𝐾))) = 𝑁)
547312, 546eqtrd 2780 . . . . . . . 8 ((𝜑𝑏𝐵) → (Σ𝑖 ∈ (1...𝐾)if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) + if((𝐾 + 1) = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if((𝐾 + 1) = 1, ((𝑏‘1) − 1), (((𝑏‘(𝐾 + 1)) − (𝑏‘((𝐾 + 1) − 1))) − 1)))) = 𝑁)
548309, 547eqtrd 2780 . . . . . . 7 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...(𝐾 + 1))if(𝑖 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑖 = 1, ((𝑏‘1) − 1), (((𝑏𝑖) − (𝑏‘(𝑖 − 1))) − 1))) = 𝑁)
549210, 548eqtrd 2780 . . . . . 6 ((𝜑𝑏𝐵) → Σ𝑖 ∈ (1...(𝐾 + 1))((𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))‘𝑖) = 𝑁)
550192, 549jca 512 . . . . 5 ((𝜑𝑏𝐵) → ((𝑘 ∈ (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 7302 . . . . . . 7 (1...(𝐾 + 1)) ∈ V
552551mptex 7094 . . . . . 6 (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) ∈ V
553 feq1 6578 . . . . . . 7 (𝑔 = (𝑘 ∈ (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 483 . . . . . . . . . 10 ((𝑔 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → 𝑔 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))
555554fveq1d 6771 . . . . . . . . 9 ((𝑔 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝑔𝑖) = ((𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))‘𝑖))
556555sumeq2dv 15405 . . . . . . . 8 (𝑔 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))((𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))‘𝑖))
557556eqeq1d 2742 . . . . . . 7 (𝑔 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) → (Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))((𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))‘𝑖) = 𝑁))
558553, 557anbi12d 631 . . . . . 6 (𝑔 = (𝑘 ∈ (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))))‘𝑖) = 𝑁)))
559552, 558elab 3611 . . . . 5 ((𝑘 ∈ (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))))‘𝑖) = 𝑁))
560550, 559sylibr 233 . . . 4 ((𝜑𝑏𝐵) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)})
561 sticksstones10.4 . . . . 5 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)}
562561a1i 11 . . . 4 ((𝜑𝑏𝐵) → 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔𝑖) = 𝑁)})
563560, 562eleqtrrd 2844 . . 3 ((𝜑𝑏𝐵) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) ∈ 𝐴)
5646, 563eqeltrrd 2842 . 2 ((𝜑𝑏𝐵) → if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) ∈ 𝐴)
565 sticksstones10.3 . 2 𝐺 = (𝑏𝐵 ↦ if(𝐾 = 0, {⟨1, 𝑁⟩}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏𝑘) − (𝑏‘(𝑘 − 1))) − 1))))))
566564, 565fmptd 6983 1 (𝜑𝐺:𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1542  wcel 2110  {cab 2717  wne 2945  wral 3066  Vcvv 3431  ifcif 4465  {csn 4567  cop 4573   class class class wbr 5079  cmpt 5162  wf 6427  cfv 6431  (class class class)co 7269  Fincfn 8708  cc 10862  cr 10863  0cc0 10864  1c1 10865   + caddc 10867   · cmul 10869   < clt 11002  cle 11003  cmin 11197  cn 11965  0cn0 12225  cz 12311  cuz 12573  ...cfz 13230  chash 14034  Σcsu 15387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580  ax-inf2 9369  ax-cnex 10920  ax-resscn 10921  ax-1cn 10922  ax-icn 10923  ax-addcl 10924  ax-addrcl 10925  ax-mulcl 10926  ax-mulrcl 10927  ax-mulcom 10928  ax-addass 10929  ax-mulass 10930  ax-distr 10931  ax-i2m1 10932  ax-1ne0 10933  ax-1rid 10934  ax-rnegex 10935  ax-rrecex 10936  ax-cnre 10937  ax-pre-lttri 10938  ax-pre-lttrn 10939  ax-pre-ltadd 10940  ax-pre-mulgt0 10941  ax-pre-sup 10942
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4846  df-int 4886  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6200  df-ord 6267  df-on 6268  df-lim 6269  df-suc 6270  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-isom 6440  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-om 7702  df-1st 7818  df-2nd 7819  df-frecs 8082  df-wrecs 8113  df-recs 8187  df-rdg 8226  df-1o 8282  df-er 8473  df-en 8709  df-dom 8710  df-sdom 8711  df-fin 8712  df-sup 9171  df-oi 9239  df-card 9690  df-pnf 11004  df-mnf 11005  df-xr 11006  df-ltxr 11007  df-le 11008  df-sub 11199  df-neg 11200  df-div 11625  df-nn 11966  df-2 12028  df-3 12029  df-n0 12226  df-z 12312  df-uz 12574  df-rp 12722  df-fz 13231  df-fzo 13374  df-seq 13712  df-exp 13773  df-hash 14035  df-cj 14800  df-re 14801  df-im 14802  df-sqrt 14936  df-abs 14937  df-clim 15187  df-sum 15388
This theorem is referenced by:  sticksstones12  40103
  Copyright terms: Public domain W3C validator