Theorem resum2sqcl

Description: The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023)

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

Proof

Step	Hyp	Ref	Expression
1		resum2sqcl.q	$$⊢Q=A^2+B^2$$
2		simpl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\in ℝ$$
3	2	resqcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A^2\in ℝ$$
4		simpr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℝ$$
5	4	resqcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B^2\in ℝ$$
6	3 5	readdcld	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A^2+B^2\in ℝ$$
7	1 6	eqeltrid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to Q\in ℝ$$