Step | Hyp | Ref
| Expression |
1 | | sticksstones7.5 |
. . . 4
β’ πΉ = (π₯ β (1...πΎ) β¦ (π₯ + Ξ£π β (1...π₯)(πΊβπ))) |
2 | 1 | a1i 11 |
. . 3
β’ (π β πΉ = (π₯ β (1...πΎ) β¦ (π₯ + Ξ£π β (1...π₯)(πΊβπ)))) |
3 | | simpr 486 |
. . . 4
β’ ((π β§ π₯ = π) β π₯ = π) |
4 | 3 | oveq2d 7374 |
. . . . 5
β’ ((π β§ π₯ = π) β (1...π₯) = (1...π)) |
5 | 4 | sumeq1d 15591 |
. . . 4
β’ ((π β§ π₯ = π) β Ξ£π β (1...π₯)(πΊβπ) = Ξ£π β (1...π)(πΊβπ)) |
6 | 3, 5 | oveq12d 7376 |
. . 3
β’ ((π β§ π₯ = π) β (π₯ + Ξ£π β (1...π₯)(πΊβπ)) = (π + Ξ£π β (1...π)(πΊβπ))) |
7 | | sticksstones7.4 |
. . 3
β’ (π β π β (1...πΎ)) |
8 | | elfznn 13476 |
. . . . . 6
β’ (π β (1...πΎ) β π β β) |
9 | 7, 8 | syl 17 |
. . . . 5
β’ (π β π β β) |
10 | 9 | nnnn0d 12478 |
. . . 4
β’ (π β π β
β0) |
11 | | fzfid 13884 |
. . . . 5
β’ (π β (1...π) β Fin) |
12 | | 1zzd 12539 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β 1 β β€) |
13 | | sticksstones7.2 |
. . . . . . . . . 10
β’ (π β πΎ β
β0) |
14 | 13 | nn0zd 12530 |
. . . . . . . . 9
β’ (π β πΎ β β€) |
15 | 14 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β πΎ β β€) |
16 | 15 | peano2zd 12615 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (πΎ + 1) β β€) |
17 | | elfzelz 13447 |
. . . . . . . 8
β’ (π β (1...π) β π β β€) |
18 | 17 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β π β β€) |
19 | | elfzle1 13450 |
. . . . . . . 8
β’ (π β (1...π) β 1 β€ π) |
20 | 19 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β 1 β€ π) |
21 | 18 | zred 12612 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β β) |
22 | 9 | nnred 12173 |
. . . . . . . . 9
β’ (π β π β β) |
23 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β β) |
24 | 16 | zred 12612 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (πΎ + 1) β β) |
25 | | elfzle2 13451 |
. . . . . . . . 9
β’ (π β (1...π) β π β€ π) |
26 | 25 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β€ π) |
27 | 13 | nn0red 12479 |
. . . . . . . . . 10
β’ (π β πΎ β β) |
28 | | 1red 11161 |
. . . . . . . . . . 11
β’ (π β 1 β
β) |
29 | 27, 28 | readdcld 11189 |
. . . . . . . . . 10
β’ (π β (πΎ + 1) β β) |
30 | | elfzle2 13451 |
. . . . . . . . . . 11
β’ (π β (1...πΎ) β π β€ πΎ) |
31 | 7, 30 | syl 17 |
. . . . . . . . . 10
β’ (π β π β€ πΎ) |
32 | 27 | lep1d 12091 |
. . . . . . . . . 10
β’ (π β πΎ β€ (πΎ + 1)) |
33 | 22, 27, 29, 31, 32 | letrd 11317 |
. . . . . . . . 9
β’ (π β π β€ (πΎ + 1)) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β€ (πΎ + 1)) |
35 | 21, 23, 24, 26, 34 | letrd 11317 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β π β€ (πΎ + 1)) |
36 | 12, 16, 18, 20, 35 | elfzd 13438 |
. . . . . 6
β’ ((π β§ π β (1...π)) β π β (1...(πΎ + 1))) |
37 | | sticksstones7.3 |
. . . . . . . 8
β’ (π β πΊ:(1...(πΎ +
1))βΆβ0) |
38 | 37 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β πΊ:(1...(πΎ +
1))βΆβ0) |
39 | 38 | ffvelcdmda 7036 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π β (1...(πΎ + 1))) β (πΊβπ) β
β0) |
40 | 36, 39 | mpdan 686 |
. . . . 5
β’ ((π β§ π β (1...π)) β (πΊβπ) β
β0) |
41 | 11, 40 | fsumnn0cl 15626 |
. . . 4
β’ (π β Ξ£π β (1...π)(πΊβπ) β
β0) |
42 | 10, 41 | nn0addcld 12482 |
. . 3
β’ (π β (π + Ξ£π β (1...π)(πΊβπ)) β
β0) |
43 | 2, 6, 7, 42 | fvmptd 6956 |
. 2
β’ (π β (πΉβπ) = (π + Ξ£π β (1...π)(πΊβπ))) |
44 | | 1zzd 12539 |
. . 3
β’ (π β 1 β
β€) |
45 | | sticksstones7.1 |
. . . . 5
β’ (π β π β
β0) |
46 | 45 | nn0zd 12530 |
. . . 4
β’ (π β π β β€) |
47 | 46, 14 | zaddcld 12616 |
. . 3
β’ (π β (π + πΎ) β β€) |
48 | 42 | nn0zd 12530 |
. . 3
β’ (π β (π + Ξ£π β (1...π)(πΊβπ)) β β€) |
49 | | eqid 2733 |
. . . . . 6
β’ 1 =
1 |
50 | | 1p0e1 12282 |
. . . . . 6
β’ (1 + 0) =
1 |
51 | 49, 50 | eqtr4i 2764 |
. . . . 5
β’ 1 = (1 +
0) |
52 | 51 | a1i 11 |
. . . 4
β’ (π β 1 = (1 +
0)) |
53 | | 0red 11163 |
. . . . 5
β’ (π β 0 β
β) |
54 | 41 | nn0red 12479 |
. . . . 5
β’ (π β Ξ£π β (1...π)(πΊβπ) β β) |
55 | 9 | nnge1d 12206 |
. . . . 5
β’ (π β 1 β€ π) |
56 | 41 | nn0ge0d 12481 |
. . . . 5
β’ (π β 0 β€ Ξ£π β (1...π)(πΊβπ)) |
57 | 28, 53, 22, 54, 55, 56 | le2addd 11779 |
. . . 4
β’ (π β (1 + 0) β€ (π + Ξ£π β (1...π)(πΊβπ))) |
58 | 52, 57 | eqbrtrd 5128 |
. . 3
β’ (π β 1 β€ (π + Ξ£π β (1...π)(πΊβπ))) |
59 | 45 | nn0red 12479 |
. . . . 5
β’ (π β π β β) |
60 | | fzfid 13884 |
. . . . . . . . . 10
β’ (π β ((π + 1)...(πΎ + 1)) β Fin) |
61 | 44 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β 1 β
β€) |
62 | 14 | peano2zd 12615 |
. . . . . . . . . . . . 13
β’ (π β (πΎ + 1) β β€) |
63 | 62 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β (πΎ + 1) β β€) |
64 | | elfzelz 13447 |
. . . . . . . . . . . . 13
β’ (π β ((π + 1)...(πΎ + 1)) β π β β€) |
65 | 64 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β π β β€) |
66 | 28 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β 1 β
β) |
67 | 22 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β π β β) |
68 | 67, 66 | readdcld 11189 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β (π + 1) β β) |
69 | 65 | zred 12612 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β π β β) |
70 | 55 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β 1 β€ π) |
71 | 67 | lep1d 12091 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β π β€ (π + 1)) |
72 | 66, 67, 68, 70, 71 | letrd 11317 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β 1 β€ (π + 1)) |
73 | | elfzle1 13450 |
. . . . . . . . . . . . . 14
β’ (π β ((π + 1)...(πΎ + 1)) β (π + 1) β€ π) |
74 | 73 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β (π + 1) β€ π) |
75 | 66, 68, 69, 72, 74 | letrd 11317 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β 1 β€ π) |
76 | | elfzle2 13451 |
. . . . . . . . . . . . 13
β’ (π β ((π + 1)...(πΎ + 1)) β π β€ (πΎ + 1)) |
77 | 76 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β π β€ (πΎ + 1)) |
78 | 61, 63, 65, 75, 77 | elfzd 13438 |
. . . . . . . . . . 11
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β π β (1...(πΎ + 1))) |
79 | 37 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...(πΎ + 1))) β (πΊβπ) β
β0) |
80 | 79 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β ((π + 1)...(πΎ + 1))) β§ π β (1...(πΎ + 1))) β (πΊβπ) β
β0) |
81 | 78, 80 | mpdan 686 |
. . . . . . . . . 10
β’ ((π β§ π β ((π + 1)...(πΎ + 1))) β (πΊβπ) β
β0) |
82 | 60, 81 | fsumnn0cl 15626 |
. . . . . . . . 9
β’ (π β Ξ£π β ((π + 1)...(πΎ + 1))(πΊβπ) β
β0) |
83 | 82 | nn0ge0d 12481 |
. . . . . . . 8
β’ (π β 0 β€ Ξ£π β ((π + 1)...(πΎ + 1))(πΊβπ)) |
84 | 82 | nn0red 12479 |
. . . . . . . . 9
β’ (π β Ξ£π β ((π + 1)...(πΎ + 1))(πΊβπ) β β) |
85 | 54, 84 | addge01d 11748 |
. . . . . . . 8
β’ (π β (0 β€ Ξ£π β ((π + 1)...(πΎ + 1))(πΊβπ) β Ξ£π β (1...π)(πΊβπ) β€ (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...(πΎ + 1))(πΊβπ)))) |
86 | 83, 85 | mpbid 231 |
. . . . . . 7
β’ (π β Ξ£π β (1...π)(πΊβπ) β€ (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...(πΎ + 1))(πΊβπ))) |
87 | 22 | ltp1d 12090 |
. . . . . . . . 9
β’ (π β π < (π + 1)) |
88 | | fzdisj 13474 |
. . . . . . . . 9
β’ (π < (π + 1) β ((1...π) β© ((π + 1)...(πΎ + 1))) = β
) |
89 | 87, 88 | syl 17 |
. . . . . . . 8
β’ (π β ((1...π) β© ((π + 1)...(πΎ + 1))) = β
) |
90 | 10 | nn0zd 12530 |
. . . . . . . . . 10
β’ (π β π β β€) |
91 | 44, 62, 90, 55, 33 | elfzd 13438 |
. . . . . . . . 9
β’ (π β π β (1...(πΎ + 1))) |
92 | | fzsplit 13473 |
. . . . . . . . 9
β’ (π β (1...(πΎ + 1)) β (1...(πΎ + 1)) = ((1...π) βͺ ((π + 1)...(πΎ + 1)))) |
93 | 91, 92 | syl 17 |
. . . . . . . 8
β’ (π β (1...(πΎ + 1)) = ((1...π) βͺ ((π + 1)...(πΎ + 1)))) |
94 | | fzfid 13884 |
. . . . . . . 8
β’ (π β (1...(πΎ + 1)) β Fin) |
95 | | nn0cn 12428 |
. . . . . . . . 9
β’ ((πΊβπ) β β0 β (πΊβπ) β β) |
96 | 79, 95 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (1...(πΎ + 1))) β (πΊβπ) β β) |
97 | 89, 93, 94, 96 | fsumsplit 15631 |
. . . . . . 7
β’ (π β Ξ£π β (1...(πΎ + 1))(πΊβπ) = (Ξ£π β (1...π)(πΊβπ) + Ξ£π β ((π + 1)...(πΎ + 1))(πΊβπ))) |
98 | 86, 97 | breqtrrd 5134 |
. . . . . 6
β’ (π β Ξ£π β (1...π)(πΊβπ) β€ Ξ£π β (1...(πΎ + 1))(πΊβπ)) |
99 | | sticksstones7.6 |
. . . . . . 7
β’ (π β Ξ£π β (1...(πΎ + 1))(πΊβπ) = π) |
100 | 99 | eqcomd 2739 |
. . . . . 6
β’ (π β π = Ξ£π β (1...(πΎ + 1))(πΊβπ)) |
101 | 98, 100 | breqtrrd 5134 |
. . . . 5
β’ (π β Ξ£π β (1...π)(πΊβπ) β€ π) |
102 | 22, 54, 27, 59, 31, 101 | le2addd 11779 |
. . . 4
β’ (π β (π + Ξ£π β (1...π)(πΊβπ)) β€ (πΎ + π)) |
103 | 13 | nn0cnd 12480 |
. . . . 5
β’ (π β πΎ β β) |
104 | 45 | nn0cnd 12480 |
. . . . 5
β’ (π β π β β) |
105 | 103, 104 | addcomd 11362 |
. . . 4
β’ (π β (πΎ + π) = (π + πΎ)) |
106 | 102, 105 | breqtrd 5132 |
. . 3
β’ (π β (π + Ξ£π β (1...π)(πΊβπ)) β€ (π + πΎ)) |
107 | 44, 47, 48, 58, 106 | elfzd 13438 |
. 2
β’ (π β (π + Ξ£π β (1...π)(πΊβπ)) β (1...(π + πΎ))) |
108 | 43, 107 | eqeltrd 2834 |
1
β’ (π β (πΉβπ) β (1...(π + πΎ))) |