Step | Hyp | Ref
| Expression |
1 | | sticksstones6.4 |
. . . . 5
β’ (π β π β (1...πΎ)) |
2 | | elfznn 13476 |
. . . . 5
β’ (π β (1...πΎ) β π β β) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β π β β) |
4 | 3 | nnred 12173 |
. . 3
β’ (π β π β β) |
5 | | fzfid 13884 |
. . . . 5
β’ (π β (1...π) β Fin) |
6 | | 1zzd 12539 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β 1 β β€) |
7 | | sticksstones6.2 |
. . . . . . . . . 10
β’ (π β πΎ β
β0) |
8 | 7 | nn0zd 12530 |
. . . . . . . . 9
β’ (π β πΎ β β€) |
9 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β πΎ β β€) |
10 | 9 | peano2zd 12615 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (πΎ + 1) β β€) |
11 | | elfznn 13476 |
. . . . . . . . 9
β’ (π β (1...π) β π β β) |
12 | 11 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β β) |
13 | 12 | nnzd 12531 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β π β β€) |
14 | 12 | nnge1d 12206 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β 1 β€ π) |
15 | 12 | nnred 12173 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β β) |
16 | 9 | zred 12612 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β πΎ β β) |
17 | 10 | zred 12612 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (πΎ + 1) β β) |
18 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β π β β) |
19 | 18 | nnred 12173 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β π β β) |
20 | | elfzle2 13451 |
. . . . . . . . . 10
β’ (π β (1...π) β π β€ π) |
21 | 20 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β π β€ π) |
22 | | elfzle2 13451 |
. . . . . . . . . . 11
β’ (π β (1...πΎ) β π β€ πΎ) |
23 | 1, 22 | syl 17 |
. . . . . . . . . 10
β’ (π β π β€ πΎ) |
24 | 23 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β π β€ πΎ) |
25 | 15, 19, 16, 21, 24 | letrd 11317 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β€ πΎ) |
26 | 16 | lep1d 12091 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β πΎ β€ (πΎ + 1)) |
27 | 15, 16, 17, 25, 26 | letrd 11317 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β π β€ (πΎ + 1)) |
28 | 6, 10, 13, 14, 27 | elfzd 13438 |
. . . . . 6
β’ ((π β§ π β (1...π)) β π β (1...(πΎ + 1))) |
29 | | sticksstones6.3 |
. . . . . . . . 9
β’ (π β πΊ:(1...(πΎ +
1))βΆβ0) |
30 | 29 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...(πΎ + 1))) β πΊ:(1...(πΎ +
1))βΆβ0) |
31 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β (1...(πΎ + 1))) β π β (1...(πΎ + 1))) |
32 | 30, 31 | ffvelcdmd 7037 |
. . . . . . 7
β’ ((π β§ π β (1...(πΎ + 1))) β (πΊβπ) β
β0) |
33 | 32 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π β (1...(πΎ + 1))) β (πΊβπ) β
β0) |
34 | 28, 33 | mpdan 686 |
. . . . 5
β’ ((π β§ π β (1...π)) β (πΊβπ) β
β0) |
35 | 5, 34 | fsumnn0cl 15626 |
. . . 4
β’ (π β Ξ£π β (1...π)(πΊβπ) β
β0) |
36 | 35 | nn0red 12479 |
. . 3
β’ (π β Ξ£π β (1...π)(πΊβπ) β β) |
37 | | sticksstones6.5 |
. . . . 5
β’ (π β π β (1...πΎ)) |
38 | | elfznn 13476 |
. . . . 5
β’ (π β (1...πΎ) β π β β) |
39 | 37, 38 | syl 17 |
. . . 4
β’ (π β π β β) |
40 | 39 | nnred 12173 |
. . 3
β’ (π β π β β) |
41 | | fzfid 13884 |
. . . . 5
β’ (π β ((π + 1)...π) β Fin) |
42 | | 1zzd 12539 |
. . . . . . . 8
β’ ((π β§ π β ((π + 1)...π)) β 1 β β€) |
43 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β πΎ β β€) |
44 | 43 | peano2zd 12615 |
. . . . . . . 8
β’ ((π β§ π β ((π + 1)...π)) β (πΎ + 1) β β€) |
45 | | elfzelz 13447 |
. . . . . . . . 9
β’ (π β ((π + 1)...π) β π β β€) |
46 | 45 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β ((π + 1)...π)) β π β β€) |
47 | | 1red 11161 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β 1 β β) |
48 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((π + 1)...π)) β π β β) |
49 | 48, 47 | readdcld 11189 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β (π + 1) β β) |
50 | 46 | zred 12612 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β π β β) |
51 | | 1red 11161 |
. . . . . . . . . . 11
β’ (π β 1 β
β) |
52 | 4, 51 | readdcld 11189 |
. . . . . . . . . . 11
β’ (π β (π + 1) β β) |
53 | 3 | nnge1d 12206 |
. . . . . . . . . . 11
β’ (π β 1 β€ π) |
54 | 4 | ltp1d 12090 |
. . . . . . . . . . . 12
β’ (π β π < (π + 1)) |
55 | 4, 52, 54 | ltled 11308 |
. . . . . . . . . . 11
β’ (π β π β€ (π + 1)) |
56 | 51, 4, 52, 53, 55 | letrd 11317 |
. . . . . . . . . 10
β’ (π β 1 β€ (π + 1)) |
57 | 56 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β 1 β€ (π + 1)) |
58 | | elfzle1 13450 |
. . . . . . . . . 10
β’ (π β ((π + 1)...π) β (π + 1) β€ π) |
59 | 58 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β (π + 1) β€ π) |
60 | 47, 49, 50, 57, 59 | letrd 11317 |
. . . . . . . 8
β’ ((π β§ π β ((π + 1)...π)) β 1 β€ π) |
61 | 40 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β π β β) |
62 | 44 | zred 12612 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β (πΎ + 1) β β) |
63 | | elfzle2 13451 |
. . . . . . . . . 10
β’ (π β ((π + 1)...π) β π β€ π) |
64 | 63 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β π β€ π) |
65 | 43 | zred 12612 |
. . . . . . . . . 10
β’ ((π β§ π β ((π + 1)...π)) β πΎ β β) |
66 | | elfzle2 13451 |
. . . . . . . . . . . 12
β’ (π β (1...πΎ) β π β€ πΎ) |
67 | 37, 66 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β€ πΎ) |
68 | 67 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((π + 1)...π)) β π β€ πΎ) |
69 | 65 | lep1d 12091 |
. . . . . . . . . 10
β’ ((π β§ π β ((π + 1)...π)) β πΎ β€ (πΎ + 1)) |
70 | 61, 65, 62, 68, 69 | letrd 11317 |
. . . . . . . . 9
β’ ((π β§ π β ((π + 1)...π)) β π β€ (πΎ + 1)) |
71 | 50, 61, 62, 64, 70 | letrd 11317 |
. . . . . . . 8
β’ ((π β§ π β ((π + 1)...π)) β π β€ (πΎ + 1)) |
72 | 42, 44, 46, 60, 71 | elfzd 13438 |
. . . . . . 7
β’ ((π β§ π β ((π + 1)...π)) β π β (1...(πΎ + 1))) |
73 | 32 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β ((π + 1)...π)) β§ π β (1...(πΎ + 1))) β (πΊβπ) β
β0) |
74 | 72, 73 | mpdan 686 |
. . . . . 6
β’ ((π β§ π β ((π + 1)...π)) β (πΊβπ) β
β0) |
75 | 74 | nn0red 12479 |
. . . . 5
β’ ((π β§ π β ((π + 1)...π)) β (πΊβπ) β β) |
76 | 41, 75 | fsumrecl 15624 |
. . . 4
β’ (π β Ξ£π β ((π + 1)...π)(πΊβπ) β β) |
77 | 36, 76 | readdcld 11189 |
. . 3
β’ (π β (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...π)(πΊβπ)) β β) |
78 | | sticksstones6.6 |
. . 3
β’ (π β π < π) |
79 | 74 | nn0ge0d 12481 |
. . . . 5
β’ ((π β§ π β ((π + 1)...π)) β 0 β€ (πΊβπ)) |
80 | 41, 75, 79 | fsumge0 15685 |
. . . 4
β’ (π β 0 β€ Ξ£π β ((π + 1)...π)(πΊβπ)) |
81 | 36, 76 | addge01d 11748 |
. . . 4
β’ (π β (0 β€ Ξ£π β ((π + 1)...π)(πΊβπ) β Ξ£π β (1...π)(πΊβπ) β€ (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...π)(πΊβπ)))) |
82 | 80, 81 | mpbid 231 |
. . 3
β’ (π β Ξ£π β (1...π)(πΊβπ) β€ (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...π)(πΊβπ))) |
83 | 4, 36, 40, 77, 78, 82 | ltleaddd 11781 |
. 2
β’ (π β (π + Ξ£π β (1...π)(πΊβπ)) < (π + (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...π)(πΊβπ)))) |
84 | | sticksstones6.7 |
. . . . 5
β’ πΉ = (π₯ β (1...πΎ) β¦ (π₯ + Ξ£π β (1...π₯)(πΊβπ))) |
85 | 84 | a1i 11 |
. . . 4
β’ (π β πΉ = (π₯ β (1...πΎ) β¦ (π₯ + Ξ£π β (1...π₯)(πΊβπ)))) |
86 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ = π) β π₯ = π) |
87 | 86 | oveq2d 7374 |
. . . . . 6
β’ ((π β§ π₯ = π) β (1...π₯) = (1...π)) |
88 | 87 | sumeq1d 15591 |
. . . . 5
β’ ((π β§ π₯ = π) β Ξ£π β (1...π₯)(πΊβπ) = Ξ£π β (1...π)(πΊβπ)) |
89 | 86, 88 | oveq12d 7376 |
. . . 4
β’ ((π β§ π₯ = π) β (π₯ + Ξ£π β (1...π₯)(πΊβπ)) = (π + Ξ£π β (1...π)(πΊβπ))) |
90 | 3 | nnnn0d 12478 |
. . . . 5
β’ (π β π β
β0) |
91 | 90, 35 | nn0addcld 12482 |
. . . 4
β’ (π β (π + Ξ£π β (1...π)(πΊβπ)) β
β0) |
92 | 85, 89, 1, 91 | fvmptd 6956 |
. . 3
β’ (π β (πΉβπ) = (π + Ξ£π β (1...π)(πΊβπ))) |
93 | 92 | eqcomd 2739 |
. 2
β’ (π β (π + Ξ£π β (1...π)(πΊβπ)) = (πΉβπ)) |
94 | | simpr 486 |
. . . . . 6
β’ ((π β§ π₯ = π) β π₯ = π) |
95 | 94 | oveq2d 7374 |
. . . . . . 7
β’ ((π β§ π₯ = π) β (1...π₯) = (1...π)) |
96 | 95 | sumeq1d 15591 |
. . . . . 6
β’ ((π β§ π₯ = π) β Ξ£π β (1...π₯)(πΊβπ) = Ξ£π β (1...π)(πΊβπ)) |
97 | 94, 96 | oveq12d 7376 |
. . . . 5
β’ ((π β§ π₯ = π) β (π₯ + Ξ£π β (1...π₯)(πΊβπ)) = (π + Ξ£π β (1...π)(πΊβπ))) |
98 | 39 | nnnn0d 12478 |
. . . . . 6
β’ (π β π β
β0) |
99 | | fzfid 13884 |
. . . . . . 7
β’ (π β (1...π) β Fin) |
100 | | 1zzd 12539 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β 1 β β€) |
101 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β πΎ β β€) |
102 | 101 | peano2zd 12615 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (πΎ + 1) β β€) |
103 | | elfzelz 13447 |
. . . . . . . . . 10
β’ (π β (1...π) β π β β€) |
104 | 103 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β π β β€) |
105 | | elfzle1 13450 |
. . . . . . . . . 10
β’ (π β (1...π) β 1 β€ π) |
106 | 105 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β 1 β€ π) |
107 | 104 | zred 12612 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β π β β) |
108 | 40 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β π β β) |
109 | 102 | zred 12612 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (πΎ + 1) β β) |
110 | | elfzle2 13451 |
. . . . . . . . . . 11
β’ (π β (1...π) β π β€ π) |
111 | 110 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β π β€ π) |
112 | 101 | zred 12612 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β πΎ β β) |
113 | 67 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β π β€ πΎ) |
114 | 112 | lep1d 12091 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β πΎ β€ (πΎ + 1)) |
115 | 108, 112,
109, 113, 114 | letrd 11317 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β π β€ (πΎ + 1)) |
116 | 107, 108,
109, 111, 115 | letrd 11317 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β π β€ (πΎ + 1)) |
117 | 100, 102,
104, 106, 116 | elfzd 13438 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β (1...(πΎ + 1))) |
118 | 32 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π β (1...(πΎ + 1))) β (πΊβπ) β
β0) |
119 | 117, 118 | mpdan 686 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (πΊβπ) β
β0) |
120 | 99, 119 | fsumnn0cl 15626 |
. . . . . 6
β’ (π β Ξ£π β (1...π)(πΊβπ) β
β0) |
121 | 98, 120 | nn0addcld 12482 |
. . . . 5
β’ (π β (π + Ξ£π β (1...π)(πΊβπ)) β
β0) |
122 | 85, 97, 37, 121 | fvmptd 6956 |
. . . 4
β’ (π β (πΉβπ) = (π + Ξ£π β (1...π)(πΊβπ))) |
123 | | fzdisj 13474 |
. . . . . . 7
β’ (π < (π + 1) β ((1...π) β© ((π + 1)...π)) = β
) |
124 | 54, 123 | syl 17 |
. . . . . 6
β’ (π β ((1...π) β© ((π + 1)...π)) = β
) |
125 | | 1zzd 12539 |
. . . . . . . 8
β’ (π β 1 β
β€) |
126 | 98 | nn0zd 12530 |
. . . . . . . 8
β’ (π β π β β€) |
127 | 90 | nn0zd 12530 |
. . . . . . . 8
β’ (π β π β β€) |
128 | 4, 40, 78 | ltled 11308 |
. . . . . . . 8
β’ (π β π β€ π) |
129 | 125, 126,
127, 53, 128 | elfzd 13438 |
. . . . . . 7
β’ (π β π β (1...π)) |
130 | | fzsplit 13473 |
. . . . . . 7
β’ (π β (1...π) β (1...π) = ((1...π) βͺ ((π + 1)...π))) |
131 | 129, 130 | syl 17 |
. . . . . 6
β’ (π β (1...π) = ((1...π) βͺ ((π + 1)...π))) |
132 | 119 | nn0red 12479 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (πΊβπ) β β) |
133 | 132 | recnd 11188 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (πΊβπ) β β) |
134 | 124, 131,
99, 133 | fsumsplit 15631 |
. . . . 5
β’ (π β Ξ£π β (1...π)(πΊβπ) = (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...π)(πΊβπ))) |
135 | 134 | oveq2d 7374 |
. . . 4
β’ (π β (π + Ξ£π β (1...π)(πΊβπ)) = (π + (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...π)(πΊβπ)))) |
136 | 122, 135 | eqtrd 2773 |
. . 3
β’ (π β (πΉβπ) = (π + (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...π)(πΊβπ)))) |
137 | 136 | eqcomd 2739 |
. 2
β’ (π β (π + (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...π)(πΊβπ))) = (πΉβπ)) |
138 | 83, 93, 137 | 3brtr3d 5137 |
1
β’ (π β (πΉβπ) < (πΉβπ)) |