Step | Hyp | Ref
| Expression |
1 | | dvlip2.j |
. . . . . . . 8
β’ π½ = ((abs β β )
βΎ (π Γ π)) |
2 | | cnxmet 24159 |
. . . . . . . . 9
β’ (abs
β β ) β (βMetββ) |
3 | | dvlip2.s |
. . . . . . . . . 10
β’ (π β π β {β, β}) |
4 | | recnprss 25291 |
. . . . . . . . . 10
β’ (π β {β, β}
β π β
β) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
β’ (π β π β β) |
6 | | xmetres2 23737 |
. . . . . . . . 9
β’ (((abs
β β ) β (βMetββ) β§ π β β) β ((abs β
β ) βΎ (π
Γ π)) β
(βMetβπ)) |
7 | 2, 5, 6 | sylancr 588 |
. . . . . . . 8
β’ (π β ((abs β β )
βΎ (π Γ π)) β
(βMetβπ)) |
8 | 1, 7 | eqeltrid 2838 |
. . . . . . 7
β’ (π β π½ β (βMetβπ)) |
9 | 8 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π½ β (βMetβπ)) |
10 | | dvlip2.a |
. . . . . . 7
β’ (π β π΄ β π) |
11 | 10 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π΄ β π) |
12 | | simplrr 777 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π β π΅) |
13 | | dvlip2.b |
. . . . . . . . 9
β’ π΅ = (π΄(ballβπ½)π
) |
14 | 12, 13 | eleqtrdi 2844 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π β (π΄(ballβπ½)π
)) |
15 | | dvlip2.r |
. . . . . . . . . 10
β’ (π β π
β
β*) |
16 | 15 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π
β
β*) |
17 | | elbl 23764 |
. . . . . . . . 9
β’ ((π½ β (βMetβπ) β§ π΄ β π β§ π
β β*) β (π β (π΄(ballβπ½)π
) β (π β π β§ (π΄π½π) < π
))) |
18 | 9, 11, 16, 17 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π β (π΄(ballβπ½)π
) β (π β π β§ (π΄π½π) < π
))) |
19 | 14, 18 | mpbid 231 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π β π β§ (π΄π½π) < π
)) |
20 | 19 | simpld 496 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π β π) |
21 | | xmetcl 23707 |
. . . . . 6
β’ ((π½ β (βMetβπ) β§ π΄ β π β§ π β π) β (π΄π½π) β
β*) |
22 | 9, 11, 20, 21 | syl3anc 1372 |
. . . . 5
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄π½π) β
β*) |
23 | | simplrl 776 |
. . . . . . . . 9
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π β π΅) |
24 | 23, 13 | eleqtrdi 2844 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π β (π΄(ballβπ½)π
)) |
25 | | elbl 23764 |
. . . . . . . . 9
β’ ((π½ β (βMetβπ) β§ π΄ β π β§ π
β β*) β (π β (π΄(ballβπ½)π
) β (π β π β§ (π΄π½π) < π
))) |
26 | 9, 11, 16, 25 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π β (π΄(ballβπ½)π
) β (π β π β§ (π΄π½π) < π
))) |
27 | 24, 26 | mpbid 231 |
. . . . . . 7
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π β π β§ (π΄π½π) < π
)) |
28 | 27 | simpld 496 |
. . . . . 6
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π β π) |
29 | | xmetcl 23707 |
. . . . . 6
β’ ((π½ β (βMetβπ) β§ π΄ β π β§ π β π) β (π΄π½π) β
β*) |
30 | 9, 11, 28, 29 | syl3anc 1372 |
. . . . 5
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄π½π) β
β*) |
31 | 22, 30 | ifcld 4536 |
. . . 4
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) β
β*) |
32 | 19 | simprd 497 |
. . . . 5
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄π½π) < π
) |
33 | 27 | simprd 497 |
. . . . 5
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄π½π) < π
) |
34 | | breq1 5112 |
. . . . . 6
β’ ((π΄π½π) = if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) β ((π΄π½π) < π
β if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π
)) |
35 | | breq1 5112 |
. . . . . 6
β’ ((π΄π½π) = if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) β ((π΄π½π) < π
β if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π
)) |
36 | 34, 35 | ifboth 4529 |
. . . . 5
β’ (((π΄π½π) < π
β§ (π΄π½π) < π
) β if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π
) |
37 | 32, 33, 36 | syl2anc 585 |
. . . 4
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π
) |
38 | | qbtwnxr 13128 |
. . . 4
β’
((if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) β β* β§ π
β β*
β§ if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π
) β βπ β β (if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π β§ π < π
)) |
39 | 31, 16, 37, 38 | syl3anc 1372 |
. . 3
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β βπ β β (if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π β§ π < π
)) |
40 | | qre 12886 |
. . . . 5
β’ (π β β β π β
β) |
41 | | rexr 11209 |
. . . . . . . 8
β’ (π β β β π β
β*) |
42 | | xrmaxlt 13109 |
. . . . . . . 8
β’ (((π΄π½π) β β* β§ (π΄π½π) β β* β§ π β β*)
β (if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π β ((π΄π½π) < π β§ (π΄π½π) < π))) |
43 | 30, 22, 41, 42 | syl2an3an 1423 |
. . . . . . 7
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β (if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π β ((π΄π½π) < π β§ (π΄π½π) < π))) |
44 | | ioossicc 13359 |
. . . . . . . . . . . . 13
β’ ((π΄ β π)(,)(π΄ + π)) β ((π΄ β π)[,](π΄ + π)) |
45 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π = β) |
46 | 28, 45 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π β β) |
47 | 46 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π β β) |
48 | | xmetsym 23723 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ β (βMetβπ) β§ π΄ β π β§ π β π) β (π΄π½π) = (ππ½π΄)) |
49 | 9, 11, 28, 48 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄π½π) = (ππ½π΄)) |
50 | 45 | sqxpeqd 5669 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π Γ π) = (β Γ
β)) |
51 | 50 | reseq2d 5941 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β ((abs β β )
βΎ (π Γ π)) = ((abs β β )
βΎ (β Γ β))) |
52 | 1, 51 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π½ = ((abs β β ) βΎ (β
Γ β))) |
53 | 52 | oveqd 7378 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (ππ½π΄) = (π((abs β β ) βΎ (β
Γ β))π΄)) |
54 | 11, 45 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π΄ β β) |
55 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
56 | 55 | remetdval 24175 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π΄ β β) β (π((abs β β ) βΎ
(β Γ β))π΄) = (absβ(π β π΄))) |
57 | 46, 54, 56 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π((abs β β ) βΎ (β
Γ β))π΄) =
(absβ(π β π΄))) |
58 | 49, 53, 57 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄π½π) = (absβ(π β π΄))) |
59 | 58 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π΄π½π) = (absβ(π β π΄))) |
60 | | simprll 778 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π΄π½π) < π) |
61 | 59, 60 | eqbrtrrd 5133 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (absβ(π β π΄)) < π) |
62 | 54 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π΄ β β) |
63 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π β β) |
64 | 47, 62, 63 | absdifltd 15327 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((absβ(π β π΄)) < π β ((π΄ β π) < π β§ π < (π΄ + π)))) |
65 | 61, 64 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((π΄ β π) < π β§ π < (π΄ + π))) |
66 | 65 | simpld 496 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π΄ β π) < π) |
67 | 65 | simprd 497 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π < (π΄ + π)) |
68 | 62, 63 | resubcld 11591 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π΄ β π) β β) |
69 | 68 | rexrd 11213 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π΄ β π) β
β*) |
70 | 62, 63 | readdcld 11192 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π΄ + π) β β) |
71 | 70 | rexrd 11213 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π΄ + π) β
β*) |
72 | | elioo2 13314 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β π) β β* β§ (π΄ + π) β β*) β (π β ((π΄ β π)(,)(π΄ + π)) β (π β β β§ (π΄ β π) < π β§ π < (π΄ + π)))) |
73 | 69, 71, 72 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π β ((π΄ β π)(,)(π΄ + π)) β (π β β β§ (π΄ β π) < π β§ π < (π΄ + π)))) |
74 | 47, 66, 67, 73 | mpbir3and 1343 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π β ((π΄ β π)(,)(π΄ + π))) |
75 | 44, 74 | sselid 3946 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π β ((π΄ β π)[,](π΄ + π))) |
76 | 75 | fvresd 6866 |
. . . . . . . . . . 11
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ) = (πΉβπ)) |
77 | 20, 45 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π β β) |
78 | 77 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π β β) |
79 | | xmetsym 23723 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ β (βMetβπ) β§ π΄ β π β§ π β π) β (π΄π½π) = (ππ½π΄)) |
80 | 9, 11, 20, 79 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄π½π) = (ππ½π΄)) |
81 | 52 | oveqd 7378 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (ππ½π΄) = (π((abs β β ) βΎ (β
Γ β))π΄)) |
82 | 55 | remetdval 24175 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π΄ β β) β (π((abs β β ) βΎ
(β Γ β))π΄) = (absβ(π β π΄))) |
83 | 77, 54, 82 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π((abs β β ) βΎ (β
Γ β))π΄) =
(absβ(π β π΄))) |
84 | 80, 81, 83 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄π½π) = (absβ(π β π΄))) |
85 | 84 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π΄π½π) = (absβ(π β π΄))) |
86 | | simprlr 779 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π΄π½π) < π) |
87 | 85, 86 | eqbrtrrd 5133 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (absβ(π β π΄)) < π) |
88 | 78, 62, 63 | absdifltd 15327 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((absβ(π β π΄)) < π β ((π΄ β π) < π β§ π < (π΄ + π)))) |
89 | 87, 88 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((π΄ β π) < π β§ π < (π΄ + π))) |
90 | 89 | simpld 496 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π΄ β π) < π) |
91 | 89 | simprd 497 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π < (π΄ + π)) |
92 | | elioo2 13314 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β π) β β* β§ (π΄ + π) β β*) β (π β ((π΄ β π)(,)(π΄ + π)) β (π β β β§ (π΄ β π) < π β§ π < (π΄ + π)))) |
93 | 69, 71, 92 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π β ((π΄ β π)(,)(π΄ + π)) β (π β β β§ (π΄ β π) < π β§ π < (π΄ + π)))) |
94 | 78, 90, 91, 93 | mpbir3and 1343 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π β ((π΄ β π)(,)(π΄ + π))) |
95 | 44, 94 | sselid 3946 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π β ((π΄ β π)[,](π΄ + π))) |
96 | 95 | fvresd 6866 |
. . . . . . . . . . 11
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ) = (πΉβπ)) |
97 | 76, 96 | oveq12d 7379 |
. . . . . . . . . 10
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ) β ((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ)) = ((πΉβπ) β (πΉβπ))) |
98 | 97 | fveq2d 6850 |
. . . . . . . . 9
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (absβ(((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ) β ((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ))) = (absβ((πΉβπ) β (πΉβπ)))) |
99 | 9 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π½ β (βMetβπ)) |
100 | | elicc2 13338 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π΄ β π) β β β§ (π΄ + π) β β) β (π₯ β ((π΄ β π)[,](π΄ + π)) β (π₯ β β β§ (π΄ β π) β€ π₯ β§ π₯ β€ (π΄ + π)))) |
101 | 68, 70, 100 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π₯ β ((π΄ β π)[,](π΄ + π)) β (π₯ β β β§ (π΄ β π) β€ π₯ β§ π₯ β€ (π΄ + π)))) |
102 | 101 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β (π₯ β β β§ (π΄ β π) β€ π₯ β§ π₯ β€ (π΄ + π))) |
103 | 102 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π₯ β β) |
104 | 45 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π = β) |
105 | 103, 104 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π₯ β π) |
106 | 11 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π΄ β π) |
107 | | xmetcl 23707 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ β (βMetβπ) β§ π₯ β π β§ π΄ β π) β (π₯π½π΄) β
β*) |
108 | 99, 105, 106, 107 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β (π₯π½π΄) β
β*) |
109 | 63 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π β β) |
110 | 109 | rexrd 11213 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π β β*) |
111 | 16 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π
β
β*) |
112 | 52 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π½ = ((abs β β ) βΎ (β
Γ β))) |
113 | 112 | oveqd 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β (π₯π½π΄) = (π₯((abs β β ) βΎ (β
Γ β))π΄)) |
114 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π΄ β β) |
115 | 55 | remetdval 24175 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β β β§ π΄ β β) β (π₯((abs β β ) βΎ
(β Γ β))π΄) = (absβ(π₯ β π΄))) |
116 | 103, 114,
115 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β (π₯((abs β β ) βΎ (β
Γ β))π΄) =
(absβ(π₯ β π΄))) |
117 | 113, 116 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β (π₯π½π΄) = (absβ(π₯ β π΄))) |
118 | 102 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β (π΄ β π) β€ π₯) |
119 | 102 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π₯ β€ (π΄ + π)) |
120 | 103, 114,
109 | absdifled 15328 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β ((absβ(π₯ β π΄)) β€ π β ((π΄ β π) β€ π₯ β§ π₯ β€ (π΄ + π)))) |
121 | 118, 119,
120 | mpbir2and 712 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β (absβ(π₯ β π΄)) β€ π) |
122 | 117, 121 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β (π₯π½π΄) β€ π) |
123 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π < π
) |
124 | 108, 110,
111, 122, 123 | xrlelttrd 13088 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β (π₯π½π΄) < π
) |
125 | | elbl3 23768 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π½ β (βMetβπ) β§ π
β β*) β§ (π΄ β π β§ π₯ β π)) β (π₯ β (π΄(ballβπ½)π
) β (π₯π½π΄) < π
)) |
126 | 99, 111, 106, 105, 125 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β (π₯ β (π΄(ballβπ½)π
) β (π₯π½π΄) < π
)) |
127 | 124, 126 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)[,](π΄ + π))) β π₯ β (π΄(ballβπ½)π
)) |
128 | 127 | ex 414 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (π₯ β ((π΄ β π)[,](π΄ + π)) β π₯ β (π΄(ballβπ½)π
))) |
129 | 128 | ssrdv 3954 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((π΄ β π)[,](π΄ + π)) β (π΄(ballβπ½)π
)) |
130 | 129, 13 | sseqtrrdi 3999 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((π΄ β π)[,](π΄ + π)) β π΅) |
131 | 130 | resabs1d 5972 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((πΉ βΎ π΅) βΎ ((π΄ β π)[,](π΄ + π))) = (πΉ βΎ ((π΄ β π)[,](π΄ + π)))) |
132 | | ax-resscn 11116 |
. . . . . . . . . . . . . . . 16
β’ β
β β |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β β β
β) |
134 | | dvlip2.f |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:πβΆβ) |
135 | 134 | ad4antr 731 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β πΉ:πβΆβ) |
136 | | dvlip2.d |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΅ β dom (π D πΉ)) |
137 | | dvlip2.x |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β π) |
138 | 5, 134, 137 | dvbss 25288 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom (π D πΉ) β π) |
139 | 136, 138 | sstrd 3958 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΅ β π) |
140 | 139 | ad4antr 731 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π΅ β π) |
141 | 135, 140 | fssresd 6713 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (πΉ βΎ π΅):π΅βΆβ) |
142 | | blssm 23794 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π½ β (βMetβπ) β§ π΄ β π β§ π
β β*) β (π΄(ballβπ½)π
) β π) |
143 | 9, 11, 16, 142 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄(ballβπ½)π
) β π) |
144 | 13, 143 | eqsstrid 3996 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π΅ β π) |
145 | 144, 45 | sseqtrd 3988 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π΅ β β) |
146 | 145 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π΅ β β) |
147 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β β β
β) |
148 | 134 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β πΉ:πβΆβ) |
149 | 137 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π β π) |
150 | 149, 45 | sseqtrd 3988 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π β β) |
151 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(TopOpenββfld) =
(TopOpenββfld) |
152 | 151 | tgioo2 24189 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
153 | 151, 152 | dvres 25298 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β β β β§ πΉ:πβΆβ) β§ (π β β β§ π΅ β β)) β (β D (πΉ βΎ π΅)) = ((β D πΉ) βΎ ((intβ(topGenβran
(,)))βπ΅))) |
154 | 147, 148,
150, 145, 153 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (β D (πΉ βΎ π΅)) = ((β D πΉ) βΎ ((intβ(topGenβran
(,)))βπ΅))) |
155 | | retop 24148 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(topGenβran (,)) β Top |
156 | 52 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (ballβπ½) = (ballβ((abs β
β ) βΎ (β Γ β)))) |
157 | 156 | oveqd 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄(ballβπ½)π
) = (π΄(ballβ((abs β β ) βΎ
(β Γ β)))π
)) |
158 | 13, 157 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π΅ = (π΄(ballβ((abs β β ) βΎ
(β Γ β)))π
)) |
159 | 52, 9 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β ((abs β β )
βΎ (β Γ β)) β (βMetβπ)) |
160 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(MetOpenβ((abs β β ) βΎ (β Γ
β))) = (MetOpenβ((abs β β ) βΎ (β Γ
β))) |
161 | 55, 160 | tgioo 24182 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(topGenβran (,)) = (MetOpenβ((abs β β ) βΎ
(β Γ β))) |
162 | 161 | blopn 23879 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((abs
β β ) βΎ (β Γ β)) β
(βMetβπ) β§
π΄ β π β§ π
β β*) β (π΄(ballβ((abs β
β ) βΎ (β Γ β)))π
) β (topGenβran
(,))) |
163 | 159, 11, 16, 162 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΄(ballβ((abs β β ) βΎ
(β Γ β)))π
) β (topGenβran
(,))) |
164 | 158, 163 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π΅ β (topGenβran
(,))) |
165 | | isopn3i 22456 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((topGenβran (,)) β Top β§ π΅ β (topGenβran (,))) β
((intβ(topGenβran (,)))βπ΅) = π΅) |
166 | 155, 164,
165 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β
((intβ(topGenβran (,)))βπ΅) = π΅) |
167 | 166 | reseq2d 5941 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β ((β D πΉ) βΎ
((intβ(topGenβran (,)))βπ΅)) = ((β D πΉ) βΎ π΅)) |
168 | 154, 167 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (β D (πΉ βΎ π΅)) = ((β D πΉ) βΎ π΅)) |
169 | 168 | dmeqd 5865 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β dom (β D (πΉ βΎ π΅)) = dom ((β D πΉ) βΎ π΅)) |
170 | | dmres 5963 |
. . . . . . . . . . . . . . . . . 18
β’ dom
((β D πΉ) βΎ
π΅) = (π΅ β© dom (β D πΉ)) |
171 | 136 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π΅ β dom (π D πΉ)) |
172 | 45 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π D πΉ) = (β D πΉ)) |
173 | 172 | dmeqd 5865 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β dom (π D πΉ) = dom (β D πΉ)) |
174 | 171, 173 | sseqtrd 3988 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β π΅ β dom (β D πΉ)) |
175 | | df-ss 3931 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΅ β dom (β D πΉ) β (π΅ β© dom (β D πΉ)) = π΅) |
176 | 174, 175 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (π΅ β© dom (β D πΉ)) = π΅) |
177 | 170, 176 | eqtrid 2785 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β dom ((β D πΉ) βΎ π΅) = π΅) |
178 | 169, 177 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β dom (β D (πΉ βΎ π΅)) = π΅) |
179 | 178 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β dom (β D (πΉ βΎ π΅)) = π΅) |
180 | | dvcn 25308 |
. . . . . . . . . . . . . . 15
β’
(((β β β β§ (πΉ βΎ π΅):π΅βΆβ β§ π΅ β β) β§ dom (β D
(πΉ βΎ π΅)) = π΅) β (πΉ βΎ π΅) β (π΅βcnββ)) |
181 | 133, 141,
146, 179, 180 | syl31anc 1374 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (πΉ βΎ π΅) β (π΅βcnββ)) |
182 | | rescncf 24283 |
. . . . . . . . . . . . . 14
β’ (((π΄ β π)[,](π΄ + π)) β π΅ β ((πΉ βΎ π΅) β (π΅βcnββ) β ((πΉ βΎ π΅) βΎ ((π΄ β π)[,](π΄ + π))) β (((π΄ β π)[,](π΄ + π))βcnββ))) |
183 | 130, 181,
182 | sylc 65 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((πΉ βΎ π΅) βΎ ((π΄ β π)[,](π΄ + π))) β (((π΄ β π)[,](π΄ + π))βcnββ)) |
184 | 131, 183 | eqeltrrd 2835 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (πΉ βΎ ((π΄ β π)[,](π΄ + π))) β (((π΄ β π)[,](π΄ + π))βcnββ)) |
185 | 130, 146 | sstrd 3958 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((π΄ β π)[,](π΄ + π)) β β) |
186 | 151, 152 | dvres 25298 |
. . . . . . . . . . . . . . . 16
β’
(((β β β β§ (πΉ βΎ π΅):π΅βΆβ) β§ (π΅ β β β§ ((π΄ β π)[,](π΄ + π)) β β)) β (β D
((πΉ βΎ π΅) βΎ ((π΄ β π)[,](π΄ + π)))) = ((β D (πΉ βΎ π΅)) βΎ ((intβ(topGenβran
(,)))β((π΄ β
π)[,](π΄ + π))))) |
187 | 133, 141,
146, 185, 186 | syl22anc 838 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (β D ((πΉ βΎ π΅) βΎ ((π΄ β π)[,](π΄ + π)))) = ((β D (πΉ βΎ π΅)) βΎ ((intβ(topGenβran
(,)))β((π΄ β
π)[,](π΄ + π))))) |
188 | 131 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (β D ((πΉ βΎ π΅) βΎ ((π΄ β π)[,](π΄ + π)))) = (β D (πΉ βΎ ((π΄ β π)[,](π΄ + π))))) |
189 | | iccntr 24207 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β π) β β β§ (π΄ + π) β β) β
((intβ(topGenβran (,)))β((π΄ β π)[,](π΄ + π))) = ((π΄ β π)(,)(π΄ + π))) |
190 | 68, 70, 189 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((intβ(topGenβran
(,)))β((π΄ β
π)[,](π΄ + π))) = ((π΄ β π)(,)(π΄ + π))) |
191 | 190 | reseq2d 5941 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((β D (πΉ βΎ π΅)) βΎ ((intβ(topGenβran
(,)))β((π΄ β
π)[,](π΄ + π)))) = ((β D (πΉ βΎ π΅)) βΎ ((π΄ β π)(,)(π΄ + π)))) |
192 | 187, 188,
191 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (β D (πΉ βΎ ((π΄ β π)[,](π΄ + π)))) = ((β D (πΉ βΎ π΅)) βΎ ((π΄ β π)(,)(π΄ + π)))) |
193 | 192 | dmeqd 5865 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β dom (β D (πΉ βΎ ((π΄ β π)[,](π΄ + π)))) = dom ((β D (πΉ βΎ π΅)) βΎ ((π΄ β π)(,)(π΄ + π)))) |
194 | | dmres 5963 |
. . . . . . . . . . . . . 14
β’ dom
((β D (πΉ βΎ
π΅)) βΎ ((π΄ β π)(,)(π΄ + π))) = (((π΄ β π)(,)(π΄ + π)) β© dom (β D (πΉ βΎ π΅))) |
195 | 44, 130 | sstrid 3959 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((π΄ β π)(,)(π΄ + π)) β π΅) |
196 | 195, 179 | sseqtrrd 3989 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((π΄ β π)(,)(π΄ + π)) β dom (β D (πΉ βΎ π΅))) |
197 | | df-ss 3931 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β π)(,)(π΄ + π)) β dom (β D (πΉ βΎ π΅)) β (((π΄ β π)(,)(π΄ + π)) β© dom (β D (πΉ βΎ π΅))) = ((π΄ β π)(,)(π΄ + π))) |
198 | 196, 197 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (((π΄ β π)(,)(π΄ + π)) β© dom (β D (πΉ βΎ π΅))) = ((π΄ β π)(,)(π΄ + π))) |
199 | 194, 198 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β dom ((β D (πΉ βΎ π΅)) βΎ ((π΄ β π)(,)(π΄ + π))) = ((π΄ β π)(,)(π΄ + π))) |
200 | 193, 199 | eqtrd 2773 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β dom (β D (πΉ βΎ ((π΄ β π)[,](π΄ + π)))) = ((π΄ β π)(,)(π΄ + π))) |
201 | | dvlip2.m |
. . . . . . . . . . . . 13
β’ (π β π β β) |
202 | 201 | ad4antr 731 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π β β) |
203 | 192 | fveq1d 6848 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((β D (πΉ βΎ ((π΄ β π)[,](π΄ + π))))βπ₯) = (((β D (πΉ βΎ π΅)) βΎ ((π΄ β π)(,)(π΄ + π)))βπ₯)) |
204 | | fvres 6865 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β ((π΄ β π)(,)(π΄ + π)) β (((β D (πΉ βΎ π΅)) βΎ ((π΄ β π)(,)(π΄ + π)))βπ₯) = ((β D (πΉ βΎ π΅))βπ₯)) |
205 | 203, 204 | sylan9eq 2793 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)(,)(π΄ + π))) β ((β D (πΉ βΎ ((π΄ β π)[,](π΄ + π))))βπ₯) = ((β D (πΉ βΎ π΅))βπ₯)) |
206 | 172 | reseq1d 5940 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β ((π D πΉ) βΎ π΅) = ((β D πΉ) βΎ π΅)) |
207 | 168, 206 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (β D (πΉ βΎ π΅)) = ((π D πΉ) βΎ π΅)) |
208 | 207 | fveq1d 6848 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β ((β D (πΉ βΎ π΅))βπ₯) = (((π D πΉ) βΎ π΅)βπ₯)) |
209 | 208 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)(,)(π΄ + π))) β ((β D (πΉ βΎ π΅))βπ₯) = (((π D πΉ) βΎ π΅)βπ₯)) |
210 | 195 | sselda 3948 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)(,)(π΄ + π))) β π₯ β π΅) |
211 | 210 | fvresd 6866 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)(,)(π΄ + π))) β (((π D πΉ) βΎ π΅)βπ₯) = ((π D πΉ)βπ₯)) |
212 | 205, 209,
211 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)(,)(π΄ + π))) β ((β D (πΉ βΎ ((π΄ β π)[,](π΄ + π))))βπ₯) = ((π D πΉ)βπ₯)) |
213 | 212 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)(,)(π΄ + π))) β (absβ((β D (πΉ βΎ ((π΄ β π)[,](π΄ + π))))βπ₯)) = (absβ((π D πΉ)βπ₯))) |
214 | | simp-4l 782 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β π) |
215 | | dvlip2.l |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΅) β (absβ((π D πΉ)βπ₯)) β€ π) |
216 | 214, 210,
215 | syl2an2r 684 |
. . . . . . . . . . . . 13
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)(,)(π΄ + π))) β (absβ((π D πΉ)βπ₯)) β€ π) |
217 | 213, 216 | eqbrtrd 5131 |
. . . . . . . . . . . 12
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ π₯ β ((π΄ β π)(,)(π΄ + π))) β (absβ((β D (πΉ βΎ ((π΄ β π)[,](π΄ + π))))βπ₯)) β€ π) |
218 | 68, 70, 184, 200, 202, 217 | dvlip 25380 |
. . . . . . . . . . 11
β’
((((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β§ (π β ((π΄ β π)[,](π΄ + π)) β§ π β ((π΄ β π)[,](π΄ + π)))) β (absβ(((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ) β ((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ))) β€ (π Β· (absβ(π β π)))) |
219 | 218 | ex 414 |
. . . . . . . . . 10
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β ((π β ((π΄ β π)[,](π΄ + π)) β§ π β ((π΄ β π)[,](π΄ + π))) β (absβ(((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ) β ((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ))) β€ (π Β· (absβ(π β π))))) |
220 | 75, 95, 219 | mp2and 698 |
. . . . . . . . 9
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (absβ(((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ) β ((πΉ βΎ ((π΄ β π)[,](π΄ + π)))βπ))) β€ (π Β· (absβ(π β π)))) |
221 | 98, 220 | eqbrtrrd 5133 |
. . . . . . . 8
β’
(((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β§ (((π΄π½π) < π β§ (π΄π½π) < π) β§ π < π
)) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))) |
222 | 221 | exp32 422 |
. . . . . . 7
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β (((π΄π½π) < π β§ (π΄π½π) < π) β (π < π
β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))))) |
223 | 43, 222 | sylbid 239 |
. . . . . 6
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β (if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π β (π < π
β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))))) |
224 | 223 | impd 412 |
. . . . 5
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β ((if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π β§ π < π
) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π))))) |
225 | 40, 224 | sylan2 594 |
. . . 4
β’ ((((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β§ π β β) β ((if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π β§ π < π
) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π))))) |
226 | 225 | rexlimdva 3149 |
. . 3
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (βπ β β (if((π΄π½π) β€ (π΄π½π), (π΄π½π), (π΄π½π)) < π β§ π < π
) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π))))) |
227 | 39, 226 | mpd 15 |
. 2
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))) |
228 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π = β) β π = β) |
229 | 228 | sqxpeqd 5669 |
. . . . . . . . . . . . 13
β’ ((π β§ π = β) β (π Γ π) = (β Γ
β)) |
230 | 229 | reseq2d 5941 |
. . . . . . . . . . . 12
β’ ((π β§ π = β) β ((abs β β )
βΎ (π Γ π)) = ((abs β β )
βΎ (β Γ β))) |
231 | | absf 15231 |
. . . . . . . . . . . . . 14
β’
abs:ββΆβ |
232 | | subf 11411 |
. . . . . . . . . . . . . 14
β’ β
:(β Γ β)βΆβ |
233 | | fco 6696 |
. . . . . . . . . . . . . 14
β’
((abs:ββΆβ β§ β :(β Γ
β)βΆβ) β (abs β β ):(β Γ
β)βΆβ) |
234 | 231, 232,
233 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (abs
β β ):(β Γ β)βΆβ |
235 | | ffn 6672 |
. . . . . . . . . . . . 13
β’ ((abs
β β ):(β Γ β)βΆβ β (abs β
β ) Fn (β Γ β)) |
236 | | fnresdm 6624 |
. . . . . . . . . . . . 13
β’ ((abs
β β ) Fn (β Γ β) β ((abs β β )
βΎ (β Γ β)) = (abs β β )) |
237 | 234, 235,
236 | mp2b 10 |
. . . . . . . . . . . 12
β’ ((abs
β β ) βΎ (β Γ β)) = (abs β β
) |
238 | 230, 237 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ ((π β§ π = β) β ((abs β β )
βΎ (π Γ π)) = (abs β β
)) |
239 | 1, 238 | eqtrid 2785 |
. . . . . . . . . 10
β’ ((π β§ π = β) β π½ = (abs β β )) |
240 | 239 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π β§ π = β) β (ballβπ½) = (ballβ(abs β
β ))) |
241 | 240 | oveqd 7378 |
. . . . . . . 8
β’ ((π β§ π = β) β (π΄(ballβπ½)π
) = (π΄(ballβ(abs β β ))π
)) |
242 | 13, 241 | eqtrid 2785 |
. . . . . . 7
β’ ((π β§ π = β) β π΅ = (π΄(ballβ(abs β β ))π
)) |
243 | 242 | eleq2d 2820 |
. . . . . 6
β’ ((π β§ π = β) β (π β π΅ β π β (π΄(ballβ(abs β β ))π
))) |
244 | 242 | eleq2d 2820 |
. . . . . 6
β’ ((π β§ π = β) β (π β π΅ β π β (π΄(ballβ(abs β β ))π
))) |
245 | 243, 244 | anbi12d 632 |
. . . . 5
β’ ((π β§ π = β) β ((π β π΅ β§ π β π΅) β (π β (π΄(ballβ(abs β β ))π
) β§ π β (π΄(ballβ(abs β β ))π
)))) |
246 | 245 | biimpa 478 |
. . . 4
β’ (((π β§ π = β) β§ (π β π΅ β§ π β π΅)) β (π β (π΄(ballβ(abs β β ))π
) β§ π β (π΄(ballβ(abs β β ))π
))) |
247 | 137 | adantr 482 |
. . . . . 6
β’ ((π β§ π = β) β π β π) |
248 | 247, 228 | sseqtrd 3988 |
. . . . 5
β’ ((π β§ π = β) β π β β) |
249 | 134 | adantr 482 |
. . . . 5
β’ ((π β§ π = β) β πΉ:πβΆβ) |
250 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ π = β) β π΄ β π) |
251 | 250, 228 | eleqtrd 2836 |
. . . . 5
β’ ((π β§ π = β) β π΄ β β) |
252 | 15 | adantr 482 |
. . . . 5
β’ ((π β§ π = β) β π
β
β*) |
253 | | eqid 2733 |
. . . . 5
β’ (π΄(ballβ(abs β β
))π
) = (π΄(ballβ(abs β β ))π
) |
254 | 136 | adantr 482 |
. . . . . 6
β’ ((π β§ π = β) β π΅ β dom (π D πΉ)) |
255 | 228 | oveq1d 7376 |
. . . . . . 7
β’ ((π β§ π = β) β (π D πΉ) = (β D πΉ)) |
256 | 255 | dmeqd 5865 |
. . . . . 6
β’ ((π β§ π = β) β dom (π D πΉ) = dom (β D πΉ)) |
257 | 254, 242,
256 | 3sstr3d 3994 |
. . . . 5
β’ ((π β§ π = β) β (π΄(ballβ(abs β β ))π
) β dom (β D πΉ)) |
258 | 201 | adantr 482 |
. . . . 5
β’ ((π β§ π = β) β π β β) |
259 | 215 | ex 414 |
. . . . . . . 8
β’ (π β (π₯ β π΅ β (absβ((π D πΉ)βπ₯)) β€ π)) |
260 | 259 | adantr 482 |
. . . . . . 7
β’ ((π β§ π = β) β (π₯ β π΅ β (absβ((π D πΉ)βπ₯)) β€ π)) |
261 | 242 | eleq2d 2820 |
. . . . . . 7
β’ ((π β§ π = β) β (π₯ β π΅ β π₯ β (π΄(ballβ(abs β β ))π
))) |
262 | 255 | fveq1d 6848 |
. . . . . . . . 9
β’ ((π β§ π = β) β ((π D πΉ)βπ₯) = ((β D πΉ)βπ₯)) |
263 | 262 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ π = β) β (absβ((π D πΉ)βπ₯)) = (absβ((β D πΉ)βπ₯))) |
264 | 263 | breq1d 5119 |
. . . . . . 7
β’ ((π β§ π = β) β ((absβ((π D πΉ)βπ₯)) β€ π β (absβ((β D πΉ)βπ₯)) β€ π)) |
265 | 260, 261,
264 | 3imtr3d 293 |
. . . . . 6
β’ ((π β§ π = β) β (π₯ β (π΄(ballβ(abs β β ))π
) β (absβ((β D
πΉ)βπ₯)) β€ π)) |
266 | 265 | imp 408 |
. . . . 5
β’ (((π β§ π = β) β§ π₯ β (π΄(ballβ(abs β β ))π
)) β (absβ((β D
πΉ)βπ₯)) β€ π) |
267 | 248, 249,
251, 252, 253, 257, 258, 266 | dvlipcn 25381 |
. . . 4
β’ (((π β§ π = β) β§ (π β (π΄(ballβ(abs β β ))π
) β§ π β (π΄(ballβ(abs β β ))π
))) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))) |
268 | 246, 267 | syldan 592 |
. . 3
β’ (((π β§ π = β) β§ (π β π΅ β§ π β π΅)) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))) |
269 | 268 | an32s 651 |
. 2
β’ (((π β§ (π β π΅ β§ π β π΅)) β§ π = β) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))) |
270 | | elpri 4612 |
. . . 4
β’ (π β {β, β}
β (π = β β¨
π =
β)) |
271 | 3, 270 | syl 17 |
. . 3
β’ (π β (π = β β¨ π = β)) |
272 | 271 | adantr 482 |
. 2
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π = β β¨ π = β)) |
273 | 227, 269,
272 | mpjaodan 958 |
1
β’ ((π β§ (π β π΅ β§ π β π΅)) β (absβ((πΉβπ) β (πΉβπ))) β€ (π Β· (absβ(π β π)))) |