Step | Hyp | Ref
| Expression |
1 | | xblss2ps.1 |
. . . . . 6
β’ (π β π· β (PsMetβπ)) |
2 | | xblss2ps.2 |
. . . . . 6
β’ (π β π β π) |
3 | | xblss2ps.4 |
. . . . . 6
β’ (π β π
β
β*) |
4 | | elblps 23756 |
. . . . . 6
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β*) β (π₯ β (π(ballβπ·)π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
5 | 1, 2, 3, 4 | syl3anc 1372 |
. . . . 5
β’ (π β (π₯ β (π(ballβπ·)π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
6 | 5 | simprbda 500 |
. . . 4
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π₯ β π) |
7 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π· β (PsMetβπ)) |
8 | | xblss2ps.3 |
. . . . . . . . 9
β’ (π β π β π) |
9 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π β π) |
10 | | psmetcl 23676 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ π β π β§ π₯ β π) β (ππ·π₯) β
β*) |
11 | 7, 9, 6, 10 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π₯) β
β*) |
12 | 11 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
β β) β (ππ·π₯) β
β*) |
13 | | xblss2ps.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 | | xblss2ps.5 |
. . . . . . 7
β’ (π β π β
β*) |
20 | 19 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
β β) β π β
β*) |
21 | 2 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π β π) |
22 | | psmetcl 23676 |
. . . . . . . . . 10
β’ ((π· β (PsMetβπ) β§ π β π β§ π₯ β π) β (ππ·π₯) β
β*) |
23 | 7, 21, 6, 22 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π₯) β
β*) |
24 | 15, 23 | xaddcld 13227 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β ((ππ·π) +π (ππ·π₯)) β
β*) |
25 | | psmettri2 23678 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ (π β π β§ π β π β§ π₯ β π)) β (ππ·π₯) β€ ((ππ·π) +π (ππ·π₯))) |
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 | | xblss2ps.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 | 11 | adantr 482 |
. . . . . . 7
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π₯) β
β*) |
46 | 13 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π) β β) |
47 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π) |
48 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π₯ β (π(ballβπ·)π
)) |
49 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π
= +β) |
50 | 49 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π(ballβπ·)π
) = (π(ballβπ·)+β)) |
51 | 48, 50 | eleqtrd 2840 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π₯ β (π(ballβπ·)+β)) |
52 | | xblpnfps 23764 |
. . . . . . . . . . . 12
β’ ((π· β (PsMetβπ) β§ π β π) β (π₯ β (π(ballβπ·)+β) β (π₯ β π β§ (ππ·π₯) β β))) |
53 | 1, 2, 52 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π₯ β (π(ballβπ·)+β) β (π₯ β π β§ (ππ·π₯) β β))) |
54 | 53 | simplbda 501 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)+β)) β (ππ·π₯) β β) |
55 | 47, 51, 54 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π₯) β β) |
56 | 46, 55 | readdcld 11191 |
. . . . . . . 8
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β ((ππ·π) + (ππ·π₯)) β β) |
57 | 56 | rexrd 11212 |
. . . . . . 7
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β ((ππ·π) + (ππ·π₯)) β
β*) |
58 | | pnfxr 11216 |
. . . . . . . 8
β’ +β
β β* |
59 | 58 | a1i 11 |
. . . . . . 7
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β +β β
β*) |
60 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π· β (PsMetβπ)) |
61 | 2 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π β π) |
62 | 8 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π β π) |
63 | 6 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π₯ β π) |
64 | 60, 61, 62, 63, 25 | syl13anc 1373 |
. . . . . . . 8
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π₯) β€ ((ππ·π) +π (ππ·π₯))) |
65 | 46, 55 | rexaddd 13160 |
. . . . . . . 8
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β ((ππ·π) +π (ππ·π₯)) = ((ππ·π) + (ππ·π₯))) |
66 | 64, 65 | breqtrd 5136 |
. . . . . . 7
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π₯) β€ ((ππ·π) + (ππ·π₯))) |
67 | 56 | ltpnfd 13049 |
. . . . . . 7
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β ((ππ·π) + (ππ·π₯)) < +β) |
68 | 45, 57, 59, 66, 67 | xrlelttrd 13086 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π₯) < +β) |
69 | | 0xr 11209 |
. . . . . . . . . . 11
β’ 0 β
β* |
70 | 69 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 β
β*) |
71 | | psmetge0 23681 |
. . . . . . . . . . 11
β’ ((π· β (PsMetβπ) β§ π β π β§ π β π) β 0 β€ (ππ·π)) |
72 | 7, 21, 9, 71 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 β€ (ππ·π)) |
73 | 70, 15, 35, 72, 37 | xrletrd 13088 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 β€ (π +π
-ππ
)) |
74 | | ge0nemnf 13099 |
. . . . . . . . 9
β’ (((π +π
-ππ
)
β β* β§ 0 β€ (π +π
-ππ
))
β (π
+π -ππ
) β -β) |
75 | 35, 73, 74 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (π +π
-ππ
)
β -β) |
76 | 75 | adantr 482 |
. . . . . . 7
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π +π
-ππ
)
β -β) |
77 | 19 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π β
β*) |
78 | | xaddmnf1 13154 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π β +β)
β (π
+π -β) = -β) |
79 | 78 | ex 414 |
. . . . . . . . . 10
β’ (π β β*
β (π β +β
β (π
+π -β) = -β)) |
80 | 77, 79 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π β +β β (π +π -β) =
-β)) |
81 | | xnegeq 13133 |
. . . . . . . . . . . . 13
β’ (π
= +β β
-ππ
=
-π+β) |
82 | 49, 81 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β
-ππ
=
-π+β) |
83 | | xnegpnf 13135 |
. . . . . . . . . . . 12
β’
-π+β = -β |
84 | 82, 83 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β
-ππ
=
-β) |
85 | 84 | oveq2d 7378 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π +π
-ππ
) =
(π +π
-β)) |
86 | 85 | eqeq1d 2739 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β ((π +π
-ππ
) =
-β β (π
+π -β) = -β)) |
87 | 80, 86 | sylibrd 259 |
. . . . . . . 8
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (π β +β β (π +π
-ππ
) =
-β)) |
88 | 87 | necon1d 2966 |
. . . . . . 7
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β ((π +π
-ππ
)
β -β β π =
+β)) |
89 | 76, 88 | mpd 15 |
. . . . . 6
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β π = +β) |
90 | 68, 89 | breqtrrd 5138 |
. . . . 5
β’ (((π β§ π₯ β (π(ballβπ·)π
)) β§ π
= +β) β (ππ·π₯) < π) |
91 | | psmetge0 23681 |
. . . . . . . . . . 11
β’ ((π· β (PsMetβπ) β§ π β π β§ π₯ β π) β 0 β€ (ππ·π₯)) |
92 | 7, 21, 6, 91 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 β€ (ππ·π₯)) |
93 | 70, 23, 16, 92, 27 | xrlelttrd 13086 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 < π
) |
94 | 70, 16, 93 | xrltled 13076 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β 0 β€ π
) |
95 | | ge0nemnf 13099 |
. . . . . . . 8
β’ ((π
β β*
β§ 0 β€ π
) β
π
β
-β) |
96 | 16, 94, 95 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π
β -β) |
97 | 16, 96 | jca 513 |
. . . . . 6
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (π
β β* β§ π
β
-β)) |
98 | | xrnemnf 13045 |
. . . . . 6
β’ ((π
β β*
β§ π
β -β)
β (π
β β
β¨ π
=
+β)) |
99 | 97, 98 | sylib 217 |
. . . . 5
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (π
β β β¨ π
= +β)) |
100 | 44, 90, 99 | mpjaodan 958 |
. . . 4
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (ππ·π₯) < π) |
101 | | elblps 23756 |
. . . . 5
β’ ((π· β (PsMetβπ) β§ π β π β§ π β β*) β (π₯ β (π(ballβπ·)π) β (π₯ β π β§ (ππ·π₯) < π))) |
102 | 7, 9, 33, 101 | syl3anc 1372 |
. . . 4
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β (π₯ β (π(ballβπ·)π) β (π₯ β π β§ (ππ·π₯) < π))) |
103 | 6, 100, 102 | mpbir2and 712 |
. . 3
β’ ((π β§ π₯ β (π(ballβπ·)π
)) β π₯ β (π(ballβπ·)π)) |
104 | 103 | ex 414 |
. 2
β’ (π β (π₯ β (π(ballβπ·)π
) β π₯ β (π(ballβπ·)π))) |
105 | 104 | ssrdv 3955 |
1
β’ (π β (π(ballβπ·)π
) β (π(ballβπ·)π)) |