Step | Hyp | Ref
| Expression |
1 | | ulmdv.g |
. . . . . 6
β’ (π β πΊ:πβΆβ) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π) β πΊ:πβΆβ) |
3 | | ulmdvlem1.y |
. . . . 5
β’ ((π β§ π) β π β π) |
4 | 2, 3 | ffvelcdmd 7041 |
. . . 4
β’ ((π β§ π) β (πΊβπ) β β) |
5 | | ulmdvlem1.c |
. . . . 5
β’ ((π β§ π) β πΆ β π) |
6 | 2, 5 | ffvelcdmd 7041 |
. . . 4
β’ ((π β§ π) β (πΊβπΆ) β β) |
7 | 4, 6 | subcld 11519 |
. . 3
β’ ((π β§ π) β ((πΊβπ) β (πΊβπΆ)) β β) |
8 | | ulmdvlem1.n |
. . . . . . . . . . 11
β’ ((π β§ π) β π β π) |
9 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβπ) = (πΉβπ)) |
10 | 9 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π = π β (π D (πΉβπ)) = (π D (πΉβπ))) |
11 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β π β¦ (π D (πΉβπ))) = (π β π β¦ (π D (πΉβπ))) |
12 | | ovex 7395 |
. . . . . . . . . . . 12
β’ (π D (πΉβπ)) β V |
13 | 10, 11, 12 | fvmpt 6953 |
. . . . . . . . . . 11
β’ (π β π β ((π β π β¦ (π D (πΉβπ)))βπ) = (π D (πΉβπ))) |
14 | 8, 13 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π) β ((π β π β¦ (π D (πΉβπ)))βπ) = (π D (πΉβπ))) |
15 | | ovex 7395 |
. . . . . . . . . . . . . . 15
β’ (π D (πΉβπ)) β V |
16 | 15 | rgenw 3069 |
. . . . . . . . . . . . . 14
β’
βπ β
π (π D (πΉβπ)) β V |
17 | 11 | fnmpt 6646 |
. . . . . . . . . . . . . 14
β’
(βπ β
π (π D (πΉβπ)) β V β (π β π β¦ (π D (πΉβπ))) Fn π) |
18 | 16, 17 | mp1i 13 |
. . . . . . . . . . . . 13
β’ (π β (π β π β¦ (π D (πΉβπ))) Fn π) |
19 | | ulmdv.u |
. . . . . . . . . . . . 13
β’ (π β (π β π β¦ (π D (πΉβπ)))(βπ’βπ)π») |
20 | | ulmf2 25759 |
. . . . . . . . . . . . 13
β’ (((π β π β¦ (π D (πΉβπ))) Fn π β§ (π β π β¦ (π D (πΉβπ)))(βπ’βπ)π») β (π β π β¦ (π D (πΉβπ))):πβΆ(β βm π)) |
21 | 18, 19, 20 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (π β π β¦ (π D (πΉβπ))):πβΆ(β βm π)) |
22 | 21 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π) β (π β π β¦ (π D (πΉβπ))):πβΆ(β βm π)) |
23 | 22, 8 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π) β ((π β π β¦ (π D (πΉβπ)))βπ) β (β βm π)) |
24 | 14, 23 | eqeltrrd 2839 |
. . . . . . . . 9
β’ ((π β§ π) β (π D (πΉβπ)) β (β βm π)) |
25 | | elmapi 8794 |
. . . . . . . . 9
β’ ((π D (πΉβπ)) β (β βm π) β (π D (πΉβπ)):πβΆβ) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
β’ ((π β§ π) β (π D (πΉβπ)):πβΆβ) |
27 | 26 | fdmd 6684 |
. . . . . . 7
β’ ((π β§ π) β dom (π D (πΉβπ)) = π) |
28 | | dvbsss 25282 |
. . . . . . 7
β’ dom
(π D (πΉβπ)) β π |
29 | 27, 28 | eqsstrrdi 4004 |
. . . . . 6
β’ ((π β§ π) β π β π) |
30 | | ulmdv.s |
. . . . . . . 8
β’ (π β π β {β, β}) |
31 | | recnprss 25284 |
. . . . . . . 8
β’ (π β {β, β}
β π β
β) |
32 | 30, 31 | syl 17 |
. . . . . . 7
β’ (π β π β β) |
33 | 32 | adantr 482 |
. . . . . 6
β’ ((π β§ π) β π β β) |
34 | 29, 33 | sstrd 3959 |
. . . . 5
β’ ((π β§ π) β π β β) |
35 | 34, 3 | sseldd 3950 |
. . . 4
β’ ((π β§ π) β π β β) |
36 | 34, 5 | sseldd 3950 |
. . . 4
β’ ((π β§ π) β πΆ β β) |
37 | 35, 36 | subcld 11519 |
. . 3
β’ ((π β§ π) β (π β πΆ) β β) |
38 | | ulmdvlem1.3 |
. . . 4
β’ ((π β§ π) β π β πΆ) |
39 | 35, 36, 38 | subne0d 11528 |
. . 3
β’ ((π β§ π) β (π β πΆ) β 0) |
40 | 7, 37, 39 | divcld 11938 |
. 2
β’ ((π β§ π) β (((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β β) |
41 | | ulmcl 25756 |
. . . . 5
β’ ((π β π β¦ (π D (πΉβπ)))(βπ’βπ)π» β π»:πβΆβ) |
42 | 19, 41 | syl 17 |
. . . 4
β’ (π β π»:πβΆβ) |
43 | 42 | adantr 482 |
. . 3
β’ ((π β§ π) β π»:πβΆβ) |
44 | 43, 5 | ffvelcdmd 7041 |
. 2
β’ ((π β§ π) β (π»βπΆ) β β) |
45 | 26, 5 | ffvelcdmd 7041 |
. 2
β’ ((π β§ π) β ((π D (πΉβπ))βπΆ) β β) |
46 | | ulmdvlem1.r |
. . 3
β’ ((π β§ π) β π
β
β+) |
47 | 46 | rpred 12964 |
. 2
β’ ((π β§ π) β π
β β) |
48 | 40, 45 | subcld 11519 |
. . . 4
β’ ((π β§ π) β ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ)) β β) |
49 | 48 | abscld 15328 |
. . 3
β’ ((π β§ π) β (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ))) β β) |
50 | | ulmdv.f |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆ(β βm π)) |
51 | 50 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π) β πΉ:πβΆ(β βm π)) |
52 | 51, 8 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π) β (πΉβπ) β (β βm π)) |
53 | | elmapi 8794 |
. . . . . . . . . 10
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π) β (πΉβπ):πβΆβ) |
55 | 54, 3 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((π β§ π) β ((πΉβπ)βπ) β β) |
56 | 54, 5 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((π β§ π) β ((πΉβπ)βπΆ) β β) |
57 | 55, 56 | subcld 11519 |
. . . . . . 7
β’ ((π β§ π) β (((πΉβπ)βπ) β ((πΉβπ)βπΆ)) β β) |
58 | 57, 37, 39 | divcld 11938 |
. . . . . 6
β’ ((π β§ π) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β β) |
59 | 40, 58 | subcld 11519 |
. . . . 5
β’ ((π β§ π) β ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ))) β β) |
60 | 59 | abscld 15328 |
. . . 4
β’ ((π β§ π) β (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)))) β β) |
61 | 58, 45 | subcld 11519 |
. . . . 5
β’ ((π β§ π) β (((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ)) β β) |
62 | 61 | abscld 15328 |
. . . 4
β’ ((π β§ π) β (absβ(((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ))) β β) |
63 | 60, 62 | readdcld 11191 |
. . 3
β’ ((π β§ π) β ((absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)))) + (absβ(((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ)))) β β) |
64 | 47 | rehalfcld 12407 |
. . 3
β’ ((π β§ π) β (π
/ 2) β β) |
65 | 40, 45, 58 | abs3difd 15352 |
. . 3
β’ ((π β§ π) β (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ))) β€ ((absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)))) + (absβ(((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ))))) |
66 | 64 | rehalfcld 12407 |
. . . . 5
β’ ((π β§ π) β ((π
/ 2) / 2) β β) |
67 | 4, 55, 6, 56 | sub4d 11568 |
. . . . . . . . . 10
β’ ((π β§ π) β (((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ))) = (((πΊβπ) β (πΊβπΆ)) β (((πΉβπ)βπ) β ((πΉβπ)βπΆ)))) |
68 | 67 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π β§ π) β ((((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ))) / (π β πΆ)) = ((((πΊβπ) β (πΊβπΆ)) β (((πΉβπ)βπ) β ((πΉβπ)βπΆ))) / (π β πΆ))) |
69 | 7, 57, 37, 39 | divsubdird 11977 |
. . . . . . . . 9
β’ ((π β§ π) β ((((πΊβπ) β (πΊβπΆ)) β (((πΉβπ)βπ) β ((πΉβπ)βπΆ))) / (π β πΆ)) = ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)))) |
70 | 68, 69 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π) β ((((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ))) / (π β πΆ)) = ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)))) |
71 | 70 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ π) β (absβ((((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ))) / (π β πΆ))) = (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ))))) |
72 | 4, 55 | subcld 11519 |
. . . . . . . . 9
β’ ((π β§ π) β ((πΊβπ) β ((πΉβπ)βπ)) β β) |
73 | 6, 56 | subcld 11519 |
. . . . . . . . 9
β’ ((π β§ π) β ((πΊβπΆ) β ((πΉβπ)βπΆ)) β β) |
74 | 72, 73 | subcld 11519 |
. . . . . . . 8
β’ ((π β§ π) β (((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ))) β β) |
75 | 74, 37, 39 | absdivd 15347 |
. . . . . . 7
β’ ((π β§ π) β (absβ((((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ))) / (π β πΆ))) = ((absβ(((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ)))) / (absβ(π β πΆ)))) |
76 | 71, 75 | eqtr3d 2779 |
. . . . . 6
β’ ((π β§ π) β (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)))) = ((absβ(((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ)))) / (absβ(π β πΆ)))) |
77 | | eqid 2737 |
. . . . . . . 8
β’
(β€β₯βπ) = (β€β₯βπ) |
78 | | ulmdv.z |
. . . . . . . . . 10
β’ π =
(β€β₯βπ) |
79 | 8, 78 | eleqtrdi 2848 |
. . . . . . . . 9
β’ ((π β§ π) β π β (β€β₯βπ)) |
80 | | eluzelz 12780 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β π β β€) |
81 | 79, 80 | syl 17 |
. . . . . . . 8
β’ ((π β§ π) β π β β€) |
82 | | ulmdv.m |
. . . . . . . . . . 11
β’ (π β π β β€) |
83 | 82 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π) β π β β€) |
84 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π§ = π β ((πΉβπ)βπ§) = ((πΉβπ)βπ)) |
85 | 84 | mpteq2dv 5212 |
. . . . . . . . . . . . 13
β’ (π§ = π β (π β π β¦ ((πΉβπ)βπ§)) = (π β π β¦ ((πΉβπ)βπ))) |
86 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π§ = π β (πΊβπ§) = (πΊβπ)) |
87 | 85, 86 | breq12d 5123 |
. . . . . . . . . . . 12
β’ (π§ = π β ((π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§) β (π β π β¦ ((πΉβπ)βπ)) β (πΊβπ))) |
88 | | ulmdv.l |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π) β (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) |
89 | 88 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ (π β βπ§ β π (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) |
90 | 89 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π) β βπ§ β π (π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§)) |
91 | 87, 90, 3 | rspcdva 3585 |
. . . . . . . . . . 11
β’ ((π β§ π) β (π β π β¦ ((πΉβπ)βπ)) β (πΊβπ)) |
92 | 78 | fvexi 6861 |
. . . . . . . . . . . . 13
β’ π β V |
93 | 92 | mptex 7178 |
. . . . . . . . . . . 12
β’ (π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ))) β V |
94 | 93 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π) β (π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ))) β V) |
95 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΉβπ) = (πΉβπ)) |
96 | 95 | fveq1d 6849 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉβπ)βπ) = ((πΉβπ)βπ)) |
97 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (π β π β¦ ((πΉβπ)βπ)) = (π β π β¦ ((πΉβπ)βπ)) |
98 | | fvex 6860 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ)βπ) β V |
99 | 96, 97, 98 | fvmpt 6953 |
. . . . . . . . . . . . 13
β’ (π β π β ((π β π β¦ ((πΉβπ)βπ))βπ) = ((πΉβπ)βπ)) |
100 | 99 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β π) β ((π β π β¦ ((πΉβπ)βπ))βπ) = ((πΉβπ)βπ)) |
101 | 51 | ffvelcdmda 7040 |
. . . . . . . . . . . . . 14
β’ (((π β§ π) β§ π β π) β (πΉβπ) β (β βm π)) |
102 | | elmapi 8794 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β π) β (πΉβπ):πβΆβ) |
104 | 3 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β π) β π β π) |
105 | 103, 104 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β π) β ((πΉβπ)βπ) β β) |
106 | 100, 105 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β π) β ((π β π β¦ ((πΉβπ)βπ))βπ) β β) |
107 | 96 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (π = π β (((πΉβπ)βπ) β ((πΉβπ)βπ)) = (((πΉβπ)βπ) β ((πΉβπ)βπ))) |
108 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ))) = (π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ))) |
109 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ)βπ) β ((πΉβπ)βπ)) β V |
110 | 107, 108,
109 | fvmpt 6953 |
. . . . . . . . . . . . 13
β’ (π β π β ((π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ)))βπ) = (((πΉβπ)βπ) β ((πΉβπ)βπ))) |
111 | 110 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β π) β ((π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ)))βπ) = (((πΉβπ)βπ) β ((πΉβπ)βπ))) |
112 | 100 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β π) β (((π β π β¦ ((πΉβπ)βπ))βπ) β ((πΉβπ)βπ)) = (((πΉβπ)βπ) β ((πΉβπ)βπ))) |
113 | 111, 112 | eqtr4d 2780 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β π) β ((π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ)))βπ) = (((π β π β¦ ((πΉβπ)βπ))βπ) β ((πΉβπ)βπ))) |
114 | 78, 83, 91, 55, 94, 106, 113 | climsubc1 15527 |
. . . . . . . . . 10
β’ ((π β§ π) β (π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ))) β ((πΊβπ) β ((πΉβπ)βπ))) |
115 | 92 | mptex 7178 |
. . . . . . . . . . 11
β’ (π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) β V |
116 | 115 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π) β (π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) β V) |
117 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π§ = πΆ β ((πΉβπ)βπ§) = ((πΉβπ)βπΆ)) |
118 | 117 | mpteq2dv 5212 |
. . . . . . . . . . . . 13
β’ (π§ = πΆ β (π β π β¦ ((πΉβπ)βπ§)) = (π β π β¦ ((πΉβπ)βπΆ))) |
119 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π§ = πΆ β (πΊβπ§) = (πΊβπΆ)) |
120 | 118, 119 | breq12d 5123 |
. . . . . . . . . . . 12
β’ (π§ = πΆ β ((π β π β¦ ((πΉβπ)βπ§)) β (πΊβπ§) β (π β π β¦ ((πΉβπ)βπΆ)) β (πΊβπΆ))) |
121 | 120, 90, 5 | rspcdva 3585 |
. . . . . . . . . . 11
β’ ((π β§ π) β (π β π β¦ ((πΉβπ)βπΆ)) β (πΊβπΆ)) |
122 | 92 | mptex 7178 |
. . . . . . . . . . . 12
β’ (π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) β V |
123 | 122 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π) β (π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) β V) |
124 | 95 | fveq1d 6849 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉβπ)βπΆ) = ((πΉβπ)βπΆ)) |
125 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (π β π β¦ ((πΉβπ)βπΆ)) = (π β π β¦ ((πΉβπ)βπΆ)) |
126 | | fvex 6860 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ)βπΆ) β V |
127 | 124, 125,
126 | fvmpt 6953 |
. . . . . . . . . . . . 13
β’ (π β π β ((π β π β¦ ((πΉβπ)βπΆ))βπ) = ((πΉβπ)βπΆ)) |
128 | 127 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β π) β ((π β π β¦ ((πΉβπ)βπΆ))βπ) = ((πΉβπ)βπΆ)) |
129 | 5 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β π) β πΆ β π) |
130 | 103, 129 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β π) β ((πΉβπ)βπΆ) β β) |
131 | 128, 130 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β π) β ((π β π β¦ ((πΉβπ)βπΆ))βπ) β β) |
132 | 124 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (π = π β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)) = (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) |
133 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) = (π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) |
134 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)) β V |
135 | 132, 133,
134 | fvmpt 6953 |
. . . . . . . . . . . . 13
β’ (π β π β ((π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))βπ) = (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) |
136 | 135 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β π) β ((π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))βπ) = (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) |
137 | 128 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β π) β (((π β π β¦ ((πΉβπ)βπΆ))βπ) β ((πΉβπ)βπΆ)) = (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) |
138 | 136, 137 | eqtr4d 2780 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β π) β ((π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))βπ) = (((π β π β¦ ((πΉβπ)βπΆ))βπ) β ((πΉβπ)βπΆ))) |
139 | 78, 83, 121, 56, 123, 131, 138 | climsubc1 15527 |
. . . . . . . . . 10
β’ ((π β§ π) β (π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) β ((πΊβπΆ) β ((πΉβπ)βπΆ))) |
140 | 55 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β π) β ((πΉβπ)βπ) β β) |
141 | 105, 140 | subcld 11519 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β π) β (((πΉβπ)βπ) β ((πΉβπ)βπ)) β β) |
142 | 111, 141 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β π) β ((π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ)))βπ) β β) |
143 | 56 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β π) β ((πΉβπ)βπΆ) β β) |
144 | 130, 143 | subcld 11519 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β π) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)) β β) |
145 | 136, 144 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β π) β ((π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))βπ) β β) |
146 | 107, 132 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ (π = π β ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) = ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) |
147 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) = (π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) |
148 | | ovex 7395 |
. . . . . . . . . . . . 13
β’ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) β V |
149 | 146, 147,
148 | fvmpt 6953 |
. . . . . . . . . . . 12
β’ (π β π β ((π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))βπ) = ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) |
150 | 149 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β π) β ((π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))βπ) = ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) |
151 | 111, 136 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β π) β (((π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ)))βπ) β ((π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))βπ)) = ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) |
152 | 150, 151 | eqtr4d 2780 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β π) β ((π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))βπ) = (((π β π β¦ (((πΉβπ)βπ) β ((πΉβπ)βπ)))βπ) β ((π β π β¦ (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))βπ))) |
153 | 78, 83, 114, 116, 139, 142, 145, 152 | climsub 15523 |
. . . . . . . . 9
β’ ((π β§ π) β (π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) β (((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ)))) |
154 | 92 | mptex 7178 |
. . . . . . . . . 10
β’ (π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) β V |
155 | 154 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π) β (π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) β V) |
156 | 141, 144 | subcld 11519 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β π) β ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) β β) |
157 | 150, 156 | eqeltrd 2838 |
. . . . . . . . 9
β’ (((π β§ π) β§ π β π) β ((π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))βπ) β β) |
158 | 146 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = π β (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) = (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) |
159 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) = (π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) |
160 | | fvex 6860 |
. . . . . . . . . . . 12
β’
(absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) β V |
161 | 158, 159,
160 | fvmpt 6953 |
. . . . . . . . . . 11
β’ (π β π β ((π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))))βπ) = (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) |
162 | 161 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β π) β ((π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))))βπ) = (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) |
163 | 150 | fveq2d 6851 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β π) β (absβ((π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))βπ)) = (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) |
164 | 162, 163 | eqtr4d 2780 |
. . . . . . . . 9
β’ (((π β§ π) β§ π β π) β ((π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))))βπ) = (absβ((π β π β¦ ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))βπ))) |
165 | 78, 153, 155, 83, 157, 164 | climabs 15493 |
. . . . . . . 8
β’ ((π β§ π) β (π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) β (absβ(((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ))))) |
166 | 37 | abscld 15328 |
. . . . . . . . . . 11
β’ ((π β§ π) β (absβ(π β πΆ)) β β) |
167 | 66, 166 | remulcld 11192 |
. . . . . . . . . 10
β’ ((π β§ π) β (((π
/ 2) / 2) Β· (absβ(π β πΆ))) β β) |
168 | 167 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π) β (((π
/ 2) / 2) Β· (absβ(π β πΆ))) β β) |
169 | 78 | eqimss2i 4008 |
. . . . . . . . . 10
β’
(β€β₯βπ) β π |
170 | 169, 92 | climconst2 15437 |
. . . . . . . . 9
β’
(((((π
/ 2) / 2)
Β· (absβ(π
β πΆ))) β β
β§ π β β€)
β (π Γ {(((π
/ 2) / 2) Β·
(absβ(π β πΆ)))}) β (((π
/ 2) / 2) Β·
(absβ(π β πΆ)))) |
171 | 168, 83, 170 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π) β (π Γ {(((π
/ 2) / 2) Β· (absβ(π β πΆ)))}) β (((π
/ 2) / 2) Β· (absβ(π β πΆ)))) |
172 | 78 | uztrn2 12789 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
173 | 8, 172 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β (β€β₯βπ)) β π β π) |
174 | 173, 161 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))))βπ) = (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) |
175 | 156 | abscld 15328 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β π) β (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) β β) |
176 | 173, 175 | syldan 592 |
. . . . . . . . 9
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) β β) |
177 | 174, 176 | eqeltrd 2838 |
. . . . . . . 8
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))))βπ) β β) |
178 | | ovex 7395 |
. . . . . . . . . . 11
β’ (((π
/ 2) / 2) Β·
(absβ(π β πΆ))) β V |
179 | 178 | fvconst2 7158 |
. . . . . . . . . 10
β’ (π β π β ((π Γ {(((π
/ 2) / 2) Β· (absβ(π β πΆ)))})βπ) = (((π
/ 2) / 2) Β· (absβ(π β πΆ)))) |
180 | 173, 179 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((π Γ {(((π
/ 2) / 2) Β· (absβ(π β πΆ)))})βπ) = (((π
/ 2) / 2) Β· (absβ(π β πΆ)))) |
181 | 167 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (((π
/ 2) / 2) Β· (absβ(π β πΆ))) β β) |
182 | 180, 181 | eqeltrd 2838 |
. . . . . . . 8
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((π Γ {(((π
/ 2) / 2) Β· (absβ(π β πΆ)))})βπ) β β) |
183 | 173, 103 | syldan 592 |
. . . . . . . . . . . . . 14
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (πΉβπ):πβΆβ) |
184 | 183 | ffnd 6674 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (πΉβπ) Fn π) |
185 | 54 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (πΉβπ):πβΆβ) |
186 | 185 | ffnd 6674 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (πΉβπ) Fn π) |
187 | | ulmscl 25754 |
. . . . . . . . . . . . . . 15
β’ ((π β π β¦ (π D (πΉβπ)))(βπ’βπ)π» β π β V) |
188 | 19, 187 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β V) |
189 | 188 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β (β€β₯βπ)) β π β V) |
190 | 3 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β (β€β₯βπ)) β π β π) |
191 | | fnfvof 7639 |
. . . . . . . . . . . . 13
β’ ((((πΉβπ) Fn π β§ (πΉβπ) Fn π) β§ (π β V β§ π β π)) β (((πΉβπ) βf β (πΉβπ))βπ) = (((πΉβπ)βπ) β ((πΉβπ)βπ))) |
192 | 184, 186,
189, 190, 191 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (((πΉβπ) βf β (πΉβπ))βπ) = (((πΉβπ)βπ) β ((πΉβπ)βπ))) |
193 | 5 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β (β€β₯βπ)) β πΆ β π) |
194 | | fnfvof 7639 |
. . . . . . . . . . . . 13
β’ ((((πΉβπ) Fn π β§ (πΉβπ) Fn π) β§ (π β V β§ πΆ β π)) β (((πΉβπ) βf β (πΉβπ))βπΆ) = (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) |
195 | 184, 186,
189, 193, 194 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (((πΉβπ) βf β (πΉβπ))βπΆ) = (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))) |
196 | 192, 195 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((((πΉβπ) βf β (πΉβπ))βπ) β (((πΉβπ) βf β (πΉβπ))βπΆ)) = ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) |
197 | 196 | fveq2d 6851 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (absβ((((πΉβπ) βf β (πΉβπ))βπ) β (((πΉβπ) βf β (πΉβπ))βπΆ))) = (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ))))) |
198 | 29, 3 | sseldd 3950 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π) β π β π) |
199 | 29, 5 | sseldd 3950 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π) β πΆ β π) |
200 | 198, 199 | ovresd 7526 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π) β (π((abs β β ) βΎ (π Γ π))πΆ) = (π(abs β β )πΆ)) |
201 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’ (abs
β β ) = (abs β β ) |
202 | 201 | cnmetdval 24150 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ πΆ β β) β (π(abs β β )πΆ) = (absβ(π β πΆ))) |
203 | 35, 36, 202 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π) β (π(abs β β )πΆ) = (absβ(π β πΆ))) |
204 | 200, 203 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π) β (π((abs β β ) βΎ (π Γ π))πΆ) = (absβ(π β πΆ))) |
205 | | ulmdvlem1.a |
. . . . . . . . . . . . . . 15
β’ ((π β§ π) β (absβ(π β πΆ)) < π) |
206 | 204, 205 | eqbrtrd 5132 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β (π((abs β β ) βΎ (π Γ π))πΆ) < π) |
207 | | cnxmet 24152 |
. . . . . . . . . . . . . . . 16
β’ (abs
β β ) β (βMetββ) |
208 | | xmetres2 23730 |
. . . . . . . . . . . . . . . 16
β’ (((abs
β β ) β (βMetββ) β§ π β β) β ((abs β
β ) βΎ (π
Γ π)) β
(βMetβπ)) |
209 | 207, 33, 208 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π) β ((abs β β ) βΎ
(π Γ π)) β
(βMetβπ)) |
210 | | ulmdvlem1.u |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π) β π β
β+) |
211 | 210 | rpxrd 12965 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π) β π β
β*) |
212 | | elbl3 23761 |
. . . . . . . . . . . . . . 15
β’ (((((abs
β β ) βΎ (π Γ π)) β (βMetβπ) β§ π β β*) β§ (πΆ β π β§ π β π)) β (π β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π) β (π((abs β β ) βΎ (π Γ π))πΆ) < π)) |
213 | 209, 211,
199, 198, 212 | syl22anc 838 |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β (π β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π) β (π((abs β β ) βΎ (π Γ π))πΆ) < π)) |
214 | 206, 213 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β π β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π)) |
215 | 214 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β π β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π)) |
216 | | blcntr 23782 |
. . . . . . . . . . . . . 14
β’ ((((abs
β β ) βΎ (π Γ π)) β (βMetβπ) β§ πΆ β π β§ π β β+) β πΆ β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π)) |
217 | 209, 199,
210, 216 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π) β πΆ β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π)) |
218 | 217 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β πΆ β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π)) |
219 | 215, 218 | jca 513 |
. . . . . . . . . . 11
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π) β§ πΆ β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π))) |
220 | 30 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β π β {β, β}) |
221 | | eqid 2737 |
. . . . . . . . . . . 12
β’ ((abs
β β ) βΎ (π Γ π)) = ((abs β β ) βΎ (π Γ π)) |
222 | 29 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β π β π) |
223 | | fvexd 6862 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β ((πΉβπ)βπ¦) β V) |
224 | | fvexd 6862 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β ((πΉβπ)βπ¦) β V) |
225 | 183 | feqmptd 6915 |
. . . . . . . . . . . . . 14
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (πΉβπ) = (π¦ β π β¦ ((πΉβπ)βπ¦))) |
226 | 185 | feqmptd 6915 |
. . . . . . . . . . . . . 14
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (πΉβπ) = (π¦ β π β¦ ((πΉβπ)βπ¦))) |
227 | 189, 223,
224, 225, 226 | offval2 7642 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((πΉβπ) βf β (πΉβπ)) = (π¦ β π β¦ (((πΉβπ)βπ¦) β ((πΉβπ)βπ¦)))) |
228 | 183 | ffvelcdmda 7040 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β ((πΉβπ)βπ¦) β β) |
229 | 185 | ffvelcdmda 7040 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β ((πΉβπ)βπ¦) β β) |
230 | 228, 229 | subcld 11519 |
. . . . . . . . . . . . 13
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β (((πΉβπ)βπ¦) β ((πΉβπ)βπ¦)) β β) |
231 | 227, 230 | fmpt3d 7069 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((πΉβπ) βf β (πΉβπ)):πβΆβ) |
232 | 199 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β πΆ β π) |
233 | 211 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β π β
β*) |
234 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (πΆ(ballβ((abs β
β ) βΎ (π
Γ π)))π) = (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π) |
235 | | ulmdvlem1.b |
. . . . . . . . . . . . . 14
β’ ((π β§ π) β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π) β π) |
236 | 235 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π) β π) |
237 | 227 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D ((πΉβπ) βf β (πΉβπ))) = (π D (π¦ β π β¦ (((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))))) |
238 | | fvexd 6862 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β ((π D (πΉβπ))βπ¦) β V) |
239 | 225 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D (πΉβπ)) = (π D (π¦ β π β¦ ((πΉβπ)βπ¦)))) |
240 | 95 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (π D (πΉβπ)) = (π D (πΉβπ))) |
241 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π D (πΉβπ)) β V |
242 | 240, 11, 241 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β ((π β π β¦ (π D (πΉβπ)))βπ) = (π D (πΉβπ))) |
243 | 173, 242 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((π β π β¦ (π D (πΉβπ)))βπ) = (π D (πΉβπ))) |
244 | 21 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π β π β¦ (π D (πΉβπ))):πβΆ(β βm π)) |
245 | 244, 173 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((π β π β¦ (π D (πΉβπ)))βπ) β (β βm π)) |
246 | 243, 245 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D (πΉβπ)) β (β βm π)) |
247 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π D (πΉβπ)) β (β βm π) β (π D (πΉβπ)):πβΆβ) |
248 | 246, 247 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D (πΉβπ)):πβΆβ) |
249 | 248 | feqmptd 6915 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D (πΉβπ)) = (π¦ β π β¦ ((π D (πΉβπ))βπ¦))) |
250 | 239, 249 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D (π¦ β π β¦ ((πΉβπ)βπ¦))) = (π¦ β π β¦ ((π D (πΉβπ))βπ¦))) |
251 | | fvexd 6862 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β ((π D (πΉβπ))βπ¦) β V) |
252 | 226 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D (πΉβπ)) = (π D (π¦ β π β¦ ((πΉβπ)βπ¦)))) |
253 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D (πΉβπ)):πβΆβ) |
254 | 253 | feqmptd 6915 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D (πΉβπ)) = (π¦ β π β¦ ((π D (πΉβπ))βπ¦))) |
255 | 252, 254 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D (π¦ β π β¦ ((πΉβπ)βπ¦))) = (π¦ β π β¦ ((π D (πΉβπ))βπ¦))) |
256 | 220, 228,
238, 250, 229, 251, 255 | dvmptsub 25347 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D (π¦ β π β¦ (((πΉβπ)βπ¦) β ((πΉβπ)βπ¦)))) = (π¦ β π β¦ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)))) |
257 | 237, 256 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (π D ((πΉβπ) βf β (πΉβπ))) = (π¦ β π β¦ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)))) |
258 | 257 | dmeqd 5866 |
. . . . . . . . . . . . . 14
β’ (((π β§ π) β§ π β (β€β₯βπ)) β dom (π D ((πΉβπ) βf β (πΉβπ))) = dom (π¦ β π β¦ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)))) |
259 | | ovex 7395 |
. . . . . . . . . . . . . . 15
β’ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)) β V |
260 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π β¦ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) = (π¦ β π β¦ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) |
261 | 259, 260 | dmmpti 6650 |
. . . . . . . . . . . . . 14
β’ dom
(π¦ β π β¦ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) = π |
262 | 258, 261 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (((π β§ π) β§ π β (β€β₯βπ)) β dom (π D ((πΉβπ) βf β (πΉβπ))) = π) |
263 | 236, 262 | sseqtrrd 3990 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π) β dom (π D ((πΉβπ) βf β (πΉβπ)))) |
264 | 66 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((π
/ 2) / 2) β β) |
265 | 236 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π)) β π¦ β π) |
266 | 257 | fveq1d 6849 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((π D ((πΉβπ) βf β (πΉβπ)))βπ¦) = ((π¦ β π β¦ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)))βπ¦)) |
267 | 260 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ β π β§ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)) β V) β ((π¦ β π β¦ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)))βπ¦) = (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) |
268 | 259, 267 | mpan2 690 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π β ((π¦ β π β¦ (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)))βπ¦) = (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) |
269 | 266, 268 | sylan9eq 2797 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β ((π D ((πΉβπ) βf β (πΉβπ)))βπ¦) = (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) |
270 | 269 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β (absβ((π D ((πΉβπ) βf β (πΉβπ)))βπ¦)) = (absβ(((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)))) |
271 | 259 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)) β V) |
272 | 220, 230,
271, 256 | dvmptcl 25339 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)) β β) |
273 | 272 | abscld 15328 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β (absβ(((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) β β) |
274 | 66 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β ((π
/ 2) / 2) β β) |
275 | 248 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β ((π D (πΉβπ))βπ¦) β β) |
276 | 253 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β ((π D (πΉβπ))βπ¦) β β) |
277 | 275, 276 | abssubd 15345 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β (absβ(((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) = (absβ(((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)))) |
278 | | ulmdvlem1.1 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π) β βπ β (β€β₯βπ)βπ₯ β π (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π
/ 2) / 2)) |
279 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β (πΉβπ) = (πΉβπ)) |
280 | 279 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (π D (πΉβπ)) = (π D (πΉβπ))) |
281 | 280 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β ((π D (πΉβπ))βπ₯) = ((π D (πΉβπ))βπ₯)) |
282 | 281 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯)) = (((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) |
283 | 282 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) = (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯)))) |
284 | 283 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π
/ 2) / 2) β (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π
/ 2) / 2))) |
285 | 284 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (βπ₯ β π (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π
/ 2) / 2) β βπ₯ β π (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π
/ 2) / 2))) |
286 | 285 | rspccva 3583 |
. . . . . . . . . . . . . . . . . 18
β’
((βπ β
(β€β₯βπ)βπ₯ β π (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π
/ 2) / 2) β§ π β (β€β₯βπ)) β βπ₯ β π (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π
/ 2) / 2)) |
287 | 278, 286 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π) β§ π β (β€β₯βπ)) β βπ₯ β π (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π
/ 2) / 2)) |
288 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π¦ β ((π D (πΉβπ))βπ₯) = ((π D (πΉβπ))βπ¦)) |
289 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π¦ β ((π D (πΉβπ))βπ₯) = ((π D (πΉβπ))βπ¦)) |
290 | 288, 289 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π¦ β (((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯)) = (((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) |
291 | 290 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π¦ β (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) = (absβ(((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦)))) |
292 | 291 | breq1d 5120 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β ((absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π
/ 2) / 2) β (absβ(((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) < ((π
/ 2) / 2))) |
293 | 292 | rspccva 3583 |
. . . . . . . . . . . . . . . . 17
β’
((βπ₯ β
π (absβ(((π D (πΉβπ))βπ₯) β ((π D (πΉβπ))βπ₯))) < ((π
/ 2) / 2) β§ π¦ β π) β (absβ(((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) < ((π
/ 2) / 2)) |
294 | 287, 293 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β (absβ(((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) < ((π
/ 2) / 2)) |
295 | 277, 294 | eqbrtrd 5132 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β (absβ(((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) < ((π
/ 2) / 2)) |
296 | 273, 274,
295 | ltled 11310 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β (absβ(((π D (πΉβπ))βπ¦) β ((π D (πΉβπ))βπ¦))) β€ ((π
/ 2) / 2)) |
297 | 270, 296 | eqbrtrd 5132 |
. . . . . . . . . . . . 13
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β π) β (absβ((π D ((πΉβπ) βf β (πΉβπ)))βπ¦)) β€ ((π
/ 2) / 2)) |
298 | 265, 297 | syldan 592 |
. . . . . . . . . . . 12
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ π¦ β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π)) β (absβ((π D ((πΉβπ) βf β (πΉβπ)))βπ¦)) β€ ((π
/ 2) / 2)) |
299 | 220, 221,
222, 231, 232, 233, 234, 263, 264, 298 | dvlip2 25375 |
. . . . . . . . . . 11
β’ ((((π β§ π) β§ π β (β€β₯βπ)) β§ (π β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π) β§ πΆ β (πΆ(ballβ((abs β β ) βΎ
(π Γ π)))π))) β (absβ((((πΉβπ) βf β (πΉβπ))βπ) β (((πΉβπ) βf β (πΉβπ))βπΆ))) β€ (((π
/ 2) / 2) Β· (absβ(π β πΆ)))) |
300 | 219, 299 | mpdan 686 |
. . . . . . . . . 10
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (absβ((((πΉβπ) βf β (πΉβπ))βπ) β (((πΉβπ) βf β (πΉβπ))βπΆ))) β€ (((π
/ 2) / 2) Β· (absβ(π β πΆ)))) |
301 | 197, 300 | eqbrtrrd 5134 |
. . . . . . . . 9
β’ (((π β§ π) β§ π β (β€β₯βπ)) β (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))) β€ (((π
/ 2) / 2) Β· (absβ(π β πΆ)))) |
302 | 301, 174,
180 | 3brtr4d 5142 |
. . . . . . . 8
β’ (((π β§ π) β§ π β (β€β₯βπ)) β ((π β π β¦ (absβ((((πΉβπ)βπ) β ((πΉβπ)βπ)) β (((πΉβπ)βπΆ) β ((πΉβπ)βπΆ)))))βπ) β€ ((π Γ {(((π
/ 2) / 2) Β· (absβ(π β πΆ)))})βπ)) |
303 | 77, 81, 165, 171, 177, 182, 302 | climle 15529 |
. . . . . . 7
β’ ((π β§ π) β (absβ(((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ)))) β€ (((π
/ 2) / 2) Β· (absβ(π β πΆ)))) |
304 | 74 | abscld 15328 |
. . . . . . . 8
β’ ((π β§ π) β (absβ(((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ)))) β β) |
305 | 37, 39 | absrpcld 15340 |
. . . . . . . 8
β’ ((π β§ π) β (absβ(π β πΆ)) β
β+) |
306 | 304, 66, 305 | ledivmul2d 13018 |
. . . . . . 7
β’ ((π β§ π) β (((absβ(((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ)))) / (absβ(π β πΆ))) β€ ((π
/ 2) / 2) β (absβ(((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ)))) β€ (((π
/ 2) / 2) Β· (absβ(π β πΆ))))) |
307 | 303, 306 | mpbird 257 |
. . . . . 6
β’ ((π β§ π) β ((absβ(((πΊβπ) β ((πΉβπ)βπ)) β ((πΊβπΆ) β ((πΉβπ)βπΆ)))) / (absβ(π β πΆ))) β€ ((π
/ 2) / 2)) |
308 | 76, 307 | eqbrtrd 5132 |
. . . . 5
β’ ((π β§ π) β (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)))) β€ ((π
/ 2) / 2)) |
309 | 210 | rpred 12964 |
. . . . . . 7
β’ ((π β§ π) β π β β) |
310 | | ulmdvlem1.v |
. . . . . . . 8
β’ ((π β§ π) β π β
β+) |
311 | 310 | rpred 12964 |
. . . . . . 7
β’ ((π β§ π) β π β β) |
312 | | ulmdvlem1.l |
. . . . . . 7
β’ ((π β§ π) β π < π) |
313 | 166, 309,
311, 205, 312 | lttrd 11323 |
. . . . . 6
β’ ((π β§ π) β (absβ(π β πΆ)) < π) |
314 | | ulmdvlem1.4 |
. . . . . 6
β’ ((π β§ π) β ((absβ(π β πΆ)) < π β (absβ(((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ))) < ((π
/ 2) / 2))) |
315 | 313, 314 | mpd 15 |
. . . . 5
β’ ((π β§ π) β (absβ(((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ))) < ((π
/ 2) / 2)) |
316 | 60, 62, 66, 66, 308, 315 | leltaddd 11784 |
. . . 4
β’ ((π β§ π) β ((absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)))) + (absβ(((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ)))) < (((π
/ 2) / 2) + ((π
/ 2) / 2))) |
317 | 64 | recnd 11190 |
. . . . 5
β’ ((π β§ π) β (π
/ 2) β β) |
318 | 317 | 2halvesd 12406 |
. . . 4
β’ ((π β§ π) β (((π
/ 2) / 2) + ((π
/ 2) / 2)) = (π
/ 2)) |
319 | 316, 318 | breqtrd 5136 |
. . 3
β’ ((π β§ π) β ((absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)))) + (absβ(((((πΉβπ)βπ) β ((πΉβπ)βπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ)))) < (π
/ 2)) |
320 | 49, 63, 64, 65, 319 | lelttrd 11320 |
. 2
β’ ((π β§ π) β (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β ((π D (πΉβπ))βπΆ))) < (π
/ 2)) |
321 | | ulmdvlem1.2 |
. 2
β’ ((π β§ π) β (absβ(((π D (πΉβπ))βπΆ) β (π»βπΆ))) < (π
/ 2)) |
322 | 40, 44, 45, 47, 320, 321 | abs3lemd 15353 |
1
β’ ((π β§ π) β (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β (π»βπΆ))) < π
) |