Metamath Proof Explorer

Theorem crne0

Description: The real representation of complex numbers is nonzero iff one of its terms is nonzero. (Contributed by NM, 29-Apr-2005) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion crne0 
|- ( ( A e. RR /\ B e. RR ) -> ( ( A =/= 0 \/ B =/= 0 ) <-> ( A + ( _i x. B ) ) =/= 0 ) )

Proof

Step Hyp Ref Expression
1 neorian 
 |-  ( ( A =/= 0 \/ B =/= 0 ) <-> -. ( A = 0 /\ B = 0 ) )
2 ax-icn 
 |-  _i e. CC
3 2 mul01i 
 |-  ( _i x. 0 ) = 0
4 3 oveq2i 
 |-  ( 0 + ( _i x. 0 ) ) = ( 0 + 0 )
5 00id 
 |-  ( 0 + 0 ) = 0
6 4 5 eqtri 
 |-  ( 0 + ( _i x. 0 ) ) = 0
7 6 eqeq2i 
 |-  ( ( A + ( _i x. B ) ) = ( 0 + ( _i x. 0 ) ) <-> ( A + ( _i x. B ) ) = 0 )
8 0re 
 |-  0 e. RR
9 cru 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 e. RR /\ 0 e. RR ) ) -> ( ( A + ( _i x. B ) ) = ( 0 + ( _i x. 0 ) ) <-> ( A = 0 /\ B = 0 ) ) )
10 8 8 9 mpanr12 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + ( _i x. B ) ) = ( 0 + ( _i x. 0 ) ) <-> ( A = 0 /\ B = 0 ) ) )
11 7 10 bitr3id 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + ( _i x. B ) ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
12 11 necon3abid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + ( _i x. B ) ) =/= 0 <-> -. ( A = 0 /\ B = 0 ) ) )
13 1 12 bitr4id 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A =/= 0 \/ B =/= 0 ) <-> ( A + ( _i x. B ) ) =/= 0 ) )