Metamath Proof Explorer

Theorem 01sqrex

Description: Existence of a square root for reals in the interval ( 0 , 1 ] . (Contributed by Mario Carneiro, 10-Jul-2013)

Ref Expression
Assertion 01sqrex ⊢ A ∈ ℝ + ∧ A ≤ 1 → ∃ x ∈ ℝ + x ≤ 1 ∧ x 2 = A

Proof

Step Hyp Ref Expression
1 eqid ⊢ y ∈ ℝ + | y 2 ≤ A = y ∈ ℝ + | y 2 ≤ A
2 eqid ⊢ sup y ∈ ℝ + | y 2 ≤ A ℝ < = sup y ∈ ℝ + | y 2 ≤ A ℝ <
3 1 2 sqrlem4 ⊢ A ∈ ℝ + ∧ A ≤ 1 → sup y ∈ ℝ + | y 2 ≤ A ℝ < ∈ ℝ + ∧ sup y ∈ ℝ + | y 2 ≤ A ℝ < ≤ 1
4 eqid ⊢ z | ∃ w ∈ y ∈ ℝ + | y 2 ≤ A ∃ x ∈ y ∈ ℝ + | y 2 ≤ A z = w ⁢ x = z | ∃ w ∈ y ∈ ℝ + | y 2 ≤ A ∃ x ∈ y ∈ ℝ + | y 2 ≤ A z = w ⁢ x
5 1 2 4 sqrlem7 ⊢ A ∈ ℝ + ∧ A ≤ 1 → sup y ∈ ℝ + | y 2 ≤ A ℝ < 2 = A
6 breq1 ⊢ x = sup y ∈ ℝ + | y 2 ≤ A ℝ < → x ≤ 1 ↔ sup y ∈ ℝ + | y 2 ≤ A ℝ < ≤ 1
7 oveq1 ⊢ x = sup y ∈ ℝ + | y 2 ≤ A ℝ < → x 2 = sup y ∈ ℝ + | y 2 ≤ A ℝ < 2
8 7 eqeq1d ⊢ x = sup y ∈ ℝ + | y 2 ≤ A ℝ < → x 2 = A ↔ sup y ∈ ℝ + | y 2 ≤ A ℝ < 2 = A
9 6 8 anbi12d ⊢ x = sup y ∈ ℝ + | y 2 ≤ A ℝ < → x ≤ 1 ∧ x 2 = A ↔ sup y ∈ ℝ + | y 2 ≤ A ℝ < ≤ 1 ∧ sup y ∈ ℝ + | y 2 ≤ A ℝ < 2 = A
10 9 rspcev ⊢ sup y ∈ ℝ + | y 2 ≤ A ℝ < ∈ ℝ + ∧ sup y ∈ ℝ + | y 2 ≤ A ℝ < ≤ 1 ∧ sup y ∈ ℝ + | y 2 ≤ A ℝ < 2 = A → ∃ x ∈ ℝ + x ≤ 1 ∧ x 2 = A
11 10 anassrs ⊢ sup y ∈ ℝ + | y 2 ≤ A ℝ < ∈ ℝ + ∧ sup y ∈ ℝ + | y 2 ≤ A ℝ < ≤ 1 ∧ sup y ∈ ℝ + | y 2 ≤ A ℝ < 2 = A → ∃ x ∈ ℝ + x ≤ 1 ∧ x 2 = A
12 3 5 11 syl2anc ⊢ A ∈ ℝ + ∧ A ≤ 1 → ∃ x ∈ ℝ + x ≤ 1 ∧ x 2 = A