This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )