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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
reclt0d.2 ⊢ ( 𝜑 → 𝐴 < 0 )
Assertion reclt0d ( 𝜑 → ( 1 / 𝐴 ) < 0 )

Proof

Step Hyp Ref Expression
1 reclt0d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 reclt0d.2 ⊢ ( 𝜑 → 𝐴 < 0 )
3 0lt1 ⊢ 0 < 1
4 3 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 1 / 𝐴 ) < 0 ) → 0 < 1 )
5 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 1 / 𝐴 ) < 0 ) → ¬ ( 1 / 𝐴 ) < 0 )
6 0red ⊢ ( ( 𝜑 ∧ ¬ ( 1 / 𝐴 ) < 0 ) → 0 ∈ ℝ )
7 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
8 2 lt0ne0d ⊢ ( 𝜑 → 𝐴 ≠ 0 )
9 7 1 8 redivcld ⊢ ( 𝜑 → ( 1 / 𝐴 ) ∈ ℝ )
10 9 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 1 / 𝐴 ) < 0 ) → ( 1 / 𝐴 ) ∈ ℝ )
11 6 10 lenltd ⊢ ( ( 𝜑 ∧ ¬ ( 1 / 𝐴 ) < 0 ) → ( 0 ≤ ( 1 / 𝐴 ) ↔ ¬ ( 1 / 𝐴 ) < 0 ) )
12 5 11 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( 1 / 𝐴 ) < 0 ) → 0 ≤ ( 1 / 𝐴 ) )
13 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
14 13 8 recidd ⊢ ( 𝜑 → ( 𝐴 · ( 1 / 𝐴 ) ) = 1 )
15 14 eqcomd ⊢ ( 𝜑 → 1 = ( 𝐴 · ( 1 / 𝐴 ) ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → 1 = ( 𝐴 · ( 1 / 𝐴 ) ) )
17 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
18 1 17 2 ltled ⊢ ( 𝜑 → 𝐴 ≤ 0 )
19 18 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → 𝐴 ≤ 0 )
20 simpr ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → 0 ≤ ( 1 / 𝐴 ) )
21 19 20 jca ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → ( 𝐴 ≤ 0 ∧ 0 ≤ ( 1 / 𝐴 ) ) )
22 21 orcd ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → ( ( 𝐴 ≤ 0 ∧ 0 ≤ ( 1 / 𝐴 ) ) ∨ ( 0 ≤ 𝐴 ∧ ( 1 / 𝐴 ) ≤ 0 ) ) )
23 mulle0b ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ≤ 0 ↔ ( ( 𝐴 ≤ 0 ∧ 0 ≤ ( 1 / 𝐴 ) ) ∨ ( 0 ≤ 𝐴 ∧ ( 1 / 𝐴 ) ≤ 0 ) ) ) )
24 1 9 23 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 · ( 1 / 𝐴 ) ) ≤ 0 ↔ ( ( 𝐴 ≤ 0 ∧ 0 ≤ ( 1 / 𝐴 ) ) ∨ ( 0 ≤ 𝐴 ∧ ( 1 / 𝐴 ) ≤ 0 ) ) ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ≤ 0 ↔ ( ( 𝐴 ≤ 0 ∧ 0 ≤ ( 1 / 𝐴 ) ) ∨ ( 0 ≤ 𝐴 ∧ ( 1 / 𝐴 ) ≤ 0 ) ) ) )
26 22 25 mpbird ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → ( 𝐴 · ( 1 / 𝐴 ) ) ≤ 0 )
27 16 26 eqbrtrd ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → 1 ≤ 0 )
28 7 adantr ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → 1 ∈ ℝ )
29 0red ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → 0 ∈ ℝ )
30 28 29 lenltd ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → ( 1 ≤ 0 ↔ ¬ 0 < 1 ) )
31 27 30 mpbid ⊢ ( ( 𝜑 ∧ 0 ≤ ( 1 / 𝐴 ) ) → ¬ 0 < 1 )
32 12 31 syldan ⊢ ( ( 𝜑 ∧ ¬ ( 1 / 𝐴 ) < 0 ) → ¬ 0 < 1 )
33 4 32 condan ⊢ ( 𝜑 → ( 1 / 𝐴 ) < 0 )