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

Metamath Proof Explorer

Theorem reclt0

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

Ref Expression
Hypotheses reclt0.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
reclt0.2 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
Assertion reclt0 ( 𝜑 → ( 𝐴 < 0 ↔ ( 1 / 𝐴 ) < 0 ) )

Proof

Step Hyp Ref Expression
1 reclt0.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 reclt0.2 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
3 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐴 ∈ ℝ )
4 simpr ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐴 < 0 )
5 3 4 reclt0d ⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 1 / 𝐴 ) < 0 )
6 5 ex ⊢ ( 𝜑 → ( 𝐴 < 0 → ( 1 / 𝐴 ) < 0 ) )
7 0red ⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → 0 ∈ ℝ )
8 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → 𝐴 ∈ ℝ )
9 2 necomd ⊢ ( 𝜑 → 0 ≠ 𝐴 )
10 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → 0 ≠ 𝐴 )
11 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → ¬ 𝐴 < 0 )
12 7 8 10 11 lttri5d ⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → 0 < 𝐴 )
13 0red ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 ∈ ℝ )
14 1 2 rereccld ⊢ ( 𝜑 → ( 1 / 𝐴 ) ∈ ℝ )
15 14 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℝ )
16 1 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
17 simpr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < 𝐴 )
18 16 17 recgt0d ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < ( 1 / 𝐴 ) )
19 13 15 18 ltled ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 ≤ ( 1 / 𝐴 ) )
20 13 15 lenltd ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 0 ≤ ( 1 / 𝐴 ) ↔ ¬ ( 1 / 𝐴 ) < 0 ) )
21 19 20 mpbid ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ¬ ( 1 / 𝐴 ) < 0 )
22 12 21 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → ¬ ( 1 / 𝐴 ) < 0 )
23 22 ex ⊢ ( 𝜑 → ( ¬ 𝐴 < 0 → ¬ ( 1 / 𝐴 ) < 0 ) )
24 23 con4d ⊢ ( 𝜑 → ( ( 1 / 𝐴 ) < 0 → 𝐴 < 0 ) )
25 24 imp ⊢ ( ( 𝜑 ∧ ( 1 / 𝐴 ) < 0 ) → 𝐴 < 0 )
26 25 ex ⊢ ( 𝜑 → ( ( 1 / 𝐴 ) < 0 → 𝐴 < 0 ) )
27 6 26 impbid ⊢ ( 𝜑 → ( 𝐴 < 0 ↔ ( 1 / 𝐴 ) < 0 ) )