Step | Hyp | Ref
| Expression |
1 | | rpreccl 12949 |
. . . . . . . . 9
β’ (π β β+
β (1 / π) β
β+) |
2 | 1 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β+) β (1 /
π) β
β+) |
3 | | rpreccl 12949 |
. . . . . . . . 9
β’ (π‘ β β+
β (1 / π‘) β
β+) |
4 | | rpcnne0 12941 |
. . . . . . . . . . . 12
β’ (π‘ β β+
β (π‘ β β
β§ π‘ β
0)) |
5 | 4 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β β+) β (π‘ β β β§ π‘ β 0)) |
6 | | recrec 11860 |
. . . . . . . . . . 11
β’ ((π‘ β β β§ π‘ β 0) β (1 / (1 / π‘)) = π‘) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π‘ β β+) β (1 / (1 /
π‘)) = π‘) |
8 | 7 | eqcomd 2739 |
. . . . . . . . 9
β’ ((π β§ π‘ β β+) β π‘ = (1 / (1 / π‘))) |
9 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = (1 / π‘) β (1 / π) = (1 / (1 / π‘))) |
10 | 9 | rspceeqv 3599 |
. . . . . . . . 9
β’ (((1 /
π‘) β
β+ β§ π‘
= (1 / (1 / π‘))) β
βπ β
β+ π‘ = (1
/ π)) |
11 | 3, 8, 10 | syl2an2 685 |
. . . . . . . 8
β’ ((π β§ π‘ β β+) β
βπ β
β+ π‘ = (1
/ π)) |
12 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π‘ = (1 / π)) β π‘ = (1 / π)) |
13 | 12 | breq1d 5119 |
. . . . . . . . . 10
β’ ((π β§ π‘ = (1 / π)) β (π‘ < π¦ β (1 / π) < π¦)) |
14 | 13 | imbi1d 342 |
. . . . . . . . 9
β’ ((π β§ π‘ = (1 / π)) β ((π‘ < π¦ β (absβ(π β πΆ)) < π§) β ((1 / π) < π¦ β (absβ(π β πΆ)) < π§))) |
15 | 14 | ralbidv 3171 |
. . . . . . . 8
β’ ((π β§ π‘ = (1 / π)) β (βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§) β βπ¦ β π΅ ((1 / π) < π¦ β (absβ(π β πΆ)) < π§))) |
16 | 2, 11, 15 | rexxfrd 5368 |
. . . . . . 7
β’ (π β (βπ‘ β β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§) β βπ β β+ βπ¦ β π΅ ((1 / π) < π¦ β (absβ(π β πΆ)) < π§))) |
17 | 16 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β β+) β
(βπ‘ β
β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§) β βπ β β+ βπ¦ β π΅ ((1 / π) < π¦ β (absβ(π β πΆ)) < π§))) |
18 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π¦ β π΅) β π β β+) |
19 | | rlimcnp.b |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β
β+) |
20 | 19 | sselda 3948 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β π΅) β π¦ β β+) |
21 | 20 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π¦ β π΅) β π¦ β β+) |
22 | | elrp 12925 |
. . . . . . . . . . . . . 14
β’ (π β β+
β (π β β
β§ 0 < π)) |
23 | | elrp 12925 |
. . . . . . . . . . . . . 14
β’ (π¦ β β+
β (π¦ β β
β§ 0 < π¦)) |
24 | | ltrec1 12050 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ 0 <
π) β§ (π¦ β β β§ 0 <
π¦)) β ((1 / π) < π¦ β (1 / π¦) < π)) |
25 | 22, 23, 24 | syl2anb 599 |
. . . . . . . . . . . . 13
β’ ((π β β+
β§ π¦ β
β+) β ((1 / π) < π¦ β (1 / π¦) < π)) |
26 | 18, 21, 25 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π¦ β π΅) β ((1 / π) < π¦ β (1 / π¦) < π)) |
27 | 26 | imbi1d 342 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π¦ β π΅) β (((1 / π) < π¦ β (absβ(π β πΆ)) < π§) β ((1 / π¦) < π β (absβ(π β πΆ)) < π§))) |
28 | 27 | ralbidva 3169 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β
(βπ¦ β π΅ ((1 / π) < π¦ β (absβ(π β πΆ)) < π§) β βπ¦ β π΅ ((1 / π¦) < π β (absβ(π β πΆ)) < π§))) |
29 | 28 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π§ β β+) β§ π β β+)
β (βπ¦ β
π΅ ((1 / π) < π¦ β (absβ(π β πΆ)) < π§) β βπ¦ β π΅ ((1 / π¦) < π β (absβ(π β πΆ)) < π§))) |
30 | | rpcn 12933 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β+
β π¦ β
β) |
31 | | rpne0 12939 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β+
β π¦ β
0) |
32 | 30, 31 | recrecd 11936 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β+
β (1 / (1 / π¦)) =
π¦) |
33 | 20, 32 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β π΅) β (1 / (1 / π¦)) = π¦) |
34 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β π΅) β π¦ β π΅) |
35 | 33, 34 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β π΅) β (1 / (1 / π¦)) β π΅) |
36 | | eleq1 2822 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (1 / π¦) β (π₯ β π΄ β (1 / π¦) β π΄)) |
37 | | oveq2 7369 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (1 / π¦) β (1 / π₯) = (1 / (1 / π¦))) |
38 | 37 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (1 / π¦) β ((1 / π₯) β π΅ β (1 / (1 / π¦)) β π΅)) |
39 | 36, 38 | bibi12d 346 |
. . . . . . . . . . . . . 14
β’ (π₯ = (1 / π¦) β ((π₯ β π΄ β (1 / π₯) β π΅) β ((1 / π¦) β π΄ β (1 / (1 / π¦)) β π΅))) |
40 | | rlimcnp.d |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β+) β (π₯ β π΄ β (1 / π₯) β π΅)) |
41 | 40 | ralrimiva 3140 |
. . . . . . . . . . . . . . 15
β’ (π β βπ₯ β β+ (π₯ β π΄ β (1 / π₯) β π΅)) |
42 | 41 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β π΅) β βπ₯ β β+ (π₯ β π΄ β (1 / π₯) β π΅)) |
43 | 20 | rpreccld 12975 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β π΅) β (1 / π¦) β
β+) |
44 | 39, 42, 43 | rspcdva 3584 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β π΅) β ((1 / π¦) β π΄ β (1 / (1 / π¦)) β π΅)) |
45 | 35, 44 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π΅) β (1 / π¦) β π΄) |
46 | 43 | rpne0d 12970 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π΅) β (1 / π¦) β 0) |
47 | | eldifsn 4751 |
. . . . . . . . . . . 12
β’ ((1 /
π¦) β (π΄ β {0}) β ((1 / π¦) β π΄ β§ (1 / π¦) β 0)) |
48 | 45, 46, 47 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΅) β (1 / π¦) β (π΄ β {0})) |
49 | | eldifi 4090 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΄ β {0}) β π₯ β π΄) |
50 | 49 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄ β {0})) β π₯ β π΄) |
51 | | rge0ssre 13382 |
. . . . . . . . . . . . . . . 16
β’
(0[,)+β) β β |
52 | | rlimcnp.a |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β (0[,)+β)) |
53 | 52 | ssdifssd 4106 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΄ β {0}) β
(0[,)+β)) |
54 | 53 | sselda 3948 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (π΄ β {0})) β π₯ β (0[,)+β)) |
55 | 51, 54 | sselid 3946 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (π΄ β {0})) β π₯ β β) |
56 | | 0re 11165 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 β
β |
57 | | pnfxr 11217 |
. . . . . . . . . . . . . . . . . . 19
β’ +β
β β* |
58 | | elico2 13337 |
. . . . . . . . . . . . . . . . . . 19
β’ ((0
β β β§ +β β β*) β (π₯ β (0[,)+β) β
(π₯ β β β§ 0
β€ π₯ β§ π₯ <
+β))) |
59 | 56, 57, 58 | mp2an 691 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (0[,)+β) β
(π₯ β β β§ 0
β€ π₯ β§ π₯ <
+β)) |
60 | 59 | simp2bi 1147 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (0[,)+β) β 0
β€ π₯) |
61 | 54, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (π΄ β {0})) β 0 β€ π₯) |
62 | | eldifsni 4754 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄ β {0}) β π₯ β 0) |
63 | 62 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (π΄ β {0})) β π₯ β 0) |
64 | 55, 61, 63 | ne0gt0d 11300 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (π΄ β {0})) β 0 < π₯) |
65 | 55, 64 | elrpd 12962 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄ β {0})) β π₯ β β+) |
66 | 65, 40 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄ β {0})) β (π₯ β π΄ β (1 / π₯) β π΅)) |
67 | 50, 66 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄ β {0})) β (1 / π₯) β π΅) |
68 | | rpcn 12933 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β+
β π₯ β
β) |
69 | | rpne0 12939 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β+
β π₯ β
0) |
70 | 68, 69 | recrecd 11936 |
. . . . . . . . . . . . . 14
β’ (π₯ β β+
β (1 / (1 / π₯)) =
π₯) |
71 | 65, 70 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄ β {0})) β (1 / (1 / π₯)) = π₯) |
72 | 71 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄ β {0})) β π₯ = (1 / (1 / π₯))) |
73 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π¦ = (1 / π₯) β (1 / π¦) = (1 / (1 / π₯))) |
74 | 73 | rspceeqv 3599 |
. . . . . . . . . . . 12
β’ (((1 /
π₯) β π΅ β§ π₯ = (1 / (1 / π₯))) β βπ¦ β π΅ π₯ = (1 / π¦)) |
75 | 67, 72, 74 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄ β {0})) β βπ¦ β π΅ π₯ = (1 / π¦)) |
76 | | breq1 5112 |
. . . . . . . . . . . . 13
β’ (π₯ = (1 / π¦) β (π₯ < π β (1 / π¦) < π)) |
77 | | rlimcnp.s |
. . . . . . . . . . . . . . 15
β’ (π₯ = (1 / π¦) β π
= π) |
78 | 77 | fvoveq1d 7383 |
. . . . . . . . . . . . . 14
β’ (π₯ = (1 / π¦) β (absβ(π
β πΆ)) = (absβ(π β πΆ))) |
79 | 78 | breq1d 5119 |
. . . . . . . . . . . . 13
β’ (π₯ = (1 / π¦) β ((absβ(π
β πΆ)) < π§ β (absβ(π β πΆ)) < π§)) |
80 | 76, 79 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π₯ = (1 / π¦) β ((π₯ < π β (absβ(π
β πΆ)) < π§) β ((1 / π¦) < π β (absβ(π β πΆ)) < π§))) |
81 | 80 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π₯ = (1 / π¦)) β ((π₯ < π β (absβ(π
β πΆ)) < π§) β ((1 / π¦) < π β (absβ(π β πΆ)) < π§))) |
82 | 48, 75, 81 | ralxfrd 5367 |
. . . . . . . . . 10
β’ (π β (βπ₯ β (π΄ β {0})(π₯ < π β (absβ(π
β πΆ)) < π§) β βπ¦ β π΅ ((1 / π¦) < π β (absβ(π β πΆ)) < π§))) |
83 | 82 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π§ β β+) β§ π β β+)
β (βπ₯ β
(π΄ β {0})(π₯ < π β (absβ(π
β πΆ)) < π§) β βπ¦ β π΅ ((1 / π¦) < π β (absβ(π β πΆ)) < π§))) |
84 | 29, 83 | bitr4d 282 |
. . . . . . . 8
β’ (((π β§ π§ β β+) β§ π β β+)
β (βπ¦ β
π΅ ((1 / π) < π¦ β (absβ(π β πΆ)) < π§) β βπ₯ β (π΄ β {0})(π₯ < π β (absβ(π
β πΆ)) < π§))) |
85 | | elsni 4607 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β {0} β π₯ = 0) |
86 | 85 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π§ β β+) β§ π₯ β {0}) β π₯ = 0) |
87 | | rlimcnp.c |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = 0 β π
= πΆ) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β β+) β§ π₯ β {0}) β π
= πΆ) |
89 | 88 | oveq1d 7376 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β β+) β§ π₯ β {0}) β (π
β πΆ) = (πΆ β πΆ)) |
90 | 87 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = 0 β (π
β β β πΆ β β)) |
91 | | rlimcnp.r |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β π΄) β π
β β) |
92 | 91 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ₯ β π΄ π
β β) |
93 | | rlimcnp.0 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β 0 β π΄) |
94 | 90, 92, 93 | rspcdva 3584 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΆ β β) |
95 | 94 | subidd 11508 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΆ β πΆ) = 0) |
96 | 95 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β β+) β§ π₯ β {0}) β (πΆ β πΆ) = 0) |
97 | 89, 96 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β β+) β§ π₯ β {0}) β (π
β πΆ) = 0) |
98 | 97 | abs00bd 15185 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β+) β§ π₯ β {0}) β
(absβ(π
β πΆ)) = 0) |
99 | | rpgt0 12935 |
. . . . . . . . . . . . . . 15
β’ (π§ β β+
β 0 < π§) |
100 | 99 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β+) β§ π₯ β {0}) β 0 < π§) |
101 | 98, 100 | eqbrtrd 5131 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β β+) β§ π₯ β {0}) β
(absβ(π
β πΆ)) < π§) |
102 | 101 | a1d 25 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β+) β§ π₯ β {0}) β (π₯ < π β (absβ(π
β πΆ)) < π§)) |
103 | 102 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ ((π β§ π§ β β+) β
βπ₯ β {0} (π₯ < π β (absβ(π
β πΆ)) < π§)) |
104 | 103 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π§ β β+) β§ π β β+)
β βπ₯ β {0}
(π₯ < π β (absβ(π
β πΆ)) < π§)) |
105 | 104 | biantrud 533 |
. . . . . . . . 9
β’ (((π β§ π§ β β+) β§ π β β+)
β (βπ₯ β
(π΄ β {0})(π₯ < π β (absβ(π
β πΆ)) < π§) β (βπ₯ β (π΄ β {0})(π₯ < π β (absβ(π
β πΆ)) < π§) β§ βπ₯ β {0} (π₯ < π β (absβ(π
β πΆ)) < π§)))) |
106 | | ralunb 4155 |
. . . . . . . . 9
β’
(βπ₯ β
((π΄ β {0}) βͺ
{0})(π₯ < π β (absβ(π
β πΆ)) < π§) β (βπ₯ β (π΄ β {0})(π₯ < π β (absβ(π
β πΆ)) < π§) β§ βπ₯ β {0} (π₯ < π β (absβ(π
β πΆ)) < π§))) |
107 | 105, 106 | bitr4di 289 |
. . . . . . . 8
β’ (((π β§ π§ β β+) β§ π β β+)
β (βπ₯ β
(π΄ β {0})(π₯ < π β (absβ(π
β πΆ)) < π§) β βπ₯ β ((π΄ β {0}) βͺ {0})(π₯ < π β (absβ(π
β πΆ)) < π§))) |
108 | | undif1 4439 |
. . . . . . . . . 10
β’ ((π΄ β {0}) βͺ {0}) =
(π΄ βͺ
{0}) |
109 | 93 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β+) β§ π β β+)
β 0 β π΄) |
110 | 109 | snssd 4773 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β+) β§ π β β+)
β {0} β π΄) |
111 | | ssequn2 4147 |
. . . . . . . . . . 11
β’ ({0}
β π΄ β (π΄ βͺ {0}) = π΄) |
112 | 110, 111 | sylib 217 |
. . . . . . . . . 10
β’ (((π β§ π§ β β+) β§ π β β+)
β (π΄ βͺ {0}) =
π΄) |
113 | 108, 112 | eqtrid 2785 |
. . . . . . . . 9
β’ (((π β§ π§ β β+) β§ π β β+)
β ((π΄ β {0})
βͺ {0}) = π΄) |
114 | 113 | raleqdv 3312 |
. . . . . . . 8
β’ (((π β§ π§ β β+) β§ π β β+)
β (βπ₯ β
((π΄ β {0}) βͺ
{0})(π₯ < π β (absβ(π
β πΆ)) < π§) β βπ₯ β π΄ (π₯ < π β (absβ(π
β πΆ)) < π§))) |
115 | 84, 107, 114 | 3bitrd 305 |
. . . . . . 7
β’ (((π β§ π§ β β+) β§ π β β+)
β (βπ¦ β
π΅ ((1 / π) < π¦ β (absβ(π β πΆ)) < π§) β βπ₯ β π΄ (π₯ < π β (absβ(π
β πΆ)) < π§))) |
116 | 115 | rexbidva 3170 |
. . . . . 6
β’ ((π β§ π§ β β+) β
(βπ β
β+ βπ¦ β π΅ ((1 / π) < π¦ β (absβ(π β πΆ)) < π§) β βπ β β+ βπ₯ β π΄ (π₯ < π β (absβ(π
β πΆ)) < π§))) |
117 | 17, 116 | bitrd 279 |
. . . . 5
β’ ((π β§ π§ β β+) β
(βπ‘ β
β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§) β βπ β β+ βπ₯ β π΄ (π₯ < π β (absβ(π
β πΆ)) < π§))) |
118 | 117 | ralbidva 3169 |
. . . 4
β’ (π β (βπ§ β β+
βπ‘ β
β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§) β βπ§ β β+ βπ β β+
βπ₯ β π΄ (π₯ < π β (absβ(π
β πΆ)) < π§))) |
119 | | nfv 1918 |
. . . . . . . . 9
β’
β²π₯(π€((abs β β ) βΎ
(π΄ Γ π΄))0) < π |
120 | | nffvmpt1 6857 |
. . . . . . . . . . 11
β’
β²π₯((π₯ β π΄ β¦ π
)βπ€) |
121 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π₯(abs
β β ) |
122 | | nffvmpt1 6857 |
. . . . . . . . . . 11
β’
β²π₯((π₯ β π΄ β¦ π
)β0) |
123 | 120, 121,
122 | nfov 7391 |
. . . . . . . . . 10
β’
β²π₯(((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) |
124 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π₯
< |
125 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π₯π§ |
126 | 123, 124,
125 | nfbr 5156 |
. . . . . . . . 9
β’
β²π₯(((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§ |
127 | 119, 126 | nfim 1900 |
. . . . . . . 8
β’
β²π₯((π€((abs β β ) βΎ
(π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§) |
128 | | nfv 1918 |
. . . . . . . 8
β’
β²π€((π₯((abs β β ) βΎ
(π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ₯)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§) |
129 | | oveq1 7368 |
. . . . . . . . . 10
β’ (π€ = π₯ β (π€((abs β β ) βΎ (π΄ Γ π΄))0) = (π₯((abs β β ) βΎ (π΄ Γ π΄))0)) |
130 | 129 | breq1d 5119 |
. . . . . . . . 9
β’ (π€ = π₯ β ((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (π₯((abs β β ) βΎ (π΄ Γ π΄))0) < π)) |
131 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π€ = π₯ β ((π₯ β π΄ β¦ π
)βπ€) = ((π₯ β π΄ β¦ π
)βπ₯)) |
132 | 131 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π€ = π₯ β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) = (((π₯ β π΄ β¦ π
)βπ₯)(abs β β )((π₯ β π΄ β¦ π
)β0))) |
133 | 132 | breq1d 5119 |
. . . . . . . . 9
β’ (π€ = π₯ β ((((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§ β (((π₯ β π΄ β¦ π
)βπ₯)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§)) |
134 | 130, 133 | imbi12d 345 |
. . . . . . . 8
β’ (π€ = π₯ β (((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§) β ((π₯((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ₯)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§))) |
135 | 127, 128,
134 | cbvralw 3288 |
. . . . . . 7
β’
(βπ€ β
π΄ ((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§) β βπ₯ β π΄ ((π₯((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ₯)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§)) |
136 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β π₯ β π΄) |
137 | 93 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β 0 β π΄) |
138 | 136, 137 | ovresd 7525 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (π₯((abs β β ) βΎ (π΄ Γ π΄))0) = (π₯(abs β β )0)) |
139 | 52, 51 | sstrdi 3960 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β β) |
140 | | ax-resscn 11116 |
. . . . . . . . . . . . . . 15
β’ β
β β |
141 | 139, 140 | sstrdi 3960 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β β) |
142 | 141 | sselda 3948 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β π₯ β β) |
143 | | 0cnd 11156 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β 0 β β) |
144 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (abs
β β ) = (abs β β ) |
145 | 144 | cnmetdval 24157 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ 0 β
β) β (π₯(abs
β β )0) = (absβ(π₯ β 0))) |
146 | 142, 143,
145 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (π₯(abs β β )0) = (absβ(π₯ β 0))) |
147 | 142 | subid1d 11509 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β (π₯ β 0) = π₯) |
148 | 147 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (absβ(π₯ β 0)) = (absβπ₯)) |
149 | 138, 146,
148 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (π₯((abs β β ) βΎ (π΄ Γ π΄))0) = (absβπ₯)) |
150 | 139 | sselda 3948 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β π₯ β β) |
151 | 52 | sselda 3948 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β π₯ β (0[,)+β)) |
152 | 151, 60 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β 0 β€ π₯) |
153 | 150, 152 | absidd 15316 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (absβπ₯) = π₯) |
154 | 149, 153 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (π₯((abs β β ) βΎ (π΄ Γ π΄))0) = π₯) |
155 | 154 | breq1d 5119 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β ((π₯((abs β β ) βΎ (π΄ Γ π΄))0) < π β π₯ < π)) |
156 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΄ β¦ π
) = (π₯ β π΄ β¦ π
) |
157 | 156 | fvmpt2 6963 |
. . . . . . . . . . . . 13
β’ ((π₯ β π΄ β§ π
β β) β ((π₯ β π΄ β¦ π
)βπ₯) = π
) |
158 | 136, 91, 157 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β ((π₯ β π΄ β¦ π
)βπ₯) = π
) |
159 | 94 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β πΆ β β) |
160 | 156, 87, 137, 159 | fvmptd3 6975 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β ((π₯ β π΄ β¦ π
)β0) = πΆ) |
161 | 158, 160 | oveq12d 7379 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (((π₯ β π΄ β¦ π
)βπ₯)(abs β β )((π₯ β π΄ β¦ π
)β0)) = (π
(abs β β )πΆ)) |
162 | 144 | cnmetdval 24157 |
. . . . . . . . . . . 12
β’ ((π
β β β§ πΆ β β) β (π
(abs β β )πΆ) = (absβ(π
β πΆ))) |
163 | 91, 159, 162 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (π
(abs β β )πΆ) = (absβ(π
β πΆ))) |
164 | 161, 163 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (((π₯ β π΄ β¦ π
)βπ₯)(abs β β )((π₯ β π΄ β¦ π
)β0)) = (absβ(π
β πΆ))) |
165 | 164 | breq1d 5119 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β ((((π₯ β π΄ β¦ π
)βπ₯)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§ β (absβ(π
β πΆ)) < π§)) |
166 | 155, 165 | imbi12d 345 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (((π₯((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ₯)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§) β (π₯ < π β (absβ(π
β πΆ)) < π§))) |
167 | 166 | ralbidva 3169 |
. . . . . . 7
β’ (π β (βπ₯ β π΄ ((π₯((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ₯)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§) β βπ₯ β π΄ (π₯ < π β (absβ(π
β πΆ)) < π§))) |
168 | 135, 167 | bitrid 283 |
. . . . . 6
β’ (π β (βπ€ β π΄ ((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§) β βπ₯ β π΄ (π₯ < π β (absβ(π
β πΆ)) < π§))) |
169 | 168 | rexbidv 3172 |
. . . . 5
β’ (π β (βπ β β+ βπ€ β π΄ ((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§) β βπ β β+ βπ₯ β π΄ (π₯ < π β (absβ(π
β πΆ)) < π§))) |
170 | 169 | ralbidv 3171 |
. . . 4
β’ (π β (βπ§ β β+
βπ β
β+ βπ€ β π΄ ((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§) β βπ§ β β+ βπ β β+
βπ₯ β π΄ (π₯ < π β (absβ(π
β πΆ)) < π§))) |
171 | 91 | fmpttd 7067 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ π
):π΄βΆβ) |
172 | 171 | biantrurd 534 |
. . . 4
β’ (π β (βπ§ β β+
βπ β
β+ βπ€ β π΄ ((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§) β ((π₯ β π΄ β¦ π
):π΄βΆβ β§ βπ§ β β+
βπ β
β+ βπ€ β π΄ ((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§)))) |
173 | 118, 170,
172 | 3bitr2d 307 |
. . 3
β’ (π β (βπ§ β β+
βπ‘ β
β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§) β ((π₯ β π΄ β¦ π
):π΄βΆβ β§ βπ§ β β+
βπ β
β+ βπ€ β π΄ ((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§)))) |
174 | 77 | eleq1d 2819 |
. . . . . . . 8
β’ (π₯ = (1 / π¦) β (π
β β β π β β)) |
175 | 92 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β π΅) β βπ₯ β π΄ π
β β) |
176 | 174, 175,
45 | rspcdva 3584 |
. . . . . . 7
β’ ((π β§ π¦ β π΅) β π β β) |
177 | 176 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ¦ β π΅ π β β) |
178 | | rpssre 12930 |
. . . . . . 7
β’
β+ β β |
179 | 19, 178 | sstrdi 3960 |
. . . . . 6
β’ (π β π΅ β β) |
180 | | 1red 11164 |
. . . . . 6
β’ (π β 1 β
β) |
181 | 177, 179,
94, 180 | rlim3 15389 |
. . . . 5
β’ (π β ((π¦ β π΅ β¦ π) βπ πΆ β βπ§ β β+
βπ‘ β
(1[,)+β)βπ¦
β π΅ (π‘ β€ π¦ β (absβ(π β πΆ)) < π§))) |
182 | | 0xr 11210 |
. . . . . . . . . 10
β’ 0 β
β* |
183 | | 0lt1 11685 |
. . . . . . . . . 10
β’ 0 <
1 |
184 | | df-ioo 13277 |
. . . . . . . . . . 11
β’ (,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) |
185 | | df-ico 13279 |
. . . . . . . . . . 11
β’ [,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ < π¦)}) |
186 | | xrltletr 13085 |
. . . . . . . . . . 11
β’ ((0
β β* β§ 1 β β* β§ π€ β β*)
β ((0 < 1 β§ 1 β€ π€) β 0 < π€)) |
187 | 184, 185,
186 | ixxss1 13291 |
. . . . . . . . . 10
β’ ((0
β β* β§ 0 < 1) β (1[,)+β) β
(0(,)+β)) |
188 | 182, 183,
187 | mp2an 691 |
. . . . . . . . 9
β’
(1[,)+β) β (0(,)+β) |
189 | | ioorp 13351 |
. . . . . . . . 9
β’
(0(,)+β) = β+ |
190 | 188, 189 | sseqtri 3984 |
. . . . . . . 8
β’
(1[,)+β) β β+ |
191 | | ssrexv 4015 |
. . . . . . . 8
β’
((1[,)+β) β β+ β (βπ‘ β
(1[,)+β)βπ¦
β π΅ (π‘ β€ π¦ β (absβ(π β πΆ)) < π§) β βπ‘ β β+ βπ¦ β π΅ (π‘ β€ π¦ β (absβ(π β πΆ)) < π§))) |
192 | 190, 191 | ax-mp 5 |
. . . . . . 7
β’
(βπ‘ β
(1[,)+β)βπ¦
β π΅ (π‘ β€ π¦ β (absβ(π β πΆ)) < π§) β βπ‘ β β+ βπ¦ β π΅ (π‘ β€ π¦ β (absβ(π β πΆ)) < π§)) |
193 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β β+) β§ π¦ β π΅) β π‘ β β+) |
194 | 178, 193 | sselid 3946 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β β+) β§ π¦ β π΅) β π‘ β β) |
195 | 179 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β β+) β π΅ β
β) |
196 | 195 | sselda 3948 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β β+) β§ π¦ β π΅) β π¦ β β) |
197 | | ltle 11251 |
. . . . . . . . . . 11
β’ ((π‘ β β β§ π¦ β β) β (π‘ < π¦ β π‘ β€ π¦)) |
198 | 194, 196,
197 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π‘ β β+) β§ π¦ β π΅) β (π‘ < π¦ β π‘ β€ π¦)) |
199 | 198 | imim1d 82 |
. . . . . . . . 9
β’ (((π β§ π‘ β β+) β§ π¦ β π΅) β ((π‘ β€ π¦ β (absβ(π β πΆ)) < π§) β (π‘ < π¦ β (absβ(π β πΆ)) < π§))) |
200 | 199 | ralimdva 3161 |
. . . . . . . 8
β’ ((π β§ π‘ β β+) β
(βπ¦ β π΅ (π‘ β€ π¦ β (absβ(π β πΆ)) < π§) β βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§))) |
201 | 200 | reximdva 3162 |
. . . . . . 7
β’ (π β (βπ‘ β β+ βπ¦ β π΅ (π‘ β€ π¦ β (absβ(π β πΆ)) < π§) β βπ‘ β β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§))) |
202 | 192, 201 | syl5 34 |
. . . . . 6
β’ (π β (βπ‘ β (1[,)+β)βπ¦ β π΅ (π‘ β€ π¦ β (absβ(π β πΆ)) < π§) β βπ‘ β β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§))) |
203 | 202 | ralimdv 3163 |
. . . . 5
β’ (π β (βπ§ β β+
βπ‘ β
(1[,)+β)βπ¦
β π΅ (π‘ β€ π¦ β (absβ(π β πΆ)) < π§) β βπ§ β β+ βπ‘ β β+
βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§))) |
204 | 181, 203 | sylbid 239 |
. . . 4
β’ (π β ((π¦ β π΅ β¦ π) βπ πΆ β βπ§ β β+
βπ‘ β
β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§))) |
205 | | ssrexv 4015 |
. . . . . . 7
β’
(β+ β β β (βπ‘ β β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§) β βπ‘ β β βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§))) |
206 | 178, 205 | ax-mp 5 |
. . . . . 6
β’
(βπ‘ β
β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§) β βπ‘ β β βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§)) |
207 | 206 | ralimi 3083 |
. . . . 5
β’
(βπ§ β
β+ βπ‘ β β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§) β βπ§ β β+ βπ‘ β β βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§)) |
208 | 177, 179,
94 | rlim2lt 15388 |
. . . . 5
β’ (π β ((π¦ β π΅ β¦ π) βπ πΆ β βπ§ β β+
βπ‘ β β
βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§))) |
209 | 207, 208 | syl5ibr 246 |
. . . 4
β’ (π β (βπ§ β β+
βπ‘ β
β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§) β (π¦ β π΅ β¦ π) βπ πΆ)) |
210 | 204, 209 | impbid 211 |
. . 3
β’ (π β ((π¦ β π΅ β¦ π) βπ πΆ β βπ§ β β+
βπ‘ β
β+ βπ¦ β π΅ (π‘ < π¦ β (absβ(π β πΆ)) < π§))) |
211 | | cnxmet 24159 |
. . . . 5
β’ (abs
β β ) β (βMetββ) |
212 | | xmetres2 23737 |
. . . . 5
β’ (((abs
β β ) β (βMetββ) β§ π΄ β β) β ((abs β
β ) βΎ (π΄
Γ π΄)) β
(βMetβπ΄)) |
213 | 211, 141,
212 | sylancr 588 |
. . . 4
β’ (π β ((abs β β )
βΎ (π΄ Γ π΄)) β
(βMetβπ΄)) |
214 | 211 | a1i 11 |
. . . 4
β’ (π β (abs β β )
β (βMetββ)) |
215 | | eqid 2733 |
. . . . 5
β’
(MetOpenβ((abs β β ) βΎ (π΄ Γ π΄))) = (MetOpenβ((abs β β )
βΎ (π΄ Γ π΄))) |
216 | | rlimcnp.j |
. . . . . 6
β’ π½ =
(TopOpenββfld) |
217 | 216 | cnfldtopn 24168 |
. . . . 5
β’ π½ = (MetOpenβ(abs β
β )) |
218 | 215, 217 | metcnp2 23921 |
. . . 4
β’ ((((abs
β β ) βΎ (π΄ Γ π΄)) β (βMetβπ΄) β§ (abs β β )
β (βMetββ) β§ 0 β π΄) β ((π₯ β π΄ β¦ π
) β (((MetOpenβ((abs β
β ) βΎ (π΄
Γ π΄))) CnP π½)β0) β ((π₯ β π΄ β¦ π
):π΄βΆβ β§ βπ§ β β+
βπ β
β+ βπ€ β π΄ ((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§)))) |
219 | 213, 214,
93, 218 | syl3anc 1372 |
. . 3
β’ (π β ((π₯ β π΄ β¦ π
) β (((MetOpenβ((abs β
β ) βΎ (π΄
Γ π΄))) CnP π½)β0) β ((π₯ β π΄ β¦ π
):π΄βΆβ β§ βπ§ β β+
βπ β
β+ βπ€ β π΄ ((π€((abs β β ) βΎ (π΄ Γ π΄))0) < π β (((π₯ β π΄ β¦ π
)βπ€)(abs β β )((π₯ β π΄ β¦ π
)β0)) < π§)))) |
220 | 173, 210,
219 | 3bitr4d 311 |
. 2
β’ (π β ((π¦ β π΅ β¦ π) βπ πΆ β (π₯ β π΄ β¦ π
) β (((MetOpenβ((abs β
β ) βΎ (π΄
Γ π΄))) CnP π½)β0))) |
221 | | rlimcnp.k |
. . . . . 6
β’ πΎ = (π½ βΎt π΄) |
222 | | eqid 2733 |
. . . . . . . 8
β’ ((abs
β β ) βΎ (π΄ Γ π΄)) = ((abs β β ) βΎ (π΄ Γ π΄)) |
223 | 222, 217,
215 | metrest 23903 |
. . . . . . 7
β’ (((abs
β β ) β (βMetββ) β§ π΄ β β) β (π½ βΎt π΄) = (MetOpenβ((abs β β )
βΎ (π΄ Γ π΄)))) |
224 | 211, 141,
223 | sylancr 588 |
. . . . . 6
β’ (π β (π½ βΎt π΄) = (MetOpenβ((abs β β )
βΎ (π΄ Γ π΄)))) |
225 | 221, 224 | eqtrid 2785 |
. . . . 5
β’ (π β πΎ = (MetOpenβ((abs β β )
βΎ (π΄ Γ π΄)))) |
226 | 225 | oveq1d 7376 |
. . . 4
β’ (π β (πΎ CnP π½) = ((MetOpenβ((abs β β )
βΎ (π΄ Γ π΄))) CnP π½)) |
227 | 226 | fveq1d 6848 |
. . 3
β’ (π β ((πΎ CnP π½)β0) = (((MetOpenβ((abs β
β ) βΎ (π΄
Γ π΄))) CnP π½)β0)) |
228 | 227 | eleq2d 2820 |
. 2
β’ (π β ((π₯ β π΄ β¦ π
) β ((πΎ CnP π½)β0) β (π₯ β π΄ β¦ π
) β (((MetOpenβ((abs β
β ) βΎ (π΄
Γ π΄))) CnP π½)β0))) |
229 | 220, 228 | bitr4d 282 |
1
β’ (π β ((π¦ β π΅ β¦ π) βπ πΆ β (π₯ β π΄ β¦ π
) β ((πΎ CnP π½)β0))) |