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

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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≠ 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 ) )