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		neorian	⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
2		ax-icn	⊢ i ∈ ℂ
3	2	mul01i	⊢ ( i · 0 ) = 0
4	3	oveq2i	⊢ ( 0 + ( i · 0 ) ) = ( 0 + 0 )
5		00id	⊢ ( 0 + 0 ) = 0
6	4 5	eqtri	⊢ ( 0 + ( i · 0 ) ) = 0
7	6	eqeq2i	⊢ ( ( 𝐴 + ( i · 𝐵 ) ) = ( 0 + ( i · 0 ) ) ↔ ( 𝐴 + ( i · 𝐵 ) ) = 0 )
8		0re	⊢ 0 ∈ ℝ
9		cru	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) ) → ( ( 𝐴 + ( i · 𝐵 ) ) = ( 0 + ( i · 0 ) ) ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
10	8 8 9	mpanr12	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) = ( 0 + ( i · 0 ) ) ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
11	7 10	bitr3id	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
12	11	necon3abid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ↔ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
13	1 12	bitr4id	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) )