Description: Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ltnegcon2 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < - 𝐵 ↔ 𝐵 < - 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | renegcl | ⊢ ( 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ ) | |
2 | ltneg | ⊢ ( ( 𝐴 ∈ ℝ ∧ - 𝐵 ∈ ℝ ) → ( 𝐴 < - 𝐵 ↔ - - 𝐵 < - 𝐴 ) ) | |
3 | 1 2 | sylan2 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < - 𝐵 ↔ - - 𝐵 < - 𝐴 ) ) |
4 | simpr | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ ) | |
5 | 4 | recnd | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℂ ) |
6 | 5 | negnegd | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → - - 𝐵 = 𝐵 ) |
7 | 6 | breq1d | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - - 𝐵 < - 𝐴 ↔ 𝐵 < - 𝐴 ) ) |
8 | 3 7 | bitrd | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < - 𝐵 ↔ 𝐵 < - 𝐴 ) ) |