resqrex

Description: Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013)

		Ref	Expression
	Assertion	resqrex	$⊢ (A \in ℝ \land 0 \leq A) \to \exists x \in ℝ (0 \leq x \land x^{2} = A)$

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		leloe	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
3	1 2	mpan	$⊢ A \in ℝ \to (0 \leq A \leftrightarrow (0 < A \lor 0 = A))$
4		elrp	$⊢ A \in ℝ^{+} \leftrightarrow (A \in ℝ \land 0 < A)$
5		01sqrex	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \exists x \in ℝ^{+} (x \leq 1 \land x^{2} = A)$
6		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
7	6	anim1i	$⊢ (x \in ℝ^{+} \land x^{2} = A) \to ((x \in ℝ \land 0 \leq x) \land x^{2} = A)$
8		anass	$⊢ ((x \in ℝ \land 0 \leq x) \land x^{2} = A) \leftrightarrow (x \in ℝ \land (0 \leq x \land x^{2} = A))$
9	7 8	sylib	$⊢ (x \in ℝ^{+} \land x^{2} = A) \to (x \in ℝ \land (0 \leq x \land x^{2} = A))$
10	9	adantrl	$⊢ (x \in ℝ^{+} \land (x \leq 1 \land x^{2} = A)) \to (x \in ℝ \land (0 \leq x \land x^{2} = A))$
11	10	reximi2	$⊢ \exists x \in ℝ^{+} (x \leq 1 \land x^{2} = A) \to \exists x \in ℝ (0 \leq x \land x^{2} = A)$
12	5 11	syl	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \exists x \in ℝ (0 \leq x \land x^{2} = A)$
13	4 12	sylanbr	$⊢ ((A \in ℝ \land 0 < A) \land A \leq 1) \to \exists x \in ℝ (0 \leq x \land x^{2} = A)$
14	13	exp31	$⊢ A \in ℝ \to (0 < A \to (A \leq 1 \to \exists x \in ℝ (0 \leq x \land x^{2} = A)))$
15		sq0	$⊢ 0^{2} = 0$
16		id	$⊢ 0 = A \to 0 = A$
17	15 16	syl5eq	$⊢ 0 = A \to 0^{2} = A$
18		0le0	$⊢ 0 \leq 0$
19	17 18	jctil	$⊢ 0 = A \to (0 \leq 0 \land 0^{2} = A)$
20		breq2	$⊢ x = 0 \to (0 \leq x \leftrightarrow 0 \leq 0)$
21		oveq1	$⊢ x = 0 \to x^{2} = 0^{2}$
22	21	eqeq1d	$⊢ x = 0 \to (x^{2} = A \leftrightarrow 0^{2} = A)$
23	20 22	anbi12d	$⊢ x = 0 \to ((0 \leq x \land x^{2} = A) \leftrightarrow (0 \leq 0 \land 0^{2} = A))$
24	23	rspcev	$⊢ (0 \in ℝ \land (0 \leq 0 \land 0^{2} = A)) \to \exists x \in ℝ (0 \leq x \land x^{2} = A)$
25	1 19 24	sylancr	$⊢ 0 = A \to \exists x \in ℝ (0 \leq x \land x^{2} = A)$
26	25	a1i13	$⊢ A \in ℝ \to (0 = A \to (A \leq 1 \to \exists x \in ℝ (0 \leq x \land x^{2} = A)))$
27	14 26	jaod	$⊢ A \in ℝ \to ((0 < A \lor 0 = A) \to (A \leq 1 \to \exists x \in ℝ (0 \leq x \land x^{2} = A)))$
28	3 27	sylbid	$⊢ A \in ℝ \to (0 \leq A \to (A \leq 1 \to \exists x \in ℝ (0 \leq x \land x^{2} = A)))$
29	28	imp	$⊢ (A \in ℝ \land 0 \leq A) \to (A \leq 1 \to \exists x \in ℝ (0 \leq x \land x^{2} = A))$
30		0lt1	$⊢ 0 < 1$
31		1re	$⊢ 1 \in ℝ$
32		ltletr	$⊢ (0 \in ℝ \land 1 \in ℝ \land A \in ℝ) \to ((0 < 1 \land 1 \leq A) \to 0 < A)$
33	1 31 32	mp3an12	$⊢ A \in ℝ \to ((0 < 1 \land 1 \leq A) \to 0 < A)$
34	30 33	mpani	$⊢ A \in ℝ \to (1 \leq A \to 0 < A)$
35	34	imp	$⊢ (A \in ℝ \land 1 \leq A) \to 0 < A$
36	4	biimpri	$⊢ (A \in ℝ \land 0 < A) \to A \in ℝ^{+}$
37	35 36	syldan	$⊢ (A \in ℝ \land 1 \leq A) \to A \in ℝ^{+}$
38	37	rpreccld	$⊢ (A \in ℝ \land 1 \leq A) \to \frac{1}{A} \in ℝ^{+}$
39		simpr	$⊢ (A \in ℝ \land 1 \leq A) \to 1 \leq A$
40		lerec	$⊢ ((1 \in ℝ \land 0 < 1) \land (A \in ℝ \land 0 < A)) \to (1 \leq A \leftrightarrow \frac{1}{A} \leq \frac{1}{1})$
41	31 30 40	mpanl12	$⊢ (A \in ℝ \land 0 < A) \to (1 \leq A \leftrightarrow \frac{1}{A} \leq \frac{1}{1})$
42	35 41	syldan	$⊢ (A \in ℝ \land 1 \leq A) \to (1 \leq A \leftrightarrow \frac{1}{A} \leq \frac{1}{1})$
43	39 42	mpbid	$⊢ (A \in ℝ \land 1 \leq A) \to \frac{1}{A} \leq \frac{1}{1}$
44		1div1e1	$⊢ \frac{1}{1} = 1$
45	43 44	breqtrdi	$⊢ (A \in ℝ \land 1 \leq A) \to \frac{1}{A} \leq 1$
46		01sqrex	$⊢ (\frac{1}{A} \in ℝ^{+} \land \frac{1}{A} \leq 1) \to \exists y \in ℝ^{+} (y \leq 1 \land y^{2} = \frac{1}{A})$
47	38 45 46	syl2anc	$⊢ (A \in ℝ \land 1 \leq A) \to \exists y \in ℝ^{+} (y \leq 1 \land y^{2} = \frac{1}{A})$
48		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
49	48	3ad2ant2	$⊢ ((A \in ℝ \land 1 \leq A) \land y \in ℝ^{+} \land (y \leq 1 \land y^{2} = \frac{1}{A})) \to y \in ℝ$
50		rpgt0	$⊢ y \in ℝ^{+} \to 0 < y$
51	50	3ad2ant2	$⊢ ((A \in ℝ \land 1 \leq A) \land y \in ℝ^{+} \land (y \leq 1 \land y^{2} = \frac{1}{A})) \to 0 < y$
52		gt0ne0	$⊢ (y \in ℝ \land 0 < y) \to y \neq 0$
53		rereccl	$⊢ (y \in ℝ \land y \neq 0) \to \frac{1}{y} \in ℝ$
54	52 53	syldan	$⊢ (y \in ℝ \land 0 < y) \to \frac{1}{y} \in ℝ$
55	49 51 54	syl2anc	$⊢ ((A \in ℝ \land 1 \leq A) \land y \in ℝ^{+} \land (y \leq 1 \land y^{2} = \frac{1}{A})) \to \frac{1}{y} \in ℝ$
56		recgt0	$⊢ (y \in ℝ \land 0 < y) \to 0 < \frac{1}{y}$
57		ltle	$⊢ (0 \in ℝ \land \frac{1}{y} \in ℝ) \to (0 < \frac{1}{y} \to 0 \leq \frac{1}{y})$
58	1 57	mpan	$⊢ \frac{1}{y} \in ℝ \to (0 < \frac{1}{y} \to 0 \leq \frac{1}{y})$
59	54 56 58	sylc	$⊢ (y \in ℝ \land 0 < y) \to 0 \leq \frac{1}{y}$
60	49 51 59	syl2anc	$⊢ ((A \in ℝ \land 1 \leq A) \land y \in ℝ^{+} \land (y \leq 1 \land y^{2} = \frac{1}{A})) \to 0 \leq \frac{1}{y}$
61		recn	$⊢ y \in ℝ \to y \in ℂ$
62	61	adantr	$⊢ (y \in ℝ \land 0 < y) \to y \in ℂ$
63	62 52	sqrecd	$⊢ (y \in ℝ \land 0 < y) \to {(\frac{1}{y})}^{2} = \frac{1}{y^{2}}$
64	49 51 63	syl2anc	$⊢ ((A \in ℝ \land 1 \leq A) \land y \in ℝ^{+} \land (y \leq 1 \land y^{2} = \frac{1}{A})) \to {(\frac{1}{y})}^{2} = \frac{1}{y^{2}}$
65		simp3r	$⊢ ((A \in ℝ \land 1 \leq A) \land y \in ℝ^{+} \land (y \leq 1 \land y^{2} = \frac{1}{A})) \to y^{2} = \frac{1}{A}$
66	65	oveq2d	$⊢ ((A \in ℝ \land 1 \leq A) \land y \in ℝ^{+} \land (y \leq 1 \land y^{2} = \frac{1}{A})) \to \frac{1}{y^{2}} = \frac{1}{\frac{1}{A}}$
67		recn	$⊢ A \in ℝ \to A \in ℂ$
68		gt0ne0	$⊢ (A \in ℝ \land 0 < A) \to A \neq 0$
69	35 68	syldan	$⊢ (A \in ℝ \land 1 \leq A) \to A \neq 0$
70		recrec	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{\frac{1}{A}} = A$
71	67 69 70	syl2an2r	$⊢ (A \in ℝ \land 1 \leq A) \to \frac{1}{\frac{1}{A}} = A$
72	71	3ad2ant1	$⊢ ((A \in ℝ \land 1 \leq A) \land y \in ℝ^{+} \land (y \leq 1 \land y^{2} = \frac{1}{A})) \to \frac{1}{\frac{1}{A}} = A$
73	64 66 72	3eqtrd	$⊢ ((A \in ℝ \land 1 \leq A) \land y \in ℝ^{+} \land (y \leq 1 \land y^{2} = \frac{1}{A})) \to {(\frac{1}{y})}^{2} = A$
74		breq2	$⊢ x = \frac{1}{y} \to (0 \leq x \leftrightarrow 0 \leq \frac{1}{y})$
75		oveq1	$⊢ x = \frac{1}{y} \to x^{2} = {(\frac{1}{y})}^{2}$
76	75	eqeq1d	$⊢ x = \frac{1}{y} \to (x^{2} = A \leftrightarrow {(\frac{1}{y})}^{2} = A)$
77	74 76	anbi12d	$⊢ x = \frac{1}{y} \to ((0 \leq x \land x^{2} = A) \leftrightarrow (0 \leq \frac{1}{y} \land {(\frac{1}{y})}^{2} = A))$
78	77	rspcev	$⊢ (\frac{1}{y} \in ℝ \land (0 \leq \frac{1}{y} \land {(\frac{1}{y})}^{2} = A)) \to \exists x \in ℝ (0 \leq x \land x^{2} = A)$
79	55 60 73 78	syl12anc	$⊢ ((A \in ℝ \land 1 \leq A) \land y \in ℝ^{+} \land (y \leq 1 \land y^{2} = \frac{1}{A})) \to \exists x \in ℝ (0 \leq x \land x^{2} = A)$
80	79	rexlimdv3a	$⊢ (A \in ℝ \land 1 \leq A) \to (\exists y \in ℝ^{+} (y \leq 1 \land y^{2} = \frac{1}{A}) \to \exists x \in ℝ (0 \leq x \land x^{2} = A))$
81	47 80	mpd	$⊢ (A \in ℝ \land 1 \leq A) \to \exists x \in ℝ (0 \leq x \land x^{2} = A)$
82	81	ex	$⊢ A \in ℝ \to (1 \leq A \to \exists x \in ℝ (0 \leq x \land x^{2} = A))$
83	82	adantr	$⊢ (A \in ℝ \land 0 \leq A) \to (1 \leq A \to \exists x \in ℝ (0 \leq x \land x^{2} = A))$
84		simpl	$⊢ (A \in ℝ \land 0 \leq A) \to A \in ℝ$
85		letric	$⊢ (A \in ℝ \land 1 \in ℝ) \to (A \leq 1 \lor 1 \leq A)$
86	84 31 85	sylancl	$⊢ (A \in ℝ \land 0 \leq A) \to (A \leq 1 \lor 1 \leq A)$
87	29 83 86	mpjaod	$⊢ (A \in ℝ \land 0 \leq A) \to \exists x \in ℝ (0 \leq x \land x^{2} = A)$

Metamath Proof Explorer

Theorem resqrex

Proof