Step | Hyp | Ref
| Expression |
1 | | xblss2.1 |
. . . . . 6
β’ (π β π· β (βMetβπ)) |
2 | | xblss2.2 |
. . . . . 6
β’ (π β π β π) |
3 | | xblss2.4 |
. . . . . 6
β’ (π β π
β
β*) |
4 | | elbl 23757 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π₯ β (π(ballβπ·)π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
5 | 1, 2, 3, 4 | syl3anc 1372 |
. . . . 5
β’ (π β (π₯ β (π(ballβπ·)π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
6 | 5 | simprbda 500 |
. . . 4
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π₯ β π) |
7 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π· β (βMetβπ)) |
8 | | xblss2.3 |
. . . . . . . . 9
β’ (π β π β π) |
9 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π β π) |
10 | | xmetcl 23700 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β π) β (ππ·π₯) β
β*) |
11 | 7, 9, 6, 10 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π₯) β
β*) |
12 | 11 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
β β) β (ππ·π₯) β
β*) |
13 | | xblss2.6 |
. . . . . . . . . 10
β’ (π β (ππ·π) β β) |
14 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π) β β) |
15 | 14 | rexrd 11212 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π) β
β*) |
16 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π
β
β*) |
17 | 15, 16 | xaddcld 13227 |
. . . . . . 7
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β ((ππ·π) +π π
) β
β*) |
18 | 17 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
β β) β ((ππ·π) +π π
) β
β*) |
19 | | xblss2.5 |
. . . . . . 7
β’ (π β π β
β*) |
20 | 19 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
β β) β π β
β*) |
21 | 2 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π β π) |
22 | | xmetcl 23700 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β π) β (ππ·π₯) β
β*) |
23 | 7, 21, 6, 22 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π₯) β
β*) |
24 | 15, 23 | xaddcld 13227 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β ((ππ·π) +π (ππ·π₯)) β
β*) |
25 | | xmettri2 23709 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ (π β π β§ π β π β§ π₯ β π)) β (ππ·π₯) β€ ((ππ·π) +π (ππ·π₯))) |
26 | 7, 21, 9, 6, 25 | syl13anc 1373 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π₯) β€ ((ππ·π) +π (ππ·π₯))) |
27 | 5 | simplbda 501 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π₯) < π
) |
28 | | xltadd2 13183 |
. . . . . . . . . 10
β’ (((ππ·π₯) β β* β§ π
β β*
β§ (ππ·π) β β) β ((ππ·π₯) < π
β ((ππ·π) +π (ππ·π₯)) < ((ππ·π) +π π
))) |
29 | 23, 16, 14, 28 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β ((ππ·π₯) < π
β ((ππ·π) +π (ππ·π₯)) < ((ππ·π) +π π
))) |
30 | 27, 29 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β ((ππ·π) +π (ππ·π₯)) < ((ππ·π) +π π
)) |
31 | 11, 24, 17, 26, 30 | xrlelttrd 13086 |
. . . . . . 7
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π₯) < ((ππ·π) +π π
)) |
32 | 31 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
β β) β (ππ·π₯) < ((ππ·π) +π π
)) |
33 | 19 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π β
β*) |
34 | 16 | xnegcld 13226 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β -ππ
β
β*) |
35 | 33, 34 | xaddcld 13227 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (π +π
-ππ
)
β β*) |
36 | | xblss2.7 |
. . . . . . . . . 10
β’ (π β (ππ·π) β€ (π +π
-ππ
)) |
37 | 36 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π) β€ (π +π
-ππ
)) |
38 | | xleadd1a 13179 |
. . . . . . . . 9
β’ ((((ππ·π) β β* β§ (π +π
-ππ
)
β β* β§ π
β β*) β§ (ππ·π) β€ (π +π
-ππ
))
β ((ππ·π) +π π
) β€ ((π +π
-ππ
)
+π π
)) |
39 | 15, 35, 16, 37, 38 | syl31anc 1374 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β ((ππ·π) +π π
) β€ ((π +π
-ππ
)
+π π
)) |
40 | 39 | adantr 482 |
. . . . . . 7
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
β β) β ((ππ·π) +π π
) β€ ((π +π
-ππ
)
+π π
)) |
41 | | xnpcan 13178 |
. . . . . . . 8
β’ ((π β β*
β§ π
β β)
β ((π
+π -ππ
) +π π
) = π) |
42 | 33, 41 | sylan 581 |
. . . . . . 7
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
β β) β ((π +π
-ππ
)
+π π
) =
π) |
43 | 40, 42 | breqtrd 5136 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
β β) β ((ππ·π) +π π
) β€ π) |
44 | 12, 18, 20, 32, 43 | xrltletrd 13087 |
. . . . 5
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
β β) β (ππ·π₯) < π) |
45 | 27 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π₯) < π
) |
46 | 36 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π) β€ (π +π
-ππ
)) |
47 | | 0xr 11209 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β* |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 β
β*) |
49 | | xmetge0 23713 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β 0 β€ (ππ·π)) |
50 | 7, 21, 9, 49 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 β€ (ππ·π)) |
51 | 48, 15, 35, 50, 37 | xrletrd 13088 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 β€ (π +π
-ππ
)) |
52 | | ge0nemnf 13099 |
. . . . . . . . . . . . . 14
β’ (((π +π
-ππ
)
β β* β§ 0 β€ (π +π
-ππ
))
β (π
+π -ππ
) β -β) |
53 | 35, 51, 52 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (π +π
-ππ
)
β -β) |
54 | 53 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π +π
-ππ
)
β -β) |
55 | 19 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π β
β*) |
56 | | xaddmnf1 13154 |
. . . . . . . . . . . . . . . 16
β’ ((π β β*
β§ π β +β)
β (π
+π -β) = -β) |
57 | 56 | ex 414 |
. . . . . . . . . . . . . . 15
β’ (π β β*
β (π β +β
β (π
+π -β) = -β)) |
58 | 55, 57 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π β +β β (π +π -β) =
-β)) |
59 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π
= +β) |
60 | | xnegeq 13133 |
. . . . . . . . . . . . . . . . . 18
β’ (π
= +β β
-ππ
=
-π+β) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β
-ππ
=
-π+β) |
62 | | xnegpnf 13135 |
. . . . . . . . . . . . . . . . 17
β’
-π+β = -β |
63 | 61, 62 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β
-ππ
=
-β) |
64 | 63 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π +π
-ππ
) =
(π +π
-β)) |
65 | 64 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β ((π +π
-ππ
) =
-β β (π
+π -β) = -β)) |
66 | 58, 65 | sylibrd 259 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π β +β β (π +π
-ππ
) =
-β)) |
67 | 66 | necon1d 2966 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β ((π +π
-ππ
)
β -β β π =
+β)) |
68 | 54, 67 | mpd 15 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π = +β) |
69 | 68, 63 | oveq12d 7380 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π +π
-ππ
) =
(+β +π -β)) |
70 | | pnfaddmnf 13156 |
. . . . . . . . . 10
β’ (+β
+π -β) = 0 |
71 | 69, 70 | eqtrdi 2793 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π +π
-ππ
) =
0) |
72 | 46, 71 | breqtrd 5136 |
. . . . . . . 8
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π) β€ 0) |
73 | 50 | biantrud 533 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β ((ππ·π) β€ 0 β ((ππ·π) β€ 0 β§ 0 β€ (ππ·π)))) |
74 | | xrletri3 13080 |
. . . . . . . . . . 11
β’ (((ππ·π) β β* β§ 0 β
β*) β ((ππ·π) = 0 β ((ππ·π) β€ 0 β§ 0 β€ (ππ·π)))) |
75 | 15, 47, 74 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β ((ππ·π) = 0 β ((ππ·π) β€ 0 β§ 0 β€ (ππ·π)))) |
76 | | xmeteq0 23707 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π β π β§ π β π) β ((ππ·π) = 0 β π = π)) |
77 | 7, 21, 9, 76 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β ((ππ·π) = 0 β π = π)) |
78 | 73, 75, 77 | 3bitr2d 307 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β ((ππ·π) β€ 0 β π = π)) |
79 | 78 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β ((ππ·π) β€ 0 β π = π)) |
80 | 72, 79 | mpbid 231 |
. . . . . . 7
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π = π) |
81 | 80 | oveq1d 7377 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π₯) = (ππ·π₯)) |
82 | 59, 68 | eqtr4d 2780 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π
= π) |
83 | 45, 81, 82 | 3brtr3d 5141 |
. . . . 5
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π₯) < π) |
84 | | xmetge0 23713 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β π) β 0 β€ (ππ·π₯)) |
85 | 7, 21, 6, 84 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 β€ (ππ·π₯)) |
86 | 48, 23, 16, 85, 27 | xrlelttrd 13086 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 < π
) |
87 | 48, 16, 86 | xrltled 13076 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 β€ π
) |
88 | | ge0nemnf 13099 |
. . . . . . . 8
β’ ((π
β β*
β§ 0 β€ π
) β
π
β
-β) |
89 | 16, 87, 88 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π
β -β) |
90 | 16, 89 | jca 513 |
. . . . . 6
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (π
β β* β§ π
β
-β)) |
91 | | xrnemnf 13045 |
. . . . . 6
β’ ((π
β β*
β§ π
β -β)
β (π
β β
β¨ π
=
+β)) |
92 | 90, 91 | sylib 217 |
. . . . 5
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (π
β β β¨ π
= +β)) |
93 | 44, 83, 92 | mpjaodan 958 |
. . . 4
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π₯) < π) |
94 | | elbl 23757 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π₯ β (π(ballβπ·)π) β (π₯ β π β§ (ππ·π₯) < π))) |
95 | 7, 9, 33, 94 | syl3anc 1372 |
. . . 4
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (π₯ β (π(ballβπ·)π) β (π₯ β π β§ (ππ·π₯) < π))) |
96 | 6, 93, 95 | mpbir2and 712 |
. . 3
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π₯ β (π(ballβπ·)π)) |
97 | 96 | ex 414 |
. 2
β’ (π β (π₯ β (π(ballβπ·)π
) β π₯ β (π(ballβπ·)π))) |
98 | 97 | ssrdv 3955 |
1
β’ (π β (π(ballβπ·)π
) β (π(ballβπ·)π)) |