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 φxAB
pimrecltpos.n φxAB0
pimrecltpos.c φC+
Assertion pimrecltpos φxA|1B<C=xA|1C<BxA|B<0

Proof

Step Hyp Ref Expression
1 pimrecltpos.x xφ
2 pimrecltpos.b φxAB
3 pimrecltpos.n φxAB0
4 pimrecltpos.c φC+
5 rabidim1 xxA|1B<CxA
6 5 adantr xxA|1B<CB<0xA
7 simpr xxA|1B<CB<0B<0
8 6 7 jca xxA|1B<CB<0xAB<0
9 rabid xxA|B<0xAB<0
10 8 9 sylibr xxA|1B<CB<0xxA|B<0
11 elun2 xxA|B<0xxA|1C<BxA|B<0
12 10 11 syl xxA|1B<CB<0xxA|1C<BxA|B<0
13 12 adantll φxxA|1B<CB<0xxA|1C<BxA|B<0
14 0red φxxA|1B<C¬B<00
15 5 2 sylan2 φxxA|1B<CB
16 15 adantr φxxA|1B<C¬B<0B
17 5 adantl φxxA|1B<CxA
18 3 necomd φxA0B
19 17 18 syldan φxxA|1B<C0B
20 19 adantr φxxA|1B<C¬B<00B
21 simpr φxxA|1B<C¬B<0¬B<0
22 14 16 20 21 lttri5d φxxA|1B<C¬B<00<B
23 17 adantr φxxA|1B<C0<BxA
24 15 adantr φxxA|1B<C0<BB
25 simpr φxxA|1B<C0<B0<B
26 24 25 elrpd φxxA|1B<C0<BB+
27 4 ad2antrr φxxA|1B<C0<BC+
28 rabidim2 xxA|1B<C1B<C
29 28 ad2antlr φxxA|1B<C0<B1B<C
30 26 27 29 ltrec1d φxxA|1B<C0<B1C<B
31 23 30 jca φxxA|1B<C0<BxA1C<B
32 rabid xxA|1C<BxA1C<B
33 31 32 sylibr φxxA|1B<C0<BxxA|1C<B
34 elun1 xxA|1C<BxxA|1C<BxA|B<0
35 33 34 syl φxxA|1B<C0<BxxA|1C<BxA|B<0
36 22 35 syldan φxxA|1B<C¬B<0xxA|1C<BxA|B<0
37 13 36 pm2.61dan φxxA|1B<CxxA|1C<BxA|B<0
38 37 ex φxxA|1B<CxxA|1C<BxA|B<0
39 32 simplbi xxA|1C<BxA
40 39 adantl φxxA|1C<BxA
41 4 adantr φxxA|1C<BC+
42 40 2 syldan φxxA|1C<BB
43 0red φxxA|1C<B0
44 41 rprecred φxxA|1C<B1C
45 4 rpred φC
46 4 rpgt0d φ0<C
47 45 46 recgt0d φ0<1C
48 47 adantr φxxA|1C<B0<1C
49 32 simprbi xxA|1C<B1C<B
50 49 adantl φxxA|1C<B1C<B
51 43 44 42 48 50 lttrd φxxA|1C<B0<B
52 42 51 elrpd φxxA|1C<BB+
53 41 52 50 ltrec1d φxxA|1C<B1B<C
54 40 53 jca φxxA|1C<BxA1B<C
55 rabid xxA|1B<CxA1B<C
56 54 55 sylibr φxxA|1C<BxxA|1B<C
57 56 adantlr φxxA|1C<BxA|B<0xxA|1C<BxxA|1B<C
58 simpll φxxA|1C<BxA|B<0¬xxA|1C<Bφ
59 elunnel1 xxA|1C<BxA|B<0¬xxA|1C<BxxA|B<0
60 59 adantll φxxA|1C<BxA|B<0¬xxA|1C<BxxA|B<0
61 9 simplbi xxA|B<0xA
62 61 adantl φxxA|B<0xA
63 2 3 rereccld φxA1B
64 62 63 syldan φxxA|B<01B
65 0red φxxA|B<00
66 45 adantr φxxA|B<0C
67 62 2 syldan φxxA|B<0B
68 9 simprbi xxA|B<0B<0
69 68 adantl φxxA|B<0B<0
70 67 69 reclt0d φxxA|B<01B<0
71 46 adantr φxxA|B<00<C
72 64 65 66 70 71 lttrd φxxA|B<01B<C
73 62 72 jca φxxA|B<0xA1B<C
74 73 55 sylibr φxxA|B<0xxA|1B<C
75 58 60 74 syl2anc φxxA|1C<BxA|B<0¬xxA|1C<BxxA|1B<C
76 57 75 pm2.61dan φxxA|1C<BxA|B<0xxA|1B<C
77 76 ex φxxA|1C<BxA|B<0xxA|1B<C
78 38 77 impbid φxxA|1B<CxxA|1C<BxA|B<0
79 1 78 alrimi φxxxA|1B<CxxA|1C<BxA|B<0
80 nfrab1 _xxA|1B<C
81 nfrab1 _xxA|1C<B
82 nfrab1 _xxA|B<0
83 81 82 nfun _xxA|1C<BxA|B<0
84 80 83 cleqf xA|1B<C=xA|1C<BxA|B<0xxxA|1B<CxxA|1C<BxA|B<0
85 79 84 sylibr φxA|1B<C=xA|1C<BxA|B<0