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	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
Assertion	resum2sqrp	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		resum2sqcl.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2	1	resum2sqcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ )
3	2	adantlr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ )
4	1	resum2sqgt0	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 0 < 𝑄 )
5	3 4	elrpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ+ )