Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ π β (1...πΎ)) β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) = (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))) |
2 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β π΄ β§ π β (1...πΎ)) β§ π = π) β π = π) |
3 | 2 | oveq2d 7425 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄ β§ π β (1...πΎ)) β§ π = π) β (1...π) = (1...π)) |
4 | 3 | sumeq1d 15647 |
. . . . . . . . . 10
β’ (((π β§ π β π΄ β§ π β (1...πΎ)) β§ π = π) β Ξ£π β (1...π)(πβπ) = Ξ£π β (1...π)(πβπ)) |
5 | 2, 4 | oveq12d 7427 |
. . . . . . . . 9
β’ (((π β§ π β π΄ β§ π β (1...πΎ)) β§ π = π) β (π + Ξ£π β (1...π)(πβπ)) = (π + Ξ£π β (1...π)(πβπ))) |
6 | | simp3 1139 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ π β (1...πΎ)) β π β (1...πΎ)) |
7 | | ovexd 7444 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ π β (1...πΎ)) β (π + Ξ£π β (1...π)(πβπ)) β V) |
8 | 1, 5, 6, 7 | fvmptd 7006 |
. . . . . . . 8
β’ ((π β§ π β π΄ β§ π β (1...πΎ)) β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ) = (π + Ξ£π β (1...π)(πβπ))) |
9 | | sticksstones8.1 |
. . . . . . . . . 10
β’ (π β π β
β0) |
10 | 9 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ π β (1...πΎ)) β π β
β0) |
11 | | sticksstones8.2 |
. . . . . . . . . 10
β’ (π β πΎ β
β0) |
12 | 11 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ π β (1...πΎ)) β πΎ β
β0) |
13 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β π β π΄) |
14 | | sticksstones8.4 |
. . . . . . . . . . . . . . 15
β’ π΄ = {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π΄ = {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)}) |
16 | 15 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} = π΄) |
17 | 13, 16 | eleqtrrd 2837 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)}) |
18 | | feq1 6699 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π:(1...(πΎ + 1))βΆβ0 β
π:(1...(πΎ +
1))βΆβ0)) |
19 | | simpl 484 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = π β§ π β (1...(πΎ + 1))) β π = π) |
20 | 19 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = π β§ π β (1...(πΎ + 1))) β (πβπ) = (πβπ)) |
21 | 20 | sumeq2dv 15649 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β Ξ£π β (1...(πΎ + 1))(πβπ) = Ξ£π β (1...(πΎ + 1))(πβπ)) |
22 | 21 | eqeq1d 2735 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (Ξ£π β (1...(πΎ + 1))(πβπ) = π β Ξ£π β (1...(πΎ + 1))(πβπ) = π)) |
23 | 18, 22 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π) β (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π))) |
24 | 23 | elabg 3667 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β (π β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π))) |
25 | 13, 24 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β (π β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π))) |
26 | 25 | biimpd 228 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β (π β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π))) |
27 | 17, 26 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)) |
28 | 27 | simpld 496 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β π:(1...(πΎ +
1))βΆβ0) |
29 | 28 | 3adant3 1133 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ π β (1...πΎ)) β π:(1...(πΎ +
1))βΆβ0) |
30 | | eqid 2733 |
. . . . . . . . 9
β’ (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) = (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) |
31 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
32 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π(1...(πΎ + 1)) |
33 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π(1...(πΎ + 1)) |
34 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π(πβπ) |
35 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π(πβπ) |
36 | 31, 32, 33, 34, 35 | cbvsum 15641 |
. . . . . . . . . . 11
β’
Ξ£π β
(1...(πΎ + 1))(πβπ) = Ξ£π β (1...(πΎ + 1))(πβπ) |
37 | 27 | simprd 497 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β Ξ£π β (1...(πΎ + 1))(πβπ) = π) |
38 | 36, 37 | eqtr3id 2787 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β Ξ£π β (1...(πΎ + 1))(πβπ) = π) |
39 | 38 | 3adant3 1133 |
. . . . . . . . 9
β’ ((π β§ π β π΄ β§ π β (1...πΎ)) β Ξ£π β (1...(πΎ + 1))(πβπ) = π) |
40 | 10, 12, 29, 6, 30, 39 | sticksstones7 40968 |
. . . . . . . 8
β’ ((π β§ π β π΄ β§ π β (1...πΎ)) β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ) β (1...(π + πΎ))) |
41 | 8, 40 | eqeltrrd 2835 |
. . . . . . 7
β’ ((π β§ π β π΄ β§ π β (1...πΎ)) β (π + Ξ£π β (1...π)(πβπ)) β (1...(π + πΎ))) |
42 | 41 | 3expa 1119 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π β (1...πΎ)) β (π + Ξ£π β (1...π)(πβπ)) β (1...(π + πΎ))) |
43 | | eqid 2733 |
. . . . . 6
β’ (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) = (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) |
44 | 42, 43 | fmptd 7114 |
. . . . 5
β’ ((π β§ π β π΄) β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))):(1...πΎ)βΆ(1...(π + πΎ))) |
45 | 9 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β π β
β0) |
46 | 45 | adantr 482 |
. . . . . . . . 9
β’
(((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β§ π₯ < π¦) β π β
β0) |
47 | 11 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β πΎ β
β0) |
48 | 47 | adantr 482 |
. . . . . . . . 9
β’
(((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β§ π₯ < π¦) β πΎ β
β0) |
49 | 24 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β (π β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π))) |
50 | 49 | biimpd 228 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β (π β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π))) |
51 | 17, 50 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)) |
52 | 51 | simpld 496 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π:(1...(πΎ +
1))βΆβ0) |
53 | 52 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π₯ β (1...πΎ)) β π:(1...(πΎ +
1))βΆβ0) |
54 | 53 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β π:(1...(πΎ +
1))βΆβ0) |
55 | 54 | adantr 482 |
. . . . . . . . 9
β’
(((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β§ π₯ < π¦) β π:(1...(πΎ +
1))βΆβ0) |
56 | | simpllr 775 |
. . . . . . . . 9
β’
(((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β§ π₯ < π¦) β π₯ β (1...πΎ)) |
57 | | simplr 768 |
. . . . . . . . 9
β’
(((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β§ π₯ < π¦) β π¦ β (1...πΎ)) |
58 | | simpr 486 |
. . . . . . . . 9
β’
(((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β§ π₯ < π¦) β π₯ < π¦) |
59 | 46, 48, 55, 56, 57, 58, 43 | sticksstones6 40967 |
. . . . . . . 8
β’
(((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β§ π₯ < π¦) β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦)) |
60 | 59 | ex 414 |
. . . . . . 7
β’ ((((π β§ π β π΄) β§ π₯ β (1...πΎ)) β§ π¦ β (1...πΎ)) β (π₯ < π¦ β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦))) |
61 | 60 | ralrimiva 3147 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π₯ β (1...πΎ)) β βπ¦ β (1...πΎ)(π₯ < π¦ β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦))) |
62 | 61 | ralrimiva 3147 |
. . . . 5
β’ ((π β§ π β π΄) β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦))) |
63 | 44, 62 | jca 513 |
. . . 4
β’ ((π β§ π β π΄) β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))):(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦)))) |
64 | | fzfid 13938 |
. . . . . 6
β’ ((π β§ π β π΄) β (1...πΎ) β Fin) |
65 | 44, 64 | fexd 7229 |
. . . . 5
β’ ((π β§ π β π΄) β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β V) |
66 | | feq1 6699 |
. . . . . . 7
β’ (π = (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β (π:(1...πΎ)βΆ(1...(π + πΎ)) β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))):(1...πΎ)βΆ(1...(π + πΎ)))) |
67 | | fveq1 6891 |
. . . . . . . . . 10
β’ (π = (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β (πβπ₯) = ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯)) |
68 | | fveq1 6891 |
. . . . . . . . . 10
β’ (π = (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β (πβπ¦) = ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦)) |
69 | 67, 68 | breq12d 5162 |
. . . . . . . . 9
β’ (π = (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β ((πβπ₯) < (πβπ¦) β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦))) |
70 | 69 | imbi2d 341 |
. . . . . . . 8
β’ (π = (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β ((π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (π₯ < π¦ β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦)))) |
71 | 70 | 2ralbidv 3219 |
. . . . . . 7
β’ (π = (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β (βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦)))) |
72 | 66, 71 | anbi12d 632 |
. . . . . 6
β’ (π = (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β ((π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦))) β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))):(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦))))) |
73 | 72 | elabg 3667 |
. . . . 5
β’ ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β V β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))} β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))):(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦))))) |
74 | 65, 73 | syl 17 |
. . . 4
β’ ((π β§ π β π΄) β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))} β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))):(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ₯) < ((π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))βπ¦))))) |
75 | 63, 74 | mpbird 257 |
. . 3
β’ ((π β§ π β π΄) β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))}) |
76 | | sticksstones8.5 |
. . . 4
β’ π΅ = {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))} |
77 | 76 | a1i 11 |
. . 3
β’ ((π β§ π β π΄) β π΅ = {π β£ (π:(1...πΎ)βΆ(1...(π + πΎ)) β§ βπ₯ β (1...πΎ)βπ¦ β (1...πΎ)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))}) |
78 | 75, 77 | eleqtrrd 2837 |
. 2
β’ ((π β§ π β π΄) β (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ))) β π΅) |
79 | | sticksstones8.3 |
. 2
β’ πΉ = (π β π΄ β¦ (π β (1...πΎ) β¦ (π + Ξ£π β (1...π)(πβπ)))) |
80 | 78, 79 | fmptd 7114 |
1
β’ (π β πΉ:π΄βΆπ΅) |