Theorem sqrlem2

Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013)

	Ref	Expression
Hypotheses	sqrlem1.1	⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
	sqrlem1.2	⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
Assertion	sqrlem2	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝐴 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		sqrlem1.1	⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2		sqrlem1.2	⊢ 𝐵 = sup ( 𝑆 , ℝ , < )
3		simpl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝐴 ∈ ℝ+ )
4		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
5		rpgt0	⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 )
6		1re	⊢ 1 ∈ ℝ
7		lemul1	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐴 ≤ 1 ↔ ( 𝐴 · 𝐴 ) ≤ ( 1 · 𝐴 ) ) )
8	6 7	mp3an2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐴 ≤ 1 ↔ ( 𝐴 · 𝐴 ) ≤ ( 1 · 𝐴 ) ) )
9	4 4 5 8	syl12anc	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ≤ 1 ↔ ( 𝐴 · 𝐴 ) ≤ ( 1 · 𝐴 ) ) )
10	9	biimpa	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐴 · 𝐴 ) ≤ ( 1 · 𝐴 ) )
11		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
12	11	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝐴 ∈ ℂ )
13		sqval	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
14	13	eqcomd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 𝐴 ) = ( 𝐴 ↑ 2 ) )
15	12 14	syl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐴 · 𝐴 ) = ( 𝐴 ↑ 2 ) )
16	11	mulid2d	⊢ ( 𝐴 ∈ ℝ+ → ( 1 · 𝐴 ) = 𝐴 )
17	16	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 1 · 𝐴 ) = 𝐴 )
18	10 15 17	3brtr3d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( 𝐴 ↑ 2 ) ≤ 𝐴 )
19		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
20	19	breq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ↑ 2 ) ≤ 𝐴 ↔ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) )
21	20 1	elrab2	⊢ ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ ℝ+ ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) )
22	3 18 21	sylanbrc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → 𝐴 ∈ 𝑆 )