Metamath Proof Explorer


Theorem negcon1

Description: Negative contraposition law. (Contributed by NM, 9-May-2004)

Ref Expression
Assertion negcon1
|- ( ( A e. CC /\ B e. CC ) -> ( -u A = B <-> -u B = A ) )

Proof

Step Hyp Ref Expression
1 negcl
 |-  ( A e. CC -> -u A e. CC )
2 neg11
 |-  ( ( -u A e. CC /\ B e. CC ) -> ( -u -u A = -u B <-> -u A = B ) )
3 1 2 sylan
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u -u A = -u B <-> -u A = B ) )
4 negneg
 |-  ( A e. CC -> -u -u A = A )
5 4 adantr
 |-  ( ( A e. CC /\ B e. CC ) -> -u -u A = A )
6 5 eqeq1d
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u -u A = -u B <-> A = -u B ) )
7 3 6 bitr3d
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u A = B <-> A = -u B ) )
8 eqcom
 |-  ( A = -u B <-> -u B = A )
9 7 8 bitrdi
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u A = B <-> -u B = A ) )