Theorem 01sqrexlem3

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	01sqrexlem3	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to \left(S\subseteq ℝ\wedge S\ne \varnothing \wedge \exists z\in ℝ\forall y\in Sy\le z\right)$$

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		ssrab2	$$⊢\left\{x\in {ℝ}^{+}|x^2\le A\right\}\subseteq {ℝ}^{+}$$
4		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
5	3 4	sstri	$$⊢\left\{x\in {ℝ}^{+}|x^2\le A\right\}\subseteq ℝ$$
6	1 5	eqsstri	$$⊢S\subseteq ℝ$$
7	6	a1i	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to S\subseteq ℝ$$
8	1 2	01sqrexlem2	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to A\in S$$
9	8	ne0d	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to S\ne \varnothing$$
10		1re	$$⊢1\in ℝ$$
11	1 2	01sqrexlem1	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to \forall y\in Sy\le 1$$
12		brralrspcev	$$⊢\left(1\in ℝ\wedge \forall y\in Sy\le 1\right)\to \exists z\in ℝ\forall y\in Sy\le z$$
13	10 11 12	sylancr	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to \exists z\in ℝ\forall y\in Sy\le z$$
14	7 9 13	3jca	$$⊢\left(A\in {ℝ}^{+}\wedge A\le 1\right)\to \left(S\subseteq ℝ\wedge S\ne \varnothing \wedge \exists z\in ℝ\forall y\in Sy\le z\right)$$