01sqrexlem4

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

Proof

Step	Hyp	Ref	Expression
1		01sqrexlem1.1	$⊢ S = \{x \in ℝ^{+} \| x^{2} \leq A\}$
2		01sqrexlem1.2	$⊢ B = sup (S ℝ <)$
3	1 2	01sqrexlem3	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (S \subseteq ℝ \land S \neq \emptyset \land \exists y \in ℝ \forall z \in S z \leq y)$
4		suprcl	$⊢ (S \subseteq ℝ \land S \neq \emptyset \land \exists y \in ℝ \forall z \in S z \leq y) \to sup (S ℝ <) \in ℝ$
5	3 4	syl	$⊢ (A \in ℝ^{+} \land A \leq 1) \to sup (S ℝ <) \in ℝ$
6	2 5	eqeltrid	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B \in ℝ$
7		rpgt0	$⊢ A \in ℝ^{+} \to 0 < A$
8	7	adantr	$⊢ (A \in ℝ^{+} \land A \leq 1) \to 0 < A$
9	1 2	01sqrexlem2	$⊢ (A \in ℝ^{+} \land A \leq 1) \to A \in S$
10		suprub	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists y \in ℝ \forall z \in S z \leq y) \land A \in S) \to A \leq sup (S ℝ <)$
11	3 9 10	syl2anc	$⊢ (A \in ℝ^{+} \land A \leq 1) \to A \leq sup (S ℝ <)$
12	11 2	breqtrrdi	$⊢ (A \in ℝ^{+} \land A \leq 1) \to A \leq B$
13		0re	$⊢ 0 \in ℝ$
14		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
15		ltletr	$⊢ (0 \in ℝ \land A \in ℝ \land B \in ℝ) \to ((0 < A \land A \leq B) \to 0 < B)$
16	13 14 6 15	mp3an2ani	$⊢ (A \in ℝ^{+} \land A \leq 1) \to ((0 < A \land A \leq B) \to 0 < B)$
17	8 12 16	mp2and	$⊢ (A \in ℝ^{+} \land A \leq 1) \to 0 < B$
18	6 17	elrpd	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B \in ℝ^{+}$
19	1 2	01sqrexlem1	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \forall z \in S z \leq 1$
20		1re	$⊢ 1 \in ℝ$
21		suprleub	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists y \in ℝ \forall z \in S z \leq y) \land 1 \in ℝ) \to (sup (S ℝ <) \leq 1 \leftrightarrow \forall z \in S z \leq 1)$
22	3 20 21	sylancl	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (sup (S ℝ <) \leq 1 \leftrightarrow \forall z \in S z \leq 1)$
23	19 22	mpbird	$⊢ (A \in ℝ^{+} \land A \leq 1) \to sup (S ℝ <) \leq 1$
24	2 23	eqbrtrid	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B \leq 1$
25	18 24	jca	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (B \in ℝ^{+} \land B \leq 1)$

Metamath Proof Explorer

Theorem 01sqrexlem4

Proof