01sqrexlem7

Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013) (Proof shortened by AV, 9-Jul-2022)

	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	01sqrexlem7	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B^{2} = 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	01sqrexlem6	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B^{2} \leq A$
5	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)$
6	5	adantr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (S \subseteq ℝ \land S \neq \emptyset \land \exists y \in ℝ \forall z \in S z \leq y)$
7	1 2	01sqrexlem4	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (B \in ℝ^{+} \land B \leq 1)$
8	7	adantr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (B \in ℝ^{+} \land B \leq 1)$
9	8	simpld	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B \in ℝ^{+}$
10		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
11	10	adantr	$⊢ (A \in ℝ^{+} \land A \leq 1) \to A \in ℝ$
12		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
13	12	adantr	$⊢ (B \in ℝ^{+} \land B \leq 1) \to B \in ℝ$
14	7 13	syl	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B \in ℝ$
15	14	resqcld	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B^{2} \in ℝ$
16	11 15	resubcld	$⊢ (A \in ℝ^{+} \land A \leq 1) \to A - B^{2} \in ℝ$
17	16	adantr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to A - B^{2} \in ℝ$
18	15 11	posdifd	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (B^{2} < A \leftrightarrow 0 < A - B^{2})$
19	18	biimpa	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 0 < A - B^{2}$
20	17 19	elrpd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to A - B^{2} \in ℝ^{+}$
21		3rp	$⊢ 3 \in ℝ^{+}$
22		rpdivcl	$⊢ (A - B^{2} \in ℝ^{+} \land 3 \in ℝ^{+}) \to \frac{A - B^{2}}{3} \in ℝ^{+}$
23	20 21 22	sylancl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to \frac{A - B^{2}}{3} \in ℝ^{+}$
24	9 23	rpaddcld	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B + (\frac{A - B^{2}}{3}) \in ℝ^{+}$
25	14	adantr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B \in ℝ$
26	25	recnd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B \in ℂ$
27		3nn	$⊢ 3 \in ℕ$
28		nndivre	$⊢ (A - B^{2} \in ℝ \land 3 \in ℕ) \to \frac{A - B^{2}}{3} \in ℝ$
29	16 27 28	sylancl	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \frac{A - B^{2}}{3} \in ℝ$
30	29	adantr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to \frac{A - B^{2}}{3} \in ℝ$
31	30	recnd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to \frac{A - B^{2}}{3} \in ℂ$
32		binom2	$⊢ (B \in ℂ \land \frac{A - B^{2}}{3} \in ℂ) \to {(B + (\frac{A - B^{2}}{3}))}^{2} = B^{2} + 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2}$
33	26 31 32	syl2anc	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to {(B + (\frac{A - B^{2}}{3}))}^{2} = B^{2} + 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2}$
34	15	adantr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B^{2} \in ℝ$
35	34	recnd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B^{2} \in ℂ$
36		2re	$⊢ 2 \in ℝ$
37	25 30	remulcld	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B (\frac{A - B^{2}}{3}) \in ℝ$
38		remulcl	$⊢ (2 \in ℝ \land B (\frac{A - B^{2}}{3}) \in ℝ) \to 2 B (\frac{A - B^{2}}{3}) \in ℝ$
39	36 37 38	sylancr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B (\frac{A - B^{2}}{3}) \in ℝ$
40	39	recnd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B (\frac{A - B^{2}}{3}) \in ℂ$
41	30	resqcld	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to {(\frac{A - B^{2}}{3})}^{2} \in ℝ$
42	41	recnd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to {(\frac{A - B^{2}}{3})}^{2} \in ℂ$
43	35 40 42	addassd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B^{2} + 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2} = B^{2} + 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2}$
44	33 43	eqtrd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to {(B + (\frac{A - B^{2}}{3}))}^{2} = B^{2} + 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2}$
45		2cn	$⊢ 2 \in ℂ$
46		mulass	$⊢ (2 \in ℂ \land B \in ℂ \land \frac{A - B^{2}}{3} \in ℂ) \to 2 B (\frac{A - B^{2}}{3}) = 2 B (\frac{A - B^{2}}{3})$
47	45 26 31 46	mp3an2i	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B (\frac{A - B^{2}}{3}) = 2 B (\frac{A - B^{2}}{3})$
48	47	eqcomd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B (\frac{A - B^{2}}{3}) = 2 B (\frac{A - B^{2}}{3})$
49	31	sqvald	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to {(\frac{A - B^{2}}{3})}^{2} = (\frac{A - B^{2}}{3}) (\frac{A - B^{2}}{3})$
50	48 49	oveq12d	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2} = 2 B (\frac{A - B^{2}}{3}) + (\frac{A - B^{2}}{3}) (\frac{A - B^{2}}{3})$
51		remulcl	$⊢ (2 \in ℝ \land B \in ℝ) \to 2 B \in ℝ$
52	36 25 51	sylancr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B \in ℝ$
53	52	recnd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B \in ℂ$
54	53 31 31	adddird	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (2 B + (\frac{A - B^{2}}{3})) (\frac{A - B^{2}}{3}) = 2 B (\frac{A - B^{2}}{3}) + (\frac{A - B^{2}}{3}) (\frac{A - B^{2}}{3})$
55	50 54	eqtr4d	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2} = (2 B + (\frac{A - B^{2}}{3})) (\frac{A - B^{2}}{3})$
56	7	simprd	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B \leq 1$
57		1red	$⊢ (A \in ℝ^{+} \land A \leq 1) \to 1 \in ℝ$
58		2rp	$⊢ 2 \in ℝ^{+}$
59	58	a1i	$⊢ (A \in ℝ^{+} \land A \leq 1) \to 2 \in ℝ^{+}$
60	14 57 59	lemul2d	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (B \leq 1 \leftrightarrow 2 B \leq 2 \cdot 1)$
61	56 60	mpbid	$⊢ (A \in ℝ^{+} \land A \leq 1) \to 2 B \leq 2 \cdot 1$
62	61	adantr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B \leq 2 \cdot 1$
63		2t1e2	$⊢ 2 \cdot 1 = 2$
64	62 63	breqtrdi	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B \leq 2$
65	11	adantr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to A \in ℝ$
66		1red	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 1 \in ℝ$
67	25	sqge0d	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 0 \leq B^{2}$
68	65 34	addge01d	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (0 \leq B^{2} \leftrightarrow A \leq A + B^{2})$
69	67 68	mpbid	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to A \leq A + B^{2}$
70	65 34 65	lesubaddd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (A - B^{2} \leq A \leftrightarrow A \leq A + B^{2})$
71	69 70	mpbird	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to A - B^{2} \leq A$
72		simplr	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to A \leq 1$
73	17 65 66 71 72	letrd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to A - B^{2} \leq 1$
74		1le3	$⊢ 1 \leq 3$
75		1re	$⊢ 1 \in ℝ$
76		3re	$⊢ 3 \in ℝ$
77		letr	$⊢ (A - B^{2} \in ℝ \land 1 \in ℝ \land 3 \in ℝ) \to ((A - B^{2} \leq 1 \land 1 \leq 3) \to A - B^{2} \leq 3)$
78	75 76 77	mp3an23	$⊢ A - B^{2} \in ℝ \to ((A - B^{2} \leq 1 \land 1 \leq 3) \to A - B^{2} \leq 3)$
79	17 78	syl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to ((A - B^{2} \leq 1 \land 1 \leq 3) \to A - B^{2} \leq 3)$
80	74 79	mpan2i	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (A - B^{2} \leq 1 \to A - B^{2} \leq 3)$
81	73 80	mpd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to A - B^{2} \leq 3$
82		3t1e3	$⊢ 3 \cdot 1 = 3$
83	81 82	breqtrrdi	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to A - B^{2} \leq 3 \cdot 1$
84		3pos	$⊢ 0 < 3$
85		ledivmul	$⊢ (A - B^{2} \in ℝ \land 1 \in ℝ \land (3 \in ℝ \land 0 < 3)) \to (\frac{A - B^{2}}{3} \leq 1 \leftrightarrow A - B^{2} \leq 3 \cdot 1)$
86	75 85	mp3an2	$⊢ (A - B^{2} \in ℝ \land (3 \in ℝ \land 0 < 3)) \to (\frac{A - B^{2}}{3} \leq 1 \leftrightarrow A - B^{2} \leq 3 \cdot 1)$
87	76 84 86	mpanr12	$⊢ A - B^{2} \in ℝ \to (\frac{A - B^{2}}{3} \leq 1 \leftrightarrow A - B^{2} \leq 3 \cdot 1)$
88	17 87	syl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (\frac{A - B^{2}}{3} \leq 1 \leftrightarrow A - B^{2} \leq 3 \cdot 1)$
89	83 88	mpbird	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to \frac{A - B^{2}}{3} \leq 1$
90		le2add	$⊢ ((2 B \in ℝ \land \frac{A - B^{2}}{3} \in ℝ) \land (2 \in ℝ \land 1 \in ℝ)) \to ((2 B \leq 2 \land \frac{A - B^{2}}{3} \leq 1) \to 2 B + (\frac{A - B^{2}}{3}) \leq 2 + 1)$
91	36 75 90	mpanr12	$⊢ (2 B \in ℝ \land \frac{A - B^{2}}{3} \in ℝ) \to ((2 B \leq 2 \land \frac{A - B^{2}}{3} \leq 1) \to 2 B + (\frac{A - B^{2}}{3}) \leq 2 + 1)$
92	52 30 91	syl2anc	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to ((2 B \leq 2 \land \frac{A - B^{2}}{3} \leq 1) \to 2 B + (\frac{A - B^{2}}{3}) \leq 2 + 1)$
93	64 89 92	mp2and	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B + (\frac{A - B^{2}}{3}) \leq 2 + 1$
94		df-3	$⊢ 3 = 2 + 1$
95	93 94	breqtrrdi	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B + (\frac{A - B^{2}}{3}) \leq 3$
96	52 30	readdcld	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B + (\frac{A - B^{2}}{3}) \in ℝ$
97	76	a1i	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 3 \in ℝ$
98	96 97 23	lemul1d	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (2 B + (\frac{A - B^{2}}{3}) \leq 3 \leftrightarrow (2 B + (\frac{A - B^{2}}{3})) (\frac{A - B^{2}}{3}) \leq 3 (\frac{A - B^{2}}{3}))$
99	95 98	mpbid	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (2 B + (\frac{A - B^{2}}{3})) (\frac{A - B^{2}}{3}) \leq 3 (\frac{A - B^{2}}{3})$
100	17	recnd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to A - B^{2} \in ℂ$
101		3cn	$⊢ 3 \in ℂ$
102		3ne0	$⊢ 3 \neq 0$
103		divcan2	$⊢ (A - B^{2} \in ℂ \land 3 \in ℂ \land 3 \neq 0) \to 3 (\frac{A - B^{2}}{3}) = A - B^{2}$
104	101 102 103	mp3an23	$⊢ A - B^{2} \in ℂ \to 3 (\frac{A - B^{2}}{3}) = A - B^{2}$
105	100 104	syl	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 3 (\frac{A - B^{2}}{3}) = A - B^{2}$
106	99 105	breqtrd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (2 B + (\frac{A - B^{2}}{3})) (\frac{A - B^{2}}{3}) \leq A - B^{2}$
107	55 106	eqbrtrd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2} \leq A - B^{2}$
108	39 41	readdcld	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2} \in ℝ$
109	34 108 65	leaddsub2d	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to (B^{2} + 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2} \leq A \leftrightarrow 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2} \leq A - B^{2})$
110	107 109	mpbird	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B^{2} + 2 B (\frac{A - B^{2}}{3}) + {(\frac{A - B^{2}}{3})}^{2} \leq A$
111	44 110	eqbrtrd	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to {(B + (\frac{A - B^{2}}{3}))}^{2} \leq A$
112		oveq1	$⊢ y = B + (\frac{A - B^{2}}{3}) \to y^{2} = {(B + (\frac{A - B^{2}}{3}))}^{2}$
113	112	breq1d	$⊢ y = B + (\frac{A - B^{2}}{3}) \to (y^{2} \leq A \leftrightarrow {(B + (\frac{A - B^{2}}{3}))}^{2} \leq A)$
114		oveq1	$⊢ x = y \to x^{2} = y^{2}$
115	114	breq1d	$⊢ x = y \to (x^{2} \leq A \leftrightarrow y^{2} \leq A)$
116	115	cbvrabv	$⊢ \{x \in ℝ^{+} \| x^{2} \leq A\} = \{y \in ℝ^{+} \| y^{2} \leq A\}$
117	1 116	eqtri	$⊢ S = \{y \in ℝ^{+} \| y^{2} \leq A\}$
118	113 117	elrab2	$⊢ B + (\frac{A - B^{2}}{3}) \in S \leftrightarrow (B + (\frac{A - B^{2}}{3}) \in ℝ^{+} \land {(B + (\frac{A - B^{2}}{3}))}^{2} \leq A)$
119	24 111 118	sylanbrc	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B + (\frac{A - B^{2}}{3}) \in S$
120		suprub	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists y \in ℝ \forall z \in S z \leq y) \land B + (\frac{A - B^{2}}{3}) \in S) \to B + (\frac{A - B^{2}}{3}) \leq sup (S ℝ <)$
121	120 2	breqtrrdi	$⊢ ((S \subseteq ℝ \land S \neq \emptyset \land \exists y \in ℝ \forall z \in S z \leq y) \land B + (\frac{A - B^{2}}{3}) \in S) \to B + (\frac{A - B^{2}}{3}) \leq B$
122	6 119 121	syl2anc	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to B + (\frac{A - B^{2}}{3}) \leq B$
123	23	rpgt0d	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to 0 < \frac{A - B^{2}}{3}$
124	29 14	ltaddposd	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (0 < \frac{A - B^{2}}{3} \leftrightarrow B < B + (\frac{A - B^{2}}{3}))$
125	14 29	readdcld	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B + (\frac{A - B^{2}}{3}) \in ℝ$
126	14 125	ltnled	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (B < B + (\frac{A - B^{2}}{3}) \leftrightarrow \neg B + (\frac{A - B^{2}}{3}) \leq B)$
127	124 126	bitrd	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (0 < \frac{A - B^{2}}{3} \leftrightarrow \neg B + (\frac{A - B^{2}}{3}) \leq B)$
128	127	biimpa	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land 0 < \frac{A - B^{2}}{3}) \to \neg B + (\frac{A - B^{2}}{3}) \leq B$
129	123 128	syldan	$⊢ ((A \in ℝ^{+} \land A \leq 1) \land B^{2} < A) \to \neg B + (\frac{A - B^{2}}{3}) \leq B$
130	122 129	pm2.65da	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \neg B^{2} < A$
131	15 11	eqleltd	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (B^{2} = A \leftrightarrow (B^{2} \leq A \land \neg B^{2} < A))$
132	4 130 131	mpbir2and	$⊢ (A \in ℝ^{+} \land A \leq 1) \to B^{2} = A$

Metamath Proof Explorer

Theorem 01sqrexlem7

Proof