Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’
(β€β₯βπ) = (β€β₯βπ) |
2 | | eluzelz 12778 |
. . . 4
β’ (π β
(β€β₯βπ) β π β β€) |
3 | | iseralt.1 |
. . . 4
β’ π =
(β€β₯βπ) |
4 | 2, 3 | eleq2s 2852 |
. . 3
β’ (π β π β π β β€) |
5 | 4 | adantl 483 |
. 2
β’ ((π β§ π β π) β π β β€) |
6 | | iseralt.5 |
. . 3
β’ (π β πΊ β 0) |
7 | 6 | adantr 482 |
. 2
β’ ((π β§ π β π) β πΊ β 0) |
8 | | iseralt.3 |
. . . . 5
β’ (π β πΊ:πβΆβ) |
9 | 8 | ffvelcdmda 7036 |
. . . 4
β’ ((π β§ π β π) β (πΊβπ) β β) |
10 | 9 | recnd 11188 |
. . 3
β’ ((π β§ π β π) β (πΊβπ) β β) |
11 | | 1z 12538 |
. . 3
β’ 1 β
β€ |
12 | | uzssz 12789 |
. . . 4
β’
(β€β₯β1) β β€ |
13 | | zex 12513 |
. . . 4
β’ β€
β V |
14 | 12, 13 | climconst2 15436 |
. . 3
β’ (((πΊβπ) β β β§ 1 β β€)
β (β€ Γ {(πΊβπ)}) β (πΊβπ)) |
15 | 10, 11, 14 | sylancl 587 |
. 2
β’ ((π β§ π β π) β (β€ Γ {(πΊβπ)}) β (πΊβπ)) |
16 | 8 | ad2antrr 725 |
. . 3
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β πΊ:πβΆβ) |
17 | 3 | uztrn2 12787 |
. . . 4
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
18 | 17 | adantll 713 |
. . 3
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
19 | 16, 18 | ffvelcdmd 7037 |
. 2
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΊβπ) β β) |
20 | | eluzelz 12778 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β β€) |
21 | 20 | adantl 483 |
. . . 4
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β β€) |
22 | | fvex 6856 |
. . . . 5
β’ (πΊβπ) β V |
23 | 22 | fvconst2 7154 |
. . . 4
β’ (π β β€ β ((β€
Γ {(πΊβπ)})βπ) = (πΊβπ)) |
24 | 21, 23 | syl 17 |
. . 3
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β ((β€ Γ
{(πΊβπ)})βπ) = (πΊβπ)) |
25 | 9 | adantr 482 |
. . 3
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΊβπ) β β) |
26 | 24, 25 | eqeltrd 2834 |
. 2
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β ((β€ Γ
{(πΊβπ)})βπ) β β) |
27 | | simpr 486 |
. . . 4
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
28 | 16 | adantr 482 |
. . . . 5
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ π β (π...π)) β πΊ:πβΆβ) |
29 | | simplr 768 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
30 | | elfzuz 13443 |
. . . . . 6
β’ (π β (π...π) β π β (β€β₯βπ)) |
31 | 3 | uztrn2 12787 |
. . . . . 6
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
32 | 29, 30, 31 | syl2an 597 |
. . . . 5
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ π β (π...π)) β π β π) |
33 | 28, 32 | ffvelcdmd 7037 |
. . . 4
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ π β (π...π)) β (πΊβπ) β β) |
34 | | simpl 484 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (π β§ π β π)) |
35 | | elfzuz 13443 |
. . . . 5
β’ (π β (π...(π β 1)) β π β (β€β₯βπ)) |
36 | 31 | adantll 713 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
37 | | iseralt.4 |
. . . . . . 7
β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) |
38 | 37 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β π) β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) |
39 | 36, 38 | syldan 592 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΊβ(π + 1)) β€ (πΊβπ)) |
40 | 34, 35, 39 | syl2an 597 |
. . . 4
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ π β (π...(π β 1))) β (πΊβ(π + 1)) β€ (πΊβπ)) |
41 | 27, 33, 40 | monoord2 13945 |
. . 3
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΊβπ) β€ (πΊβπ)) |
42 | 41, 24 | breqtrrd 5134 |
. 2
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΊβπ) β€ ((β€ Γ {(πΊβπ)})βπ)) |
43 | 1, 5, 7, 15, 19, 26, 42 | climle 15528 |
1
β’ ((π β§ π β π) β 0 β€ (πΊβπ)) |