Proof of Theorem sticksstones7
| Step | Hyp | Ref
| Expression |
| 1 | | sticksstones7.5 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖))) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖)))) |
| 3 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) |
| 4 | 3 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (1...𝑥) = (1...𝑋)) |
| 5 | 4 | sumeq1d 15736 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖) = Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) |
| 6 | 3, 5 | oveq12d 7449 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖)) = (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖))) |
| 7 | | sticksstones7.4 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (1...𝐾)) |
| 8 | | elfznn 13593 |
. . . . . 6
⊢ (𝑋 ∈ (1...𝐾) → 𝑋 ∈ ℕ) |
| 9 | 7, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℕ) |
| 10 | 9 | nnnn0d 12587 |
. . . 4
⊢ (𝜑 → 𝑋 ∈
ℕ0) |
| 11 | | fzfid 14014 |
. . . . 5
⊢ (𝜑 → (1...𝑋) ∈ Fin) |
| 12 | | 1zzd 12648 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 1 ∈ ℤ) |
| 13 | | sticksstones7.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 14 | 13 | nn0zd 12639 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝐾 ∈ ℤ) |
| 16 | 15 | peano2zd 12725 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → (𝐾 + 1) ∈ ℤ) |
| 17 | | elfzelz 13564 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑋) → 𝑖 ∈ ℤ) |
| 18 | 17 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑖 ∈ ℤ) |
| 19 | | elfzle1 13567 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑋) → 1 ≤ 𝑖) |
| 20 | 19 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 1 ≤ 𝑖) |
| 21 | 18 | zred 12722 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑖 ∈ ℝ) |
| 22 | 9 | nnred 12281 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑋 ∈ ℝ) |
| 24 | 16 | zred 12722 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → (𝐾 + 1) ∈ ℝ) |
| 25 | | elfzle2 13568 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑋) → 𝑖 ≤ 𝑋) |
| 26 | 25 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑖 ≤ 𝑋) |
| 27 | 13 | nn0red 12588 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℝ) |
| 28 | | 1red 11262 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℝ) |
| 29 | 27, 28 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 + 1) ∈ ℝ) |
| 30 | | elfzle2 13568 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (1...𝐾) → 𝑋 ≤ 𝐾) |
| 31 | 7, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ≤ 𝐾) |
| 32 | 27 | lep1d 12199 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ≤ (𝐾 + 1)) |
| 33 | 22, 27, 29, 31, 32 | letrd 11418 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≤ (𝐾 + 1)) |
| 34 | 33 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑋 ≤ (𝐾 + 1)) |
| 35 | 21, 23, 24, 26, 34 | letrd 11418 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑖 ≤ (𝐾 + 1)) |
| 36 | 12, 16, 18, 20, 35 | elfzd 13555 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑖 ∈ (1...(𝐾 + 1))) |
| 37 | | sticksstones7.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:(1...(𝐾 +
1))⟶ℕ0) |
| 38 | 37 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝐺:(1...(𝐾 +
1))⟶ℕ0) |
| 39 | 38 | ffvelcdmda 7104 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑋)) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝐺‘𝑖) ∈
ℕ0) |
| 40 | 36, 39 | mpdan 687 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → (𝐺‘𝑖) ∈
ℕ0) |
| 41 | 11, 40 | fsumnn0cl 15772 |
. . . 4
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ∈
ℕ0) |
| 42 | 10, 41 | nn0addcld 12591 |
. . 3
⊢ (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) ∈
ℕ0) |
| 43 | 2, 6, 7, 42 | fvmptd 7023 |
. 2
⊢ (𝜑 → (𝐹‘𝑋) = (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖))) |
| 44 | | 1zzd 12648 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
| 45 | | sticksstones7.1 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 46 | 45 | nn0zd 12639 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 47 | 46, 14 | zaddcld 12726 |
. . 3
⊢ (𝜑 → (𝑁 + 𝐾) ∈ ℤ) |
| 48 | 42 | nn0zd 12639 |
. . 3
⊢ (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) ∈ ℤ) |
| 49 | | eqid 2737 |
. . . . . 6
⊢ 1 =
1 |
| 50 | | 1p0e1 12390 |
. . . . . 6
⊢ (1 + 0) =
1 |
| 51 | 49, 50 | eqtr4i 2768 |
. . . . 5
⊢ 1 = (1 +
0) |
| 52 | 51 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 = (1 +
0)) |
| 53 | | 0red 11264 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℝ) |
| 54 | 41 | nn0red 12588 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ∈ ℝ) |
| 55 | 9 | nnge1d 12314 |
. . . . 5
⊢ (𝜑 → 1 ≤ 𝑋) |
| 56 | 41 | nn0ge0d 12590 |
. . . . 5
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) |
| 57 | 28, 53, 22, 54, 55, 56 | le2addd 11882 |
. . . 4
⊢ (𝜑 → (1 + 0) ≤ (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖))) |
| 58 | 52, 57 | eqbrtrd 5165 |
. . 3
⊢ (𝜑 → 1 ≤ (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖))) |
| 59 | 45 | nn0red 12588 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 60 | | fzfid 14014 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 + 1)...(𝐾 + 1)) ∈ Fin) |
| 61 | 44 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ∈
ℤ) |
| 62 | 14 | peano2zd 12725 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 + 1) ∈ ℤ) |
| 63 | 62 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝐾 + 1) ∈ ℤ) |
| 64 | | elfzelz 13564 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1)) → 𝑖 ∈ ℤ) |
| 65 | 64 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ∈ ℤ) |
| 66 | 28 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ∈
ℝ) |
| 67 | 22 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑋 ∈ ℝ) |
| 68 | 67, 66 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝑋 + 1) ∈ ℝ) |
| 69 | 65 | zred 12722 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ∈ ℝ) |
| 70 | 55 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ≤ 𝑋) |
| 71 | 67 | lep1d 12199 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑋 ≤ (𝑋 + 1)) |
| 72 | 66, 67, 68, 70, 71 | letrd 11418 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ≤ (𝑋 + 1)) |
| 73 | | elfzle1 13567 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1)) → (𝑋 + 1) ≤ 𝑖) |
| 74 | 73 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝑋 + 1) ≤ 𝑖) |
| 75 | 66, 68, 69, 72, 74 | letrd 11418 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ≤ 𝑖) |
| 76 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1)) → 𝑖 ≤ (𝐾 + 1)) |
| 77 | 76 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ≤ (𝐾 + 1)) |
| 78 | 61, 63, 65, 75, 77 | elfzd 13555 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ∈ (1...(𝐾 + 1))) |
| 79 | 37 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝐺‘𝑖) ∈
ℕ0) |
| 80 | 79 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝐺‘𝑖) ∈
ℕ0) |
| 81 | 78, 80 | mpdan 687 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝐺‘𝑖) ∈
ℕ0) |
| 82 | 60, 81 | fsumnn0cl 15772 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖) ∈
ℕ0) |
| 83 | 82 | nn0ge0d 12590 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖)) |
| 84 | 82 | nn0red 12588 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖) ∈ ℝ) |
| 85 | 54, 84 | addge01d 11851 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖) ↔ Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ≤ (Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) + Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖)))) |
| 86 | 83, 85 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ≤ (Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) + Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖))) |
| 87 | 22 | ltp1d 12198 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 < (𝑋 + 1)) |
| 88 | | fzdisj 13591 |
. . . . . . . . 9
⊢ (𝑋 < (𝑋 + 1) → ((1...𝑋) ∩ ((𝑋 + 1)...(𝐾 + 1))) = ∅) |
| 89 | 87, 88 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((1...𝑋) ∩ ((𝑋 + 1)...(𝐾 + 1))) = ∅) |
| 90 | 10 | nn0zd 12639 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℤ) |
| 91 | 44, 62, 90, 55, 33 | elfzd 13555 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (1...(𝐾 + 1))) |
| 92 | | fzsplit 13590 |
. . . . . . . . 9
⊢ (𝑋 ∈ (1...(𝐾 + 1)) → (1...(𝐾 + 1)) = ((1...𝑋) ∪ ((𝑋 + 1)...(𝐾 + 1)))) |
| 93 | 91, 92 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1...(𝐾 + 1)) = ((1...𝑋) ∪ ((𝑋 + 1)...(𝐾 + 1)))) |
| 94 | | fzfid 14014 |
. . . . . . . 8
⊢ (𝜑 → (1...(𝐾 + 1)) ∈ Fin) |
| 95 | | nn0cn 12536 |
. . . . . . . . 9
⊢ ((𝐺‘𝑖) ∈ ℕ0 → (𝐺‘𝑖) ∈ ℂ) |
| 96 | 79, 95 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝐺‘𝑖) ∈ ℂ) |
| 97 | 89, 93, 94, 96 | fsumsplit 15777 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖) = (Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) + Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖))) |
| 98 | 86, 97 | breqtrrd 5171 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ≤ Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖)) |
| 99 | | sticksstones7.6 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖) = 𝑁) |
| 100 | 99 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → 𝑁 = Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖)) |
| 101 | 98, 100 | breqtrrd 5171 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ≤ 𝑁) |
| 102 | 22, 54, 27, 59, 31, 101 | le2addd 11882 |
. . . 4
⊢ (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) ≤ (𝐾 + 𝑁)) |
| 103 | 13 | nn0cnd 12589 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 104 | 45 | nn0cnd 12589 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 105 | 103, 104 | addcomd 11463 |
. . . 4
⊢ (𝜑 → (𝐾 + 𝑁) = (𝑁 + 𝐾)) |
| 106 | 102, 105 | breqtrd 5169 |
. . 3
⊢ (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) ≤ (𝑁 + 𝐾)) |
| 107 | 44, 47, 48, 58, 106 | elfzd 13555 |
. 2
⊢ (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) ∈ (1...(𝑁 + 𝐾))) |
| 108 | 43, 107 | eqeltrd 2841 |
1
⊢ (𝜑 → (𝐹‘𝑋) ∈ (1...(𝑁 + 𝐾))) |