Theorem resum2sqgt0

Description: The sum of the square of a nonzero real number and the square of another real number is greater than zero. (Contributed by AV, 7-Feb-2023)

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

Proof

Step	Hyp	Ref	Expression
1		resum2sqcl.q	$$⊢Q=A^2+B^2$$
2		simpl	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to A\in ℝ$$
3	2	resqcld	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to A^2\in ℝ$$
4	3	adantr	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to A^2\in ℝ$$
5		simpr	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to B\in ℝ$$
6	5	resqcld	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to B^2\in ℝ$$
7		sqgt0	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to 0<A^2$$
8	7	adantr	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to 0<A^2$$
9		sqge0	$$⊢B\in ℝ\to 0\le B^2$$
10	9	adantl	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to 0\le B^2$$
11	4 6 8 10	addgtge0d	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to 0<A^2+B^2$$
12	11 1	breqtrrdi	$$⊢\left(\left(A\in ℝ\wedge A\ne 0\right)\wedge B\in ℝ\right)\to 0<Q$$