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 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) ≤ 𝐴 ↔ 𝐵 ≤ 0 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leaddsub2 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) ≤ 𝐴 ↔ 𝐵 ≤ ( 𝐴 − 𝐴 ) ) ) | |
| 2 | 1 | 3anidm13 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) ≤ 𝐴 ↔ 𝐵 ≤ ( 𝐴 − 𝐴 ) ) ) |
| 3 | recn | ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) | |
| 4 | 3 | subidd | ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 𝐴 ) = 0 ) |
| 5 | 4 | adantr | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 − 𝐴 ) = 0 ) |
| 6 | 5 | breq2d | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ≤ ( 𝐴 − 𝐴 ) ↔ 𝐵 ≤ 0 ) ) |
| 7 | 2 6 | bitrd | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) ≤ 𝐴 ↔ 𝐵 ≤ 0 ) ) |