Step | Hyp | Ref
| Expression |
1 | | xmetf 23705 |
. 2
β’ (π· β (βMetβπ) β π·:(π Γ π)βΆβ*) |
2 | | rphalfcl 12950 |
. . . . 5
β’ (π β β+
β (π / 2) β
β+) |
3 | | xmetdcn2.1 |
. . . . . . . 8
β’ π½ = (MetOpenβπ·) |
4 | | xmetdcn2.2 |
. . . . . . . 8
β’ πΆ =
(distββ*π ) |
5 | | xmetdcn2.3 |
. . . . . . . 8
β’ πΎ = (MetOpenβπΆ) |
6 | | simp-4l 782 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
(π₯ β π β§ π¦ β π)) β§ π β β+) β§ (π§ β π β§ π€ β π)) β§ ((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2))) β π· β (βMetβπ)) |
7 | | simplrl 776 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β§ π β β+) β π₯ β π) |
8 | 7 | ad2antrr 725 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
(π₯ β π β§ π¦ β π)) β§ π β β+) β§ (π§ β π β§ π€ β π)) β§ ((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2))) β π₯ β π) |
9 | | simplrr 777 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β§ π β β+) β π¦ β π) |
10 | 9 | ad2antrr 725 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
(π₯ β π β§ π¦ β π)) β§ π β β+) β§ (π§ β π β§ π€ β π)) β§ ((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2))) β π¦ β π) |
11 | | simpllr 775 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
(π₯ β π β§ π¦ β π)) β§ π β β+) β§ (π§ β π β§ π€ β π)) β§ ((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2))) β π β β+) |
12 | | simplrl 776 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
(π₯ β π β§ π¦ β π)) β§ π β β+) β§ (π§ β π β§ π€ β π)) β§ ((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2))) β π§ β π) |
13 | | simplrr 777 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
(π₯ β π β§ π¦ β π)) β§ π β β+) β§ (π§ β π β§ π€ β π)) β§ ((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2))) β π€ β π) |
14 | | simprl 770 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
(π₯ β π β§ π¦ β π)) β§ π β β+) β§ (π§ β π β§ π€ β π)) β§ ((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2))) β (π₯π·π§) < (π / 2)) |
15 | | simprr 772 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
(π₯ β π β§ π¦ β π)) β§ π β β+) β§ (π§ β π β§ π€ β π)) β§ ((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2))) β (π¦π·π€) < (π / 2)) |
16 | 3, 4, 5, 6, 8, 10,
11, 12, 13, 14, 15 | metdcnlem 24222 |
. . . . . . 7
β’
(((((π· β
(βMetβπ) β§
(π₯ β π β§ π¦ β π)) β§ π β β+) β§ (π§ β π β§ π€ β π)) β§ ((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2))) β ((π₯π·π¦)πΆ(π§π·π€)) < π) |
17 | 16 | ex 414 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β§ π β β+) β§ (π§ β π β§ π€ β π)) β (((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2)) β ((π₯π·π¦)πΆ(π§π·π€)) < π)) |
18 | 17 | ralrimivva 3194 |
. . . . 5
β’ (((π· β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β§ π β β+) β
βπ§ β π βπ€ β π (((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2)) β ((π₯π·π¦)πΆ(π§π·π€)) < π)) |
19 | | breq2 5113 |
. . . . . . . . 9
β’ (π = (π / 2) β ((π₯π·π§) < π β (π₯π·π§) < (π / 2))) |
20 | | breq2 5113 |
. . . . . . . . 9
β’ (π = (π / 2) β ((π¦π·π€) < π β (π¦π·π€) < (π / 2))) |
21 | 19, 20 | anbi12d 632 |
. . . . . . . 8
β’ (π = (π / 2) β (((π₯π·π§) < π β§ (π¦π·π€) < π ) β ((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2)))) |
22 | 21 | imbi1d 342 |
. . . . . . 7
β’ (π = (π / 2) β ((((π₯π·π§) < π β§ (π¦π·π€) < π ) β ((π₯π·π¦)πΆ(π§π·π€)) < π) β (((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2)) β ((π₯π·π¦)πΆ(π§π·π€)) < π))) |
23 | 22 | 2ralbidv 3209 |
. . . . . 6
β’ (π = (π / 2) β (βπ§ β π βπ€ β π (((π₯π·π§) < π β§ (π¦π·π€) < π ) β ((π₯π·π¦)πΆ(π§π·π€)) < π) β βπ§ β π βπ€ β π (((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2)) β ((π₯π·π¦)πΆ(π§π·π€)) < π))) |
24 | 23 | rspcev 3583 |
. . . . 5
β’ (((π / 2) β β+
β§ βπ§ β
π βπ€ β π (((π₯π·π§) < (π / 2) β§ (π¦π·π€) < (π / 2)) β ((π₯π·π¦)πΆ(π§π·π€)) < π)) β βπ β β+ βπ§ β π βπ€ β π (((π₯π·π§) < π β§ (π¦π·π€) < π ) β ((π₯π·π¦)πΆ(π§π·π€)) < π)) |
25 | 2, 18, 24 | syl2an2 685 |
. . . 4
β’ (((π· β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β§ π β β+) β
βπ β
β+ βπ§ β π βπ€ β π (((π₯π·π§) < π β§ (π¦π·π€) < π ) β ((π₯π·π¦)πΆ(π§π·π€)) < π)) |
26 | 25 | ralrimiva 3140 |
. . 3
β’ ((π· β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β βπ β β+ βπ β β+
βπ§ β π βπ€ β π (((π₯π·π§) < π β§ (π¦π·π€) < π ) β ((π₯π·π¦)πΆ(π§π·π€)) < π)) |
27 | 26 | ralrimivva 3194 |
. 2
β’ (π· β (βMetβπ) β βπ₯ β π βπ¦ β π βπ β β+ βπ β β+
βπ§ β π βπ€ β π (((π₯π·π§) < π β§ (π¦π·π€) < π ) β ((π₯π·π¦)πΆ(π§π·π€)) < π)) |
28 | | id 22 |
. . 3
β’ (π· β (βMetβπ) β π· β (βMetβπ)) |
29 | 4 | xrsxmet 24195 |
. . . 4
β’ πΆ β
(βMetββ*) |
30 | 29 | a1i 11 |
. . 3
β’ (π· β (βMetβπ) β πΆ β
(βMetββ*)) |
31 | 3, 3, 5 | txmetcn 23927 |
. . 3
β’ ((π· β (βMetβπ) β§ π· β (βMetβπ) β§ πΆ β
(βMetββ*)) β (π· β ((π½ Γt π½) Cn πΎ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π βπ β β+ βπ β β+
βπ§ β π βπ€ β π (((π₯π·π§) < π β§ (π¦π·π€) < π ) β ((π₯π·π¦)πΆ(π§π·π€)) < π)))) |
32 | 28, 30, 31 | mpd3an23 1464 |
. 2
β’ (π· β (βMetβπ) β (π· β ((π½ Γt π½) Cn πΎ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π βπ β β+ βπ β β+
βπ§ β π βπ€ β π (((π₯π·π§) < π β§ (π¦π·π€) < π ) β ((π₯π·π¦)πΆ(π§π·π€)) < π)))) |
33 | 1, 27, 32 | mpbir2and 712 |
1
β’ (π· β (βMetβπ) β π· β ((π½ Γt π½) Cn πΎ)) |