01sqrexlem6

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

Proof

Step	Hyp	Ref	Expression
1		01sqrexlem1.1	$⊢ S = \{x \in ℝ^{+} \| x^{2} \leq A\}$
2		01sqrexlem1.2	$⊢ B = sup (S ℝ <)$
3		01sqrexlem5.3	$⊢ T = \{y \| \exists a \in S \exists b \in S y = a b\}$
4	1 2 3	01sqrexlem5	$⊢ (A \in ℝ^{+} \land A \leq 1) \to ((T \subseteq ℝ \land T \neq \emptyset \land \exists v \in ℝ \forall u \in T u \leq v) \land B^{2} = sup (T ℝ <))$
5	4	simprd	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B^{2} = sup (T ℝ <)$
6		vex	$⊢ v \in V$
7		eqeq1	$⊢ y = v \to (y = a b \leftrightarrow v = a b)$
8	7	2rexbidv	$⊢ y = v \to (\exists a \in S \exists b \in S y = a b \leftrightarrow \exists a \in S \exists b \in S v = a b)$
9	6 8 3	elab2	$⊢ v \in T \leftrightarrow \exists a \in S \exists b \in S v = a b$
10		oveq1	$⊢ x = a \to x^{2} = a^{2}$
11	10	breq1d	$⊢ x = a \to (x^{2} \leq A \leftrightarrow a^{2} \leq A)$
12	11 1	elrab2	$⊢ a \in S \leftrightarrow (a \in ℝ^{+} \land a^{2} \leq A)$
13	12	simplbi	$⊢ a \in S \to a \in ℝ^{+}$
14		oveq1	$⊢ x = b \to x^{2} = b^{2}$
15	14	breq1d	$⊢ x = b \to (x^{2} \leq A \leftrightarrow b^{2} \leq A)$
16	15 1	elrab2	$⊢ b \in S \leftrightarrow (b \in ℝ^{+} \land b^{2} \leq A)$
17	16	simplbi	$⊢ b \in S \to b \in ℝ^{+}$
18		rpre	$⊢ a \in ℝ^{+} \to a \in ℝ$
19	18	adantr	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to a \in ℝ$
20		rpre	$⊢ b \in ℝ^{+} \to b \in ℝ$
21	20	adantl	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to b \in ℝ$
22		rpgt0	$⊢ b \in ℝ^{+} \to 0 < b$
23	22	adantl	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to 0 < b$
24		lemul1	$⊢ (a \in ℝ \land b \in ℝ \land (b \in ℝ \land 0 < b)) \to (a \leq b \leftrightarrow a b \leq b b)$
25	19 21 21 23 24	syl112anc	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to (a \leq b \leftrightarrow a b \leq b b)$
26	13 17 25	syl2an	$⊢ (a \in S \land b \in S) \to (a \leq b \leftrightarrow a b \leq b b)$
27	17	rpcnd	$⊢ b \in S \to b \in ℂ$
28	27	sqvald	$⊢ b \in S \to b^{2} = b b$
29	28	breq2d	$⊢ b \in S \to (a b \leq b^{2} \leftrightarrow a b \leq b b)$
30	29	adantl	$⊢ (a \in S \land b \in S) \to (a b \leq b^{2} \leftrightarrow a b \leq b b)$
31	26 30	bitr4d	$⊢ (a \in S \land b \in S) \to (a \leq b \leftrightarrow a b \leq b^{2})$
32	31	adantl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to (a \leq b \leftrightarrow a b \leq b^{2})$
33	16	simprbi	$⊢ b \in S \to b^{2} \leq A$
34	33	ad2antll	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to b^{2} \leq A$
35	13	rpred	$⊢ a \in S \to a \in ℝ$
36	17	rpred	$⊢ b \in S \to b \in ℝ$
37		remulcl	$⊢ (a \in ℝ \land b \in ℝ) \to a b \in ℝ$
38	35 36 37	syl2an	$⊢ (a \in S \land b \in S) \to a b \in ℝ$
39	38	adantl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to a b \in ℝ$
40	36	resqcld	$⊢ b \in S \to b^{2} \in ℝ$
41	40	ad2antll	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to b^{2} \in ℝ$
42		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
43	42	ad2antrr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to A \in ℝ$
44		letr	$⊢ (a b \in ℝ \land b^{2} \in ℝ \land A \in ℝ) \to ((a b \leq b^{2} \land b^{2} \leq A) \to a b \leq A)$
45	39 41 43 44	syl3anc	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to ((a b \leq b^{2} \land b^{2} \leq A) \to a b \leq A)$
46	34 45	mpan2d	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to (a b \leq b^{2} \to a b \leq A)$
47	32 46	sylbid	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to (a \leq b \to a b \leq A)$
48		rpgt0	$⊢ a \in ℝ^{+} \to 0 < a$
49	48	adantr	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to 0 < a$
50		lemul2	$⊢ (b \in ℝ \land a \in ℝ \land (a \in ℝ \land 0 < a)) \to (b \leq a \leftrightarrow a b \leq a a)$
51	21 19 19 49 50	syl112anc	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to (b \leq a \leftrightarrow a b \leq a a)$
52	13 17 51	syl2an	$⊢ (a \in S \land b \in S) \to (b \leq a \leftrightarrow a b \leq a a)$
53	13	rpcnd	$⊢ a \in S \to a \in ℂ$
54	53	sqvald	$⊢ a \in S \to a^{2} = a a$
55	54	breq2d	$⊢ a \in S \to (a b \leq a^{2} \leftrightarrow a b \leq a a)$
56	55	adantr	$⊢ (a \in S \land b \in S) \to (a b \leq a^{2} \leftrightarrow a b \leq a a)$
57	52 56	bitr4d	$⊢ (a \in S \land b \in S) \to (b \leq a \leftrightarrow a b \leq a^{2})$
58	57	adantl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to (b \leq a \leftrightarrow a b \leq a^{2})$
59	12	simprbi	$⊢ a \in S \to a^{2} \leq A$
60	59	ad2antrl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to a^{2} \leq A$
61	35	resqcld	$⊢ a \in S \to a^{2} \in ℝ$
62	61	ad2antrl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to a^{2} \in ℝ$
63		letr	$⊢ (a b \in ℝ \land a^{2} \in ℝ \land A \in ℝ) \to ((a b \leq a^{2} \land a^{2} \leq A) \to a b \leq A)$
64	39 62 43 63	syl3anc	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to ((a b \leq a^{2} \land a^{2} \leq A) \to a b \leq A)$
65	60 64	mpan2d	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to (a b \leq a^{2} \to a b \leq A)$
66	58 65	sylbid	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to (b \leq a \to a b \leq A)$
67	1 2	01sqrexlem3	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (S \subseteq ℝ \land S \neq \emptyset \land \exists y \in ℝ \forall v \in S v \leq y)$
68	67	simp1d	$⊢ (A \in ℝ^{+} \land A \leq 1) \to S \subseteq ℝ$
69	68	sseld	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (a \in S \to a \in ℝ)$
70	68	sseld	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (b \in S \to b \in ℝ)$
71	69 70	anim12d	$⊢ (A \in ℝ^{+} \land A \leq 1) \to ((a \in S \land b \in S) \to (a \in ℝ \land b \in ℝ))$
72	71	imp	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to (a \in ℝ \land b \in ℝ)$
73		letric	$⊢ (a \in ℝ \land b \in ℝ) \to (a \leq b \lor b \leq a)$
74	72 73	syl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to (a \leq b \lor b \leq a)$
75	47 66 74	mpjaod	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land (a \in S \land b \in S)) \to a b \leq A$
76	75	ex	$⊢ (A \in ℝ^{+} \land A \leq 1) \to ((a \in S \land b \in S) \to a b \leq A)$
77		breq1	$⊢ v = a b \to (v \leq A \leftrightarrow a b \leq A)$
78	77	biimprcd	$⊢ a b \leq A \to (v = a b \to v \leq A)$
79	76 78	syl6	$⊢ (A \in ℝ^{+} \land A \leq 1) \to ((a \in S \land b \in S) \to (v = a b \to v \leq A))$
80	79	rexlimdvv	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (\exists a \in S \exists b \in S v = a b \to v \leq A)$
81	9 80	biimtrid	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (v \in T \to v \leq A)$
82	81	ralrimiv	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \forall v \in T v \leq A$
83	4	simpld	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (T \subseteq ℝ \land T \neq \emptyset \land \exists v \in ℝ \forall u \in T u \leq v)$
84	42	adantr	$⊢ (A \in ℝ^{+} \land A \leq 1) \to A \in ℝ$
85		suprleub	$⊢ ((T \subseteq ℝ \land T \neq \emptyset \land \exists v \in ℝ \forall u \in T u \leq v) \land A \in ℝ) \to (sup (T ℝ <) \leq A \leftrightarrow \forall v \in T v \leq A)$
86	83 84 85	syl2anc	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (sup (T ℝ <) \leq A \leftrightarrow \forall v \in T v \leq A)$
87	82 86	mpbird	$⊢ (A \in ℝ^{+} \land A \leq 1) \to sup (T ℝ <) \leq A$
88	5 87	eqbrtrd	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B^{2} \leq A$

Metamath Proof Explorer

Theorem 01sqrexlem6

Proof