Metamath Proof Explorer

Theorem recextlem2

Description: Lemma for recex . (Contributed by Eric Schmidt, 23-May-2007)

Ref Expression
Assertion recextlem2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A + i ⁢ B ≠ 0 → A ⁢ A + B ⁢ B ≠ 0

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ B = 0 → i ⁢ B = i ⋅ 0
2 ax-icn ⊢ i ∈ ℂ
3 2 mul01i ⊢ i ⋅ 0 = 0
4 1 3 eqtrdi ⊢ B = 0 → i ⁢ B = 0
5 oveq12 ⊢ A = 0 ∧ i ⁢ B = 0 → A + i ⁢ B = 0 + 0
6 4 5 sylan2 ⊢ A = 0 ∧ B = 0 → A + i ⁢ B = 0 + 0
7 00id ⊢ 0 + 0 = 0
8 6 7 eqtrdi ⊢ A = 0 ∧ B = 0 → A + i ⁢ B = 0
9 8 necon3ai ⊢ A + i ⁢ B ≠ 0 → ¬ A = 0 ∧ B = 0
10 neorian ⊢ A ≠ 0 ∨ B ≠ 0 ↔ ¬ A = 0 ∧ B = 0
11 9 10 sylibr ⊢ A + i ⁢ B ≠ 0 → A ≠ 0 ∨ B ≠ 0
12 remulcl ⊢ A ∈ ℝ ∧ A ∈ ℝ → A ⁢ A ∈ ℝ
13 12 anidms ⊢ A ∈ ℝ → A ⁢ A ∈ ℝ
14 remulcl ⊢ B ∈ ℝ ∧ B ∈ ℝ → B ⁢ B ∈ ℝ
15 14 anidms ⊢ B ∈ ℝ → B ⁢ B ∈ ℝ
16 13 15 anim12i ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ A ∈ ℝ ∧ B ⁢ B ∈ ℝ
17 msqgt0 ⊢ A ∈ ℝ ∧ A ≠ 0 → 0 < A ⁢ A
18 msqge0 ⊢ B ∈ ℝ → 0 ≤ B ⁢ B
19 17 18 anim12i ⊢ A ∈ ℝ ∧ A ≠ 0 ∧ B ∈ ℝ → 0 < A ⁢ A ∧ 0 ≤ B ⁢ B
20 19 an32s ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≠ 0 → 0 < A ⁢ A ∧ 0 ≤ B ⁢ B
21 addgtge0 ⊢ A ⁢ A ∈ ℝ ∧ B ⁢ B ∈ ℝ ∧ 0 < A ⁢ A ∧ 0 ≤ B ⁢ B → 0 < A ⁢ A + B ⁢ B
22 16 20 21 syl2an2r ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≠ 0 → 0 < A ⁢ A + B ⁢ B
23 msqge0 ⊢ A ∈ ℝ → 0 ≤ A ⁢ A
24 msqgt0 ⊢ B ∈ ℝ ∧ B ≠ 0 → 0 < B ⁢ B
25 23 24 anim12i ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≠ 0 → 0 ≤ A ⁢ A ∧ 0 < B ⁢ B
26 25 anassrs ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≠ 0 → 0 ≤ A ⁢ A ∧ 0 < B ⁢ B
27 addgegt0 ⊢ A ⁢ A ∈ ℝ ∧ B ⁢ B ∈ ℝ ∧ 0 ≤ A ⁢ A ∧ 0 < B ⁢ B → 0 < A ⁢ A + B ⁢ B
28 16 26 27 syl2an2r ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≠ 0 → 0 < A ⁢ A + B ⁢ B
29 22 28 jaodan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≠ 0 ∨ B ≠ 0 → 0 < A ⁢ A + B ⁢ B
30 11 29 sylan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A + i ⁢ B ≠ 0 → 0 < A ⁢ A + B ⁢ B
31 30 3impa ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A + i ⁢ B ≠ 0 → 0 < A ⁢ A + B ⁢ B
32 31 gt0ne0d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A + i ⁢ B ≠ 0 → A ⁢ A + B ⁢ B ≠ 0