Step | Hyp | Ref
| Expression |
1 | | sticksstones22.4 |
. . . 4
β’ π΄ = {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π)} |
2 | 1 | a1i 11 |
. . 3
β’ (π β π΄ = {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π)}) |
3 | 2 | fveq2d 6847 |
. 2
β’ (π β (β―βπ΄) = (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π)})) |
4 | | sticksstones22.1 |
. . 3
β’ (π β π β
β0) |
5 | | breq2 5110 |
. . . . . . . 8
β’ (π₯ = 0 β (Ξ£π β π (πβπ) β€ π₯ β Ξ£π β π (πβπ) β€ 0)) |
6 | 5 | anbi2d 630 |
. . . . . . 7
β’ (π₯ = 0 β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0))) |
7 | 6 | abbidv 2802 |
. . . . . 6
β’ (π₯ = 0 β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)} = {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)}) |
8 | 7 | fveq2d 6847 |
. . . . 5
β’ (π₯ = 0 β
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)}) = (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)})) |
9 | | oveq1 7365 |
. . . . . 6
β’ (π₯ = 0 β (π₯ + (β―βπ)) = (0 + (β―βπ))) |
10 | 9 | oveq1d 7373 |
. . . . 5
β’ (π₯ = 0 β ((π₯ + (β―βπ))C(β―βπ)) = ((0 + (β―βπ))C(β―βπ))) |
11 | 8, 10 | eqeq12d 2749 |
. . . 4
β’ (π₯ = 0 β
((β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)}) = ((π₯ + (β―βπ))C(β―βπ)) β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)}) = ((0 + (β―βπ))C(β―βπ)))) |
12 | | breq2 5110 |
. . . . . . . 8
β’ (π₯ = π¦ β (Ξ£π β π (πβπ) β€ π₯ β Ξ£π β π (πβπ) β€ π¦)) |
13 | 12 | anbi2d 630 |
. . . . . . 7
β’ (π₯ = π¦ β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦))) |
14 | 13 | abbidv 2802 |
. . . . . 6
β’ (π₯ = π¦ β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)} = {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) |
15 | 14 | fveq2d 6847 |
. . . . 5
β’ (π₯ = π¦ β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)}) = (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)})) |
16 | | oveq1 7365 |
. . . . . 6
β’ (π₯ = π¦ β (π₯ + (β―βπ)) = (π¦ + (β―βπ))) |
17 | 16 | oveq1d 7373 |
. . . . 5
β’ (π₯ = π¦ β ((π₯ + (β―βπ))C(β―βπ)) = ((π¦ + (β―βπ))C(β―βπ))) |
18 | 15, 17 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π¦ β ((β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)}) = ((π₯ + (β―βπ))C(β―βπ)) β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ)))) |
19 | | breq2 5110 |
. . . . . . . 8
β’ (π₯ = (π¦ + 1) β (Ξ£π β π (πβπ) β€ π₯ β Ξ£π β π (πβπ) β€ (π¦ + 1))) |
20 | 19 | anbi2d 630 |
. . . . . . 7
β’ (π₯ = (π¦ + 1) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1)))) |
21 | 20 | abbidv 2802 |
. . . . . 6
β’ (π₯ = (π¦ + 1) β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)} = {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))}) |
22 | 21 | fveq2d 6847 |
. . . . 5
β’ (π₯ = (π¦ + 1) β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)}) = (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))})) |
23 | | oveq1 7365 |
. . . . . 6
β’ (π₯ = (π¦ + 1) β (π₯ + (β―βπ)) = ((π¦ + 1) + (β―βπ))) |
24 | 23 | oveq1d 7373 |
. . . . 5
β’ (π₯ = (π¦ + 1) β ((π₯ + (β―βπ))C(β―βπ)) = (((π¦ + 1) + (β―βπ))C(β―βπ))) |
25 | 22, 24 | eqeq12d 2749 |
. . . 4
β’ (π₯ = (π¦ + 1) β ((β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)}) = ((π₯ + (β―βπ))C(β―βπ)) β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))}) = (((π¦ + 1) + (β―βπ))C(β―βπ)))) |
26 | | breq2 5110 |
. . . . . . . 8
β’ (π₯ = π β (Ξ£π β π (πβπ) β€ π₯ β Ξ£π β π (πβπ) β€ π)) |
27 | 26 | anbi2d 630 |
. . . . . . 7
β’ (π₯ = π β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π))) |
28 | 27 | abbidv 2802 |
. . . . . 6
β’ (π₯ = π β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)} = {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π)}) |
29 | 28 | fveq2d 6847 |
. . . . 5
β’ (π₯ = π β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)}) = (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π)})) |
30 | | oveq1 7365 |
. . . . . 6
β’ (π₯ = π β (π₯ + (β―βπ)) = (π + (β―βπ))) |
31 | 30 | oveq1d 7373 |
. . . . 5
β’ (π₯ = π β ((π₯ + (β―βπ))C(β―βπ)) = ((π + (β―βπ))C(β―βπ))) |
32 | 29, 31 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π β ((β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π₯)}) = ((π₯ + (β―βπ))C(β―βπ)) β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π)}) = ((π + (β―βπ))C(β―βπ)))) |
33 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β π:πβΆβ0) |
34 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β Ξ£π β π (πβπ) β€ 0) |
35 | | sticksstones22.2 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β Fin) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π:πβΆβ0) β π β Fin) |
37 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π:πβΆβ0) β π:πβΆβ0) |
38 | 37 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π:πβΆβ0) β§ π β π) β (πβπ) β
β0) |
39 | 36, 38 | fsumnn0cl 15626 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π:πβΆβ0) β
Ξ£π β π (πβπ) β
β0) |
40 | 33, 39 | syldan 592 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β Ξ£π β π (πβπ) β
β0) |
41 | 40 | nn0ge0d 12481 |
. . . . . . . . . . . . 13
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β 0 β€ Ξ£π β π (πβπ)) |
42 | | 0red 11163 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β 0 β
β) |
43 | 40 | nn0red 12479 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β Ξ£π β π (πβπ) β β) |
44 | 42, 43 | lenltd 11306 |
. . . . . . . . . . . . 13
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β (0 β€ Ξ£π β π (πβπ) β Β¬ Ξ£π β π (πβπ) < 0)) |
45 | 41, 44 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β Β¬ Ξ£π β π (πβπ) < 0) |
46 | 34, 45 | jca 513 |
. . . . . . . . . . 11
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β (Ξ£π β π (πβπ) β€ 0 β§ Β¬ Ξ£π β π (πβπ) < 0)) |
47 | 43, 42 | eqleltd 11304 |
. . . . . . . . . . 11
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β (Ξ£π β π (πβπ) = 0 β (Ξ£π β π (πβπ) β€ 0 β§ Β¬ Ξ£π β π (πβπ) < 0))) |
48 | 46, 47 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β Ξ£π β π (πβπ) = 0) |
49 | 33, 48 | jca 513 |
. . . . . . . . 9
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)) |
50 | 49 | ex 414 |
. . . . . . . 8
β’ (π β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0))) |
51 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)) β π:πβΆβ0) |
52 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)) β Ξ£π β π (πβπ) = 0) |
53 | | 0red 11163 |
. . . . . . . . . . . 12
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)) β 0 β
β) |
54 | 53 | leidd 11726 |
. . . . . . . . . . 11
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)) β 0 β€ 0) |
55 | 52, 54 | eqbrtrd 5128 |
. . . . . . . . . 10
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)) β Ξ£π β π (πβπ) β€ 0) |
56 | 51, 55 | jca 513 |
. . . . . . . . 9
β’ ((π β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)) |
57 | 56 | ex 414 |
. . . . . . . 8
β’ (π β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0))) |
58 | 50, 57 | impbid 211 |
. . . . . . 7
β’ (π β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0))) |
59 | 58 | abbidv 2802 |
. . . . . 6
β’ (π β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)} = {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)}) |
60 | 59 | fveq2d 6847 |
. . . . 5
β’ (π β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)}) = (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)})) |
61 | | 0nn0 12433 |
. . . . . . . 8
β’ 0 β
β0 |
62 | 61 | a1i 11 |
. . . . . . 7
β’ (π β 0 β
β0) |
63 | | sticksstones22.3 |
. . . . . . 7
β’ (π β π β β
) |
64 | | eqid 2733 |
. . . . . . 7
β’ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)} = {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)} |
65 | 62, 35, 63, 64 | sticksstones21 40621 |
. . . . . 6
β’ (π β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)}) = ((0 + ((β―βπ) β
1))C((β―βπ)
β 1))) |
66 | | hashnncl 14272 |
. . . . . . . . . . . . . . . 16
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
67 | 35, 66 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((β―βπ) β β β π β β
)) |
68 | 67 | bicomd 222 |
. . . . . . . . . . . . . 14
β’ (π β (π β β
β (β―βπ) β
β)) |
69 | 68 | biimpd 228 |
. . . . . . . . . . . . 13
β’ (π β (π β β
β (β―βπ) β
β)) |
70 | 63, 69 | mpd 15 |
. . . . . . . . . . . 12
β’ (π β (β―βπ) β
β) |
71 | 70 | nncnd 12174 |
. . . . . . . . . . 11
β’ (π β (β―βπ) β
β) |
72 | | 1cnd 11155 |
. . . . . . . . . . 11
β’ (π β 1 β
β) |
73 | 71, 72 | subcld 11517 |
. . . . . . . . . 10
β’ (π β ((β―βπ) β 1) β
β) |
74 | 73 | addid2d 11361 |
. . . . . . . . 9
β’ (π β (0 + ((β―βπ) β 1)) =
((β―βπ) β
1)) |
75 | 74 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((0 +
((β―βπ) β
1))C((β―βπ)
β 1)) = (((β―βπ) β 1)C((β―βπ) β 1))) |
76 | | nnm1nn0 12459 |
. . . . . . . . . 10
β’
((β―βπ)
β β β ((β―βπ) β 1) β
β0) |
77 | 70, 76 | syl 17 |
. . . . . . . . 9
β’ (π β ((β―βπ) β 1) β
β0) |
78 | | bcnn 14218 |
. . . . . . . . 9
β’
(((β―βπ)
β 1) β β0 β (((β―βπ) β 1)C((β―βπ) β 1)) =
1) |
79 | 77, 78 | syl 17 |
. . . . . . . 8
β’ (π β (((β―βπ) β
1)C((β―βπ)
β 1)) = 1) |
80 | 75, 79 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((0 +
((β―βπ) β
1))C((β―βπ)
β 1)) = 1) |
81 | | eqidd 2734 |
. . . . . . 7
β’ (π β 1 = 1) |
82 | 70 | nnnn0d 12478 |
. . . . . . . . . 10
β’ (π β (β―βπ) β
β0) |
83 | | bcnn 14218 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β ((β―βπ)C(β―βπ)) = 1) |
84 | 82, 83 | syl 17 |
. . . . . . . . 9
β’ (π β ((β―βπ)C(β―βπ)) = 1) |
85 | 84 | eqcomd 2739 |
. . . . . . . 8
β’ (π β 1 = ((β―βπ)C(β―βπ))) |
86 | 71 | addid2d 11361 |
. . . . . . . . . 10
β’ (π β (0 + (β―βπ)) = (β―βπ)) |
87 | 86 | eqcomd 2739 |
. . . . . . . . 9
β’ (π β (β―βπ) = (0 + (β―βπ))) |
88 | 87 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((β―βπ)C(β―βπ)) = ((0 + (β―βπ))C(β―βπ))) |
89 | 85, 88 | eqtrd 2773 |
. . . . . . 7
β’ (π β 1 = ((0 +
(β―βπ))C(β―βπ))) |
90 | 80, 81, 89 | 3eqtrd 2777 |
. . . . . 6
β’ (π β ((0 +
((β―βπ) β
1))C((β―βπ)
β 1)) = ((0 + (β―βπ))C(β―βπ))) |
91 | 65, 90 | eqtrd 2773 |
. . . . 5
β’ (π β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = 0)}) = ((0 + (β―βπ))C(β―βπ))) |
92 | 60, 91 | eqtrd 2773 |
. . . 4
β’ (π β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ 0)}) = ((0 + (β―βπ))C(β―βπ))) |
93 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β π:πβΆβ0) |
94 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β Ξ£π β π (πβπ) β€ (π¦ + 1)) |
95 | 35 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π¦ β β0) β§ π:πβΆβ0) β π β Fin) |
96 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π¦ β β0) β§ π:πβΆβ0) β π:πβΆβ0) |
97 | 96 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π¦ β β0) β§ π:πβΆβ0) β§ π β π) β (πβπ) β
β0) |
98 | 95, 97 | fsumnn0cl 15626 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β β0) β§ π:πβΆβ0) β
Ξ£π β π (πβπ) β
β0) |
99 | 93, 98 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β Ξ£π β π (πβπ) β
β0) |
100 | 99 | nn0red 12479 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β Ξ£π β π (πβπ) β β) |
101 | | nn0re 12427 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β β0
β π¦ β
β) |
102 | 101 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β β0) β π¦ β
β) |
103 | 102 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β π¦ β β) |
104 | | 1red 11161 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β 1 β
β) |
105 | 103, 104 | readdcld 11189 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β (π¦ + 1) β β) |
106 | 100, 105 | leloed 11303 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β (Ξ£π β π (πβπ) β€ (π¦ + 1) β (Ξ£π β π (πβπ) < (π¦ + 1) β¨ Ξ£π β π (πβπ) = (π¦ + 1)))) |
107 | 94, 106 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β (Ξ£π β π (πβπ) < (π¦ + 1) β¨ Ξ£π β π (πβπ) = (π¦ + 1))) |
108 | 99 | nn0zd 12530 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β Ξ£π β π (πβπ) β β€) |
109 | | nn0z 12529 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β β0
β π¦ β
β€) |
110 | 109 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β β0) β π¦ β
β€) |
111 | 110 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β π¦ β β€) |
112 | | zleltp1 12559 |
. . . . . . . . . . . . . . . . 17
β’
((Ξ£π β
π (πβπ) β β€ β§ π¦ β β€) β (Ξ£π β π (πβπ) β€ π¦ β Ξ£π β π (πβπ) < (π¦ + 1))) |
113 | 112 | bicomd 222 |
. . . . . . . . . . . . . . . 16
β’
((Ξ£π β
π (πβπ) β β€ β§ π¦ β β€) β (Ξ£π β π (πβπ) < (π¦ + 1) β Ξ£π β π (πβπ) β€ π¦)) |
114 | 108, 111,
113 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β (Ξ£π β π (πβπ) < (π¦ + 1) β Ξ£π β π (πβπ) β€ π¦)) |
115 | 114 | orbi1d 916 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β ((Ξ£π β π (πβπ) < (π¦ + 1) β¨ Ξ£π β π (πβπ) = (π¦ + 1)) β (Ξ£π β π (πβπ) β€ π¦ β¨ Ξ£π β π (πβπ) = (π¦ + 1)))) |
116 | 107, 115 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β (Ξ£π β π (πβπ) β€ π¦ β¨ Ξ£π β π (πβπ) = (π¦ + 1))) |
117 | 93, 116 | jca 513 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β (π:πβΆβ0 β§
(Ξ£π β π (πβπ) β€ π¦ β¨ Ξ£π β π (πβπ) = (π¦ + 1)))) |
118 | | andi 1007 |
. . . . . . . . . . . . 13
β’ ((π:πβΆβ0 β§
(Ξ£π β π (πβπ) β€ π¦ β¨ Ξ£π β π (πβπ) = (π¦ + 1))) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β¨ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))) |
119 | 118 | bicomi 223 |
. . . . . . . . . . . 12
β’ (((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β¨ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β (π:πβΆβ0 β§
(Ξ£π β π (πβπ) β€ π¦ β¨ Ξ£π β π (πβπ) = (π¦ + 1)))) |
120 | 117, 119 | sylibr 233 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β¨ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))) |
121 | 120 | ex 414 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β0) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1)) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β¨ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))))) |
122 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β π:πβΆβ0) |
123 | 122, 98 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Ξ£π β π (πβπ) β
β0) |
124 | 123 | nn0red 12479 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Ξ£π β π (πβπ) β β) |
125 | 102 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β π¦ β β) |
126 | | 1red 11161 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β 1 β β) |
127 | 125, 126 | readdcld 11189 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β (π¦ + 1) β β) |
128 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Ξ£π β π (πβπ) β€ π¦) |
129 | 125 | lep1d 12091 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β π¦ β€ (π¦ + 1)) |
130 | 124, 125,
127, 128, 129 | letrd 11317 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Ξ£π β π (πβπ) β€ (π¦ + 1)) |
131 | 122, 130 | jca 513 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) |
132 | 131 | ex 414 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β0) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1)))) |
133 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β π:πβΆβ0) |
134 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β Ξ£π β π (πβπ) = (π¦ + 1)) |
135 | 102 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β π¦ β β) |
136 | | 1red 11161 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β 1 β
β) |
137 | 135, 136 | readdcld 11189 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β (π¦ + 1) β β) |
138 | 137 | leidd 11726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β (π¦ + 1) β€ (π¦ + 1)) |
139 | 134, 138 | eqbrtrd 5128 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β Ξ£π β π (πβπ) β€ (π¦ + 1)) |
140 | 133, 139 | jca 513 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))) |
141 | 140 | ex 414 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β0) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1)))) |
142 | 132, 141 | jaod 858 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β0) β (((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β¨ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1)))) |
143 | 121, 142 | impbid 211 |
. . . . . . . . 9
β’ ((π β§ π¦ β β0) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1)) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β¨ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))))) |
144 | 143 | abbidv 2802 |
. . . . . . . 8
β’ ((π β§ π¦ β β0) β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))} = {π β£ ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β¨ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))}) |
145 | | unab 4259 |
. . . . . . . . . 10
β’ ({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} βͺ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}) = {π β£ ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β¨ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))} |
146 | 145 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π¦ β β0) β ({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} βͺ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}) = {π β£ ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β¨ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))}) |
147 | 146 | eqcomd 2739 |
. . . . . . . 8
β’ ((π β§ π¦ β β0) β {π β£ ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β¨ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))} = ({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} βͺ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))})) |
148 | 144, 147 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π¦ β β0) β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))} = ({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} βͺ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))})) |
149 | 148 | adantr 482 |
. . . . . 6
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))} = ({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} βͺ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))})) |
150 | 149 | fveq2d 6847 |
. . . . 5
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))}) = (β―β({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} βͺ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}))) |
151 | 35 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β β0) β π β Fin) |
152 | | fzfid 13884 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β β0) β
(0...π¦) β
Fin) |
153 | 151, 152 | jca 513 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β0) β (π β Fin β§ (0...π¦) β Fin)) |
154 | | xpfi 9264 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ (0...π¦) β Fin) β (π Γ (0...π¦)) β Fin) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β0) β (π Γ (0...π¦)) β Fin) |
156 | | pwfi 9125 |
. . . . . . . . . . 11
β’ ((π Γ (0...π¦)) β Fin β π« (π Γ (0...π¦)) β Fin) |
157 | 155, 156 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β0) β π«
(π Γ (0...π¦)) β Fin) |
158 | | fsetsspwxp 8794 |
. . . . . . . . . . 11
β’ {π β£ π:πβΆ(0...π¦)} β π« (π Γ (0...π¦)) |
159 | 158 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β0) β {π β£ π:πβΆ(0...π¦)} β π« (π Γ (0...π¦))) |
160 | 157, 159 | ssfid 9214 |
. . . . . . . . 9
β’ ((π β§ π¦ β β0) β {π β£ π:πβΆ(0...π¦)} β Fin) |
161 | | ffn 6669 |
. . . . . . . . . . . . . 14
β’ (π:πβΆβ0 β π Fn π) |
162 | 122, 161 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β π Fn π) |
163 | | 0zd 12516 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β 0 β β€) |
164 | 110 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β π¦ β β€) |
165 | 164 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β π¦ β β€) |
166 | 122 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β (πβπ ) β
β0) |
167 | 166 | nn0zd 12530 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β (πβπ ) β β€) |
168 | 166 | nn0ge0d 12481 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β 0 β€ (πβπ )) |
169 | 128 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β§ π¦ < (πβπ )) β Ξ£π β π (πβπ) β€ π¦) |
170 | 125 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β§ π¦ < (πβπ )) β π¦ β β) |
171 | 166 | nn0red 12479 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β (πβπ ) β β) |
172 | 171 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β§ π¦ < (πβπ )) β (πβπ ) β β) |
173 | 124 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β Ξ£π β π (πβπ) β β) |
174 | 173 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β§ π¦ < (πβπ )) β Ξ£π β π (πβπ) β β) |
175 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β§ π¦ < (πβπ )) β π¦ < (πβπ )) |
176 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β π) |
177 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β π¦ β β0) |
178 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β π:πβΆβ0) |
179 | 176, 177,
178 | jca31 516 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β ((π β§ π¦ β β0) β§ π:πβΆβ0)) |
180 | | difssd 4093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (π β {π }) β π) |
181 | 35, 180 | ssfid 9214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π β {π }) β Fin) |
182 | 181 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π¦ β β0) β (π β {π }) β Fin) |
183 | 182 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π¦ β β0) β§ π:πβΆβ0) β (π β {π }) β Fin) |
184 | | eldifi 4087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π β {π }) β π β π) |
185 | 184 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π¦ β β0) β§ π:πβΆβ0) β§ π β (π β {π })) β π β π) |
186 | 97 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ π¦ β β0)
β§ π:πβΆβ0) β§ π β (π β {π })) β§ π β π) β (πβπ) β
β0) |
187 | 185, 186 | mpdan 686 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π¦ β β0) β§ π:πβΆβ0) β§ π β (π β {π })) β (πβπ) β
β0) |
188 | 183, 187 | fsumnn0cl 15626 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π¦ β β0) β§ π:πβΆβ0) β
Ξ£π β (π β {π })(πβπ) β
β0) |
189 | 179, 188 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β Ξ£π β (π β {π })(πβπ) β
β0) |
190 | 189 | nn0ge0d 12481 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β 0 β€ Ξ£π β (π β {π })(πβπ)) |
191 | | difssd 4093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π¦ β β0) β§ π:πβΆβ0) β (π β {π }) β π) |
192 | 95, 191 | ssfid 9214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π¦ β β0) β§ π:πβΆβ0) β (π β {π }) β Fin) |
193 | 192, 187 | fsumnn0cl 15626 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π¦ β β0) β§ π:πβΆβ0) β
Ξ£π β (π β {π })(πβπ) β
β0) |
194 | 179, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β Ξ£π β (π β {π })(πβπ) β
β0) |
195 | 194 | nn0red 12479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β Ξ£π β (π β {π })(πβπ) β β) |
196 | 171, 195 | addge01d 11748 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β (0 β€ Ξ£π β (π β {π })(πβπ) β (πβπ ) β€ ((πβπ ) + Ξ£π β (π β {π })(πβπ)))) |
197 | 190, 196 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β (πβπ ) β€ ((πβπ ) + Ξ£π β (π β {π })(πβπ))) |
198 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β π β π) |
199 | 179, 198 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β (((π β§ π¦ β β0) β§ π:πβΆβ0) β§ π β π)) |
200 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π(((π β§ π¦ β β0) β§ π:πβΆβ0) β§ π β π) |
201 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π(πβπ ) |
202 | 95 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π¦ β β0) β§ π:πβΆβ0) β§ π β π) β π β Fin) |
203 | 97 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π¦ β β0)
β§ π:πβΆβ0) β§ π β π) β§ π β π) β (πβπ) β
β0) |
204 | 203 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π¦ β β0)
β§ π:πβΆβ0) β§ π β π) β§ π β π) β (πβπ) β β) |
205 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π¦ β β0) β§ π:πβΆβ0) β§ π β π) β π β π) |
206 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β (πβπ) = (πβπ )) |
207 | 200, 201,
202, 204, 205, 206 | fsumsplit1 15635 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π¦ β β0) β§ π:πβΆβ0) β§ π β π) β Ξ£π β π (πβπ) = ((πβπ ) + Ξ£π β (π β {π })(πβπ))) |
208 | 199, 207 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β Ξ£π β π (πβπ) = ((πβπ ) + Ξ£π β (π β {π })(πβπ))) |
209 | 208 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β ((πβπ ) + Ξ£π β (π β {π })(πβπ)) = Ξ£π β π (πβπ)) |
210 | 197, 209 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β (πβπ ) β€ Ξ£π β π (πβπ)) |
211 | 210 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β§ π¦ < (πβπ )) β (πβπ ) β€ Ξ£π β π (πβπ)) |
212 | 170, 172,
174, 175, 211 | ltletrd 11320 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β§ π¦ < (πβπ )) β π¦ < Ξ£π β π (πβπ)) |
213 | 170, 174 | ltnled 11307 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β§ π¦ < (πβπ )) β (π¦ < Ξ£π β π (πβπ) β Β¬ Ξ£π β π (πβπ) β€ π¦)) |
214 | 212, 213 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β§ π¦ < (πβπ )) β Β¬ Ξ£π β π (πβπ) β€ π¦) |
215 | 169, 214 | pm2.21dd 194 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β§ π¦ < (πβπ )) β Β¬ π¦ < (πβπ )) |
216 | 215 | pm2.01da 798 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β Β¬ π¦ < (πβπ )) |
217 | 177, 101 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β π¦ β β) |
218 | 171, 217 | lenltd 11306 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β ((πβπ ) β€ π¦ β Β¬ π¦ < (πβπ ))) |
219 | 216, 218 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β (πβπ ) β€ π¦) |
220 | 163, 165,
167, 168, 219 | elfzd 13438 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β§ π β π) β (πβπ ) β (0...π¦)) |
221 | 220 | ralrimiva 3140 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β βπ β π (πβπ ) β (0...π¦)) |
222 | 162, 221 | jca 513 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β (π Fn π β§ βπ β π (πβπ ) β (0...π¦))) |
223 | | ffnfv 7067 |
. . . . . . . . . . . 12
β’ (π:πβΆ(0...π¦) β (π Fn π β§ βπ β π (πβπ ) β (0...π¦))) |
224 | 222, 223 | sylibr 233 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β π:πβΆ(0...π¦)) |
225 | 224 | ex 414 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β0) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β π:πβΆ(0...π¦))) |
226 | 225 | ss2abdv 4021 |
. . . . . . . . 9
β’ ((π β§ π¦ β β0) β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} β {π β£ π:πβΆ(0...π¦)}) |
227 | 160, 226 | ssfid 9214 |
. . . . . . . 8
β’ ((π β§ π¦ β β0) β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} β Fin) |
228 | 227 | adantr 482 |
. . . . . . 7
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} β Fin) |
229 | | fzfid 13884 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β β0) β
(0...(π¦ + 1)) β
Fin) |
230 | 151, 229 | jca 513 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β0) β (π β Fin β§ (0...(π¦ + 1)) β
Fin)) |
231 | | xpfi 9264 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ (0...(π¦ + 1)) β Fin) β (π Γ (0...(π¦ + 1))) β
Fin) |
232 | 230, 231 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β0) β (π Γ (0...(π¦ + 1))) β
Fin) |
233 | | pwfi 9125 |
. . . . . . . . . . 11
β’ ((π Γ (0...(π¦ + 1))) β Fin β
π« (π Γ
(0...(π¦ + 1))) β
Fin) |
234 | 232, 233 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β0) β π«
(π Γ (0...(π¦ + 1))) β
Fin) |
235 | | fsetsspwxp 8794 |
. . . . . . . . . . 11
β’ {π β£ π:πβΆ(0...(π¦ + 1))} β π« (π Γ (0...(π¦ + 1))) |
236 | 235 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β0) β {π β£ π:πβΆ(0...(π¦ + 1))} β π« (π Γ (0...(π¦ + 1)))) |
237 | 234, 236 | ssfid 9214 |
. . . . . . . . 9
β’ ((π β§ π¦ β β0) β {π β£ π:πβΆ(0...(π¦ + 1))} β Fin) |
238 | 161 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β π Fn π) |
239 | | 0zd 12516 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β 0 β β€) |
240 | | simpllr 775 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β π¦ β β0) |
241 | 240 | nn0zd 12530 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β π¦ β β€) |
242 | 241 | peano2zd 12615 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β (π¦ + 1) β β€) |
243 | 133 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β (πβπ ) β
β0) |
244 | 243 | nn0zd 12530 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β (πβπ ) β β€) |
245 | 243 | nn0ge0d 12481 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β 0 β€ (πβπ )) |
246 | 134 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β Ξ£π β π (πβπ) = (π¦ + 1)) |
247 | 137 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β (π¦ + 1) β β) |
248 | 133 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β π:πβΆβ0) |
249 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β π β π) |
250 | 248, 249 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β (πβπ ) β
β0) |
251 | 250 | nn0red 12479 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β (πβπ ) β β) |
252 | 246, 247 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β Ξ£π β π (πβπ) β β) |
253 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β (π¦ + 1) < (πβπ )) |
254 | 133, 188 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β Ξ£π β (π β {π })(πβπ) β
β0) |
255 | 254 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β Ξ£π β (π β {π })(πβπ) β
β0) |
256 | 255 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β Ξ£π β (π β {π })(πβπ) β
β0) |
257 | 256 | nn0ge0d 12481 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β 0 β€ Ξ£π β (π β {π })(πβπ)) |
258 | 256 | nn0red 12479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β Ξ£π β (π β {π })(πβπ) β β) |
259 | 251, 258 | addge01d 11748 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β (0 β€ Ξ£π β (π β {π })(πβπ) β (πβπ ) β€ ((πβπ ) + Ξ£π β (π β {π })(πβπ)))) |
260 | 257, 259 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β (πβπ ) β€ ((πβπ ) + Ξ£π β (π β {π })(πβπ))) |
261 | 133, 207 | syldanl 603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β Ξ£π β π (πβπ) = ((πβπ ) + Ξ£π β (π β {π })(πβπ))) |
262 | 261 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β Ξ£π β π (πβπ) = ((πβπ ) + Ξ£π β (π β {π })(πβπ))) |
263 | 262 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β ((πβπ ) + Ξ£π β (π β {π })(πβπ)) = Ξ£π β π (πβπ)) |
264 | 260, 263 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β (πβπ ) β€ Ξ£π β π (πβπ)) |
265 | 247, 251,
252, 253, 264 | ltletrd 11320 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β (π¦ + 1) < Ξ£π β π (πβπ)) |
266 | 247, 265 | ltned 11296 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β (π¦ + 1) β Ξ£π β π (πβπ)) |
267 | 266 | necomd 2996 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β Ξ£π β π (πβπ) β (π¦ + 1)) |
268 | 246, 267 | pm2.21ddne 3026 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π¦ β β0)
β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β§ (π¦ + 1) < (πβπ )) β Β¬ (π¦ + 1) < (πβπ )) |
269 | 268 | pm2.01da 798 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β Β¬ (π¦ + 1) < (πβπ )) |
270 | 243 | nn0red 12479 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β (πβπ ) β β) |
271 | 137 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β (π¦ + 1) β β) |
272 | 270, 271 | lenltd 11306 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β ((πβπ ) β€ (π¦ + 1) β Β¬ (π¦ + 1) < (πβπ ))) |
273 | 269, 272 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β (πβπ ) β€ (π¦ + 1)) |
274 | 239, 242,
244, 245, 273 | elfzd 13438 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β§ π β π) β (πβπ ) β (0...(π¦ + 1))) |
275 | 274 | ralrimiva 3140 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β βπ β π (πβπ ) β (0...(π¦ + 1))) |
276 | 238, 275 | jca 513 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β (π Fn π β§ βπ β π (πβπ ) β (0...(π¦ + 1)))) |
277 | | ffnfv 7067 |
. . . . . . . . . . . 12
β’ (π:πβΆ(0...(π¦ + 1)) β (π Fn π β§ βπ β π (πβπ ) β (0...(π¦ + 1)))) |
278 | 276, 277 | sylibr 233 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) β π:πβΆ(0...(π¦ + 1))) |
279 | 278 | ex 414 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β0) β ((π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)) β π:πβΆ(0...(π¦ + 1)))) |
280 | 279 | ss2abdv 4021 |
. . . . . . . . 9
β’ ((π β§ π¦ β β0) β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))} β {π β£ π:πβΆ(0...(π¦ + 1))}) |
281 | 237, 280 | ssfid 9214 |
. . . . . . . 8
β’ ((π β§ π¦ β β0) β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))} β Fin) |
282 | 281 | adantr 482 |
. . . . . . 7
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))} β Fin) |
283 | | inab 4260 |
. . . . . . . . . 10
β’ ({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} β© {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}) = {π β£ ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))} |
284 | 283 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π¦ β β0) β ({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} β© {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}) = {π β£ ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))}) |
285 | 98 | adantrr 716 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Ξ£π β π (πβπ) β
β0) |
286 | 285 | nn0zd 12530 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Ξ£π β π (πβπ) β β€) |
287 | 286 | zred 12612 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Ξ£π β π (πβπ) β β) |
288 | 125 | ltp1d 12090 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β π¦ < (π¦ + 1)) |
289 | 287, 125,
127, 128, 288 | lelttrd 11318 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Ξ£π β π (πβπ) < (π¦ + 1)) |
290 | 287, 289 | ltned 11296 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Ξ£π β π (πβπ) β (π¦ + 1)) |
291 | 290 | neneqd 2945 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Β¬ Ξ£π β π (πβπ) = (π¦ + 1)) |
292 | 291 | intnand 490 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Β¬ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))) |
293 | | nan 829 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β0) β Β¬
((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))) β (((π β§ π¦ β β0) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)) β Β¬ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))) |
294 | 292, 293 | mpbir 230 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β0) β Β¬
((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))) |
295 | 294 | alrimiv 1931 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β0) β
βπ Β¬ ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))) |
296 | | ab0 4335 |
. . . . . . . . . 10
β’ ({π β£ ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))} = β
β βπ Β¬ ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))) |
297 | 295, 296 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ π¦ β β0) β {π β£ ((π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦) β§ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1)))} = β
) |
298 | 284, 297 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π¦ β β0) β ({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} β© {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}) = β
) |
299 | 298 | adantr 482 |
. . . . . . 7
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β ({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} β© {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}) = β
) |
300 | | hashun 14288 |
. . . . . . 7
β’ (({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} β Fin β§ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))} β Fin β§ ({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} β© {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}) = β
) β
(β―β({π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} βͺ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))})) = ((β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) + (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}))) |
301 | 228, 282,
299, 300 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (β―β({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} βͺ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))})) = ((β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) + (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}))) |
302 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) |
303 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β π¦ β β0) |
304 | | 1nn0 12434 |
. . . . . . . . . . 11
β’ 1 β
β0 |
305 | 304 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β 1 β
β0) |
306 | 303, 305 | nn0addcld 12482 |
. . . . . . . . 9
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (π¦ + 1) β
β0) |
307 | 35 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β π β Fin) |
308 | 63 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β π β β
) |
309 | | eqid 2733 |
. . . . . . . . 9
β’ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))} = {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))} |
310 | 306, 307,
308, 309 | sticksstones21 40621 |
. . . . . . . 8
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))}) = (((π¦ + 1) + ((β―βπ) β 1))C((β―βπ) β 1))) |
311 | 302, 310 | oveq12d 7376 |
. . . . . . 7
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β ((β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) + (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))})) = (((π¦ + (β―βπ))C(β―βπ)) + (((π¦ + 1) + ((β―βπ) β 1))C((β―βπ) β 1)))) |
312 | 303 | nn0cnd 12480 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β π¦ β β) |
313 | | 1cnd 11155 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β 1 β
β) |
314 | 71 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (β―βπ) β β) |
315 | 312, 313,
314 | ppncand 11557 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β ((π¦ + 1) + ((β―βπ) β 1)) = (π¦ + (β―βπ))) |
316 | 315 | oveq1d 7373 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (((π¦ + 1) + ((β―βπ) β 1))C((β―βπ) β 1)) = ((π¦ + (β―βπ))C((β―βπ) β 1))) |
317 | 316 | oveq2d 7374 |
. . . . . . . . 9
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (((π¦ + (β―βπ))C(β―βπ)) + (((π¦ + 1) + ((β―βπ) β 1))C((β―βπ) β 1))) = (((π¦ + (β―βπ))C(β―βπ)) + ((π¦ + (β―βπ))C((β―βπ) β 1)))) |
318 | 82 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (β―βπ) β
β0) |
319 | 303, 318 | nn0addcld 12482 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (π¦ + (β―βπ)) β
β0) |
320 | 318 | nn0zd 12530 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (β―βπ) β β€) |
321 | | bcpasc 14227 |
. . . . . . . . . 10
β’ (((π¦ + (β―βπ)) β β0
β§ (β―βπ)
β β€) β (((π¦
+ (β―βπ))C(β―βπ)) + ((π¦ + (β―βπ))C((β―βπ) β 1))) = (((π¦ + (β―βπ)) + 1)C(β―βπ))) |
322 | 319, 320,
321 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (((π¦ + (β―βπ))C(β―βπ)) + ((π¦ + (β―βπ))C((β―βπ) β 1))) = (((π¦ + (β―βπ)) + 1)C(β―βπ))) |
323 | 317, 322 | eqtrd 2773 |
. . . . . . . 8
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (((π¦ + (β―βπ))C(β―βπ)) + (((π¦ + 1) + ((β―βπ) β 1))C((β―βπ) β 1))) = (((π¦ + (β―βπ)) + 1)C(β―βπ))) |
324 | 312, 314,
313 | add32d 11387 |
. . . . . . . . 9
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β ((π¦ + (β―βπ)) + 1) = ((π¦ + 1) + (β―βπ))) |
325 | 324 | oveq1d 7373 |
. . . . . . . 8
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (((π¦ + (β―βπ)) + 1)C(β―βπ)) = (((π¦ + 1) + (β―βπ))C(β―βπ))) |
326 | 323, 325 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (((π¦ + (β―βπ))C(β―βπ)) + (((π¦ + 1) + ((β―βπ) β 1))C((β―βπ) β 1))) = (((π¦ + 1) + (β―βπ))C(β―βπ))) |
327 | 311, 326 | eqtrd 2773 |
. . . . . 6
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β ((β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) + (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))})) = (((π¦ + 1) + (β―βπ))C(β―βπ))) |
328 | 301, 327 | eqtrd 2773 |
. . . . 5
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (β―β({π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)} βͺ {π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) = (π¦ + 1))})) = (((π¦ + 1) + (β―βπ))C(β―βπ))) |
329 | 150, 328 | eqtrd 2773 |
. . . 4
β’ (((π β§ π¦ β β0) β§
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π¦)}) = ((π¦ + (β―βπ))C(β―βπ))) β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ (π¦ + 1))}) = (((π¦ + 1) + (β―βπ))C(β―βπ))) |
330 | 11, 18, 25, 32, 92, 329 | nn0indd 12605 |
. . 3
β’ ((π β§ π β β0) β
(β―β{π β£
(π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π)}) = ((π + (β―βπ))C(β―βπ))) |
331 | 4, 330 | mpdan 686 |
. 2
β’ (π β (β―β{π β£ (π:πβΆβ0 β§
Ξ£π β π (πβπ) β€ π)}) = ((π + (β―βπ))C(β―βπ))) |
332 | 3, 331 | eqtrd 2773 |
1
β’ (π β (β―βπ΄) = ((π + (β―βπ))C(β―βπ))) |