Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ ((π β§ πΌ β (1...π)) β π) |
2 | | stoweidlem15.3 |
. . . . . 6
β’ (π β πΊ:(1...π)βΆπ) |
3 | 2 | ffvelcdmda 7039 |
. . . . 5
β’ ((π β§ πΌ β (1...π)) β (πΊβπΌ) β π) |
4 | | elrabi 3643 |
. . . . . 6
β’ ((πΊβπΌ) β {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} β (πΊβπΌ) β π΄) |
5 | | stoweidlem15.1 |
. . . . . 6
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
6 | 4, 5 | eleq2s 2852 |
. . . . 5
β’ ((πΊβπΌ) β π β (πΊβπΌ) β π΄) |
7 | 3, 6 | syl 17 |
. . . 4
β’ ((π β§ πΌ β (1...π)) β (πΊβπΌ) β π΄) |
8 | | eleq1 2822 |
. . . . . . . 8
β’ (π = (πΊβπΌ) β (π β π΄ β (πΊβπΌ) β π΄)) |
9 | 8 | anbi2d 630 |
. . . . . . 7
β’ (π = (πΊβπΌ) β ((π β§ π β π΄) β (π β§ (πΊβπΌ) β π΄))) |
10 | | feq1 6653 |
. . . . . . 7
β’ (π = (πΊβπΌ) β (π:πβΆβ β (πΊβπΌ):πβΆβ)) |
11 | 9, 10 | imbi12d 345 |
. . . . . 6
β’ (π = (πΊβπΌ) β (((π β§ π β π΄) β π:πβΆβ) β ((π β§ (πΊβπΌ) β π΄) β (πΊβπΌ):πβΆβ))) |
12 | | stoweidlem15.4 |
. . . . . 6
β’ ((π β§ π β π΄) β π:πβΆβ) |
13 | 11, 12 | vtoclg 3527 |
. . . . 5
β’ ((πΊβπΌ) β π΄ β ((π β§ (πΊβπΌ) β π΄) β (πΊβπΌ):πβΆβ)) |
14 | 7, 13 | syl 17 |
. . . 4
β’ ((π β§ πΌ β (1...π)) β ((π β§ (πΊβπΌ) β π΄) β (πΊβπΌ):πβΆβ)) |
15 | 1, 7, 14 | mp2and 698 |
. . 3
β’ ((π β§ πΌ β (1...π)) β (πΊβπΌ):πβΆβ) |
16 | 15 | ffvelcdmda 7039 |
. 2
β’ (((π β§ πΌ β (1...π)) β§ π β π) β ((πΊβπΌ)βπ) β β) |
17 | 3, 5 | eleqtrdi 2844 |
. . . . . . 7
β’ ((π β§ πΌ β (1...π)) β (πΊβπΌ) β {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))}) |
18 | | fveq1 6845 |
. . . . . . . . . 10
β’ (β = (πΊβπΌ) β (ββπ) = ((πΊβπΌ)βπ)) |
19 | 18 | eqeq1d 2735 |
. . . . . . . . 9
β’ (β = (πΊβπΌ) β ((ββπ) = 0 β ((πΊβπΌ)βπ) = 0)) |
20 | | fveq1 6845 |
. . . . . . . . . . . 12
β’ (β = (πΊβπΌ) β (ββπ‘) = ((πΊβπΌ)βπ‘)) |
21 | 20 | breq2d 5121 |
. . . . . . . . . . 11
β’ (β = (πΊβπΌ) β (0 β€ (ββπ‘) β 0 β€ ((πΊβπΌ)βπ‘))) |
22 | 20 | breq1d 5119 |
. . . . . . . . . . 11
β’ (β = (πΊβπΌ) β ((ββπ‘) β€ 1 β ((πΊβπΌ)βπ‘) β€ 1)) |
23 | 21, 22 | anbi12d 632 |
. . . . . . . . . 10
β’ (β = (πΊβπΌ) β ((0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1))) |
24 | 23 | ralbidv 3171 |
. . . . . . . . 9
β’ (β = (πΊβπΌ) β (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1))) |
25 | 19, 24 | anbi12d 632 |
. . . . . . . 8
β’ (β = (πΊβπΌ) β (((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)) β (((πΊβπΌ)βπ) = 0 β§ βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1)))) |
26 | 25 | elrab 3649 |
. . . . . . 7
β’ ((πΊβπΌ) β {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} β ((πΊβπΌ) β π΄ β§ (((πΊβπΌ)βπ) = 0 β§ βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1)))) |
27 | 17, 26 | sylib 217 |
. . . . . 6
β’ ((π β§ πΌ β (1...π)) β ((πΊβπΌ) β π΄ β§ (((πΊβπΌ)βπ) = 0 β§ βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1)))) |
28 | 27 | simprd 497 |
. . . . 5
β’ ((π β§ πΌ β (1...π)) β (((πΊβπΌ)βπ) = 0 β§ βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1))) |
29 | 28 | simprd 497 |
. . . 4
β’ ((π β§ πΌ β (1...π)) β βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1)) |
30 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π‘ β ((πΊβπΌ)βπ ) = ((πΊβπΌ)βπ‘)) |
31 | 30 | breq2d 5121 |
. . . . . . 7
β’ (π = π‘ β (0 β€ ((πΊβπΌ)βπ ) β 0 β€ ((πΊβπΌ)βπ‘))) |
32 | 30 | breq1d 5119 |
. . . . . . 7
β’ (π = π‘ β (((πΊβπΌ)βπ ) β€ 1 β ((πΊβπΌ)βπ‘) β€ 1)) |
33 | 31, 32 | anbi12d 632 |
. . . . . 6
β’ (π = π‘ β ((0 β€ ((πΊβπΌ)βπ ) β§ ((πΊβπΌ)βπ ) β€ 1) β (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1))) |
34 | 33 | cbvralvw 3224 |
. . . . 5
β’
(βπ β
π (0 β€ ((πΊβπΌ)βπ ) β§ ((πΊβπΌ)βπ ) β€ 1) β βπ‘ β π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1)) |
35 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β ((πΊβπΌ)βπ ) = ((πΊβπΌ)βπ)) |
36 | 35 | breq2d 5121 |
. . . . . . 7
β’ (π = π β (0 β€ ((πΊβπΌ)βπ ) β 0 β€ ((πΊβπΌ)βπ))) |
37 | 35 | breq1d 5119 |
. . . . . . 7
β’ (π = π β (((πΊβπΌ)βπ ) β€ 1 β ((πΊβπΌ)βπ) β€ 1)) |
38 | 36, 37 | anbi12d 632 |
. . . . . 6
β’ (π = π β ((0 β€ ((πΊβπΌ)βπ ) β§ ((πΊβπΌ)βπ ) β€ 1) β (0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1))) |
39 | 38 | rspccva 3582 |
. . . . 5
β’
((βπ β
π (0 β€ ((πΊβπΌ)βπ ) β§ ((πΊβπΌ)βπ ) β€ 1) β§ π β π) β (0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1)) |
40 | 34, 39 | sylanbr 583 |
. . . 4
β’
((βπ‘ β
π (0 β€ ((πΊβπΌ)βπ‘) β§ ((πΊβπΌ)βπ‘) β€ 1) β§ π β π) β (0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1)) |
41 | 29, 40 | sylan 581 |
. . 3
β’ (((π β§ πΌ β (1...π)) β§ π β π) β (0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1)) |
42 | 41 | simpld 496 |
. 2
β’ (((π β§ πΌ β (1...π)) β§ π β π) β 0 β€ ((πΊβπΌ)βπ)) |
43 | 41 | simprd 497 |
. 2
β’ (((π β§ πΌ β (1...π)) β§ π β π) β ((πΊβπΌ)βπ) β€ 1) |
44 | 16, 42, 43 | 3jca 1129 |
1
β’ (((π β§ πΌ β (1...π)) β§ π β π) β (((πΊβπΌ)βπ) β β β§ 0 β€ ((πΊβπΌ)βπ) β§ ((πΊβπΌ)βπ) β€ 1)) |