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

Proof

Step Hyp Ref Expression
1 pimrecltneg.x 
 |-  F/ x ph
2 pimrecltneg.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
3 pimrecltneg.n 
 |-  ( ( ph /\ x e. A ) -> B =/= 0 )
4 pimrecltneg.c 
 |-  ( ph -> C e. RR )
5 pimrecltneg.l 
 |-  ( ph -> C < 0 )
6 rabidim1 
 |-  ( x e. { x e. A | ( 1 / B ) < C } -> x e. A )
7 6 adantl 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> x e. A )
8 1red 
 |-  ( ph -> 1 e. RR )
9 4 5 ltned 
 |-  ( ph -> C =/= 0 )
10 8 4 9 redivcld 
 |-  ( ph -> ( 1 / C ) e. RR )
11 10 rexrd 
 |-  ( ph -> ( 1 / C ) e. RR* )
12 11 adantr 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> ( 1 / C ) e. RR* )
13 0xr 
 |-  0 e. RR*
14 13 a1i 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> 0 e. RR* )
15 6 2 sylan2 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> B e. RR )
16 rabidim2 
 |-  ( x e. { x e. A | ( 1 / B ) < C } -> ( 1 / B ) < C )
17 16 adantl 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> ( 1 / B ) < C )
18 8 adantr 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> 1 e. RR )
19 7 3 syldan 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> B =/= 0 )
20 15 19 rereccld 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> ( 1 / B ) e. RR )
21 4 adantr 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> C e. RR )
22 0red 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> 0 e. RR )
23 5 adantr 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> C < 0 )
24 20 21 22 17 23 lttrd 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> ( 1 / B ) < 0 )
25 15 19 reclt0 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> ( B < 0 <-> ( 1 / B ) < 0 ) )
26 24 25 mpbird 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> B < 0 )
27 18 15 26 21 23 ltdiv23neg 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> ( ( 1 / B ) < C <-> ( 1 / C ) < B ) )
28 17 27 mpbid 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> ( 1 / C ) < B )
29 12 14 15 28 26 eliood 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> B e. ( ( 1 / C ) (,) 0 ) )
30 7 29 jca 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> ( x e. A /\ B e. ( ( 1 / C ) (,) 0 ) ) )
31 rabid 
 |-  ( x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } <-> ( x e. A /\ B e. ( ( 1 / C ) (,) 0 ) ) )
32 30 31 sylibr 
 |-  ( ( ph /\ x e. { x e. A | ( 1 / B ) < C } ) -> x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } )
33 32 ex 
 |-  ( ph -> ( x e. { x e. A | ( 1 / B ) < C } -> x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) )
34 31 simplbi 
 |-  ( x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } -> x e. A )
35 34 adantl 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> x e. A )
36 11 adantr 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> ( 1 / C ) e. RR* )
37 13 a1i 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> 0 e. RR* )
38 31 simprbi 
 |-  ( x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } -> B e. ( ( 1 / C ) (,) 0 ) )
39 38 adantl 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> B e. ( ( 1 / C ) (,) 0 ) )
40 36 37 39 ioogtlbd 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> ( 1 / C ) < B )
41 8 adantr 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> 1 e. RR )
42 4 adantr 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> C e. RR )
43 5 adantr 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> C < 0 )
44 35 2 syldan 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> B e. RR )
45 36 37 39 iooltubd 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> B < 0 )
46 41 42 43 44 45 ltdiv23neg 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> ( ( 1 / C ) < B <-> ( 1 / B ) < C ) )
47 40 46 mpbid 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> ( 1 / B ) < C )
48 35 47 jca 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> ( x e. A /\ ( 1 / B ) < C ) )
49 rabid 
 |-  ( x e. { x e. A | ( 1 / B ) < C } <-> ( x e. A /\ ( 1 / B ) < C ) )
50 48 49 sylibr 
 |-  ( ( ph /\ x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) -> x e. { x e. A | ( 1 / B ) < C } )
51 50 ex 
 |-  ( ph -> ( x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } -> x e. { x e. A | ( 1 / B ) < C } ) )
52 33 51 impbid 
 |-  ( ph -> ( x e. { x e. A | ( 1 / B ) < C } <-> x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) )
53 1 52 alrimi 
 |-  ( ph -> A. x ( x e. { x e. A | ( 1 / B ) < C } <-> x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) )
54 nfrab1 
 |-  F/_ x { x e. A | ( 1 / B ) < C }
55 nfrab1 
 |-  F/_ x { x e. A | B e. ( ( 1 / C ) (,) 0 ) }
56 54 55 cleqf 
 |-  ( { x e. A | ( 1 / B ) < C } = { x e. A | B e. ( ( 1 / C ) (,) 0 ) } <-> A. x ( x e. { x e. A | ( 1 / B ) < C } <-> x e. { x e. A | B e. ( ( 1 / C ) (,) 0 ) } ) )
57 53 56 sylibr 
 |-  ( ph -> { x e. A | ( 1 / B ) < C } = { x e. A | B e. ( ( 1 / C ) (,) 0 ) } )