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 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ) ) |