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φ
pimrecltneg.b ⊢φ∧x∈A→B∈ℝ
pimrecltneg.n ⊢φ∧x∈A→B≠0
pimrecltneg.c ⊢φ→C∈ℝ
pimrecltneg.l ⊢φ→C<0
Assertion pimrecltneg ⊢φ→x∈A|1B<C=x∈A|B∈1C0

Proof

Step Hyp Ref Expression
1 pimrecltneg.x ⊢Ⅎxφ
2 pimrecltneg.b ⊢φ∧x∈A→B∈ℝ
3 pimrecltneg.n ⊢φ∧x∈A→B≠0
4 pimrecltneg.c ⊢φ→C∈ℝ
5 pimrecltneg.l ⊢φ→C<0
6 rabidim1 ⊢x∈x∈A|1B<C→x∈A
7 6 adantl ⊢φ∧x∈x∈A|1B<C→x∈A
8 1red ⊢φ→1∈ℝ
9 4 5 ltned ⊢φ→C≠0
10 8 4 9 redivcld ⊢φ→1C∈ℝ
11 10 rexrd ⊢φ→1C∈ℝ*
12 11 adantr ⊢φ∧x∈x∈A|1B<C→1C∈ℝ*
13 0xr ⊢0∈ℝ*
14 13 a1i ⊢φ∧x∈x∈A|1B<C→0∈ℝ*
15 6 2 sylan2 ⊢φ∧x∈x∈A|1B<C→B∈ℝ
16 rabidim2 ⊢x∈x∈A|1B<C→1B<C
17 16 adantl ⊢φ∧x∈x∈A|1B<C→1B<C
18 8 adantr ⊢φ∧x∈x∈A|1B<C→1∈ℝ
19 7 3 syldan ⊢φ∧x∈x∈A|1B<C→B≠0
20 15 19 rereccld ⊢φ∧x∈x∈A|1B<C→1B∈ℝ
21 4 adantr ⊢φ∧x∈x∈A|1B<C→C∈ℝ
22 0red ⊢φ∧x∈x∈A|1B<C→0∈ℝ
23 5 adantr ⊢φ∧x∈x∈A|1B<C→C<0
24 20 21 22 17 23 lttrd ⊢φ∧x∈x∈A|1B<C→1B<0
25 15 19 reclt0 ⊢φ∧x∈x∈A|1B<C→B<0↔1B<0
26 24 25 mpbird ⊢φ∧x∈x∈A|1B<C→B<0
27 18 15 26 21 23 ltdiv23neg ⊢φ∧x∈x∈A|1B<C→1B<C↔1C<B
28 17 27 mpbid ⊢φ∧x∈x∈A|1B<C→1C<B
29 12 14 15 28 26 eliood ⊢φ∧x∈x∈A|1B<C→B∈1C0
30 7 29 jca ⊢φ∧x∈x∈A|1B<C→x∈A∧B∈1C0
31 rabid ⊢x∈x∈A|B∈1C0↔x∈A∧B∈1C0
32 30 31 sylibr ⊢φ∧x∈x∈A|1B<C→x∈x∈A|B∈1C0
33 32 ex ⊢φ→x∈x∈A|1B<C→x∈x∈A|B∈1C0
34 31 simplbi ⊢x∈x∈A|B∈1C0→x∈A
35 34 adantl ⊢φ∧x∈x∈A|B∈1C0→x∈A
36 11 adantr ⊢φ∧x∈x∈A|B∈1C0→1C∈ℝ*
37 13 a1i ⊢φ∧x∈x∈A|B∈1C0→0∈ℝ*
38 31 simprbi ⊢x∈x∈A|B∈1C0→B∈1C0
39 38 adantl ⊢φ∧x∈x∈A|B∈1C0→B∈1C0
40 36 37 39 ioogtlbd ⊢φ∧x∈x∈A|B∈1C0→1C<B
41 8 adantr ⊢φ∧x∈x∈A|B∈1C0→1∈ℝ
42 4 adantr ⊢φ∧x∈x∈A|B∈1C0→C∈ℝ
43 5 adantr ⊢φ∧x∈x∈A|B∈1C0→C<0
44 35 2 syldan ⊢φ∧x∈x∈A|B∈1C0→B∈ℝ
45 36 37 39 iooltubd ⊢φ∧x∈x∈A|B∈1C0→B<0
46 41 42 43 44 45 ltdiv23neg ⊢φ∧x∈x∈A|B∈1C0→1C<B↔1B<C
47 40 46 mpbid ⊢φ∧x∈x∈A|B∈1C0→1B<C
48 35 47 jca ⊢φ∧x∈x∈A|B∈1C0→x∈A∧1B<C
49 rabid ⊢x∈x∈A|1B<C↔x∈A∧1B<C
50 48 49 sylibr ⊢φ∧x∈x∈A|B∈1C0→x∈x∈A|1B<C
51 50 ex ⊢φ→x∈x∈A|B∈1C0→x∈x∈A|1B<C
52 33 51 impbid ⊢φ→x∈x∈A|1B<C↔x∈x∈A|B∈1C0
53 1 52 alrimi ⊢φ→∀xx∈x∈A|1B<C↔x∈x∈A|B∈1C0
54 nfrab1 ⊢Ⅎ_xx∈A|1B<C
55 nfrab1 ⊢Ⅎ_xx∈A|B∈1C0
56 54 55 cleqf ⊢x∈A|1B<C=x∈A|B∈1C0↔∀xx∈x∈A|1B<C↔x∈x∈A|B∈1C0
57 53 56 sylibr ⊢φ→x∈A|1B<C=x∈A|B∈1C0