This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 01sqrexlem2

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

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

Proof

Step Hyp Ref Expression
1 01sqrexlem1.1 ⊢ 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2 01sqrexlem1.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 mullidd ⊢ ( 𝐴 ∈ ℝ+ → ( 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 ) → 𝐴 ∈ 𝑆 )