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 ${⊢}\left({A}\in {ℝ}^{+}\wedge {A}\le 1\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({x}\le 1\wedge {{x}}^{2}={A}\right)$

Proof

Step Hyp Ref Expression
1 eqid ${⊢}\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\}=\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\}$
2 eqid ${⊢}sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)=sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)$
3 1 2 sqrlem4 ${⊢}\left({A}\in {ℝ}^{+}\wedge {A}\le 1\right)\to \left(sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\in {ℝ}^{+}\wedge sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\le 1\right)$
4 eqid ${⊢}\left\{{z}|\exists {w}\in \left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\}\phantom{\rule{.4em}{0ex}}\exists {x}\in \left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\}\phantom{\rule{.4em}{0ex}}{z}={w}{x}\right\}=\left\{{z}|\exists {w}\in \left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\}\phantom{\rule{.4em}{0ex}}\exists {x}\in \left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\}\phantom{\rule{.4em}{0ex}}{z}={w}{x}\right\}$
5 1 2 4 sqrlem7 ${⊢}\left({A}\in {ℝ}^{+}\wedge {A}\le 1\right)\to {sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)}^{2}={A}$
6 breq1 ${⊢}{x}=sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\to \left({x}\le 1↔sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\le 1\right)$
7 oveq1 ${⊢}{x}=sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\to {{x}}^{2}={sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)}^{2}$
8 7 eqeq1d ${⊢}{x}=sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\to \left({{x}}^{2}={A}↔{sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)}^{2}={A}\right)$
9 6 8 anbi12d ${⊢}{x}=sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\to \left(\left({x}\le 1\wedge {{x}}^{2}={A}\right)↔\left(sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\le 1\wedge {sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)}^{2}={A}\right)\right)$
10 9 rspcev ${⊢}\left(sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\in {ℝ}^{+}\wedge \left(sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\le 1\wedge {sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)}^{2}={A}\right)\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({x}\le 1\wedge {{x}}^{2}={A}\right)$
11 10 anassrs ${⊢}\left(\left(sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\in {ℝ}^{+}\wedge sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)\le 1\right)\wedge {sup\left(\left\{{y}\in {ℝ}^{+}|{{y}}^{2}\le {A}\right\},ℝ,<\right)}^{2}={A}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({x}\le 1\wedge {{x}}^{2}={A}\right)$
12 3 5 11 syl2anc ${⊢}\left({A}\in {ℝ}^{+}\wedge {A}\le 1\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({x}\le 1\wedge {{x}}^{2}={A}\right)$