Step | Hyp | Ref
| Expression |
1 | | isxmetd.0 |
. 2
β’ (π β π β V) |
2 | | isxmetd.1 |
. 2
β’ (π β π·:(π Γ π)βΆβ*) |
3 | 2 | fovcdmda 6020 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) β
β*) |
4 | | 0xr 8006 |
. . . 4
β’ 0 β
β* |
5 | | xrletri3 9806 |
. . . 4
β’ (((π₯π·π¦) β β* β§ 0 β
β*) β ((π₯π·π¦) = 0 β ((π₯π·π¦) β€ 0 β§ 0 β€ (π₯π·π¦)))) |
6 | 3, 4, 5 | sylancl 413 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = 0 β ((π₯π·π¦) β€ 0 β§ 0 β€ (π₯π·π¦)))) |
7 | | isxmet2d.2 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β 0 β€ (π₯π·π¦)) |
8 | 7 | biantrud 304 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) β€ 0 β ((π₯π·π¦) β€ 0 β§ 0 β€ (π₯π·π¦)))) |
9 | | isxmet2d.3 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) β€ 0 β π₯ = π¦)) |
10 | 6, 8, 9 | 3bitr2d 216 |
. 2
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = 0 β π₯ = π¦)) |
11 | | isxmet2d.4 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) |
12 | 11 | 3expa 1203 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) |
13 | | rexadd 9854 |
. . . . . . 7
β’ (((π§π·π₯) β β β§ (π§π·π¦) β β) β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π₯) + (π§π·π¦))) |
14 | 13 | adantl 277 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π₯) + (π§π·π¦))) |
15 | 12, 14 | breqtrrd 4033 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
16 | 15 | anassrs 400 |
. . . 4
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) β β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
17 | 3 | 3adantr3 1158 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β
β*) |
18 | | pnfge 9791 |
. . . . . . 7
β’ ((π₯π·π¦) β β* β (π₯π·π¦) β€ +β) |
19 | 17, 18 | syl 14 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β€ +β) |
20 | 19 | ad2antrr 488 |
. . . . 5
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = +β) β (π₯π·π¦) β€ +β) |
21 | | oveq2 5885 |
. . . . . 6
β’ ((π§π·π¦) = +β β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π₯) +π
+β)) |
22 | 2 | ffnd 5368 |
. . . . . . . . . . 11
β’ (π β π· Fn (π Γ π)) |
23 | | elxrge0 9980 |
. . . . . . . . . . . . 13
β’ ((π₯π·π¦) β (0[,]+β) β ((π₯π·π¦) β β* β§ 0 β€
(π₯π·π¦))) |
24 | 3, 7, 23 | sylanbrc 417 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) β (0[,]+β)) |
25 | 24 | ralrimivva 2559 |
. . . . . . . . . . 11
β’ (π β βπ₯ β π βπ¦ β π (π₯π·π¦) β (0[,]+β)) |
26 | | ffnov 5981 |
. . . . . . . . . . 11
β’ (π·:(π Γ π)βΆ(0[,]+β) β (π· Fn (π Γ π) β§ βπ₯ β π βπ¦ β π (π₯π·π¦) β (0[,]+β))) |
27 | 22, 25, 26 | sylanbrc 417 |
. . . . . . . . . 10
β’ (π β π·:(π Γ π)βΆ(0[,]+β)) |
28 | 27 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π·:(π Γ π)βΆ(0[,]+β)) |
29 | | simpr3 1005 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π§ β π) |
30 | | simpr1 1003 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π₯ β π) |
31 | 28, 29, 30 | fovcdmd 6021 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π₯) β (0[,]+β)) |
32 | | elxrge0 9980 |
. . . . . . . . 9
β’ ((π§π·π₯) β (0[,]+β) β ((π§π·π₯) β β* β§ 0 β€
(π§π·π₯))) |
33 | 32 | simplbi 274 |
. . . . . . . 8
β’ ((π§π·π₯) β (0[,]+β) β (π§π·π₯) β
β*) |
34 | 31, 33 | syl 14 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π₯) β
β*) |
35 | | renemnf 8008 |
. . . . . . 7
β’ ((π§π·π₯) β β β (π§π·π₯) β -β) |
36 | | xaddpnf1 9848 |
. . . . . . 7
β’ (((π§π·π₯) β β* β§ (π§π·π₯) β -β) β ((π§π·π₯) +π +β) =
+β) |
37 | 34, 35, 36 | syl2an 289 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β ((π§π·π₯) +π +β) =
+β) |
38 | 21, 37 | sylan9eqr 2232 |
. . . . 5
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = +β) β ((π§π·π₯) +π (π§π·π¦)) = +β) |
39 | 20, 38 | breqtrrd 4033 |
. . . 4
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = +β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
40 | | simpr2 1004 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π¦ β π) |
41 | 28, 29, 40 | fovcdmd 6021 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π¦) β (0[,]+β)) |
42 | | elxrge0 9980 |
. . . . . . . . . . 11
β’ ((π§π·π¦) β (0[,]+β) β ((π§π·π¦) β β* β§ 0 β€
(π§π·π¦))) |
43 | 42 | simplbi 274 |
. . . . . . . . . 10
β’ ((π§π·π¦) β (0[,]+β) β (π§π·π¦) β
β*) |
44 | 41, 43 | syl 14 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π¦) β
β*) |
45 | 42 | simprbi 275 |
. . . . . . . . . 10
β’ ((π§π·π¦) β (0[,]+β) β 0 β€ (π§π·π¦)) |
46 | 41, 45 | syl 14 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β 0 β€ (π§π·π¦)) |
47 | | ge0nemnf 9826 |
. . . . . . . . 9
β’ (((π§π·π¦) β β* β§ 0 β€
(π§π·π¦)) β (π§π·π¦) β -β) |
48 | 44, 46, 47 | syl2anc 411 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π¦) β -β) |
49 | 48 | neneqd 2368 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β Β¬ (π§π·π¦) = -β) |
50 | 49 | pm2.21d 619 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π§π·π¦) = -β β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
51 | 50 | adantr 276 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β ((π§π·π¦) = -β β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
52 | 51 | imp 124 |
. . . 4
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = -β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
53 | 44 | adantr 276 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β (π§π·π¦) β
β*) |
54 | | elxr 9778 |
. . . . 5
β’ ((π§π·π¦) β β* β ((π§π·π¦) β β β¨ (π§π·π¦) = +β β¨ (π§π·π¦) = -β)) |
55 | 53, 54 | sylib 122 |
. . . 4
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β ((π§π·π¦) β β β¨ (π§π·π¦) = +β β¨ (π§π·π¦) = -β)) |
56 | 16, 39, 52, 55 | mpjao3dan 1307 |
. . 3
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
57 | 19 | adantr 276 |
. . . 4
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = +β) β (π₯π·π¦) β€ +β) |
58 | | oveq1 5884 |
. . . . 5
β’ ((π§π·π₯) = +β β ((π§π·π₯) +π (π§π·π¦)) = (+β +π (π§π·π¦))) |
59 | | xaddpnf2 9849 |
. . . . . 6
β’ (((π§π·π¦) β β* β§ (π§π·π¦) β -β) β (+β
+π (π§π·π¦)) = +β) |
60 | 44, 48, 59 | syl2anc 411 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (+β +π
(π§π·π¦)) = +β) |
61 | 58, 60 | sylan9eqr 2232 |
. . . 4
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = +β) β ((π§π·π₯) +π (π§π·π¦)) = +β) |
62 | 57, 61 | breqtrrd 4033 |
. . 3
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = +β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
63 | 32 | simprbi 275 |
. . . . . . . 8
β’ ((π§π·π₯) β (0[,]+β) β 0 β€ (π§π·π₯)) |
64 | 31, 63 | syl 14 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β 0 β€ (π§π·π₯)) |
65 | | ge0nemnf 9826 |
. . . . . . 7
β’ (((π§π·π₯) β β* β§ 0 β€
(π§π·π₯)) β (π§π·π₯) β -β) |
66 | 34, 64, 65 | syl2anc 411 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π₯) β -β) |
67 | 66 | neneqd 2368 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β Β¬ (π§π·π₯) = -β) |
68 | 67 | pm2.21d 619 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π§π·π₯) = -β β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
69 | 68 | imp 124 |
. . 3
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = -β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
70 | | elxr 9778 |
. . . 4
β’ ((π§π·π₯) β β* β ((π§π·π₯) β β β¨ (π§π·π₯) = +β β¨ (π§π·π₯) = -β)) |
71 | 34, 70 | sylib 122 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π§π·π₯) β β β¨ (π§π·π₯) = +β β¨ (π§π·π₯) = -β)) |
72 | 56, 62, 69, 71 | mpjao3dan 1307 |
. 2
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
73 | 1, 2, 10, 72 | isxmetd 13886 |
1
β’ (π β π· β (βMetβπ)) |