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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2	1	mul01i	⊢ ( i · 0 ) = 0
3	2	oveq2i	⊢ ( 0 + ( i · 0 ) ) = ( 0 + 0 )
4		00id	⊢ ( 0 + 0 ) = 0
5	3 4	eqtri	⊢ ( 0 + ( i · 0 ) ) = 0
6	5	eqeq2i	⊢ ( ( 𝐴 + ( i · 𝐵 ) ) = ( 0 + ( i · 0 ) ) ↔ ( 𝐴 + ( i · 𝐵 ) ) = 0 )
7		0re	⊢ 0 ∈ ℝ
8		cru	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) = ( 0 + ( i · 0 ) ) ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
9	7 7 8	mpanr12	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) = ( 0 + ( i · 0 ) ) ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
10	6 9	bitr3id	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
11	10	necon3abid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ↔ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
12		neorian	⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
13	11 12	syl6rbbr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) )