Metamath Proof Explorer

Theorem pimrecltpos

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

Ref Expression
Hypotheses pimrecltpos.x ⊢ Ⅎ x φ
pimrecltpos.b ⊢ φ ∧ x ∈ A → B ∈ ℝ
pimrecltpos.n ⊢ φ ∧ x ∈ A → B ≠ 0
pimrecltpos.c ⊢ φ → C ∈ ℝ +
Assertion pimrecltpos ⊢ φ → x ∈ A | 1 B < C = x ∈ A | 1 C < B ∪ x ∈ A | B < 0

Proof

Step Hyp Ref Expression
1 pimrecltpos.x ⊢ Ⅎ x φ
2 pimrecltpos.b ⊢ φ ∧ x ∈ A → B ∈ ℝ
3 pimrecltpos.n ⊢ φ ∧ x ∈ A → B ≠ 0
4 pimrecltpos.c ⊢ φ → C ∈ ℝ +
5 rabidim1 ⊢ x ∈ x ∈ A | 1 B < C → x ∈ A
6 5 adantr ⊢ x ∈ x ∈ A | 1 B < C ∧ B < 0 → x ∈ A
7 simpr ⊢ x ∈ x ∈ A | 1 B < C ∧ B < 0 → B < 0
8 6 7 jca ⊢ x ∈ x ∈ A | 1 B < C ∧ B < 0 → x ∈ A ∧ B < 0
9 rabid ⊢ x ∈ x ∈ A | B < 0 ↔ x ∈ A ∧ B < 0
10 8 9 sylibr ⊢ x ∈ x ∈ A | 1 B < C ∧ B < 0 → x ∈ x ∈ A | B < 0
11 elun2 ⊢ x ∈ x ∈ A | B < 0 → x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
12 10 11 syl ⊢ x ∈ x ∈ A | 1 B < C ∧ B < 0 → x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
13 12 adantll ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ B < 0 → x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
14 0red ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ ¬ B < 0 → 0 ∈ ℝ
15 5 2 sylan2 ⊢ φ ∧ x ∈ x ∈ A | 1 B < C → B ∈ ℝ
16 15 adantr ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ ¬ B < 0 → B ∈ ℝ
17 5 adantl ⊢ φ ∧ x ∈ x ∈ A | 1 B < C → x ∈ A
18 3 necomd ⊢ φ ∧ x ∈ A → 0 ≠ B
19 17 18 syldan ⊢ φ ∧ x ∈ x ∈ A | 1 B < C → 0 ≠ B
20 19 adantr ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ ¬ B < 0 → 0 ≠ B
21 simpr ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ ¬ B < 0 → ¬ B < 0
22 14 16 20 21 lttri5d ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ ¬ B < 0 → 0 < B
23 17 adantr ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ 0 < B → x ∈ A
24 15 adantr ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ 0 < B → B ∈ ℝ
25 simpr ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ 0 < B → 0 < B
26 24 25 elrpd ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ 0 < B → B ∈ ℝ +
27 4 ad2antrr ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ 0 < B → C ∈ ℝ +
28 rabidim2 ⊢ x ∈ x ∈ A | 1 B < C → 1 B < C
29 28 ad2antlr ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ 0 < B → 1 B < C
30 26 27 29 ltrec1d ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ 0 < B → 1 C < B
31 23 30 jca ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ 0 < B → x ∈ A ∧ 1 C < B
32 rabid ⊢ x ∈ x ∈ A | 1 C < B ↔ x ∈ A ∧ 1 C < B
33 31 32 sylibr ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ 0 < B → x ∈ x ∈ A | 1 C < B
34 elun1 ⊢ x ∈ x ∈ A | 1 C < B → x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
35 33 34 syl ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ 0 < B → x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
36 22 35 syldan ⊢ φ ∧ x ∈ x ∈ A | 1 B < C ∧ ¬ B < 0 → x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
37 13 36 pm2.61dan ⊢ φ ∧ x ∈ x ∈ A | 1 B < C → x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
38 37 ex ⊢ φ → x ∈ x ∈ A | 1 B < C → x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
39 32 simplbi ⊢ x ∈ x ∈ A | 1 C < B → x ∈ A
40 39 adantl ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → x ∈ A
41 4 adantr ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → C ∈ ℝ +
42 40 2 syldan ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → B ∈ ℝ
43 0red ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → 0 ∈ ℝ
44 41 rprecred ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → 1 C ∈ ℝ
45 4 rpred ⊢ φ → C ∈ ℝ
46 4 rpgt0d ⊢ φ → 0 < C
47 45 46 recgt0d ⊢ φ → 0 < 1 C
48 47 adantr ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → 0 < 1 C
49 32 simprbi ⊢ x ∈ x ∈ A | 1 C < B → 1 C < B
50 49 adantl ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → 1 C < B
51 43 44 42 48 50 lttrd ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → 0 < B
52 42 51 elrpd ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → B ∈ ℝ +
53 41 52 50 ltrec1d ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → 1 B < C
54 40 53 jca ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → x ∈ A ∧ 1 B < C
55 rabid ⊢ x ∈ x ∈ A | 1 B < C ↔ x ∈ A ∧ 1 B < C
56 54 55 sylibr ⊢ φ ∧ x ∈ x ∈ A | 1 C < B → x ∈ x ∈ A | 1 B < C
57 56 adantlr ⊢ φ ∧ x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0 ∧ x ∈ x ∈ A | 1 C < B → x ∈ x ∈ A | 1 B < C
58 simpll ⊢ φ ∧ x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0 ∧ ¬ x ∈ x ∈ A | 1 C < B → φ
59 elunnel1 ⊢ x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0 ∧ ¬ x ∈ x ∈ A | 1 C < B → x ∈ x ∈ A | B < 0
60 59 adantll ⊢ φ ∧ x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0 ∧ ¬ x ∈ x ∈ A | 1 C < B → x ∈ x ∈ A | B < 0
61 9 simplbi ⊢ x ∈ x ∈ A | B < 0 → x ∈ A
62 61 adantl ⊢ φ ∧ x ∈ x ∈ A | B < 0 → x ∈ A
63 2 3 rereccld ⊢ φ ∧ x ∈ A → 1 B ∈ ℝ
64 62 63 syldan ⊢ φ ∧ x ∈ x ∈ A | B < 0 → 1 B ∈ ℝ
65 0red ⊢ φ ∧ x ∈ x ∈ A | B < 0 → 0 ∈ ℝ
66 45 adantr ⊢ φ ∧ x ∈ x ∈ A | B < 0 → C ∈ ℝ
67 62 2 syldan ⊢ φ ∧ x ∈ x ∈ A | B < 0 → B ∈ ℝ
68 9 simprbi ⊢ x ∈ x ∈ A | B < 0 → B < 0
69 68 adantl ⊢ φ ∧ x ∈ x ∈ A | B < 0 → B < 0
70 67 69 reclt0d ⊢ φ ∧ x ∈ x ∈ A | B < 0 → 1 B < 0
71 46 adantr ⊢ φ ∧ x ∈ x ∈ A | B < 0 → 0 < C
72 64 65 66 70 71 lttrd ⊢ φ ∧ x ∈ x ∈ A | B < 0 → 1 B < C
73 62 72 jca ⊢ φ ∧ x ∈ x ∈ A | B < 0 → x ∈ A ∧ 1 B < C
74 73 55 sylibr ⊢ φ ∧ x ∈ x ∈ A | B < 0 → x ∈ x ∈ A | 1 B < C
75 58 60 74 syl2anc ⊢ φ ∧ x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0 ∧ ¬ x ∈ x ∈ A | 1 C < B → x ∈ x ∈ A | 1 B < C
76 57 75 pm2.61dan ⊢ φ ∧ x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0 → x ∈ x ∈ A | 1 B < C
77 76 ex ⊢ φ → x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0 → x ∈ x ∈ A | 1 B < C
78 38 77 impbid ⊢ φ → x ∈ x ∈ A | 1 B < C ↔ x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
79 1 78 alrimi ⊢ φ → ∀ x x ∈ x ∈ A | 1 B < C ↔ x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
80 nfrab1 ⊢ Ⅎ _ x x ∈ A | 1 B < C
81 nfrab1 ⊢ Ⅎ _ x x ∈ A | 1 C < B
82 nfrab1 ⊢ Ⅎ _ x x ∈ A | B < 0
83 81 82 nfun ⊢ Ⅎ _ x x ∈ A | 1 C < B ∪ x ∈ A | B < 0
84 80 83 cleqf ⊢ x ∈ A | 1 B < C = x ∈ A | 1 C < B ∪ x ∈ A | B < 0 ↔ ∀ x x ∈ x ∈ A | 1 B < C ↔ x ∈ x ∈ A | 1 C < B ∪ x ∈ A | B < 0
85 79 84 sylibr ⊢ φ → x ∈ A | 1 B < C = x ∈ A | 1 C < B ∪ x ∈ A | B < 0