Step | Hyp | Ref
| Expression |
1 | | resqcl 14112 |
. . . . . . . 8
β’ (π
β β β (π
β2) β
β) |
2 | 1 | adantr 480 |
. . . . . . 7
β’ ((π
β β β§ 0 β€
π
) β (π
β2) β
β) |
3 | 2 | adantr 480 |
. . . . . 6
β’ (((π
β β β§ 0 β€
π
) β§ π‘ β (-π
[,]π
)) β (π
β2) β β) |
4 | | renegcl 11545 |
. . . . . . . . . 10
β’ (π
β β β -π
β
β) |
5 | | iccssre 13430 |
. . . . . . . . . 10
β’ ((-π
β β β§ π
β β) β (-π
[,]π
) β β) |
6 | 4, 5 | mpancom 687 |
. . . . . . . . 9
β’ (π
β β β (-π
[,]π
) β β) |
7 | 6 | sselda 3978 |
. . . . . . . 8
β’ ((π
β β β§ π‘ β (-π
[,]π
)) β π‘ β β) |
8 | 7 | resqcld 14113 |
. . . . . . 7
β’ ((π
β β β§ π‘ β (-π
[,]π
)) β (π‘β2) β β) |
9 | 8 | adantlr 714 |
. . . . . 6
β’ (((π
β β β§ 0 β€
π
) β§ π‘ β (-π
[,]π
)) β (π‘β2) β β) |
10 | 3, 9 | resubcld 11664 |
. . . . 5
β’ (((π
β β β§ 0 β€
π
) β§ π‘ β (-π
[,]π
)) β ((π
β2) β (π‘β2)) β β) |
11 | | elicc2 13413 |
. . . . . . . . 9
β’ ((-π
β β β§ π
β β) β (π‘ β (-π
[,]π
) β (π‘ β β β§ -π
β€ π‘ β§ π‘ β€ π
))) |
12 | 4, 11 | mpancom 687 |
. . . . . . . 8
β’ (π
β β β (π‘ β (-π
[,]π
) β (π‘ β β β§ -π
β€ π‘ β§ π‘ β€ π
))) |
13 | 12 | adantr 480 |
. . . . . . 7
β’ ((π
β β β§ 0 β€
π
) β (π‘ β (-π
[,]π
) β (π‘ β β β§ -π
β€ π‘ β§ π‘ β€ π
))) |
14 | 1 | 3ad2ant1 1131 |
. . . . . . . . . . . . . 14
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β (π
β2) β β) |
15 | | resqcl 14112 |
. . . . . . . . . . . . . . 15
β’ (π‘ β β β (π‘β2) β
β) |
16 | 15 | 3ad2ant3 1133 |
. . . . . . . . . . . . . 14
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β (π‘β2) β β) |
17 | 14, 16 | subge0d 11826 |
. . . . . . . . . . . . 13
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β (0 β€ ((π
β2) β (π‘β2)) β (π‘β2) β€ (π
β2))) |
18 | | absresq 15273 |
. . . . . . . . . . . . . . 15
β’ (π‘ β β β
((absβπ‘)β2) =
(π‘β2)) |
19 | 18 | 3ad2ant3 1133 |
. . . . . . . . . . . . . 14
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β ((absβπ‘)β2) = (π‘β2)) |
20 | 19 | breq1d 5152 |
. . . . . . . . . . . . 13
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β (((absβπ‘)β2) β€ (π
β2) β (π‘β2) β€ (π
β2))) |
21 | 17, 20 | bitr4d 282 |
. . . . . . . . . . . 12
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β (0 β€ ((π
β2) β (π‘β2)) β
((absβπ‘)β2) β€
(π
β2))) |
22 | | recn 11220 |
. . . . . . . . . . . . . . 15
β’ (π‘ β β β π‘ β
β) |
23 | 22 | abscld 15407 |
. . . . . . . . . . . . . 14
β’ (π‘ β β β
(absβπ‘) β
β) |
24 | 23 | 3ad2ant3 1133 |
. . . . . . . . . . . . 13
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β (absβπ‘) β
β) |
25 | | simp1 1134 |
. . . . . . . . . . . . 13
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β π
β β) |
26 | 22 | absge0d 15415 |
. . . . . . . . . . . . . 14
β’ (π‘ β β β 0 β€
(absβπ‘)) |
27 | 26 | 3ad2ant3 1133 |
. . . . . . . . . . . . 13
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β 0 β€
(absβπ‘)) |
28 | | simp2 1135 |
. . . . . . . . . . . . 13
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β 0 β€ π
) |
29 | 24, 25, 27, 28 | le2sqd 14243 |
. . . . . . . . . . . 12
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β ((absβπ‘) β€ π
β ((absβπ‘)β2) β€ (π
β2))) |
30 | | simp3 1136 |
. . . . . . . . . . . . 13
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β π‘ β β) |
31 | 30, 25 | absled 15401 |
. . . . . . . . . . . 12
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β ((absβπ‘) β€ π
β (-π
β€ π‘ β§ π‘ β€ π
))) |
32 | 21, 29, 31 | 3bitr2d 307 |
. . . . . . . . . . 11
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β (0 β€ ((π
β2) β (π‘β2)) β (-π
β€ π‘ β§ π‘ β€ π
))) |
33 | 32 | biimprd 247 |
. . . . . . . . . 10
β’ ((π
β β β§ 0 β€
π
β§ π‘ β β) β ((-π
β€ π‘ β§ π‘ β€ π
) β 0 β€ ((π
β2) β (π‘β2)))) |
34 | 33 | 3expa 1116 |
. . . . . . . . 9
β’ (((π
β β β§ 0 β€
π
) β§ π‘ β β) β ((-π
β€ π‘ β§ π‘ β€ π
) β 0 β€ ((π
β2) β (π‘β2)))) |
35 | 34 | exp4b 430 |
. . . . . . . 8
β’ ((π
β β β§ 0 β€
π
) β (π‘ β β β (-π
β€ π‘ β (π‘ β€ π
β 0 β€ ((π
β2) β (π‘β2)))))) |
36 | 35 | 3impd 1346 |
. . . . . . 7
β’ ((π
β β β§ 0 β€
π
) β ((π‘ β β β§ -π
β€ π‘ β§ π‘ β€ π
) β 0 β€ ((π
β2) β (π‘β2)))) |
37 | 13, 36 | sylbid 239 |
. . . . . 6
β’ ((π
β β β§ 0 β€
π
) β (π‘ β (-π
[,]π
) β 0 β€ ((π
β2) β (π‘β2)))) |
38 | 37 | imp 406 |
. . . . 5
β’ (((π
β β β§ 0 β€
π
) β§ π‘ β (-π
[,]π
)) β 0 β€ ((π
β2) β (π‘β2))) |
39 | | elrege0 13455 |
. . . . 5
β’ (((π
β2) β (π‘β2)) β (0[,)+β)
β (((π
β2) β
(π‘β2)) β β
β§ 0 β€ ((π
β2)
β (π‘β2)))) |
40 | 10, 38, 39 | sylanbrc 582 |
. . . 4
β’ (((π
β β β§ 0 β€
π
) β§ π‘ β (-π
[,]π
)) β ((π
β2) β (π‘β2)) β
(0[,)+β)) |
41 | | fvres 6910 |
. . . 4
β’ (((π
β2) β (π‘β2)) β (0[,)+β)
β ((β βΎ (0[,)+β))β((π
β2) β (π‘β2))) = (ββ((π
β2) β (π‘β2)))) |
42 | 40, 41 | syl 17 |
. . 3
β’ (((π
β β β§ 0 β€
π
) β§ π‘ β (-π
[,]π
)) β ((β βΎ
(0[,)+β))β((π
β2) β (π‘β2))) = (ββ((π
β2) β (π‘β2)))) |
43 | 42 | mpteq2dva 5242 |
. 2
β’ ((π
β β β§ 0 β€
π
) β (π‘ β (-π
[,]π
) β¦ ((β βΎ
(0[,)+β))β((π
β2) β (π‘β2)))) = (π‘ β (-π
[,]π
) β¦ (ββ((π
β2) β (π‘β2))))) |
44 | | eqid 2727 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
45 | 44 | cnfldtopon 24686 |
. . . . . 6
β’
(TopOpenββfld) β
(TopOnββ) |
46 | | ax-resscn 11187 |
. . . . . . 7
β’ β
β β |
47 | 6, 46 | sstrdi 3990 |
. . . . . 6
β’ (π
β β β (-π
[,]π
) β β) |
48 | | resttopon 23052 |
. . . . . 6
β’
(((TopOpenββfld) β (TopOnββ)
β§ (-π
[,]π
) β β) β
((TopOpenββfld) βΎt (-π
[,]π
)) β (TopOnβ(-π
[,]π
))) |
49 | 45, 47, 48 | sylancr 586 |
. . . . 5
β’ (π
β β β
((TopOpenββfld) βΎt (-π
[,]π
)) β (TopOnβ(-π
[,]π
))) |
50 | 49 | adantr 480 |
. . . 4
β’ ((π
β β β§ 0 β€
π
) β
((TopOpenββfld) βΎt (-π
[,]π
)) β (TopOnβ(-π
[,]π
))) |
51 | 47 | resmptd 6038 |
. . . . . . 7
β’ (π
β β β ((π‘ β β β¦ ((π
β2) β (π‘β2))) βΎ (-π
[,]π
)) = (π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2)))) |
52 | 45 | a1i 11 |
. . . . . . . . 9
β’ (π
β β β
(TopOpenββfld) β
(TopOnββ)) |
53 | | recn 11220 |
. . . . . . . . . . 11
β’ (π
β β β π
β
β) |
54 | 53 | sqcld 14132 |
. . . . . . . . . 10
β’ (π
β β β (π
β2) β
β) |
55 | 52, 52, 54 | cnmptc 23553 |
. . . . . . . . 9
β’ (π
β β β (π‘ β β β¦ (π
β2)) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
56 | 44 | sqcn 24781 |
. . . . . . . . . 10
β’ (π‘ β β β¦ (π‘β2)) β
((TopOpenββfld) Cn
(TopOpenββfld)) |
57 | 56 | a1i 11 |
. . . . . . . . 9
β’ (π
β β β (π‘ β β β¦ (π‘β2)) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
58 | 44 | subcn 24769 |
. . . . . . . . . 10
β’ β
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
59 | 58 | a1i 11 |
. . . . . . . . 9
β’ (π
β β β β
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
60 | 52, 55, 57, 59 | cnmpt12f 23557 |
. . . . . . . 8
β’ (π
β β β (π‘ β β β¦ ((π
β2) β (π‘β2))) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
61 | 45 | toponunii 22805 |
. . . . . . . . 9
β’ β =
βͺ
(TopOpenββfld) |
62 | 61 | cnrest 23176 |
. . . . . . . 8
β’ (((π‘ β β β¦ ((π
β2) β (π‘β2))) β
((TopOpenββfld) Cn
(TopOpenββfld)) β§ (-π
[,]π
) β β) β ((π‘ β β β¦ ((π
β2) β (π‘β2))) βΎ (-π
[,]π
)) β
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn
(TopOpenββfld))) |
63 | 60, 47, 62 | syl2anc 583 |
. . . . . . 7
β’ (π
β β β ((π‘ β β β¦ ((π
β2) β (π‘β2))) βΎ (-π
[,]π
)) β
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn
(TopOpenββfld))) |
64 | 51, 63 | eqeltrrd 2829 |
. . . . . 6
β’ (π
β β β (π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) β
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn
(TopOpenββfld))) |
65 | 64 | adantr 480 |
. . . . 5
β’ ((π
β β β§ 0 β€
π
) β (π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) β
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn
(TopOpenββfld))) |
66 | 45 | a1i 11 |
. . . . . 6
β’ ((π
β β β§ 0 β€
π
) β
(TopOpenββfld) β
(TopOnββ)) |
67 | | eqid 2727 |
. . . . . . . 8
β’ (π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) = (π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) |
68 | 67 | rnmpt 5951 |
. . . . . . 7
β’ ran
(π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) = {π’ β£ βπ‘ β (-π
[,]π
)π’ = ((π
β2) β (π‘β2))} |
69 | | simp3 1136 |
. . . . . . . . . 10
β’ (((π
β β β§ 0 β€
π
) β§ π‘ β (-π
[,]π
) β§ π’ = ((π
β2) β (π‘β2))) β π’ = ((π
β2) β (π‘β2))) |
70 | 40 | 3adant3 1130 |
. . . . . . . . . 10
β’ (((π
β β β§ 0 β€
π
) β§ π‘ β (-π
[,]π
) β§ π’ = ((π
β2) β (π‘β2))) β ((π
β2) β (π‘β2)) β
(0[,)+β)) |
71 | 69, 70 | eqeltrd 2828 |
. . . . . . . . 9
β’ (((π
β β β§ 0 β€
π
) β§ π‘ β (-π
[,]π
) β§ π’ = ((π
β2) β (π‘β2))) β π’ β (0[,)+β)) |
72 | 71 | rexlimdv3a 3154 |
. . . . . . . 8
β’ ((π
β β β§ 0 β€
π
) β (βπ‘ β (-π
[,]π
)π’ = ((π
β2) β (π‘β2)) β π’ β (0[,)+β))) |
73 | 72 | abssdv 4061 |
. . . . . . 7
β’ ((π
β β β§ 0 β€
π
) β {π’ β£ βπ‘ β (-π
[,]π
)π’ = ((π
β2) β (π‘β2))} β
(0[,)+β)) |
74 | 68, 73 | eqsstrid 4026 |
. . . . . 6
β’ ((π
β β β§ 0 β€
π
) β ran (π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) β
(0[,)+β)) |
75 | | rge0ssre 13457 |
. . . . . . . 8
β’
(0[,)+β) β β |
76 | 75, 46 | sstri 3987 |
. . . . . . 7
β’
(0[,)+β) β β |
77 | 76 | a1i 11 |
. . . . . 6
β’ ((π
β β β§ 0 β€
π
) β (0[,)+β)
β β) |
78 | | cnrest2 23177 |
. . . . . 6
β’
(((TopOpenββfld) β (TopOnββ)
β§ ran (π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) β (0[,)+β) β§
(0[,)+β) β β) β ((π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) β
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn (TopOpenββfld))
β (π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) β
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn ((TopOpenββfld)
βΎt (0[,)+β))))) |
79 | 66, 74, 77, 78 | syl3anc 1369 |
. . . . 5
β’ ((π
β β β§ 0 β€
π
) β ((π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) β
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn (TopOpenββfld))
β (π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) β
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn ((TopOpenββfld)
βΎt (0[,)+β))))) |
80 | 65, 79 | mpbid 231 |
. . . 4
β’ ((π
β β β§ 0 β€
π
) β (π‘ β (-π
[,]π
) β¦ ((π
β2) β (π‘β2))) β
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn ((TopOpenββfld)
βΎt (0[,)+β)))) |
81 | | ssid 4000 |
. . . . . . . 8
β’ β
β β |
82 | | cncfss 24806 |
. . . . . . . 8
β’ ((β
β β β§ β β β) β
((0[,)+β)βcnββ)
β ((0[,)+β)βcnββ)) |
83 | 46, 81, 82 | mp2an 691 |
. . . . . . 7
β’
((0[,)+β)βcnββ) β ((0[,)+β)βcnββ) |
84 | | resqrtcn 26671 |
. . . . . . 7
β’ (β
βΎ (0[,)+β)) β ((0[,)+β)βcnββ) |
85 | 83, 84 | sselii 3975 |
. . . . . 6
β’ (β
βΎ (0[,)+β)) β ((0[,)+β)βcnββ) |
86 | | eqid 2727 |
. . . . . . . 8
β’
((TopOpenββfld) βΎt
(0[,)+β)) = ((TopOpenββfld) βΎt
(0[,)+β)) |
87 | | eqid 2727 |
. . . . . . . 8
β’
((TopOpenββfld) βΎt β) =
((TopOpenββfld) βΎt
β) |
88 | 44, 86, 87 | cncfcn 24817 |
. . . . . . 7
β’
(((0[,)+β) β β β§ β β β) β
((0[,)+β)βcnββ) =
(((TopOpenββfld) βΎt (0[,)+β)) Cn
((TopOpenββfld) βΎt
β))) |
89 | 76, 81, 88 | mp2an 691 |
. . . . . 6
β’
((0[,)+β)βcnββ) =
(((TopOpenββfld) βΎt (0[,)+β)) Cn
((TopOpenββfld) βΎt
β)) |
90 | 85, 89 | eleqtri 2826 |
. . . . 5
β’ (β
βΎ (0[,)+β)) β (((TopOpenββfld)
βΎt (0[,)+β)) Cn ((TopOpenββfld)
βΎt β)) |
91 | 90 | a1i 11 |
. . . 4
β’ ((π
β β β§ 0 β€
π
) β (β βΎ
(0[,)+β)) β (((TopOpenββfld)
βΎt (0[,)+β)) Cn ((TopOpenββfld)
βΎt β))) |
92 | 50, 80, 91 | cnmpt11f 23555 |
. . 3
β’ ((π
β β β§ 0 β€
π
) β (π‘ β (-π
[,]π
) β¦ ((β βΎ
(0[,)+β))β((π
β2) β (π‘β2)))) β
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn ((TopOpenββfld)
βΎt β))) |
93 | | eqid 2727 |
. . . . . 6
β’
((TopOpenββfld) βΎt (-π
[,]π
)) = ((TopOpenββfld)
βΎt (-π
[,]π
)) |
94 | 44, 93, 87 | cncfcn 24817 |
. . . . 5
β’ (((-π
[,]π
) β β β§ β β
β) β ((-π
[,]π
)βcnββ) =
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn ((TopOpenββfld)
βΎt β))) |
95 | 47, 81, 94 | sylancl 585 |
. . . 4
β’ (π
β β β ((-π
[,]π
)βcnββ) =
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn ((TopOpenββfld)
βΎt β))) |
96 | 95 | adantr 480 |
. . 3
β’ ((π
β β β§ 0 β€
π
) β ((-π
[,]π
)βcnββ) =
(((TopOpenββfld) βΎt (-π
[,]π
)) Cn ((TopOpenββfld)
βΎt β))) |
97 | 92, 96 | eleqtrrd 2831 |
. 2
β’ ((π
β β β§ 0 β€
π
) β (π‘ β (-π
[,]π
) β¦ ((β βΎ
(0[,)+β))β((π
β2) β (π‘β2)))) β ((-π
[,]π
)βcnββ)) |
98 | 43, 97 | eqeltrrd 2829 |
1
β’ ((π
β β β§ 0 β€
π
) β (π‘ β (-π
[,]π
) β¦ (ββ((π
β2) β (π‘β2)))) β ((-π
[,]π
)βcnββ)) |