Description: Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | ltaddpos2 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 ↔ 𝐵 < ( 𝐴 + 𝐵 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltaddpos | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 ↔ 𝐵 < ( 𝐵 + 𝐴 ) ) ) | |
2 | recn | ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) | |
3 | recn | ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ ) | |
4 | addcom | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) ) | |
5 | 2 3 4 | syl2an | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) ) |
6 | 5 | breq2d | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < ( 𝐴 + 𝐵 ) ↔ 𝐵 < ( 𝐵 + 𝐴 ) ) ) |
7 | 1 6 | bitr4d | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 ↔ 𝐵 < ( 𝐴 + 𝐵 ) ) ) |