Step | Hyp | Ref
| Expression |
1 | | addcn.2 |
. 2
β’ + :(β
Γ β)βΆβ |
2 | | addcn.3 |
. . . . 5
β’ ((π β β+
β§ π β β
β§ π β β)
β βπ¦ β
β+ βπ§ β β+ βπ’ β β βπ£ β β
(((absβ(π’ β
π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ((π’ + π£) β (π + π))) < π)) |
3 | 2 | 3coml 1128 |
. . . 4
β’ ((π β β β§ π β β β§ π β β+)
β βπ¦ β
β+ βπ§ β β+ βπ’ β β βπ£ β β
(((absβ(π’ β
π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ((π’ + π£) β (π + π))) < π)) |
4 | | ifcl 4535 |
. . . . . . 7
β’ ((π¦ β β+
β§ π§ β
β+) β if(π¦ β€ π§, π¦, π§) β
β+) |
5 | 4 | adantl 483 |
. . . . . 6
β’ (((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β if(π¦ β€ π§, π¦, π§) β
β+) |
6 | | simpll1 1213 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β π β β) |
7 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β π’ β β) |
8 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (abs
β β ) = (abs β β ) |
9 | 8 | cnmetdval 24157 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π’ β β) β (π(abs β β )π’) = (absβ(π β π’))) |
10 | | abssub 15220 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π’ β β) β
(absβ(π β π’)) = (absβ(π’ β π))) |
11 | 9, 10 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π’ β β) β (π(abs β β )π’) = (absβ(π’ β π))) |
12 | 6, 7, 11 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β (π(abs β β )π’) = (absβ(π’ β π))) |
13 | 12 | breq1d 5119 |
. . . . . . . . . . 11
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((π(abs β β )π’) < if(π¦ β€ π§, π¦, π§) β (absβ(π’ β π)) < if(π¦ β€ π§, π¦, π§))) |
14 | 7, 6 | subcld 11520 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β (π’ β π) β β) |
15 | 14 | abscld 15330 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β (absβ(π’ β π)) β β) |
16 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β π¦ β β+) |
17 | 16 | rpred 12965 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β π¦ β β) |
18 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β π§ β β+) |
19 | 18 | rpred 12965 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β π§ β β) |
20 | | ltmin 13122 |
. . . . . . . . . . . 12
β’
(((absβ(π’
β π)) β β
β§ π¦ β β
β§ π§ β β)
β ((absβ(π’
β π)) < if(π¦ β€ π§, π¦, π§) β ((absβ(π’ β π)) < π¦ β§ (absβ(π’ β π)) < π§))) |
21 | 15, 17, 19, 20 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((absβ(π’ β π)) < if(π¦ β€ π§, π¦, π§) β ((absβ(π’ β π)) < π¦ β§ (absβ(π’ β π)) < π§))) |
22 | 13, 21 | bitrd 279 |
. . . . . . . . . 10
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((π(abs β β )π’) < if(π¦ β€ π§, π¦, π§) β ((absβ(π’ β π)) < π¦ β§ (absβ(π’ β π)) < π§))) |
23 | | simpl 484 |
. . . . . . . . . 10
β’
(((absβ(π’
β π)) < π¦ β§ (absβ(π’ β π)) < π§) β (absβ(π’ β π)) < π¦) |
24 | 22, 23 | syl6bi 253 |
. . . . . . . . 9
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((π(abs β β )π’) < if(π¦ β€ π§, π¦, π§) β (absβ(π’ β π)) < π¦)) |
25 | | simpll2 1214 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β π β β) |
26 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β π£ β β) |
27 | 8 | cnmetdval 24157 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π£ β β) β (π(abs β β )π£) = (absβ(π β π£))) |
28 | | abssub 15220 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π£ β β) β
(absβ(π β π£)) = (absβ(π£ β π))) |
29 | 27, 28 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π£ β β) β (π(abs β β )π£) = (absβ(π£ β π))) |
30 | 25, 26, 29 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β (π(abs β β )π£) = (absβ(π£ β π))) |
31 | 30 | breq1d 5119 |
. . . . . . . . . . 11
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((π(abs β β )π£) < if(π¦ β€ π§, π¦, π§) β (absβ(π£ β π)) < if(π¦ β€ π§, π¦, π§))) |
32 | 26, 25 | subcld 11520 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β (π£ β π) β β) |
33 | 32 | abscld 15330 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β (absβ(π£ β π)) β β) |
34 | | ltmin 13122 |
. . . . . . . . . . . 12
β’
(((absβ(π£
β π)) β β
β§ π¦ β β
β§ π§ β β)
β ((absβ(π£
β π)) < if(π¦ β€ π§, π¦, π§) β ((absβ(π£ β π)) < π¦ β§ (absβ(π£ β π)) < π§))) |
35 | 33, 17, 19, 34 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((absβ(π£ β π)) < if(π¦ β€ π§, π¦, π§) β ((absβ(π£ β π)) < π¦ β§ (absβ(π£ β π)) < π§))) |
36 | 31, 35 | bitrd 279 |
. . . . . . . . . 10
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((π(abs β β )π£) < if(π¦ β€ π§, π¦, π§) β ((absβ(π£ β π)) < π¦ β§ (absβ(π£ β π)) < π§))) |
37 | | simpr 486 |
. . . . . . . . . 10
β’
(((absβ(π£
β π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ(π£ β π)) < π§) |
38 | 36, 37 | syl6bi 253 |
. . . . . . . . 9
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((π(abs β β )π£) < if(π¦ β€ π§, π¦, π§) β (absβ(π£ β π)) < π§)) |
39 | 24, 38 | anim12d 610 |
. . . . . . . 8
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β (((π(abs β β )π’) < if(π¦ β€ π§, π¦, π§) β§ (π(abs β β )π£) < if(π¦ β€ π§, π¦, π§)) β ((absβ(π’ β π)) < π¦ β§ (absβ(π£ β π)) < π§))) |
40 | 1 | fovcl 7488 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β (π + π) β β) |
41 | 6, 25, 40 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β (π + π) β β) |
42 | 1 | fovcl 7488 |
. . . . . . . . . . . 12
β’ ((π’ β β β§ π£ β β) β (π’ + π£) β β) |
43 | 42 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β (π’ + π£) β β) |
44 | 8 | cnmetdval 24157 |
. . . . . . . . . . . 12
β’ (((π + π) β β β§ (π’ + π£) β β) β ((π + π)(abs β β )(π’ + π£)) = (absβ((π + π) β (π’ + π£)))) |
45 | | abssub 15220 |
. . . . . . . . . . . 12
β’ (((π + π) β β β§ (π’ + π£) β β) β (absβ((π + π) β (π’ + π£))) = (absβ((π’ + π£) β (π + π)))) |
46 | 44, 45 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((π + π) β β β§ (π’ + π£) β β) β ((π + π)(abs β β )(π’ + π£)) = (absβ((π’ + π£) β (π + π)))) |
47 | 41, 43, 46 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((π + π)(abs β β )(π’ + π£)) = (absβ((π’ + π£) β (π + π)))) |
48 | 47 | breq1d 5119 |
. . . . . . . . 9
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β (((π + π)(abs β β )(π’ + π£)) < π β (absβ((π’ + π£) β (π + π))) < π)) |
49 | 48 | biimprd 248 |
. . . . . . . 8
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((absβ((π’ + π£) β (π + π))) < π β ((π + π)(abs β β )(π’ + π£)) < π)) |
50 | 39, 49 | imim12d 81 |
. . . . . . 7
β’ ((((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β§ (π’ β β β§ π£ β β)) β ((((absβ(π’ β π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ((π’ + π£) β (π + π))) < π) β (((π(abs β β )π’) < if(π¦ β€ π§, π¦, π§) β§ (π(abs β β )π£) < if(π¦ β€ π§, π¦, π§)) β ((π + π)(abs β β )(π’ + π£)) < π))) |
51 | 50 | ralimdvva 3198 |
. . . . . 6
β’ (((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β (βπ’ β β βπ£ β β (((absβ(π’ β π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ((π’ + π£) β (π + π))) < π) β βπ’ β β βπ£ β β (((π(abs β β )π’) < if(π¦ β€ π§, π¦, π§) β§ (π(abs β β )π£) < if(π¦ β€ π§, π¦, π§)) β ((π + π)(abs β β )(π’ + π£)) < π))) |
52 | | breq2 5113 |
. . . . . . . . . 10
β’ (π₯ = if(π¦ β€ π§, π¦, π§) β ((π(abs β β )π’) < π₯ β (π(abs β β )π’) < if(π¦ β€ π§, π¦, π§))) |
53 | | breq2 5113 |
. . . . . . . . . 10
β’ (π₯ = if(π¦ β€ π§, π¦, π§) β ((π(abs β β )π£) < π₯ β (π(abs β β )π£) < if(π¦ β€ π§, π¦, π§))) |
54 | 52, 53 | anbi12d 632 |
. . . . . . . . 9
β’ (π₯ = if(π¦ β€ π§, π¦, π§) β (((π(abs β β )π’) < π₯ β§ (π(abs β β )π£) < π₯) β ((π(abs β β )π’) < if(π¦ β€ π§, π¦, π§) β§ (π(abs β β )π£) < if(π¦ β€ π§, π¦, π§)))) |
55 | 54 | imbi1d 342 |
. . . . . . . 8
β’ (π₯ = if(π¦ β€ π§, π¦, π§) β ((((π(abs β β )π’) < π₯ β§ (π(abs β β )π£) < π₯) β ((π + π)(abs β β )(π’ + π£)) < π) β (((π(abs β β )π’) < if(π¦ β€ π§, π¦, π§) β§ (π(abs β β )π£) < if(π¦ β€ π§, π¦, π§)) β ((π + π)(abs β β )(π’ + π£)) < π))) |
56 | 55 | 2ralbidv 3209 |
. . . . . . 7
β’ (π₯ = if(π¦ β€ π§, π¦, π§) β (βπ’ β β βπ£ β β (((π(abs β β )π’) < π₯ β§ (π(abs β β )π£) < π₯) β ((π + π)(abs β β )(π’ + π£)) < π) β βπ’ β β βπ£ β β (((π(abs β β )π’) < if(π¦ β€ π§, π¦, π§) β§ (π(abs β β )π£) < if(π¦ β€ π§, π¦, π§)) β ((π + π)(abs β β )(π’ + π£)) < π))) |
57 | 56 | rspcev 3583 |
. . . . . 6
β’
((if(π¦ β€ π§, π¦, π§) β β+ β§
βπ’ β β
βπ£ β β
(((π(abs β β
)π’) < if(π¦ β€ π§, π¦, π§) β§ (π(abs β β )π£) < if(π¦ β€ π§, π¦, π§)) β ((π + π)(abs β β )(π’ + π£)) < π)) β βπ₯ β β+ βπ’ β β βπ£ β β (((π(abs β β )π’) < π₯ β§ (π(abs β β )π£) < π₯) β ((π + π)(abs β β )(π’ + π£)) < π)) |
58 | 5, 51, 57 | syl6an 683 |
. . . . 5
β’ (((π β β β§ π β β β§ π β β+)
β§ (π¦ β
β+ β§ π§
β β+)) β (βπ’ β β βπ£ β β (((absβ(π’ β π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ((π’ + π£) β (π + π))) < π) β βπ₯ β β+ βπ’ β β βπ£ β β (((π(abs β β )π’) < π₯ β§ (π(abs β β )π£) < π₯) β ((π + π)(abs β β )(π’ + π£)) < π))) |
59 | 58 | rexlimdvva 3202 |
. . . 4
β’ ((π β β β§ π β β β§ π β β+)
β (βπ¦ β
β+ βπ§ β β+ βπ’ β β βπ£ β β
(((absβ(π’ β
π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ((π’ + π£) β (π + π))) < π) β βπ₯ β β+ βπ’ β β βπ£ β β (((π(abs β β )π’) < π₯ β§ (π(abs β β )π£) < π₯) β ((π + π)(abs β β )(π’ + π£)) < π))) |
60 | 3, 59 | mpd 15 |
. . 3
β’ ((π β β β§ π β β β§ π β β+)
β βπ₯ β
β+ βπ’ β β βπ£ β β (((π(abs β β )π’) < π₯ β§ (π(abs β β )π£) < π₯) β ((π + π)(abs β β )(π’ + π£)) < π)) |
61 | 60 | rgen3 3196 |
. 2
β’
βπ β
β βπ β
β βπ β
β+ βπ₯ β β+ βπ’ β β βπ£ β β (((π(abs β β )π’) < π₯ β§ (π(abs β β )π£) < π₯) β ((π + π)(abs β β )(π’ + π£)) < π) |
62 | | cnxmet 24159 |
. . 3
β’ (abs
β β ) β (βMetββ) |
63 | | addcn.j |
. . . . 5
β’ π½ =
(TopOpenββfld) |
64 | 63 | cnfldtopn 24168 |
. . . 4
β’ π½ = (MetOpenβ(abs β
β )) |
65 | 64, 64, 64 | txmetcn 23927 |
. . 3
β’ (((abs
β β ) β (βMetββ) β§ (abs β β
) β (βMetββ) β§ (abs β β ) β
(βMetββ)) β ( + β ((π½ Γt π½) Cn π½) β ( + :(β Γ
β)βΆβ β§ βπ β β βπ β β βπ β β+ βπ₯ β β+
βπ’ β β
βπ£ β β
(((π(abs β β
)π’) < π₯ β§ (π(abs β β )π£) < π₯) β ((π + π)(abs β β )(π’ + π£)) < π)))) |
66 | 62, 62, 62, 65 | mp3an 1462 |
. 2
β’ ( + β
((π½ Γt
π½) Cn π½) β ( + :(β Γ
β)βΆβ β§ βπ β β βπ β β βπ β β+ βπ₯ β β+
βπ’ β β
βπ£ β β
(((π(abs β β
)π’) < π₯ β§ (π(abs β β )π£) < π₯) β ((π + π)(abs β β )(π’ + π£)) < π))) |
67 | 1, 61, 66 | mpbir2an 710 |
1
β’ + β
((π½ Γt
π½) Cn π½) |