Description: Negative contraposition law. (Contributed by NM, 9-May-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | negcon1 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 = 𝐵 ↔ - 𝐵 = 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negcl | ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ ) | |
2 | neg11 | ⊢ ( ( - 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - - 𝐴 = - 𝐵 ↔ - 𝐴 = 𝐵 ) ) | |
3 | 1 2 | sylan | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - - 𝐴 = - 𝐵 ↔ - 𝐴 = 𝐵 ) ) |
4 | negneg | ⊢ ( 𝐴 ∈ ℂ → - - 𝐴 = 𝐴 ) | |
5 | 4 | adantr | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - - 𝐴 = 𝐴 ) |
6 | 5 | eqeq1d | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - - 𝐴 = - 𝐵 ↔ 𝐴 = - 𝐵 ) ) |
7 | 3 6 | bitr3d | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 = 𝐵 ↔ 𝐴 = - 𝐵 ) ) |
8 | eqcom | ⊢ ( 𝐴 = - 𝐵 ↔ - 𝐵 = 𝐴 ) | |
9 | 7 8 | bitrdi | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 = 𝐵 ↔ - 𝐵 = 𝐴 ) ) |