Step | Hyp | Ref
| Expression |
1 | | lmrel 22726 |
. 2
β’ Rel
(βπ‘βπ½) |
2 | | fvex 6902 |
. . . . . . . 8
β’ ( β
β(π‘ β β
β¦ ((πΉβπ‘)βπ))) β V |
3 | | rrncms.7 |
. . . . . . . 8
β’ π = (π β πΌ β¦ ( β β(π‘ β β β¦ ((πΉβπ‘)βπ)))) |
4 | 2, 3 | fnmpti 6691 |
. . . . . . 7
β’ π Fn πΌ |
5 | 4 | a1i 11 |
. . . . . 6
β’ (π β π Fn πΌ) |
6 | | nnuz 12862 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
7 | | 1zzd 12590 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β 1 β β€) |
8 | | fveq2 6889 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = π β (πΉβπ‘) = (πΉβπ)) |
9 | 8 | fveq1d 6891 |
. . . . . . . . . . . . . . 15
β’ (π‘ = π β ((πΉβπ‘)βπ) = ((πΉβπ)βπ)) |
10 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π‘ β β β¦ ((πΉβπ‘)βπ)) = (π‘ β β β¦ ((πΉβπ‘)βπ)) |
11 | | fvex 6902 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ)βπ) β V |
12 | 9, 10, 11 | fvmpt 6996 |
. . . . . . . . . . . . . 14
β’ (π β β β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) = ((πΉβπ)βπ)) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΌ) β§ π β β) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) = ((πΉβπ)βπ)) |
14 | | rrncms.6 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ:ββΆπ) |
15 | 14 | ffvelcdmda 7084 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (πΉβπ) β π) |
16 | | rrnval.1 |
. . . . . . . . . . . . . . . . 17
β’ π = (β βm
πΌ) |
17 | 15, 16 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πΉβπ) β (β βm πΌ)) |
18 | | elmapi 8840 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β (β βm πΌ) β (πΉβπ):πΌβΆβ) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΉβπ):πΌβΆβ) |
20 | 19 | ffvelcdmda 7084 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β πΌ) β ((πΉβπ)βπ) β β) |
21 | 20 | an32s 651 |
. . . . . . . . . . . . 13
β’ (((π β§ π β πΌ) β§ π β β) β ((πΉβπ)βπ) β β) |
22 | 13, 21 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΌ) β§ π β β) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β β) |
23 | 22 | recnd 11239 |
. . . . . . . . . . 11
β’ (((π β§ π β πΌ) β§ π β β) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β β) |
24 | | rrncms.5 |
. . . . . . . . . . . . . 14
β’ (π β πΉ β
(Cauβ(βnβπΌ))) |
25 | | rrncms.4 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΌ β Fin) |
26 | 16 | rrnmet 36686 |
. . . . . . . . . . . . . . . . 17
β’ (πΌ β Fin β
(βnβπΌ) β (Metβπ)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β
(βnβπΌ) β (Metβπ)) |
28 | | metxmet 23832 |
. . . . . . . . . . . . . . . 16
β’
((βnβπΌ) β (Metβπ) β
(βnβπΌ) β (βMetβπ)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β
(βnβπΌ) β (βMetβπ)) |
30 | | 1zzd 12590 |
. . . . . . . . . . . . . . 15
β’ (π β 1 β
β€) |
31 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΉβπ) = (πΉβπ)) |
32 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΉβπ) = (πΉβπ)) |
33 | 6, 29, 30, 31, 32, 14 | iscauf 24789 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ β
(Cauβ(βnβπΌ)) β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)(πΉβπ)) < π₯)) |
34 | 24, 33 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)(πΉβπ)) < π₯) |
35 | 34 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)(πΉβπ)) < π₯) |
36 | 25 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β πΌ β Fin) |
37 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β π β πΌ) |
38 | 14 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β πΉ:ββΆπ) |
39 | | eluznn 12899 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
40 | 39 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β π β β) |
41 | 38, 40 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) β π) |
42 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β π β β) |
43 | 38, 42 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) β π) |
44 | | rrndstprj1.1 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = ((abs β β )
βΎ (β Γ β)) |
45 | 16, 44 | rrndstprj1 36687 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΌ β Fin β§ π β πΌ) β§ ((πΉβπ) β π β§ (πΉβπ) β π)) β (((πΉβπ)βπ)π((πΉβπ)βπ)) β€ ((πΉβπ)(βnβπΌ)(πΉβπ))) |
46 | 36, 37, 41, 43, 45 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β (((πΉβπ)βπ)π((πΉβπ)βπ)) β€ ((πΉβπ)(βnβπΌ)(πΉβπ))) |
47 | 27 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β
(βnβπΌ) β (Metβπ)) |
48 | | metsym 23848 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((βnβπΌ) β (Metβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)(βnβπΌ)(πΉβπ)) = ((πΉβπ)(βnβπΌ)(πΉβπ))) |
49 | 47, 41, 43, 48 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ)(βnβπΌ)(πΉβπ)) = ((πΉβπ)(βnβπΌ)(πΉβπ))) |
50 | 46, 49 | breqtrd 5174 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β (((πΉβπ)βπ)π((πΉβπ)βπ)) β€ ((πΉβπ)(βnβπΌ)(πΉβπ))) |
51 | 50 | adantllr 718 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β πΌ) β§ π₯ β β+) β§ π β β) β§ π β
(β€β₯βπ)) β (((πΉβπ)βπ)π((πΉβπ)βπ)) β€ ((πΉβπ)(βnβπΌ)(πΉβπ))) |
52 | 44 | remet 24298 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π β
(Metββ) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β π β
(Metββ)) |
54 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β (π β§ π β πΌ)) |
55 | 54, 40, 21 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ) β β) |
56 | 14 | ffvelcdmda 7084 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β (πΉβπ) β π) |
57 | 56, 16 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β (πΉβπ) β (β βm πΌ)) |
58 | | elmapi 8840 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉβπ) β (β βm πΌ) β (πΉβπ):πΌβΆβ) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β (πΉβπ):πΌβΆβ) |
60 | 59 | ffvelcdmda 7084 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β πΌ) β ((πΉβπ)βπ) β β) |
61 | 60 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β πΌ) β§ π β β) β ((πΉβπ)βπ) β β) |
62 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ) β β) |
63 | | metcl 23830 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (Metββ)
β§ ((πΉβπ)βπ) β β β§ ((πΉβπ)βπ) β β) β (((πΉβπ)βπ)π((πΉβπ)βπ)) β β) |
64 | 53, 55, 62, 63 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β (((πΉβπ)βπ)π((πΉβπ)βπ)) β β) |
65 | 64 | adantllr 718 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β πΌ) β§ π₯ β β+) β§ π β β) β§ π β
(β€β₯βπ)) β (((πΉβπ)βπ)π((πΉβπ)βπ)) β β) |
66 | | metcl 23830 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((βnβπΌ) β (Metβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)(βnβπΌ)(πΉβπ)) β β) |
67 | 47, 43, 41, 66 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ)(βnβπΌ)(πΉβπ)) β β) |
68 | 67 | adantllr 718 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β πΌ) β§ π₯ β β+) β§ π β β) β§ π β
(β€β₯βπ)) β ((πΉβπ)(βnβπΌ)(πΉβπ)) β β) |
69 | | rpre 12979 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β+
β π₯ β
β) |
70 | 69 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β πΌ) β§ π₯ β β+) β π₯ β
β) |
71 | 70 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β πΌ) β§ π₯ β β+) β§ π β β) β§ π β
(β€β₯βπ)) β π₯ β β) |
72 | | lelttr 11301 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉβπ)βπ)π((πΉβπ)βπ)) β β β§ ((πΉβπ)(βnβπΌ)(πΉβπ)) β β β§ π₯ β β) β (((((πΉβπ)βπ)π((πΉβπ)βπ)) β€ ((πΉβπ)(βnβπΌ)(πΉβπ)) β§ ((πΉβπ)(βnβπΌ)(πΉβπ)) < π₯) β (((πΉβπ)βπ)π((πΉβπ)βπ)) < π₯)) |
73 | 65, 68, 71, 72 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β πΌ) β§ π₯ β β+) β§ π β β) β§ π β
(β€β₯βπ)) β (((((πΉβπ)βπ)π((πΉβπ)βπ)) β€ ((πΉβπ)(βnβπΌ)(πΉβπ)) β§ ((πΉβπ)(βnβπΌ)(πΉβπ)) < π₯) β (((πΉβπ)βπ)π((πΉβπ)βπ)) < π₯)) |
74 | 51, 73 | mpand 694 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β πΌ) β§ π₯ β β+) β§ π β β) β§ π β
(β€β₯βπ)) β (((πΉβπ)(βnβπΌ)(πΉβπ)) < π₯ β (((πΉβπ)βπ)π((πΉβπ)βπ)) < π₯)) |
75 | 74 | ralimdva 3168 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β πΌ) β§ π₯ β β+) β§ π β β) β
(βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)(πΉβπ)) < π₯ β βπ β (β€β₯βπ)(((πΉβπ)βπ)π((πΉβπ)βπ)) < π₯)) |
76 | 75 | reximdva 3169 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β πΌ) β§ π₯ β β+) β
(βπ β β
βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)(πΉβπ)) < π₯ β βπ β β βπ β (β€β₯βπ)(((πΉβπ)βπ)π((πΉβπ)βπ)) < π₯)) |
77 | 76 | ralimdva 3168 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β (βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)(πΉβπ)) < π₯ β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(((πΉβπ)βπ)π((πΉβπ)βπ)) < π₯)) |
78 | 44 | remetdval 24297 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΉβπ)βπ) β β β§ ((πΉβπ)βπ) β β) β (((πΉβπ)βπ)π((πΉβπ)βπ)) = (absβ(((πΉβπ)βπ) β ((πΉβπ)βπ)))) |
79 | 55, 62, 78 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β (((πΉβπ)βπ)π((πΉβπ)βπ)) = (absβ(((πΉβπ)βπ) β ((πΉβπ)βπ)))) |
80 | 40, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) = ((πΉβπ)βπ)) |
81 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π β (πΉβπ‘) = (πΉβπ)) |
82 | 81 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ = π β ((πΉβπ‘)βπ) = ((πΉβπ)βπ)) |
83 | | fvex 6902 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΉβπ)βπ) β V |
84 | 82, 10, 83 | fvmpt 6996 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) = ((πΉβπ)βπ)) |
85 | 84 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) = ((πΉβπ)βπ)) |
86 | 80, 85 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β (((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ)) = (((πΉβπ)βπ) β ((πΉβπ)βπ))) |
87 | 86 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β (absβ(((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ))) = (absβ(((πΉβπ)βπ) β ((πΉβπ)βπ)))) |
88 | 79, 87 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β (((πΉβπ)βπ)π((πΉβπ)βπ)) = (absβ(((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ)))) |
89 | 88 | breq1d 5158 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β ((((πΉβπ)βπ)π((πΉβπ)βπ)) < π₯ β (absβ(((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ))) < π₯)) |
90 | 89 | ralbidva 3176 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β πΌ) β§ π β β) β (βπ β
(β€β₯βπ)(((πΉβπ)βπ)π((πΉβπ)βπ)) < π₯ β βπ β (β€β₯βπ)(absβ(((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ))) < π₯)) |
91 | 90 | rexbidva 3177 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΌ) β (βπ β β βπ β (β€β₯βπ)(((πΉβπ)βπ)π((πΉβπ)βπ)) < π₯ β βπ β β βπ β (β€β₯βπ)(absβ(((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ))) < π₯)) |
92 | 91 | ralbidv 3178 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β (βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(((πΉβπ)βπ)π((πΉβπ)βπ)) < π₯ β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(absβ(((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ))) < π₯)) |
93 | 77, 92 | sylibd 238 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β (βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)(πΉβπ)) < π₯ β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(absβ(((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ))) < π₯)) |
94 | 35, 93 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)(absβ(((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ))) < π₯) |
95 | | nnex 12215 |
. . . . . . . . . . . . 13
β’ β
β V |
96 | 95 | mptex 7222 |
. . . . . . . . . . . 12
β’ (π‘ β β β¦ ((πΉβπ‘)βπ)) β V |
97 | 96 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β (π‘ β β β¦ ((πΉβπ‘)βπ)) β V) |
98 | 6, 23, 94, 97 | caucvg 15622 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (π‘ β β β¦ ((πΉβπ‘)βπ)) β dom β ) |
99 | | climdm 15495 |
. . . . . . . . . 10
β’ ((π‘ β β β¦ ((πΉβπ‘)βπ)) β dom β β (π‘ β β β¦ ((πΉβπ‘)βπ)) β ( β β(π‘ β β β¦ ((πΉβπ‘)βπ)))) |
100 | 98, 99 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (π‘ β β β¦ ((πΉβπ‘)βπ)) β ( β β(π‘ β β β¦ ((πΉβπ‘)βπ)))) |
101 | | fveq2 6889 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ‘)βπ) = ((πΉβπ‘)βπ)) |
102 | 101 | mpteq2dv 5250 |
. . . . . . . . . . . 12
β’ (π = π β (π‘ β β β¦ ((πΉβπ‘)βπ)) = (π‘ β β β¦ ((πΉβπ‘)βπ))) |
103 | 102 | fveq2d 6893 |
. . . . . . . . . . 11
β’ (π = π β ( β β(π‘ β β β¦ ((πΉβπ‘)βπ))) = ( β β(π‘ β β β¦ ((πΉβπ‘)βπ)))) |
104 | | fvex 6902 |
. . . . . . . . . . 11
β’ ( β
β(π‘ β β
β¦ ((πΉβπ‘)βπ))) β V |
105 | 103, 3, 104 | fvmpt 6996 |
. . . . . . . . . 10
β’ (π β πΌ β (πβπ) = ( β β(π‘ β β β¦ ((πΉβπ‘)βπ)))) |
106 | 105 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (πβπ) = ( β β(π‘ β β β¦ ((πΉβπ‘)βπ)))) |
107 | 100, 106 | breqtrrd 5176 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (π‘ β β β¦ ((πΉβπ‘)βπ)) β (πβπ)) |
108 | 6, 7, 107, 22 | climrecl 15524 |
. . . . . . 7
β’ ((π β§ π β πΌ) β (πβπ) β β) |
109 | 108 | ralrimiva 3147 |
. . . . . 6
β’ (π β βπ β πΌ (πβπ) β β) |
110 | | ffnfv 7115 |
. . . . . 6
β’ (π:πΌβΆβ β (π Fn πΌ β§ βπ β πΌ (πβπ) β β)) |
111 | 5, 109, 110 | sylanbrc 584 |
. . . . 5
β’ (π β π:πΌβΆβ) |
112 | | reex 11198 |
. . . . . 6
β’ β
β V |
113 | | elmapg 8830 |
. . . . . 6
β’ ((β
β V β§ πΌ β
Fin) β (π β
(β βm πΌ) β π:πΌβΆβ)) |
114 | 112, 25, 113 | sylancr 588 |
. . . . 5
β’ (π β (π β (β βm πΌ) β π:πΌβΆβ)) |
115 | 111, 114 | mpbird 257 |
. . . 4
β’ (π β π β (β βm πΌ)) |
116 | 115, 16 | eleqtrrdi 2845 |
. . 3
β’ (π β π β π) |
117 | | 1nn 12220 |
. . . . . . 7
β’ 1 β
β |
118 | 25 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β πΌ β Fin) |
119 | 15 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β (πΉβπ) β π) |
120 | 116 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β π β π) |
121 | 16 | rrnmval 36685 |
. . . . . . . . . . . 12
β’ ((πΌ β Fin β§ (πΉβπ) β π β§ π β π) β ((πΉβπ)(βnβπΌ)π) = (ββΞ£π¦ β πΌ ((((πΉβπ)βπ¦) β (πβπ¦))β2))) |
122 | 118, 119,
120, 121 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β ((πΉβπ)(βnβπΌ)π) = (ββΞ£π¦ β πΌ ((((πΉβπ)βπ¦) β (πβπ¦))β2))) |
123 | | simplrr 777 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β πΌ = β
) |
124 | 123 | sumeq1d 15644 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β
Ξ£π¦ β πΌ ((((πΉβπ)βπ¦) β (πβπ¦))β2) = Ξ£π¦ β β
((((πΉβπ)βπ¦) β (πβπ¦))β2)) |
125 | | sum0 15664 |
. . . . . . . . . . . . 13
β’
Ξ£π¦ β
β
((((πΉβπ)βπ¦) β (πβπ¦))β2) = 0 |
126 | 124, 125 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β
Ξ£π¦ β πΌ ((((πΉβπ)βπ¦) β (πβπ¦))β2) = 0) |
127 | 126 | fveq2d 6893 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β
(ββΞ£π¦
β πΌ ((((πΉβπ)βπ¦) β (πβπ¦))β2)) =
(ββ0)) |
128 | 122, 127 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β ((πΉβπ)(βnβπΌ)π) = (ββ0)) |
129 | | sqrt0 15185 |
. . . . . . . . . 10
β’
(ββ0) = 0 |
130 | 128, 129 | eqtrdi 2789 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β ((πΉβπ)(βnβπΌ)π) = 0) |
131 | | simplrl 776 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β π₯ β
β+) |
132 | 131 | rpgt0d 13016 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β 0 <
π₯) |
133 | 130, 132 | eqbrtrd 5170 |
. . . . . . . 8
β’ (((π β§ (π₯ β β+ β§ πΌ = β
)) β§ π β β) β ((πΉβπ)(βnβπΌ)π) < π₯) |
134 | 133 | ralrimiva 3147 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ πΌ = β
)) β
βπ β β
((πΉβπ)(βnβπΌ)π) < π₯) |
135 | | fveq2 6889 |
. . . . . . . . . 10
β’ (π = 1 β
(β€β₯βπ) =
(β€β₯β1)) |
136 | 135, 6 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π = 1 β
(β€β₯βπ) = β) |
137 | 136 | raleqdv 3326 |
. . . . . . . 8
β’ (π = 1 β (βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯ β βπ β β ((πΉβπ)(βnβπΌ)π) < π₯)) |
138 | 137 | rspcev 3613 |
. . . . . . 7
β’ ((1
β β β§ βπ β β ((πΉβπ)(βnβπΌ)π) < π₯) β βπ β β βπ β (β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯) |
139 | 117, 134,
138 | sylancr 588 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ πΌ = β
)) β βπ β β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯) |
140 | 139 | expr 458 |
. . . . 5
β’ ((π β§ π₯ β β+) β (πΌ = β
β βπ β β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯)) |
141 | | 1zzd 12590 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β 1 β β€) |
142 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β π₯ β
β+) |
143 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β πΌ β β
) |
144 | 25 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β πΌ β Fin) |
145 | | hashnncl 14323 |
. . . . . . . . . . . . . . . . 17
β’ (πΌ β Fin β
((β―βπΌ) β
β β πΌ β
β
)) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β
((β―βπΌ) β
β β πΌ β
β
)) |
147 | 143, 146 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β
(β―βπΌ) β
β) |
148 | 147 | nnrpd 13011 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β
(β―βπΌ) β
β+) |
149 | 148 | rpsqrtcld 15355 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β
(ββ(β―βπΌ)) β
β+) |
150 | 142, 149 | rpdivcld 13030 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β (π₯ /
(ββ(β―βπΌ))) β
β+) |
151 | 150 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β (π₯ / (ββ(β―βπΌ))) β
β+) |
152 | 12 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β§ π β β) β ((π‘ β β β¦ ((πΉβπ‘)βπ))βπ) = ((πΉβπ)βπ)) |
153 | 107 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β (π‘ β β β¦ ((πΉβπ‘)βπ)) β (πβπ)) |
154 | 6, 141, 151, 152, 153 | climi2 15452 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β βπ β β βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ) β (πβπ))) < (π₯ / (ββ(β―βπΌ)))) |
155 | | 1z 12589 |
. . . . . . . . . . . 12
β’ 1 β
β€ |
156 | 6 | rexuz3 15292 |
. . . . . . . . . . . 12
β’ (1 β
β€ β (βπ
β β βπ
β (β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β β€ βπ β
(β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))))) |
157 | 155, 156 | ax-mp 5 |
. . . . . . . . . . 11
β’
(βπ β
β βπ β
(β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β β€ βπ β
(β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ)))) |
158 | 21 | adantllr 718 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β§ π β β) β ((πΉβπ)βπ) β β) |
159 | 108 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β (πβπ) β β) |
160 | 159 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β§ π β β) β (πβπ) β β) |
161 | 44 | remetdval 24297 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ)βπ) β β β§ (πβπ) β β) β (((πΉβπ)βπ)π(πβπ)) = (absβ(((πΉβπ)βπ) β (πβπ)))) |
162 | 158, 160,
161 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β§ π β β) β (((πΉβπ)βπ)π(πβπ)) = (absβ(((πΉβπ)βπ) β (πβπ)))) |
163 | 162 | breq1d 5158 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β§ π β β) β ((((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β (absβ(((πΉβπ)βπ) β (πβπ))) < (π₯ / (ββ(β―βπΌ))))) |
164 | 39, 163 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β§ (π β β β§ π β (β€β₯βπ))) β ((((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β (absβ(((πΉβπ)βπ) β (πβπ))) < (π₯ / (ββ(β―βπΌ))))) |
165 | 164 | anassrs 469 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π₯ β β+
β§ πΌ β β
))
β§ π β πΌ) β§ π β β) β§ π β (β€β₯βπ)) β ((((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β (absβ(((πΉβπ)βπ) β (πβπ))) < (π₯ / (ββ(β―βπΌ))))) |
166 | 165 | ralbidva 3176 |
. . . . . . . . . . . 12
β’ ((((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β§ π β β) β (βπ β
(β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β
(β€β₯βπ)(absβ(((πΉβπ)βπ) β (πβπ))) < (π₯ / (ββ(β―βπΌ))))) |
167 | 166 | rexbidva 3177 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β (βπ β β βπ β (β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β β βπ β
(β€β₯βπ)(absβ(((πΉβπ)βπ) β (πβπ))) < (π₯ / (ββ(β―βπΌ))))) |
168 | 157, 167 | bitr3id 285 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β (βπ β β€ βπ β (β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β β βπ β
(β€β₯βπ)(absβ(((πΉβπ)βπ) β (πβπ))) < (π₯ / (ββ(β―βπΌ))))) |
169 | 154, 168 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β πΌ) β βπ β β€ βπ β (β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ)))) |
170 | 169 | ralrimiva 3147 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β
βπ β πΌ βπ β β€ βπ β (β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ)))) |
171 | 6 | rexuz3 15292 |
. . . . . . . . . 10
β’ (1 β
β€ β (βπ
β β βπ
β (β€β₯βπ)βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β β€ βπ β
(β€β₯βπ)βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))))) |
172 | 155, 171 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ β
β βπ β
(β€β₯βπ)βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β β€ βπ β
(β€β₯βπ)βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ)))) |
173 | | rexfiuz 15291 |
. . . . . . . . . 10
β’ (πΌ β Fin β (βπ β β€ βπ β
(β€β₯βπ)βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β πΌ βπ β β€ βπ β (β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))))) |
174 | 144, 173 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β
(βπ β β€
βπ β
(β€β₯βπ)βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β πΌ βπ β β€ βπ β (β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))))) |
175 | 172, 174 | bitrid 283 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β
(βπ β β
βπ β
(β€β₯βπ)βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β πΌ βπ β β€ βπ β (β€β₯βπ)(((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))))) |
176 | 170, 175 | mpbird 257 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β
βπ β β
βπ β
(β€β₯βπ)βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ)))) |
177 | 25 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β πΌ β Fin) |
178 | | simplrr 777 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β πΌ β β
) |
179 | | eldifsn 4790 |
. . . . . . . . . . . . . 14
β’ (πΌ β (Fin β {β
})
β (πΌ β Fin β§
πΌ β
β
)) |
180 | 177, 178,
179 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β πΌ β (Fin β
{β
})) |
181 | 14 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β πΉ:ββΆπ) |
182 | 181 | ffvelcdmda 7084 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β (πΉβπ) β π) |
183 | 116 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β π β π) |
184 | 150 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β (π₯ /
(ββ(β―βπΌ))) β
β+) |
185 | 16, 44 | rrndstprj2 36688 |
. . . . . . . . . . . . . 14
β’ (((πΌ β (Fin β {β
})
β§ (πΉβπ) β π β§ π β π) β§ ((π₯ / (ββ(β―βπΌ))) β β+
β§ βπ β
πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))))) β ((πΉβπ)(βnβπΌ)π) < ((π₯ / (ββ(β―βπΌ))) Β·
(ββ(β―βπΌ)))) |
186 | 185 | expr 458 |
. . . . . . . . . . . . 13
β’ (((πΌ β (Fin β {β
})
β§ (πΉβπ) β π β§ π β π) β§ (π₯ / (ββ(β―βπΌ))) β β+)
β (βπ β
πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β ((πΉβπ)(βnβπΌ)π) < ((π₯ / (ββ(β―βπΌ))) Β·
(ββ(β―βπΌ))))) |
187 | 180, 182,
183, 184, 186 | syl31anc 1374 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β
(βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β ((πΉβπ)(βnβπΌ)π) < ((π₯ / (ββ(β―βπΌ))) Β·
(ββ(β―βπΌ))))) |
188 | | simplrl 776 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β π₯ β
β+) |
189 | 188 | rpcnd 13015 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β π₯ β
β) |
190 | 149 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β
(ββ(β―βπΌ)) β
β+) |
191 | 190 | rpcnd 13015 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β
(ββ(β―βπΌ)) β β) |
192 | 190 | rpne0d 13018 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β
(ββ(β―βπΌ)) β 0) |
193 | 189, 191,
192 | divcan1d 11988 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β ((π₯ /
(ββ(β―βπΌ))) Β·
(ββ(β―βπΌ))) = π₯) |
194 | 193 | breq2d 5160 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β (((πΉβπ)(βnβπΌ)π) < ((π₯ / (ββ(β―βπΌ))) Β·
(ββ(β―βπΌ))) β ((πΉβπ)(βnβπΌ)π) < π₯)) |
195 | 187, 194 | sylibd 238 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β
(βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β ((πΉβπ)(βnβπΌ)π) < π₯)) |
196 | 39, 195 | sylan2 594 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ (π β β β§ π β
(β€β₯βπ))) β (βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β ((πΉβπ)(βnβπΌ)π) < π₯)) |
197 | 196 | anassrs 469 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β§ π β
(β€β₯βπ)) β (βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β ((πΉβπ)(βnβπΌ)π) < π₯)) |
198 | 197 | ralimdva 3168 |
. . . . . . . 8
β’ (((π β§ (π₯ β β+ β§ πΌ β β
)) β§ π β β) β
(βπ β
(β€β₯βπ)βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯)) |
199 | 198 | reximdva 3169 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β
(βπ β β
βπ β
(β€β₯βπ)βπ β πΌ (((πΉβπ)βπ)π(πβπ)) < (π₯ / (ββ(β―βπΌ))) β βπ β β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯)) |
200 | 176, 199 | mpd 15 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ πΌ β β
)) β
βπ β β
βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯) |
201 | 200 | expr 458 |
. . . . 5
β’ ((π β§ π₯ β β+) β (πΌ β β
β
βπ β β
βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯)) |
202 | 140, 201 | pm2.61dne 3029 |
. . . 4
β’ ((π β§ π₯ β β+) β
βπ β β
βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯) |
203 | 202 | ralrimiva 3147 |
. . 3
β’ (π β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯) |
204 | | rrncms.3 |
. . . 4
β’ π½ =
(MetOpenβ(βnβπΌ)) |
205 | 204, 29, 6, 30, 31, 14 | lmmbrf 24771 |
. . 3
β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)(βnβπΌ)π) < π₯))) |
206 | 116, 203,
205 | mpbir2and 712 |
. 2
β’ (π β πΉ(βπ‘βπ½)π) |
207 | | releldm 5942 |
. 2
β’ ((Rel
(βπ‘βπ½) β§ πΉ(βπ‘βπ½)π) β πΉ β dom
(βπ‘βπ½)) |
208 | 1, 206, 207 | sylancr 588 |
1
β’ (π β πΉ β dom
(βπ‘βπ½)) |