recextlem2

		Ref	Expression
	Assertion	recextlem2	$⊢ (A \in ℝ \land B \in ℝ \land A + i B \neq 0) \to A A + B B \neq 0$

Proof

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

Metamath Proof Explorer

Theorem recextlem2

Proof