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 ⊢ φ → A ∈ ℝ
reclt0d.2 ⊢ φ → A < 0
Assertion reclt0d ⊢ φ → 1 A < 0

Proof

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