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