Description: Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | ltnegcon1 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐴 < 𝐵 ↔ - 𝐵 < 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | renegcl | ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ ) | |
2 | ltneg | ⊢ ( ( - 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐴 < 𝐵 ↔ - 𝐵 < - - 𝐴 ) ) | |
3 | 1 2 | sylan | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐴 < 𝐵 ↔ - 𝐵 < - - 𝐴 ) ) |
4 | simpl | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ ) | |
5 | 4 | recnd | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℂ ) |
6 | 5 | negnegd | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → - - 𝐴 = 𝐴 ) |
7 | 6 | breq2d | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐵 < - - 𝐴 ↔ - 𝐵 < 𝐴 ) ) |
8 | 3 7 | bitrd | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐴 < 𝐵 ↔ - 𝐵 < 𝐴 ) ) |