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	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 ≤ 1 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } = { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 }
2		eqid	⊢ sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) = sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < )
3	1 2	sqrlem4	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ∈ ℝ+ ∧ sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ≤ 1 ) )
4		eqid	⊢ { 𝑧 ∣ ∃ 𝑤 ∈ { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } ∃ 𝑥 ∈ { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } 𝑧 = ( 𝑤 · 𝑥 ) } = { 𝑧 ∣ ∃ 𝑤 ∈ { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } ∃ 𝑥 ∈ { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } 𝑧 = ( 𝑤 · 𝑥 ) }
5	1 2 4	sqrlem7	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ↑ 2 ) = 𝐴 )
6		breq1	⊢ ( 𝑥 = sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) → ( 𝑥 ≤ 1 ↔ sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ≤ 1 ) )
7		oveq1	⊢ ( 𝑥 = sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) → ( 𝑥 ↑ 2 ) = ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ↑ 2 ) )
8	7	eqeq1d	⊢ ( 𝑥 = sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) → ( ( 𝑥 ↑ 2 ) = 𝐴 ↔ ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ↑ 2 ) = 𝐴 ) )
9	6 8	anbi12d	⊢ ( 𝑥 = sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) → ( ( 𝑥 ≤ 1 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) ↔ ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ≤ 1 ∧ ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ↑ 2 ) = 𝐴 ) ) )
10	9	rspcev	⊢ ( ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ∈ ℝ+ ∧ ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ≤ 1 ∧ ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ↑ 2 ) = 𝐴 ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 ≤ 1 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) )
11	10	anassrs	⊢ ( ( ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ∈ ℝ+ ∧ sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ≤ 1 ) ∧ ( sup ( { 𝑦 ∈ ℝ+ ∣ ( 𝑦 ↑ 2 ) ≤ 𝐴 } , ℝ , < ) ↑ 2 ) = 𝐴 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 ≤ 1 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) )
12	3 5 11	syl2anc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 ≤ 1 ∧ ( 𝑥 ↑ 2 ) = 𝐴 ) )