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 
|- F/ x ph
pimrecltpos.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
pimrecltpos.n 
|- ( ( ph /\ x e. A ) -> B =/= 0 )
pimrecltpos.c 
|- ( ph -> C e. RR+ )
Assertion pimrecltpos 
|- ( ph -> { x e. A | ( 1 / B ) < C } = ( { x e. A | ( 1 / C ) < B } u. { x e. A | B < 0 } ) )

Proof

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