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 | 1 B < C = x ∈ A | B ∈ 1 C 0

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