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