Metamath Proof Explorer

Theorem sqrlem4

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

Ref Expression
Hypotheses sqrlem1.1 ⊢ S = x ∈ ℝ + | x 2 ≤ A
sqrlem1.2 ⊢ B = sup S ℝ <
Assertion sqrlem4 ⊢ A ∈ ℝ + ∧ A ≤ 1 → B ∈ ℝ + ∧ B ≤ 1

Proof

Step Hyp Ref Expression
1 sqrlem1.1 ⊢ S = x ∈ ℝ + | x 2 ≤ A
2 sqrlem1.2 ⊢ B = sup S ℝ <
3 1 2 sqrlem3 ⊢ A ∈ ℝ + ∧ A ≤ 1 → S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ S z ≤ y
4 suprcl ⊢ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ S z ≤ y → sup S ℝ < ∈ ℝ
5 3 4 syl ⊢ A ∈ ℝ + ∧ A ≤ 1 → sup S ℝ < ∈ ℝ
6 2 5 eqeltrid ⊢ A ∈ ℝ + ∧ A ≤ 1 → B ∈ ℝ
7 rpgt0 ⊢ A ∈ ℝ + → 0 < A
8 7 adantr ⊢ A ∈ ℝ + ∧ A ≤ 1 → 0 < A
9 1 2 sqrlem2 ⊢ A ∈ ℝ + ∧ A ≤ 1 → A ∈ S
10 suprub ⊢ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ S z ≤ y ∧ A ∈ S → A ≤ sup S ℝ <
11 3 9 10 syl2anc ⊢ A ∈ ℝ + ∧ A ≤ 1 → A ≤ sup S ℝ <
12 11 2 breqtrrdi ⊢ A ∈ ℝ + ∧ A ≤ 1 → A ≤ B
13 0re ⊢ 0 ∈ ℝ
14 rpre ⊢ A ∈ ℝ + → A ∈ ℝ
15 ltletr ⊢ 0 ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ∧ A ≤ B → 0 < B
16 13 14 6 15 mp3an2ani ⊢ A ∈ ℝ + ∧ A ≤ 1 → 0 < A ∧ A ≤ B → 0 < B
17 8 12 16 mp2and ⊢ A ∈ ℝ + ∧ A ≤ 1 → 0 < B
18 6 17 elrpd ⊢ A ∈ ℝ + ∧ A ≤ 1 → B ∈ ℝ +
19 1 2 sqrlem1 ⊢ A ∈ ℝ + ∧ A ≤ 1 → ∀ z ∈ S z ≤ 1
20 1re ⊢ 1 ∈ ℝ
21 suprleub ⊢ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ S z ≤ y ∧ 1 ∈ ℝ → sup S ℝ < ≤ 1 ↔ ∀ z ∈ S z ≤ 1
22 3 20 21 sylancl ⊢ A ∈ ℝ + ∧ A ≤ 1 → sup S ℝ < ≤ 1 ↔ ∀ z ∈ S z ≤ 1
23 19 22 mpbird ⊢ A ∈ ℝ + ∧ A ≤ 1 → sup S ℝ < ≤ 1
24 2 23 eqbrtrid ⊢ A ∈ ℝ + ∧ A ≤ 1 → B ≤ 1
25 18 24 jca ⊢ A ∈ ℝ + ∧ A ≤ 1 → B ∈ ℝ + ∧ B ≤ 1