# Metamath Proof Explorer

## Theorem pimrecltneg

Description: The preimage of an unbounded below, open interval, with negative upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses pimrecltneg.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
pimrecltneg.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
pimrecltneg.n ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\ne 0$
pimrecltneg.c ${⊢}{\phi }\to {C}\in ℝ$
pimrecltneg.l ${⊢}{\phi }\to {C}<0$
Assertion pimrecltneg ${⊢}{\phi }\to \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}=\left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}$

### Proof

Step Hyp Ref Expression
1 pimrecltneg.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 pimrecltneg.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
3 pimrecltneg.n ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\ne 0$
4 pimrecltneg.c ${⊢}{\phi }\to {C}\in ℝ$
5 pimrecltneg.l ${⊢}{\phi }\to {C}<0$
6 rabidim1 ${⊢}{x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\to {x}\in {A}$
7 6 adantl ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to {x}\in {A}$
8 1red ${⊢}{\phi }\to 1\in ℝ$
9 4 5 ltned ${⊢}{\phi }\to {C}\ne 0$
10 8 4 9 redivcld ${⊢}{\phi }\to \frac{1}{{C}}\in ℝ$
11 10 rexrd ${⊢}{\phi }\to \frac{1}{{C}}\in {ℝ}^{*}$
12 11 adantr ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to \frac{1}{{C}}\in {ℝ}^{*}$
13 0xr ${⊢}0\in {ℝ}^{*}$
14 13 a1i ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to 0\in {ℝ}^{*}$
15 6 2 sylan2 ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to {B}\in ℝ$
16 rabidim2 ${⊢}{x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\to \frac{1}{{B}}<{C}$
17 16 adantl ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to \frac{1}{{B}}<{C}$
18 8 adantr ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to 1\in ℝ$
19 7 3 syldan ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to {B}\ne 0$
20 15 19 rereccld ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to \frac{1}{{B}}\in ℝ$
21 4 adantr ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to {C}\in ℝ$
22 0red ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to 0\in ℝ$
23 5 adantr ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to {C}<0$
24 20 21 22 17 23 lttrd ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to \frac{1}{{B}}<0$
25 15 19 reclt0 ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to \left({B}<0↔\frac{1}{{B}}<0\right)$
26 24 25 mpbird ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to {B}<0$
27 18 15 26 21 23 ltdiv23neg ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to \left(\frac{1}{{B}}<{C}↔\frac{1}{{C}}<{B}\right)$
28 17 27 mpbid ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to \frac{1}{{C}}<{B}$
29 12 14 15 28 26 eliood ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to {B}\in \left(\frac{1}{{C}},0\right)$
30 7 29 jca ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to \left({x}\in {A}\wedge {B}\in \left(\frac{1}{{C}},0\right)\right)$
31 rabid ${⊢}{x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}↔\left({x}\in {A}\wedge {B}\in \left(\frac{1}{{C}},0\right)\right)$
32 30 31 sylibr ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)\to {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}$
33 32 ex ${⊢}{\phi }\to \left({x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\to {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)$
34 31 simplbi ${⊢}{x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\to {x}\in {A}$
35 34 adantl ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to {x}\in {A}$
36 11 adantr ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to \frac{1}{{C}}\in {ℝ}^{*}$
37 13 a1i ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to 0\in {ℝ}^{*}$
38 31 simprbi ${⊢}{x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\to {B}\in \left(\frac{1}{{C}},0\right)$
39 38 adantl ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to {B}\in \left(\frac{1}{{C}},0\right)$
40 36 37 39 ioogtlbd ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to \frac{1}{{C}}<{B}$
41 8 adantr ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to 1\in ℝ$
42 4 adantr ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to {C}\in ℝ$
43 5 adantr ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to {C}<0$
44 35 2 syldan ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to {B}\in ℝ$
45 36 37 39 iooltubd ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to {B}<0$
46 41 42 43 44 45 ltdiv23neg ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to \left(\frac{1}{{C}}<{B}↔\frac{1}{{B}}<{C}\right)$
47 40 46 mpbid ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to \frac{1}{{B}}<{C}$
48 35 47 jca ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to \left({x}\in {A}\wedge \frac{1}{{B}}<{C}\right)$
49 rabid ${⊢}{x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}↔\left({x}\in {A}\wedge \frac{1}{{B}}<{C}\right)$
50 48 49 sylibr ${⊢}\left({\phi }\wedge {x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)\to {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}$
51 50 ex ${⊢}{\phi }\to \left({x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\to {x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}\right)$
52 33 51 impbid ${⊢}{\phi }\to \left({x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}↔{x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)$
53 1 52 alrimi ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}↔{x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)$
54 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}$
55 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}$
56 54 55 cleqf ${⊢}\left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}=\left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}↔{x}\in \left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}\right)$
57 53 56 sylibr ${⊢}{\phi }\to \left\{{x}\in {A}|\frac{1}{{B}}<{C}\right\}=\left\{{x}\in {A}|{B}\in \left(\frac{1}{{C}},0\right)\right\}$