Theorem 01sqrexlem2

Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013)

	Ref	Expression
Hypotheses	01sqrexlem1.1	$$⊢S=\left\{x\in {ℝ}^{+}|x^2\le A\right\}$$
	01sqrexlem1.2	$$⊢B=sup\left(S,ℝ,<\right)$$
Assertion	01sqrexlem2	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to A\in S$$

Proof

Step	Hyp	Ref	Expression
1		01sqrexlem1.1	$$⊢S=\left\{x\in {ℝ}^{+}|x^2\le A\right\}$$
2		01sqrexlem1.2	$$⊢B=sup\left(S,ℝ,<\right)$$
3		simpl	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to A\in {ℝ}^{+}$$
4		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
5		rpgt0	$$⊢A\in {ℝ}^{+}\to 0<A$$
6		1re	$$⊢1\in ℝ$$
7		lemul1	$$⊢\left(A\in ℝ\wedge 1\in ℝ\wedge \left(A\in ℝ\wedge 0<A\right)\right)\to \left(A\le 1\leftrightarrow AA\le 1A\right)$$
8	6 7	mp3an2	$$⊢\left(A\in ℝ\wedge \left(A\in ℝ\wedge 0<A\right)\right)\to \left(A\le 1\leftrightarrow AA\le 1A\right)$$
9	4 4 5 8	syl12anc	$$⊢A\in {ℝ}^{+}\to \left(A\le 1\leftrightarrow AA\le 1A\right)$$
10	9	biimpa	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to AA\le 1A$$
11		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
12	11	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to A\in ℂ$$
13		sqval	$$⊢A\in ℂ\to A^2=AA$$
14	13	eqcomd	$$⊢A\in ℂ\to AA=A^2$$
15	12 14	syl	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to AA=A^2$$
16	11	mullidd	$$⊢A\in {ℝ}^{+}\to 1A=A$$
17	16	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to 1A=A$$
18	10 15 17	3brtr3d	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to A^2\le A$$
19		oveq1	$$⊢x=A\to x^2=A^2$$
20	19	breq1d	$$⊢x=A\to \left(x^2\le A\leftrightarrow A^2\le A\right)$$
21	20 1	elrab2	$$⊢A\in S\leftrightarrow \left(A\in {ℝ}^{+}\wedge A^2\le A\right)$$
22	3 18 21	sylanbrc	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to A\in S$$