resum2sqorgt0

Description: The sum of the square of two real numbers is greater than zero if at least one of the real numbers is nonzero. (Contributed by AV, 26-Feb-2023)

		Ref	Expression
	Hypothesis	resum2sqcl.q	$⊢ Q = A^{2} + B^{2}$
	Assertion	resum2sqorgt0	$⊢ (A \in ℝ \land B \in ℝ \land (A \neq 0 \lor B \neq 0)) \to 0 < Q$

Proof

Step	Hyp	Ref	Expression
1		resum2sqcl.q	$⊢ Q = A^{2} + B^{2}$
2	1	resum2sqgt0	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ) \to 0 < Q$
3	2	ex	$⊢ (A \in ℝ \land A \neq 0) \to (B \in ℝ \to 0 < Q)$
4	3	expcom	$⊢ A \neq 0 \to (A \in ℝ \to (B \in ℝ \to 0 < Q))$
5	4	com23	$⊢ A \neq 0 \to (B \in ℝ \to (A \in ℝ \to 0 < Q))$
6		eqid	$⊢ B^{2} + A^{2} = B^{2} + A^{2}$
7	6	resum2sqgt0	$⊢ ((B \in ℝ \land B \neq 0) \land A \in ℝ) \to 0 < B^{2} + A^{2}$
8	1	breq2i	$⊢ 0 < Q \leftrightarrow 0 < A^{2} + B^{2}$
9		resqcl	$⊢ A \in ℝ \to A^{2} \in ℝ$
10	9	adantl	$⊢ ((B \in ℝ \land B \neq 0) \land A \in ℝ) \to A^{2} \in ℝ$
11	10	recnd	$⊢ ((B \in ℝ \land B \neq 0) \land A \in ℝ) \to A^{2} \in ℂ$
12		resqcl	$⊢ B \in ℝ \to B^{2} \in ℝ$
13	12	ad2antrr	$⊢ ((B \in ℝ \land B \neq 0) \land A \in ℝ) \to B^{2} \in ℝ$
14	13	recnd	$⊢ ((B \in ℝ \land B \neq 0) \land A \in ℝ) \to B^{2} \in ℂ$
15	11 14	addcomd	$⊢ ((B \in ℝ \land B \neq 0) \land A \in ℝ) \to A^{2} + B^{2} = B^{2} + A^{2}$
16	15	breq2d	$⊢ ((B \in ℝ \land B \neq 0) \land A \in ℝ) \to (0 < A^{2} + B^{2} \leftrightarrow 0 < B^{2} + A^{2})$
17	8 16	bitrid	$⊢ ((B \in ℝ \land B \neq 0) \land A \in ℝ) \to (0 < Q \leftrightarrow 0 < B^{2} + A^{2})$
18	7 17	mpbird	$⊢ ((B \in ℝ \land B \neq 0) \land A \in ℝ) \to 0 < Q$
19	18	ex	$⊢ (B \in ℝ \land B \neq 0) \to (A \in ℝ \to 0 < Q)$
20	19	expcom	$⊢ B \neq 0 \to (B \in ℝ \to (A \in ℝ \to 0 < Q))$
21	5 20	jaoi	$⊢ (A \neq 0 \lor B \neq 0) \to (B \in ℝ \to (A \in ℝ \to 0 < Q))$
22	21	3imp31	$⊢ (A \in ℝ \land B \in ℝ \land (A \neq 0 \lor B \neq 0)) \to 0 < Q$

Metamath Proof Explorer

Theorem resum2sqorgt0

Proof