resqrtcl

Description: Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013)

		Ref	Expression
	Assertion	resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		resqrex	$⊢ (A \in ℝ \land 0 \leq A) \to \exists y \in ℝ (0 \leq y \land y^{2} = A)$
2		simp1l	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to A \in ℝ$
3		recn	$⊢ A \in ℝ \to A \in ℂ$
4		sqrtval	$⊢ A \in ℂ \to \sqrt{A} = (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
5	2 3 4	3syl	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to \sqrt{A} = (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
6		simp3r	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to y^{2} = A$
7		simp3l	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to 0 \leq y$
8		rere	$⊢ y \in ℝ \to ℜ (y) = y$
9	8	3ad2ant2	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to ℜ (y) = y$
10	7 9	breqtrrd	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to 0 \leq ℜ (y)$
11		rennim	$⊢ y \in ℝ \to i y \notin ℝ^{+}$
12	11	3ad2ant2	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to i y \notin ℝ^{+}$
13	6 10 12	3jca	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+})$
14		recn	$⊢ y \in ℝ \to y \in ℂ$
15	14	3ad2ant2	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to y \in ℂ$
16		resqreu	$⊢ (A \in ℝ \land 0 \leq A) \to \exists! x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
17	16	3ad2ant1	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to \exists! x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
18		oveq1	$⊢ x = y \to x^{2} = y^{2}$
19	18	eqeq1d	$⊢ x = y \to (x^{2} = A \leftrightarrow y^{2} = A)$
20		fveq2	$⊢ x = y \to ℜ (x) = ℜ (y)$
21	20	breq2d	$⊢ x = y \to (0 \leq ℜ (x) \leftrightarrow 0 \leq ℜ (y))$
22		oveq2	$⊢ x = y \to i x = i y$
23		neleq1	$⊢ i x = i y \to (i x \notin ℝ^{+} \leftrightarrow i y \notin ℝ^{+})$
24	22 23	syl	$⊢ x = y \to (i x \notin ℝ^{+} \leftrightarrow i y \notin ℝ^{+})$
25	19 21 24	3anbi123d	$⊢ x = y \to ((x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow (y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}))$
26	25	riota2	$⊢ (y \in ℂ \land \exists! x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \to ((y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}) \leftrightarrow (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = y)$
27	15 17 26	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to ((y^{2} = A \land 0 \leq ℜ (y) \land i y \notin ℝ^{+}) \leftrightarrow (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = y)$
28	13 27	mpbid	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = y$
29	5 28	eqtrd	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to \sqrt{A} = y$
30		simp2	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to y \in ℝ$
31	29 30	eqeltrd	$⊢ ((A \in ℝ \land 0 \leq A) \land y \in ℝ \land (0 \leq y \land y^{2} = A)) \to \sqrt{A} \in ℝ$
32	31	rexlimdv3a	$⊢ (A \in ℝ \land 0 \leq A) \to (\exists y \in ℝ (0 \leq y \land y^{2} = A) \to \sqrt{A} \in ℝ)$
33	1 32	mpd	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$

Metamath Proof Explorer

Theorem resqrtcl

Proof