Step | Hyp | Ref
| Expression |
1 | | isxmetd.0 |
. 2
β’ (π β π β π) |
2 | | isxmetd.1 |
. 2
β’ (π β π·:(π Γ π)βΆβ*) |
3 | 2 | fovcdmda 7517 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) β
β*) |
4 | | 0xr 11135 |
. . . 4
β’ 0 β
β* |
5 | | xrletri3 13001 |
. . . 4
β’ (((π₯π·π¦) β β* β§ 0 β
β*) β ((π₯π·π¦) = 0 β ((π₯π·π¦) β€ 0 β§ 0 β€ (π₯π·π¦)))) |
6 | 3, 4, 5 | sylancl 586 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = 0 β ((π₯π·π¦) β€ 0 β§ 0 β€ (π₯π·π¦)))) |
7 | | isxmet2d.2 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β 0 β€ (π₯π·π¦)) |
8 | 7 | biantrud 532 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) β€ 0 β ((π₯π·π¦) β€ 0 β§ 0 β€ (π₯π·π¦)))) |
9 | | isxmet2d.3 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) β€ 0 β π₯ = π¦)) |
10 | 6, 8, 9 | 3bitr2d 306 |
. 2
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = 0 β π₯ = π¦)) |
11 | | isxmet2d.4 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) |
12 | 11 | 3expa 1118 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) |
13 | | rexadd 13079 |
. . . . . . 7
β’ (((π§π·π₯) β β β§ (π§π·π¦) β β) β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π₯) + (π§π·π¦))) |
14 | 13 | adantl 482 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π₯) + (π§π·π¦))) |
15 | 12, 14 | breqtrrd 5131 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
16 | 15 | anassrs 468 |
. . . 4
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) β β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
17 | 3 | 3adantr3 1171 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β
β*) |
18 | | pnfge 12979 |
. . . . . . 7
β’ ((π₯π·π¦) β β* β (π₯π·π¦) β€ +β) |
19 | 17, 18 | syl 17 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β€ +β) |
20 | 19 | ad2antrr 724 |
. . . . 5
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = +β) β (π₯π·π¦) β€ +β) |
21 | | oveq2 7357 |
. . . . . 6
β’ ((π§π·π¦) = +β β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·π₯) +π
+β)) |
22 | 2 | ffnd 6664 |
. . . . . . . . . . 11
β’ (π β π· Fn (π Γ π)) |
23 | | elxrge0 13302 |
. . . . . . . . . . . . 13
β’ ((π₯π·π¦) β (0[,]+β) β ((π₯π·π¦) β β* β§ 0 β€
(π₯π·π¦))) |
24 | 3, 7, 23 | sylanbrc 583 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) β (0[,]+β)) |
25 | 24 | ralrimivva 3195 |
. . . . . . . . . . 11
β’ (π β βπ₯ β π βπ¦ β π (π₯π·π¦) β (0[,]+β)) |
26 | | ffnov 7475 |
. . . . . . . . . . 11
β’ (π·:(π Γ π)βΆ(0[,]+β) β (π· Fn (π Γ π) β§ βπ₯ β π βπ¦ β π (π₯π·π¦) β (0[,]+β))) |
27 | 22, 25, 26 | sylanbrc 583 |
. . . . . . . . . 10
β’ (π β π·:(π Γ π)βΆ(0[,]+β)) |
28 | 27 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π·:(π Γ π)βΆ(0[,]+β)) |
29 | | simpr3 1196 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π§ β π) |
30 | | simpr1 1194 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π₯ β π) |
31 | 28, 29, 30 | fovcdmd 7518 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π₯) β (0[,]+β)) |
32 | | eliccxr 13280 |
. . . . . . . 8
β’ ((π§π·π₯) β (0[,]+β) β (π§π·π₯) β
β*) |
33 | 31, 32 | syl 17 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π₯) β
β*) |
34 | | renemnf 11137 |
. . . . . . 7
β’ ((π§π·π₯) β β β (π§π·π₯) β -β) |
35 | | xaddpnf1 13073 |
. . . . . . 7
β’ (((π§π·π₯) β β* β§ (π§π·π₯) β -β) β ((π§π·π₯) +π +β) =
+β) |
36 | 33, 34, 35 | syl2an 596 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β ((π§π·π₯) +π +β) =
+β) |
37 | 21, 36 | sylan9eqr 2799 |
. . . . 5
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = +β) β ((π§π·π₯) +π (π§π·π¦)) = +β) |
38 | 20, 37 | breqtrrd 5131 |
. . . 4
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = +β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
39 | | simpr2 1195 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β π¦ β π) |
40 | 28, 29, 39 | fovcdmd 7518 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π¦) β (0[,]+β)) |
41 | | eliccxr 13280 |
. . . . . . . . . 10
β’ ((π§π·π¦) β (0[,]+β) β (π§π·π¦) β
β*) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π¦) β
β*) |
43 | | elxrge0 13302 |
. . . . . . . . . . 11
β’ ((π§π·π¦) β (0[,]+β) β ((π§π·π¦) β β* β§ 0 β€
(π§π·π¦))) |
44 | 43 | simprbi 497 |
. . . . . . . . . 10
β’ ((π§π·π¦) β (0[,]+β) β 0 β€ (π§π·π¦)) |
45 | 40, 44 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β 0 β€ (π§π·π¦)) |
46 | | ge0nemnf 13020 |
. . . . . . . . 9
β’ (((π§π·π¦) β β* β§ 0 β€
(π§π·π¦)) β (π§π·π¦) β -β) |
47 | 42, 45, 46 | syl2anc 584 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π¦) β -β) |
48 | 47 | a1d 25 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (Β¬ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β (π§π·π¦) β -β)) |
49 | 48 | necon4bd 2961 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π§π·π¦) = -β β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
50 | 49 | adantr 481 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β ((π§π·π¦) = -β β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
51 | 50 | imp 407 |
. . . 4
β’ ((((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β§ (π§π·π¦) = -β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
52 | 42 | adantr 481 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β (π§π·π¦) β
β*) |
53 | | elxr 12965 |
. . . . 5
β’ ((π§π·π¦) β β* β ((π§π·π¦) β β β¨ (π§π·π¦) = +β β¨ (π§π·π¦) = -β)) |
54 | 52, 53 | sylib 217 |
. . . 4
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β ((π§π·π¦) β β β¨ (π§π·π¦) = +β β¨ (π§π·π¦) = -β)) |
55 | 16, 38, 51, 54 | mpjao3dan 1431 |
. . 3
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) β β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
56 | 19 | adantr 481 |
. . . 4
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = +β) β (π₯π·π¦) β€ +β) |
57 | | oveq1 7356 |
. . . . 5
β’ ((π§π·π₯) = +β β ((π§π·π₯) +π (π§π·π¦)) = (+β +π (π§π·π¦))) |
58 | | xaddpnf2 13074 |
. . . . . 6
β’ (((π§π·π¦) β β* β§ (π§π·π¦) β -β) β (+β
+π (π§π·π¦)) = +β) |
59 | 42, 47, 58 | syl2anc 584 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (+β +π
(π§π·π¦)) = +β) |
60 | 57, 59 | sylan9eqr 2799 |
. . . 4
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = +β) β ((π§π·π₯) +π (π§π·π¦)) = +β) |
61 | 56, 60 | breqtrrd 5131 |
. . 3
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = +β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
62 | | elxrge0 13302 |
. . . . . . . . 9
β’ ((π§π·π₯) β (0[,]+β) β ((π§π·π₯) β β* β§ 0 β€
(π§π·π₯))) |
63 | 62 | simprbi 497 |
. . . . . . . 8
β’ ((π§π·π₯) β (0[,]+β) β 0 β€ (π§π·π₯)) |
64 | 31, 63 | syl 17 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β 0 β€ (π§π·π₯)) |
65 | | ge0nemnf 13020 |
. . . . . . 7
β’ (((π§π·π₯) β β* β§ 0 β€
(π§π·π₯)) β (π§π·π₯) β -β) |
66 | 33, 64, 65 | syl2anc 584 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π§π·π₯) β -β) |
67 | 66 | a1d 25 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (Β¬ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β (π§π·π₯) β -β)) |
68 | 67 | necon4bd 2961 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π§π·π₯) = -β β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
69 | 68 | imp 407 |
. . 3
β’ (((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β§ (π§π·π₯) = -β) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
70 | | elxr 12965 |
. . . 4
β’ ((π§π·π₯) β β* β ((π§π·π₯) β β β¨ (π§π·π₯) = +β β¨ (π§π·π₯) = -β)) |
71 | 33, 70 | sylib 217 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π§π·π₯) β β β¨ (π§π·π₯) = +β β¨ (π§π·π₯) = -β)) |
72 | 55, 61, 69, 71 | mpjao3dan 1431 |
. 2
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) |
73 | 1, 2, 10, 72 | isxmetd 23601 |
1
β’ (π β π· β (βMetβπ)) |