Theorem resum2sqrp

Description: The sum of the square of a nonzero real number and the square of another real number is a positive real number. (Contributed by AV, 2-May-2023)

	Ref	Expression
Hypothesis	resum2sqcl.q	$$⊢Q=A^2+B^2$$
Assertion	resum2sqrp	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to Q\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		resum2sqcl.q	$$⊢Q=A^2+B^2$$
2	1	resum2sqcl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to Q\in ℝ$$
3	2	adantlr	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to Q\in ℝ$$
4	1	resum2sqgt0	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to 0<Q$$
5	3 4	elrpd	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to Q\in {ℝ}^{+}$$