# Metamath Proof Explorer

## Theorem recextlem2

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

Ref Expression
Assertion recextlem2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}+\mathrm{i}{B}\ne 0\right)\to {A}{A}+{B}{B}\ne 0$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{B}=0\to \mathrm{i}{B}=\mathrm{i}\cdot 0$
2 ax-icn ${⊢}\mathrm{i}\in ℂ$
3 2 mul01i ${⊢}\mathrm{i}\cdot 0=0$
4 1 3 syl6eq ${⊢}{B}=0\to \mathrm{i}{B}=0$
5 oveq12 ${⊢}\left({A}=0\wedge \mathrm{i}{B}=0\right)\to {A}+\mathrm{i}{B}=0+0$
6 4 5 sylan2 ${⊢}\left({A}=0\wedge {B}=0\right)\to {A}+\mathrm{i}{B}=0+0$
7 00id ${⊢}0+0=0$
8 6 7 syl6eq ${⊢}\left({A}=0\wedge {B}=0\right)\to {A}+\mathrm{i}{B}=0$
9 8 necon3ai ${⊢}{A}+\mathrm{i}{B}\ne 0\to ¬\left({A}=0\wedge {B}=0\right)$
10 neorian ${⊢}\left({A}\ne 0\vee {B}\ne 0\right)↔¬\left({A}=0\wedge {B}=0\right)$
11 9 10 sylibr ${⊢}{A}+\mathrm{i}{B}\ne 0\to \left({A}\ne 0\vee {B}\ne 0\right)$
12 remulcl ${⊢}\left({A}\in ℝ\wedge {A}\in ℝ\right)\to {A}{A}\in ℝ$
13 12 anidms ${⊢}{A}\in ℝ\to {A}{A}\in ℝ$
14 remulcl ${⊢}\left({B}\in ℝ\wedge {B}\in ℝ\right)\to {B}{B}\in ℝ$
15 14 anidms ${⊢}{B}\in ℝ\to {B}{B}\in ℝ$
16 13 15 anim12i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}{A}\in ℝ\wedge {B}{B}\in ℝ\right)$
17 msqgt0 ${⊢}\left({A}\in ℝ\wedge {A}\ne 0\right)\to 0<{A}{A}$
18 msqge0 ${⊢}{B}\in ℝ\to 0\le {B}{B}$
19 17 18 anim12i ${⊢}\left(\left({A}\in ℝ\wedge {A}\ne 0\right)\wedge {B}\in ℝ\right)\to \left(0<{A}{A}\wedge 0\le {B}{B}\right)$
20 19 an32s ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\ne 0\right)\to \left(0<{A}{A}\wedge 0\le {B}{B}\right)$
21 addgtge0 ${⊢}\left(\left({A}{A}\in ℝ\wedge {B}{B}\in ℝ\right)\wedge \left(0<{A}{A}\wedge 0\le {B}{B}\right)\right)\to 0<{A}{A}+{B}{B}$
22 16 20 21 syl2an2r ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\ne 0\right)\to 0<{A}{A}+{B}{B}$
23 msqge0 ${⊢}{A}\in ℝ\to 0\le {A}{A}$
24 msqgt0 ${⊢}\left({B}\in ℝ\wedge {B}\ne 0\right)\to 0<{B}{B}$
25 23 24 anim12i ${⊢}\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge {B}\ne 0\right)\right)\to \left(0\le {A}{A}\wedge 0<{B}{B}\right)$
26 25 anassrs ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {B}\ne 0\right)\to \left(0\le {A}{A}\wedge 0<{B}{B}\right)$
27 addgegt0 ${⊢}\left(\left({A}{A}\in ℝ\wedge {B}{B}\in ℝ\right)\wedge \left(0\le {A}{A}\wedge 0<{B}{B}\right)\right)\to 0<{A}{A}+{B}{B}$
28 16 26 27 syl2an2r ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {B}\ne 0\right)\to 0<{A}{A}+{B}{B}$
29 22 28 jaodan ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({A}\ne 0\vee {B}\ne 0\right)\right)\to 0<{A}{A}+{B}{B}$
30 11 29 sylan2 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}+\mathrm{i}{B}\ne 0\right)\to 0<{A}{A}+{B}{B}$
31 30 3impa ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}+\mathrm{i}{B}\ne 0\right)\to 0<{A}{A}+{B}{B}$
32 31 gt0ne0d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}+\mathrm{i}{B}\ne 0\right)\to {A}{A}+{B}{B}\ne 0$