Step | Hyp | Ref
| Expression |
1 | | isxmetd.0 |
. 2
β’ (π β π β π) |
2 | | isxmetd.1 |
. 2
β’ (π β π·:(π Γ π)βΆβ*) |
3 | 2 | fovcdmda 7518 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) β
β*) |
4 | | 0xr 11136 |
. . . 4
β’ 0 β
β* |
5 | | xrletri3 13002 |
. . . 4
β’ (((π₯π·π¦) β β* β§ 0 β
β*) β ((π₯π·π¦) = 0 β ((π₯π·π¦) β€ 0 β§ 0 β€ (π₯π·π¦)))) |
6 | 3, 4, 5 | sylancl 587 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = 0 β ((π₯π·π¦) β€ 0 β§ 0 β€ (π₯π·π¦)))) |
7 | | isxmet2d.2 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β 0 β€ (π₯π·π¦)) |
8 | 7 | biantrud 533 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) β€ 0 β ((π₯π·π¦) β€ 0 β§ 0 β€ (π₯π·π¦)))) |
9 | | isxmet2d.3 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) β€ 0 β π₯ = π¦)) |
10 | 6, 8, 9 | 3bitr2d 307 |
. 2
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = 0 β π₯ = π¦)) |
11 | | isxmet2d.4 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) |
12 | 11 | 3expa 1119 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) |
13 | | rexadd 13080 |
. . . . . . 7
β’ (((π§π·π₯) β β β§ (π§π·π¦) β β) β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π₯) + (π§π·π¦))) |
14 | 13 | adantl 483 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π₯) + (π§π·π¦))) |
15 | 12, 14 | breqtrrd 5132 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
16 | 15 | anassrs 469 |
. . . 4
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) β β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
17 | 3 | 3adantr3 1172 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β
β*) |
18 | | pnfge 12980 |
. . . . . . 7
β’ ((π₯π·π¦) β β* β (π₯π·π¦) β€ +β) |
19 | 17, 18 | syl 17 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β€ +β) |
20 | 19 | ad2antrr 725 |
. . . . 5
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = +β) β (π₯π·π¦) β€ +β) |
21 | | oveq2 7358 |
. . . . . 6
β’ ((π§π·π¦) = +β β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π₯) +π
+β)) |
22 | 2 | ffnd 6665 |
. . . . . . . . . . 11
β’ (π β π· Fn (π Γ π)) |
23 | | elxrge0 13303 |
. . . . . . . . . . . . 13
β’ ((π₯π·π¦) β (0[,]+β) β ((π₯π·π¦) β β* β§ 0 β€
(π₯π·π¦))) |
24 | 3, 7, 23 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) β (0[,]+β)) |
25 | 24 | ralrimivva 3196 |
. . . . . . . . . . 11
β’ (π β βπ₯ β π βπ¦ β π (π₯π·π¦) β (0[,]+β)) |
26 | | ffnov 7476 |
. . . . . . . . . . 11
β’ (π·:(π Γ π)βΆ(0[,]+β) β (π· Fn (π Γ π) β§ βπ₯ β π βπ¦ β π (π₯π·π¦) β (0[,]+β))) |
27 | 22, 25, 26 | sylanbrc 584 |
. . . . . . . . . 10
β’ (π β π·:(π Γ π)βΆ(0[,]+β)) |
28 | 27 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π·:(π Γ π)βΆ(0[,]+β)) |
29 | | simpr3 1197 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π§ β π) |
30 | | simpr1 1195 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π₯ β π) |
31 | 28, 29, 30 | fovcdmd 7519 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π₯) β (0[,]+β)) |
32 | | eliccxr 13281 |
. . . . . . . 8
β’ ((π§π·π₯) β (0[,]+β) β (π§π·π₯) β
β*) |
33 | 31, 32 | syl 17 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π₯) β
β*) |
34 | | renemnf 11138 |
. . . . . . 7
β’ ((π§π·π₯) β β β (π§π·π₯) β -β) |
35 | | xaddpnf1 13074 |
. . . . . . 7
β’ (((π§π·π₯) β β* β§ (π§π·π₯) β -β) β ((π§π·π₯) +π +β) =
+β) |
36 | 33, 34, 35 | syl2an 597 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β ((π§π·π₯) +π +β) =
+β) |
37 | 21, 36 | sylan9eqr 2800 |
. . . . 5
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = +β) β ((π§π·π₯) +π (π§π·π¦)) = +β) |
38 | 20, 37 | breqtrrd 5132 |
. . . 4
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = +β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
39 | | simpr2 1196 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π¦ β π) |
40 | 28, 29, 39 | fovcdmd 7519 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π¦) β (0[,]+β)) |
41 | | eliccxr 13281 |
. . . . . . . . . 10
β’ ((π§π·π¦) β (0[,]+β) β (π§π·π¦) β
β*) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π¦) β
β*) |
43 | | elxrge0 13303 |
. . . . . . . . . . 11
β’ ((π§π·π¦) β (0[,]+β) β ((π§π·π¦) β β* β§ 0 β€
(π§π·π¦))) |
44 | 43 | simprbi 498 |
. . . . . . . . . 10
β’ ((π§π·π¦) β (0[,]+β) β 0 β€ (π§π·π¦)) |
45 | 40, 44 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β 0 β€ (π§π·π¦)) |
46 | | ge0nemnf 13021 |
. . . . . . . . 9
β’ (((π§π·π¦) β β* β§ 0 β€
(π§π·π¦)) β (π§π·π¦) β -β) |
47 | 42, 45, 46 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π¦) β -β) |
48 | 47 | a1d 25 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (Β¬ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β (π§π·π¦) β -β)) |
49 | 48 | necon4bd 2962 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π§π·π¦) = -β β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
50 | 49 | adantr 482 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β ((π§π·π¦) = -β β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
51 | 50 | imp 408 |
. . . 4
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = -β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
52 | 42 | adantr 482 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β (π§π·π¦) β
β*) |
53 | | elxr 12966 |
. . . . 5
β’ ((π§π·π¦) β β* β ((π§π·π¦) β β β¨ (π§π·π¦) = +β β¨ (π§π·π¦) = -β)) |
54 | 52, 53 | sylib 217 |
. . . 4
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β ((π§π·π¦) β β β¨ (π§π·π¦) = +β β¨ (π§π·π¦) = -β)) |
55 | 16, 38, 51, 54 | mpjao3dan 1432 |
. . 3
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
56 | 19 | adantr 482 |
. . . 4
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = +β) β (π₯π·π¦) β€ +β) |
57 | | oveq1 7357 |
. . . . 5
β’ ((π§π·π₯) = +β β ((π§π·π₯) +π (π§π·π¦)) = (+β +π (π§π·π¦))) |
58 | | xaddpnf2 13075 |
. . . . . 6
β’ (((π§π·π¦) β β* β§ (π§π·π¦) β -β) β (+β
+π (π§π·π¦)) = +β) |
59 | 42, 47, 58 | syl2anc 585 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (+β +π
(π§π·π¦)) = +β) |
60 | 57, 59 | sylan9eqr 2800 |
. . . 4
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = +β) β ((π§π·π₯) +π (π§π·π¦)) = +β) |
61 | 56, 60 | breqtrrd 5132 |
. . 3
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = +β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
62 | | elxrge0 13303 |
. . . . . . . . 9
β’ ((π§π·π₯) β (0[,]+β) β ((π§π·π₯) β β* β§ 0 β€
(π§π·π₯))) |
63 | 62 | simprbi 498 |
. . . . . . . 8
β’ ((π§π·π₯) β (0[,]+β) β 0 β€ (π§π·π₯)) |
64 | 31, 63 | syl 17 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β 0 β€ (π§π·π₯)) |
65 | | ge0nemnf 13021 |
. . . . . . 7
β’ (((π§π·π₯) β β* β§ 0 β€
(π§π·π₯)) β (π§π·π₯) β -β) |
66 | 33, 64, 65 | syl2anc 585 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π₯) β -β) |
67 | 66 | a1d 25 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (Β¬ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β (π§π·π₯) β -β)) |
68 | 67 | necon4bd 2962 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π§π·π₯) = -β β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
69 | 68 | imp 408 |
. . 3
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = -β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
70 | | elxr 12966 |
. . . 4
β’ ((π§π·π₯) β β* β ((π§π·π₯) β β β¨ (π§π·π₯) = +β β¨ (π§π·π₯) = -β)) |
71 | 33, 70 | sylib 217 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π§π·π₯) β β β¨ (π§π·π₯) = +β β¨ (π§π·π₯) = -β)) |
72 | 55, 61, 69, 71 | mpjao3dan 1432 |
. 2
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
73 | 1, 2, 10, 72 | isxmetd 23601 |
1
β’ (π β π· β (βMetβπ)) |