Metamath Proof Explorer

Theorem leaddle0

Description: The sum of a real number and a second real number is less than the real number iff the second real number is negative. (Contributed by Alexander van der Vekens, 30-May-2018)

Ref Expression
Assertion leaddle0 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ≤ A ↔ B ≤ 0

Proof

Step Hyp Ref Expression
1 leaddsub2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → A + B ≤ A ↔ B ≤ A − A
2 1 3anidm13 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ≤ A ↔ B ≤ A − A
3 recn ⊢ A ∈ ℝ → A ∈ ℂ
4 3 subidd ⊢ A ∈ ℝ → A − A = 0
5 4 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − A = 0
6 5 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A − A ↔ B ≤ 0
7 2 6 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ≤ A ↔ B ≤ 0