01sqrexlem7

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

	Ref	Expression
Hypotheses	01sqrexlem1.1	⊢ 𝑆 = { 𝑥 ∈ ℝ⁺ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
	01sqrexlem1.2	⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
	01sqrexlem5.3	⊢ 𝑇 = { 𝑦 ∣ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
Assertion	01sqrexlem7	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		01sqrexlem1.1	⊢ 𝑆 = { 𝑥 ∈ ℝ⁺ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2		01sqrexlem1.2	⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
3		01sqrexlem5.3	⊢ 𝑇 = { 𝑦 ∣ ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑦 = ( 𝑎 · 𝑏 ) }
4	1 2 3	01sqrexlem6	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) ≤ 𝐴 )
5	1 2	01sqrexlem3	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑦 ) )
6	5	adantr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑦 ) )
7	1 2	01sqrexlem4	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ∈ ℝ⁺ ∧ 𝐵 ≤ 1 ) )
8	7	adantr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 ∈ ℝ⁺ ∧ 𝐵 ≤ 1 ) )
9	8	simpld	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐵 ∈ ℝ⁺ )
10		rpre	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ∈ ℝ )
11	10	adantr	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → 𝐴 ∈ ℝ )
12		rpre	⊢ ( 𝐵 ∈ ℝ⁺ → 𝐵 ∈ ℝ )
13	12	adantr	⊢ ( ( 𝐵 ∈ ℝ⁺ ∧ 𝐵 ≤ 1 ) → 𝐵 ∈ ℝ )
14	7 13	syl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → 𝐵 ∈ ℝ )
15	14	resqcld	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
16	11 15	resubcld	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ )
17	16	adantr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ )
18	15 11	posdifd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( ( 𝐵 ↑ 2 ) < 𝐴 ↔ 0 < ( 𝐴 − ( 𝐵 ↑ 2 ) ) ) )
19	18	biimpa	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 0 < ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
20	17 19	elrpd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ⁺ )
21		3rp	⊢ 3 ∈ ℝ⁺
22		rpdivcl	⊢ ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ⁺ ∧ 3 ∈ ℝ⁺ ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ⁺ )
23	20 21 22	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ⁺ )
24	9 23	rpaddcld	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ⁺ )
25	14	adantr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐵 ∈ ℝ )
26	25	recnd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐵 ∈ ℂ )
27		3nn	⊢ 3 ∈ ℕ
28		nndivre	⊢ ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ )
29	16 27 28	sylancl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ )
30	29	adantr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ )
31	30	recnd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℂ )
32		binom2	⊢ ( ( 𝐵 ∈ ℂ ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℂ ) → ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) = ( ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) )
33	26 31 32	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) = ( ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) )
34	15	adantr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
35	34	recnd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
36		2re	⊢ 2 ∈ ℝ
37	25 30	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ )
38		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ ) → ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ∈ ℝ )
39	36 37 38	sylancr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ∈ ℝ )
40	39	recnd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ∈ ℂ )
41	30	resqcld	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ∈ ℝ )
42	41	recnd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ∈ ℂ )
43	35 40 42	addassd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐵 ↑ 2 ) + ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ) )
44	33 43	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) + ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ) )
45		2cn	⊢ 2 ∈ ℂ
46		mulass	⊢ ( ( 2 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℂ ) → ( ( 2 · 𝐵 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
47	45 26 31 46	mp3an2i	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · 𝐵 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
48	47	eqcomd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) = ( ( 2 · 𝐵 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) )
49	31	sqvald	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) = ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) )
50	48 49	oveq12d	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) = ( ( ( 2 · 𝐵 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
51		remulcl	⊢ ( ( 2 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2 · 𝐵 ) ∈ ℝ )
52	36 25 51	sylancr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · 𝐵 ) ∈ ℝ )
53	52	recnd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · 𝐵 ) ∈ ℂ )
54	53 31 31	adddird	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( ( ( 2 · 𝐵 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
55	50 54	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) = ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) )
56	7	simprd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → 𝐵 ≤ 1 )
57		1red	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → 1 ∈ ℝ )
58		2rp	⊢ 2 ∈ ℝ⁺
59	58	a1i	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → 2 ∈ ℝ⁺ )
60	14 57 59	lemul2d	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ≤ 1 ↔ ( 2 · 𝐵 ) ≤ ( 2 · 1 ) ) )
61	56 60	mpbid	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 2 · 𝐵 ) ≤ ( 2 · 1 ) )
62	61	adantr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · 𝐵 ) ≤ ( 2 · 1 ) )
63		2t1e2	⊢ ( 2 · 1 ) = 2
64	62 63	breqtrdi	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 2 · 𝐵 ) ≤ 2 )
65	11	adantr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐴 ∈ ℝ )
66		1red	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 1 ∈ ℝ )
67	25	sqge0d	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 0 ≤ ( 𝐵 ↑ 2 ) )
68	65 34	addge01d	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 0 ≤ ( 𝐵 ↑ 2 ) ↔ 𝐴 ≤ ( 𝐴 + ( 𝐵 ↑ 2 ) ) ) )
69	67 68	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐴 ≤ ( 𝐴 + ( 𝐵 ↑ 2 ) ) )
70	65 34 65	lesubaddd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 𝐴 ↔ 𝐴 ≤ ( 𝐴 + ( 𝐵 ↑ 2 ) ) ) )
71	69 70	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 𝐴 )
72		simplr	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 𝐴 ≤ 1 )
73	17 65 66 71 72	letrd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 1 )
74		1le3	⊢ 1 ≤ 3
75		1re	⊢ 1 ∈ ℝ
76		3re	⊢ 3 ∈ ℝ
77		letr	⊢ ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 3 ∈ ℝ ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 1 ∧ 1 ≤ 3 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 3 ) )
78	75 76 77	mp3an23	⊢ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 1 ∧ 1 ≤ 3 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 3 ) )
79	17 78	syl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 1 ∧ 1 ≤ 3 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 3 ) )
80	74 79	mpan2i	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 1 → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 3 ) )
81	73 80	mpd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ 3 )
82		3t1e3	⊢ ( 3 · 1 ) = 3
83	81 82	breqtrrdi	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ ( 3 · 1 ) )
84		3pos	⊢ 0 < 3
85		ledivmul	⊢ ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ↔ ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ ( 3 · 1 ) ) )
86	75 85	mp3an2	⊢ ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ↔ ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ ( 3 · 1 ) ) )
87	76 84 86	mpanr12	⊢ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℝ → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ↔ ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ ( 3 · 1 ) ) )
88	17 87	syl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ↔ ( 𝐴 − ( 𝐵 ↑ 2 ) ) ≤ ( 3 · 1 ) ) )
89	83 88	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 )
90		le2add	⊢ ( ( ( ( 2 · 𝐵 ) ∈ ℝ ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ ) ∧ ( 2 ∈ ℝ ∧ 1 ∈ ℝ ) ) → ( ( ( 2 · 𝐵 ) ≤ 2 ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 2 + 1 ) ) )
91	36 75 90	mpanr12	⊢ ( ( ( 2 · 𝐵 ) ∈ ℝ ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ∈ ℝ ) → ( ( ( 2 · 𝐵 ) ≤ 2 ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 2 + 1 ) ) )
92	52 30 91	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 2 · 𝐵 ) ≤ 2 ∧ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ≤ 1 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 2 + 1 ) ) )
93	64 89 92	mp2and	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 2 + 1 ) )
94		df-3	⊢ 3 = ( 2 + 1 )
95	93 94	breqtrrdi	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 3 )
96	52 30	readdcld	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ )
97	76	a1i	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 3 ∈ ℝ )
98	96 97 23	lemul1d	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 3 ↔ ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 3 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
99	95 98	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 3 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) )
100	17	recnd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℂ )
101		3cn	⊢ 3 ∈ ℂ
102		3ne0	⊢ 3 ≠ 0
103		divcan2	⊢ ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( 3 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
104	101 102 103	mp3an23	⊢ ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) ∈ ℂ → ( 3 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
105	100 104	syl	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 3 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) = ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
106	99 105	breqtrd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 2 · 𝐵 ) + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
107	55 106	eqbrtrd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ≤ ( 𝐴 − ( 𝐵 ↑ 2 ) ) )
108	39 41	readdcld	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ∈ ℝ )
109	34 108 65	leaddsub2d	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( ( 𝐵 ↑ 2 ) + ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ) ≤ 𝐴 ↔ ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ≤ ( 𝐴 − ( 𝐵 ↑ 2 ) ) ) )
110	107 109	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐵 ↑ 2 ) + ( ( 2 · ( 𝐵 · ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) + ( ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↑ 2 ) ) ) ≤ 𝐴 )
111	44 110	eqbrtrd	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) ≤ 𝐴 )
112		oveq1	⊢ ( 𝑦 = ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) → ( 𝑦 ↑ 2 ) = ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) )
113	112	breq1d	⊢ ( 𝑦 = ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) → ( ( 𝑦 ↑ 2 ) ≤ 𝐴 ↔ ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) ≤ 𝐴 ) )
114		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
115	114	breq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 2 ) ≤ 𝐴 ↔ ( 𝑦 ↑ 2 ) ≤ 𝐴 ) )
116	115	cbvrabv	⊢ { 𝑥 ∈ ℝ⁺ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 } = { 𝑦 ∈ ℝ⁺ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 }
117	1 116	eqtri	⊢ 𝑆 = { 𝑦 ∈ ℝ⁺ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 }
118	113 117	elrab2	⊢ ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ 𝑆 ↔ ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ⁺ ∧ ( ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↑ 2 ) ≤ 𝐴 ) )
119	24 111 118	sylanbrc	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ 𝑆 )
120		suprub	⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑦 ) ∧ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ 𝑆 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ sup ( 𝑆 , ℝ , < ) )
121	120 2	breqtrrdi	⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑦 ) ∧ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ 𝑆 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 )
122	6 119 121	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 )
123	23	rpgt0d	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → 0 < ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) )
124	29 14	ltaddposd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 0 < ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↔ 𝐵 < ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ) )
125	14 29	readdcld	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ∈ ℝ )
126	14 125	ltnled	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 𝐵 < ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ↔ ¬ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 ) )
127	124 126	bitrd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 0 < ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ↔ ¬ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 ) )
128	127	biimpa	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ 0 < ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) → ¬ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 )
129	123 128	syldan	⊢ ( ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) ∧ ( 𝐵 ↑ 2 ) < 𝐴 ) → ¬ ( 𝐵 + ( ( 𝐴 − ( 𝐵 ↑ 2 ) ) / 3 ) ) ≤ 𝐵 )
130	122 129	pm2.65da	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ¬ ( 𝐵 ↑ 2 ) < 𝐴 )
131	15 11	eqleltd	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( ( 𝐵 ↑ 2 ) = 𝐴 ↔ ( ( 𝐵 ↑ 2 ) ≤ 𝐴 ∧ ¬ ( 𝐵 ↑ 2 ) < 𝐴 ) ) )
132	4 130 131	mpbir2and	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐴 ≤ 1 ) → ( 𝐵 ↑ 2 ) = 𝐴 )

Metamath Proof Explorer

Theorem 01sqrexlem7

Proof