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

Proof

Step	Hyp	Ref	Expression
1		resum2sqcl.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ )
3	2	resqcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
4	3	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
5		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
6	5	resqcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
7		sqgt0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 ↑ 2 ) )
8	7	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 0 < ( 𝐴 ↑ 2 ) )
9		sqge0	⊢ ( 𝐵 ∈ ℝ → 0 ≤ ( 𝐵 ↑ 2 ) )
10	9	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( 𝐵 ↑ 2 ) )
11	4 6 8 10	addgtge0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 0 < ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
12	11 1	breqtrrdi	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 0 < 𝑄 )