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 ∈ ℝ ∧ B ∈ ℝ → A ≠ 0 ∨ B ≠ 0 ↔ A + i ⁢ B ≠ 0

Proof

Step Hyp Ref Expression
1 neorian ⊢ A ≠ 0 ∨ B ≠ 0 ↔ ¬ A = 0 ∧ B = 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 ⊢ A + i ⁢ B = 0 + i ⋅ 0 ↔ A + i ⁢ B = 0
8 0re ⊢ 0 ∈ ℝ
9 cru ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ∈ ℝ → A + i ⁢ B = 0 + i ⋅ 0 ↔ A = 0 ∧ B = 0
10 8 8 9 mpanr12 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B = 0 + i ⋅ 0 ↔ A = 0 ∧ B = 0
11 7 10 bitr3id ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B = 0 ↔ A = 0 ∧ B = 0
12 11 necon3abid ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B ≠ 0 ↔ ¬ A = 0 ∧ B = 0
13 1 12 bitr4id ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≠ 0 ∨ B ≠ 0 ↔ A + i ⁢ B ≠ 0