Metamath Proof Explorer


Theorem sqrlem3

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

Ref Expression
Hypotheses sqrlem1.1 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
sqrlem1.2 𝐵 = sup ( 𝑆 , ℝ , < )
Assertion sqrlem3 ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑦𝑆 𝑦𝑧 ) )

Proof

Step Hyp Ref Expression
1 sqrlem1.1 𝑆 = { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 }
2 sqrlem1.2 𝐵 = sup ( 𝑆 , ℝ , < )
3 ssrab2 { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 } ⊆ ℝ+
4 rpssre + ⊆ ℝ
5 3 4 sstri { 𝑥 ∈ ℝ+ ∣ ( 𝑥 ↑ 2 ) ≤ 𝐴 } ⊆ ℝ
6 1 5 eqsstri 𝑆 ⊆ ℝ
7 6 a1i ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝑆 ⊆ ℝ )
8 1 2 sqrlem2 ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝐴𝑆 )
9 8 ne0d ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → 𝑆 ≠ ∅ )
10 1re 1 ∈ ℝ
11 1 2 sqrlem1 ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ∀ 𝑦𝑆 𝑦 ≤ 1 )
12 brralrspcev ( ( 1 ∈ ℝ ∧ ∀ 𝑦𝑆 𝑦 ≤ 1 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑦𝑆 𝑦𝑧 )
13 10 11 12 sylancr ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑦𝑆 𝑦𝑧 )
14 7 9 13 3jca ( ( 𝐴 ∈ ℝ+𝐴 ≤ 1 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑦𝑆 𝑦𝑧 ) )