Proof of Theorem sticksstones7
Step | Hyp | Ref
| Expression |
1 | | sticksstones7.5 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖))) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖)))) |
3 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) |
4 | 3 | oveq2d 7247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (1...𝑥) = (1...𝑋)) |
5 | 4 | sumeq1d 15289 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖) = Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) |
6 | 3, 5 | oveq12d 7249 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺‘𝑖)) = (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖))) |
7 | | sticksstones7.4 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (1...𝐾)) |
8 | | elfznn 13165 |
. . . . . 6
⊢ (𝑋 ∈ (1...𝐾) → 𝑋 ∈ ℕ) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℕ) |
10 | 9 | nnnn0d 12174 |
. . . 4
⊢ (𝜑 → 𝑋 ∈
ℕ0) |
11 | | fzfid 13570 |
. . . . 5
⊢ (𝜑 → (1...𝑋) ∈ Fin) |
12 | | 1zzd 12232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 1 ∈ ℤ) |
13 | | sticksstones7.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
14 | 13 | nn0zd 12304 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℤ) |
15 | 14 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝐾 ∈ ℤ) |
16 | 15 | peano2zd 12309 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → (𝐾 + 1) ∈ ℤ) |
17 | | elfzelz 13136 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑋) → 𝑖 ∈ ℤ) |
18 | 17 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑖 ∈ ℤ) |
19 | | elfzle1 13139 |
. . . . . . . 8
⊢ (𝑖 ∈ (1...𝑋) → 1 ≤ 𝑖) |
20 | 19 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 1 ≤ 𝑖) |
21 | 18 | zred 12306 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑖 ∈ ℝ) |
22 | 9 | nnred 11869 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) |
23 | 22 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑋 ∈ ℝ) |
24 | 16 | zred 12306 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → (𝐾 + 1) ∈ ℝ) |
25 | | elfzle2 13140 |
. . . . . . . . 9
⊢ (𝑖 ∈ (1...𝑋) → 𝑖 ≤ 𝑋) |
26 | 25 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑖 ≤ 𝑋) |
27 | 13 | nn0red 12175 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℝ) |
28 | | 1red 10858 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℝ) |
29 | 27, 28 | readdcld 10886 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 + 1) ∈ ℝ) |
30 | | elfzle2 13140 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (1...𝐾) → 𝑋 ≤ 𝐾) |
31 | 7, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ≤ 𝐾) |
32 | 27 | lep1d 11787 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ≤ (𝐾 + 1)) |
33 | 22, 27, 29, 31, 32 | letrd 11013 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≤ (𝐾 + 1)) |
34 | 33 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑋 ≤ (𝐾 + 1)) |
35 | 21, 23, 24, 26, 34 | letrd 11013 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑖 ≤ (𝐾 + 1)) |
36 | 12, 16, 18, 20, 35 | elfzd 13127 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝑖 ∈ (1...(𝐾 + 1))) |
37 | | sticksstones7.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:(1...(𝐾 +
1))⟶ℕ0) |
38 | 37 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → 𝐺:(1...(𝐾 +
1))⟶ℕ0) |
39 | 38 | ffvelrnda 6922 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑋)) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝐺‘𝑖) ∈
ℕ0) |
40 | 36, 39 | mpdan 687 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑋)) → (𝐺‘𝑖) ∈
ℕ0) |
41 | 11, 40 | fsumnn0cl 15324 |
. . . 4
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ∈
ℕ0) |
42 | 10, 41 | nn0addcld 12178 |
. . 3
⊢ (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) ∈
ℕ0) |
43 | 2, 6, 7, 42 | fvmptd 6843 |
. 2
⊢ (𝜑 → (𝐹‘𝑋) = (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖))) |
44 | | 1zzd 12232 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
45 | | sticksstones7.1 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
46 | 45 | nn0zd 12304 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
47 | 46, 14 | zaddcld 12310 |
. . 3
⊢ (𝜑 → (𝑁 + 𝐾) ∈ ℤ) |
48 | 42 | nn0zd 12304 |
. . 3
⊢ (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) ∈ ℤ) |
49 | | eqid 2738 |
. . . . . 6
⊢ 1 =
1 |
50 | | 1p0e1 11978 |
. . . . . 6
⊢ (1 + 0) =
1 |
51 | 49, 50 | eqtr4i 2769 |
. . . . 5
⊢ 1 = (1 +
0) |
52 | 51 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 = (1 +
0)) |
53 | | 0red 10860 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℝ) |
54 | 41 | nn0red 12175 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ∈ ℝ) |
55 | 9 | nnge1d 11902 |
. . . . 5
⊢ (𝜑 → 1 ≤ 𝑋) |
56 | 41 | nn0ge0d 12177 |
. . . . 5
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) |
57 | 28, 53, 22, 54, 55, 56 | le2addd 11475 |
. . . 4
⊢ (𝜑 → (1 + 0) ≤ (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖))) |
58 | 52, 57 | eqbrtrd 5089 |
. . 3
⊢ (𝜑 → 1 ≤ (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖))) |
59 | 45 | nn0red 12175 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
60 | | fzfid 13570 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 + 1)...(𝐾 + 1)) ∈ Fin) |
61 | 44 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ∈
ℤ) |
62 | 14 | peano2zd 12309 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 + 1) ∈ ℤ) |
63 | 62 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝐾 + 1) ∈ ℤ) |
64 | | elfzelz 13136 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1)) → 𝑖 ∈ ℤ) |
65 | 64 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ∈ ℤ) |
66 | 28 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ∈
ℝ) |
67 | 22 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑋 ∈ ℝ) |
68 | 67, 66 | readdcld 10886 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝑋 + 1) ∈ ℝ) |
69 | 65 | zred 12306 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ∈ ℝ) |
70 | 55 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ≤ 𝑋) |
71 | 67 | lep1d 11787 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑋 ≤ (𝑋 + 1)) |
72 | 66, 67, 68, 70, 71 | letrd 11013 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ≤ (𝑋 + 1)) |
73 | | elfzle1 13139 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1)) → (𝑋 + 1) ≤ 𝑖) |
74 | 73 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝑋 + 1) ≤ 𝑖) |
75 | 66, 68, 69, 72, 74 | letrd 11013 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ≤ 𝑖) |
76 | | elfzle2 13140 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1)) → 𝑖 ≤ (𝐾 + 1)) |
77 | 76 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ≤ (𝐾 + 1)) |
78 | 61, 63, 65, 75, 77 | elfzd 13127 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ∈ (1...(𝐾 + 1))) |
79 | 37 | ffvelrnda 6922 |
. . . . . . . . . . . 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 15324 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖) ∈
ℕ0) |
83 | 82 | nn0ge0d 12177 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖)) |
84 | 82 | nn0red 12175 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖) ∈ ℝ) |
85 | 54, 84 | addge01d 11444 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖) ↔ Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ≤ (Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) + Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖)))) |
86 | 83, 85 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ≤ (Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) + Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖))) |
87 | 22 | ltp1d 11786 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 < (𝑋 + 1)) |
88 | | fzdisj 13163 |
. . . . . . . . 9
⊢ (𝑋 < (𝑋 + 1) → ((1...𝑋) ∩ ((𝑋 + 1)...(𝐾 + 1))) = ∅) |
89 | 87, 88 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((1...𝑋) ∩ ((𝑋 + 1)...(𝐾 + 1))) = ∅) |
90 | 10 | nn0zd 12304 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℤ) |
91 | 44, 62, 90, 55, 33 | elfzd 13127 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (1...(𝐾 + 1))) |
92 | | fzsplit 13162 |
. . . . . . . . 9
⊢ (𝑋 ∈ (1...(𝐾 + 1)) → (1...(𝐾 + 1)) = ((1...𝑋) ∪ ((𝑋 + 1)...(𝐾 + 1)))) |
93 | 91, 92 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1...(𝐾 + 1)) = ((1...𝑋) ∪ ((𝑋 + 1)...(𝐾 + 1)))) |
94 | | fzfid 13570 |
. . . . . . . 8
⊢ (𝜑 → (1...(𝐾 + 1)) ∈ Fin) |
95 | | nn0cn 12124 |
. . . . . . . . 9
⊢ ((𝐺‘𝑖) ∈ ℕ0 → (𝐺‘𝑖) ∈ ℂ) |
96 | 79, 95 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝐺‘𝑖) ∈ ℂ) |
97 | 89, 93, 94, 96 | fsumsplit 15329 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖) = (Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) + Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺‘𝑖))) |
98 | 86, 97 | breqtrrd 5095 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ≤ Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖)) |
99 | | sticksstones7.6 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖) = 𝑁) |
100 | 99 | eqcomd 2744 |
. . . . . 6
⊢ (𝜑 → 𝑁 = Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺‘𝑖)) |
101 | 98, 100 | breqtrrd 5095 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖) ≤ 𝑁) |
102 | 22, 54, 27, 59, 31, 101 | le2addd 11475 |
. . . 4
⊢ (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) ≤ (𝐾 + 𝑁)) |
103 | 13 | nn0cnd 12176 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℂ) |
104 | 45 | nn0cnd 12176 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℂ) |
105 | 103, 104 | addcomd 11058 |
. . . 4
⊢ (𝜑 → (𝐾 + 𝑁) = (𝑁 + 𝐾)) |
106 | 102, 105 | breqtrd 5093 |
. . 3
⊢ (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) ≤ (𝑁 + 𝐾)) |
107 | 44, 47, 48, 58, 106 | elfzd 13127 |
. 2
⊢ (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺‘𝑖)) ∈ (1...(𝑁 + 𝐾))) |
108 | 43, 107 | eqeltrd 2839 |
1
⊢ (𝜑 → (𝐹‘𝑋) ∈ (1...(𝑁 + 𝐾))) |