This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reclt0d

Description: The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses reclt0d.1 
|- ( ph -> A e. RR )
reclt0d.2 
|- ( ph -> A < 0 )
Assertion reclt0d 
|- ( ph -> ( 1 / A ) < 0 )

Proof

Step Hyp Ref Expression
1 reclt0d.1 
 |-  ( ph -> A e. RR )
2 reclt0d.2 
 |-  ( ph -> A < 0 )
3 0lt1 
 |-  0 < 1
4 3 a1i 
 |-  ( ( ph /\ -. ( 1 / A ) < 0 ) -> 0 < 1 )
5 simpr 
 |-  ( ( ph /\ -. ( 1 / A ) < 0 ) -> -. ( 1 / A ) < 0 )
6 0red 
 |-  ( ( ph /\ -. ( 1 / A ) < 0 ) -> 0 e. RR )
7 1red 
 |-  ( ph -> 1 e. RR )
8 2 lt0ne0d 
 |-  ( ph -> A =/= 0 )
9 7 1 8 redivcld 
 |-  ( ph -> ( 1 / A ) e. RR )
10 9 adantr 
 |-  ( ( ph /\ -. ( 1 / A ) < 0 ) -> ( 1 / A ) e. RR )
11 6 10 lenltd 
 |-  ( ( ph /\ -. ( 1 / A ) < 0 ) -> ( 0 <_ ( 1 / A ) <-> -. ( 1 / A ) < 0 ) )
12 5 11 mpbird 
 |-  ( ( ph /\ -. ( 1 / A ) < 0 ) -> 0 <_ ( 1 / A ) )
13 1 recnd 
 |-  ( ph -> A e. CC )
14 13 8 recidd 
 |-  ( ph -> ( A x. ( 1 / A ) ) = 1 )
15 14 eqcomd 
 |-  ( ph -> 1 = ( A x. ( 1 / A ) ) )
16 15 adantr 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> 1 = ( A x. ( 1 / A ) ) )
17 0red 
 |-  ( ph -> 0 e. RR )
18 1 17 2 ltled 
 |-  ( ph -> A <_ 0 )
19 18 adantr 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> A <_ 0 )
20 simpr 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> 0 <_ ( 1 / A ) )
21 19 20 jca 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> ( A <_ 0 /\ 0 <_ ( 1 / A ) ) )
22 21 orcd 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> ( ( A <_ 0 /\ 0 <_ ( 1 / A ) ) \/ ( 0 <_ A /\ ( 1 / A ) <_ 0 ) ) )
23 mulle0b 
 |-  ( ( A e. RR /\ ( 1 / A ) e. RR ) -> ( ( A x. ( 1 / A ) ) <_ 0 <-> ( ( A <_ 0 /\ 0 <_ ( 1 / A ) ) \/ ( 0 <_ A /\ ( 1 / A ) <_ 0 ) ) ) )
24 1 9 23 syl2anc 
 |-  ( ph -> ( ( A x. ( 1 / A ) ) <_ 0 <-> ( ( A <_ 0 /\ 0 <_ ( 1 / A ) ) \/ ( 0 <_ A /\ ( 1 / A ) <_ 0 ) ) ) )
25 24 adantr 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> ( ( A x. ( 1 / A ) ) <_ 0 <-> ( ( A <_ 0 /\ 0 <_ ( 1 / A ) ) \/ ( 0 <_ A /\ ( 1 / A ) <_ 0 ) ) ) )
26 22 25 mpbird 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> ( A x. ( 1 / A ) ) <_ 0 )
27 16 26 eqbrtrd 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> 1 <_ 0 )
28 7 adantr 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> 1 e. RR )
29 0red 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> 0 e. RR )
30 28 29 lenltd 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> ( 1 <_ 0 <-> -. 0 < 1 ) )
31 27 30 mpbid 
 |-  ( ( ph /\ 0 <_ ( 1 / A ) ) -> -. 0 < 1 )
32 12 31 syldan 
 |-  ( ( ph /\ -. ( 1 / A ) < 0 ) -> -. 0 < 1 )
33 4 32 condan 
 |-  ( ph -> ( 1 / A ) < 0 )