Step | Hyp | Ref
| Expression |
1 | | ulmshft.z |
. . . . . 6
β’ π =
(β€β₯βπ) |
2 | | ulmshft.m |
. . . . . . 7
β’ (π β π β β€) |
3 | 2 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β π β
β€) |
4 | | ulmshft.f |
. . . . . . 7
β’ (π β πΉ:πβΆ(β βm π)) |
5 | 4 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β πΉ:πβΆ(β βm π)) |
6 | | eqidd 2738 |
. . . . . 6
β’ ((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
7 | | eqidd 2738 |
. . . . . 6
β’ ((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π§ β π) β (πΊβπ§) = (πΊβπ§)) |
8 | | simplr 768 |
. . . . . 6
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β πΉ(βπ’βπ)πΊ) |
9 | | simpr 486 |
. . . . . 6
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β π₯ β
β+) |
10 | 1, 3, 5, 6, 7, 8, 9 | ulmi 25761 |
. . . . 5
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) |
11 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β π β π) |
12 | 11, 1 | eleqtrdi 2848 |
. . . . . . . . 9
β’ ((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β π β (β€β₯βπ)) |
13 | | ulmshft.k |
. . . . . . . . . 10
β’ (π β πΎ β β€) |
14 | 13 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β πΎ β β€) |
15 | | eluzadd 12799 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ πΎ β β€) β (π + πΎ) β
(β€β₯β(π + πΎ))) |
16 | 12, 14, 15 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β (π + πΎ) β
(β€β₯β(π + πΎ))) |
17 | | ulmshft.w |
. . . . . . . 8
β’ π =
(β€β₯β(π + πΎ)) |
18 | 16, 17 | eleqtrrdi 2849 |
. . . . . . 7
β’ ((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β (π + πΎ) β π) |
19 | | eluzelz 12780 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β π β β€) |
20 | 12, 19 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β π β β€) |
21 | 20 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯β(π + πΎ))) β π β β€) |
22 | 13 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ πΉ(βπ’βπ)πΊ) β πΎ β β€) |
23 | 22 | ad3antrrr 729 |
. . . . . . . . . 10
β’
(((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯β(π + πΎ))) β πΎ β β€) |
24 | | simpr 486 |
. . . . . . . . . 10
β’
(((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯β(π + πΎ))) β π β (β€β₯β(π + πΎ))) |
25 | | eluzsub 12800 |
. . . . . . . . . 10
β’ ((π β β€ β§ πΎ β β€ β§ π β
(β€β₯β(π + πΎ))) β (π β πΎ) β (β€β₯βπ)) |
26 | 21, 23, 24, 25 | syl3anc 1372 |
. . . . . . . . 9
β’
(((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯β(π + πΎ))) β (π β πΎ) β (β€β₯βπ)) |
27 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = (π β πΎ) β (πΉβπ) = (πΉβ(π β πΎ))) |
28 | 27 | fveq1d 6849 |
. . . . . . . . . . . . 13
β’ (π = (π β πΎ) β ((πΉβπ)βπ§) = ((πΉβ(π β πΎ))βπ§)) |
29 | 28 | fvoveq1d 7384 |
. . . . . . . . . . . 12
β’ (π = (π β πΎ) β (absβ(((πΉβπ)βπ§) β (πΊβπ§))) = (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§)))) |
30 | 29 | breq1d 5120 |
. . . . . . . . . . 11
β’ (π = (π β πΎ) β ((absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯)) |
31 | 30 | ralbidv 3175 |
. . . . . . . . . 10
β’ (π = (π β πΎ) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯)) |
32 | 31 | rspcv 3580 |
. . . . . . . . 9
β’ ((π β πΎ) β (β€β₯βπ) β (βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯)) |
33 | 26, 32 | syl 17 |
. . . . . . . 8
β’
(((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯β(π + πΎ))) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯)) |
34 | 33 | ralrimdva 3152 |
. . . . . . 7
β’ ((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ β (β€β₯β(π + πΎ))βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯)) |
35 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = (π + πΎ) β (β€β₯βπ) =
(β€β₯β(π + πΎ))) |
36 | 35 | raleqdv 3316 |
. . . . . . . 8
β’ (π = (π + πΎ) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯ β βπ β (β€β₯β(π + πΎ))βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯)) |
37 | 36 | rspcev 3584 |
. . . . . . 7
β’ (((π + πΎ) β π β§ βπ β (β€β₯β(π + πΎ))βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯) β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯) |
38 | 18, 34, 37 | syl6an 683 |
. . . . . 6
β’ ((((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯)) |
39 | 38 | rexlimdva 3153 |
. . . . 5
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β
(βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯)) |
40 | 10, 39 | mpd 15 |
. . . 4
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ π₯ β β+) β
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯) |
41 | 40 | ralrimiva 3144 |
. . 3
β’ ((π β§ πΉ(βπ’βπ)πΊ) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯) |
42 | 2, 13 | zaddcld 12618 |
. . . . 5
β’ (π β (π + πΎ) β β€) |
43 | 42 | adantr 482 |
. . . 4
β’ ((π β§ πΉ(βπ’βπ)πΊ) β (π + πΎ) β β€) |
44 | | ulmshft.h |
. . . . . 6
β’ (π β π» = (π β π β¦ (πΉβ(π β πΎ)))) |
45 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β πΉ:πβΆ(β βm π)) |
46 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β β€) |
47 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π) β πΎ β β€) |
48 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
49 | 48, 17 | eleqtrdi 2848 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β (β€β₯β(π + πΎ))) |
50 | | eluzsub 12800 |
. . . . . . . . 9
β’ ((π β β€ β§ πΎ β β€ β§ π β
(β€β₯β(π + πΎ))) β (π β πΎ) β (β€β₯βπ)) |
51 | 46, 47, 49, 50 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β π) β (π β πΎ) β (β€β₯βπ)) |
52 | 51, 1 | eleqtrrdi 2849 |
. . . . . . 7
β’ ((π β§ π β π) β (π β πΎ) β π) |
53 | 45, 52 | ffvelcdmd 7041 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβ(π β πΎ)) β (β βm π)) |
54 | 44, 53 | fmpt3d 7069 |
. . . . 5
β’ (π β π»:πβΆ(β βm π)) |
55 | 54 | adantr 482 |
. . . 4
β’ ((π β§ πΉ(βπ’βπ)πΊ) β π»:πβΆ(β βm π)) |
56 | 44 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ (π β π β§ π§ β π)) β π» = (π β π β¦ (πΉβ(π β πΎ)))) |
57 | 56 | fveq1d 6849 |
. . . . . 6
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ (π β π β§ π§ β π)) β (π»βπ) = ((π β π β¦ (πΉβ(π β πΎ)))βπ)) |
58 | | fvoveq1 7385 |
. . . . . . . 8
β’ (π = π β (πΉβ(π β πΎ)) = (πΉβ(π β πΎ))) |
59 | | eqid 2737 |
. . . . . . . 8
β’ (π β π β¦ (πΉβ(π β πΎ))) = (π β π β¦ (πΉβ(π β πΎ))) |
60 | | fvex 6860 |
. . . . . . . 8
β’ (πΉβ(π β πΎ)) β V |
61 | 58, 59, 60 | fvmpt 6953 |
. . . . . . 7
β’ (π β π β ((π β π β¦ (πΉβ(π β πΎ)))βπ) = (πΉβ(π β πΎ))) |
62 | 61 | ad2antrl 727 |
. . . . . 6
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ (π β π β§ π§ β π)) β ((π β π β¦ (πΉβ(π β πΎ)))βπ) = (πΉβ(π β πΎ))) |
63 | 57, 62 | eqtrd 2777 |
. . . . 5
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ (π β π β§ π§ β π)) β (π»βπ) = (πΉβ(π β πΎ))) |
64 | 63 | fveq1d 6849 |
. . . 4
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ (π β π β§ π§ β π)) β ((π»βπ)βπ§) = ((πΉβ(π β πΎ))βπ§)) |
65 | | eqidd 2738 |
. . . 4
β’ (((π β§ πΉ(βπ’βπ)πΊ) β§ π§ β π) β (πΊβπ§) = (πΊβπ§)) |
66 | | ulmcl 25756 |
. . . . 5
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) |
67 | 66 | adantl 483 |
. . . 4
β’ ((π β§ πΉ(βπ’βπ)πΊ) β πΊ:πβΆβ) |
68 | | ulmscl 25754 |
. . . . 5
β’ (πΉ(βπ’βπ)πΊ β π β V) |
69 | 68 | adantl 483 |
. . . 4
β’ ((π β§ πΉ(βπ’βπ)πΊ) β π β V) |
70 | 17, 43, 55, 64, 65, 67, 69 | ulm2 25760 |
. . 3
β’ ((π β§ πΉ(βπ’βπ)πΊ) β (π»(βπ’βπ)πΊ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβ(π β πΎ))βπ§) β (πΊβπ§))) < π₯)) |
71 | 41, 70 | mpbird 257 |
. 2
β’ ((π β§ πΉ(βπ’βπ)πΊ) β π»(βπ’βπ)πΊ) |
72 | 71 | ex 414 |
1
β’ (π β (πΉ(βπ’βπ)πΊ β π»(βπ’βπ)πΊ)) |