01sqrexlem1

	Ref	Expression
Hypotheses	01sqrexlem1.1	$⊢ S = \{x \in ℝ^{+} \| x^{2} \leq A\}$
	01sqrexlem1.2	$⊢ B = sup (S ℝ <)$
Assertion	01sqrexlem1	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \forall y \in S y \leq 1$

Proof

Step	Hyp	Ref	Expression
1		01sqrexlem1.1	$⊢ S = \{x \in ℝ^{+} \| x^{2} \leq A\}$
2		01sqrexlem1.2	$⊢ B = sup (S ℝ <)$
3		oveq1	$⊢ x = y \to x^{2} = y^{2}$
4	3	breq1d	$⊢ x = y \to (x^{2} \leq A \leftrightarrow y^{2} \leq A)$
5	4 1	elrab2	$⊢ y \in S \leftrightarrow (y \in ℝ^{+} \land y^{2} \leq A)$
6		simprr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to y^{2} \leq A$
7		simplr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to A \leq 1$
8		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
9	8	ad2antrl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to y \in ℝ$
10	9	resqcld	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to y^{2} \in ℝ$
11		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
12	11	ad2antrr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to A \in ℝ$
13		1re	$⊢ 1 \in ℝ$
14		letr	$⊢ (y^{2} \in ℝ \land A \in ℝ \land 1 \in ℝ) \to ((y^{2} \leq A \land A \leq 1) \to y^{2} \leq 1)$
15	13 14	mp3an3	$⊢ (y^{2} \in ℝ \land A \in ℝ) \to ((y^{2} \leq A \land A \leq 1) \to y^{2} \leq 1)$
16	10 12 15	syl2anc	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to ((y^{2} \leq A \land A \leq 1) \to y^{2} \leq 1)$
17	6 7 16	mp2and	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to y^{2} \leq 1$
18		sq1	$⊢ 1^{2} = 1$
19	17 18	breqtrrdi	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to y^{2} \leq 1^{2}$
20		rpge0	$⊢ y \in ℝ^{+} \to 0 \leq y$
21	20	ad2antrl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to 0 \leq y$
22		0le1	$⊢ 0 \leq 1$
23		le2sq	$⊢ ((y \in ℝ \land 0 \leq y) \land (1 \in ℝ \land 0 \leq 1)) \to (y \leq 1 \leftrightarrow y^{2} \leq 1^{2})$
24	13 22 23	mpanr12	$⊢ (y \in ℝ \land 0 \leq y) \to (y \leq 1 \leftrightarrow y^{2} \leq 1^{2})$
25	9 21 24	syl2anc	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to (y \leq 1 \leftrightarrow y^{2} \leq 1^{2})$
26	19 25	mpbird	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (y \in ℝ^{+} \land y^{2} \leq A)) \to y \leq 1$
27	26	ex	$⊢ (A \in ℝ^{+} \land A \leq 1) \to ((y \in ℝ^{+} \land y^{2} \leq A) \to y \leq 1)$
28	5 27	biimtrid	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (y \in S \to y \leq 1)$
29	28	ralrimiv	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \forall y \in S y \leq 1$

Metamath Proof Explorer

Theorem 01sqrexlem1

Proof