Existence of square roots of nonnegative reals

Existence of square roots of nonnegative reals
Tag	`068BZBXE0C`
URI	`m2://068BZBXE0C`
Kind	statement, theorem
Writing	W0 stub
MSC	26A09
Status	This copy of the site has no build data. Run `m2 status 068BZBXE0C`.
Uses	Completeness axiom

Markdown · JSON · Edit

Statement

Let $x$ be a real number with $x \ge 0$ . Then there is exactly one real number $y$ with $y \ge 0$ and $y^2 = x$ .

Remarks

Existence uses the completeness axiom: take $y = \sup \{t \ge 0 : t^2 \le x\}$ and show that $y^2 < x$ and $y^2 > x$ are both impossible. Uniqueness: if $y, z \ge 0$ and $y^2 = z^2$ , then $(y - z)(y + z) = 0$ , thus $y = z$ . In $\mathbb{Q}$ the existence fails: $2$ has no rational square root, by the irrationality of the square root of 2.

Explanations

L1 human

Every nonnegative real number is the area of exactly one square, and the side of that square is the square root. This needs the real numbers: among the fractions, no square has area exactly $2$ .

What this node needs for W1

an inventory row: the row of the inventory that the node accounts for (0 of 1)

The writing levels say how complete the text of a node is. They do not measure its truth.

What this needs

To read this node, read these 5 nodes in this order. The foundations come first, and the list ends with this node.

Each node uses the nodes above it. The colour of the bar on a box shows the evidence level, and the box also gives it as text. The list below has the same nodes.

no evidence level

Real numbers object
Set bounded above definition
Supremum definition
Completeness axiom statement
Existence of square roots of nonnegative reals statement

What depends on this

88 nodes use this node, directly or through other nodes.

Modulus of the conjugate 00KRCVE7CK
Residue at a simple pole 01991NCP7H
Derivative of the complex exponential 019H1Z6419
Cauchy's integral theorem 01MPZXYVYF
Arguments add under multiplication 01W6RKJP01
Holomorphic functions on a disc have primitives 02AC7JR6G6
Casorati–Weierstrass theorem 02HHNPC8ED
Chebyshev's inequality 02HZ1BK3MW
Riemann mapping theorem 02WHMEG5ZR
The real part of a holomorphic function is harmonic 031BG625Y3
Residue theorem 032HKYS329
Formula for the modulus 034FGCEYX4
Open mapping theorem 03YEM7JEDN
Entire function 0419794R0T
Uniform limits of holomorphic functions are holomorphic 0431RN0R1N
Maximum modulus principle 048F2P90WR
Correlation coefficient 04CTY6XYWN
Density of the irrationals 04J6G4H78J
The nth roots of unity 057BH3JC9S
Order of a zero 064N002TX4
Branch cut 06JYC06JHY
Existence of Laurent expansions on an annulus 06WHRARZKY
Holomorphic functions are analytic 0826SGV3R0
Picard's great theorem 08QA8QTM71
Domain in the complex plane 097KNJFJ7V
Power series of the complex logarithm 09BG0Y7SZD
Annulus 0AJ0YVK743
Weak law of large numbers 0BFDHF2H7N
Goursat's theorem 0BRG85WXYC
Polar form 0BRXFNQ5JV
Riemann's theorem on removable singularities 0BSQDZWF34
Kurtosis 0CBQVVNBMP
Harmonic conjugate 0CC56MJ4FG
Zero of a holomorphic function 0CEGEASY49
exp(2 pi i/n) is a primitive root of unity 0CF0XGYHNJ
Complex differentiability 0D1C9Y1EXA
Rouché's theorem 0D430QR02W
Strong law of large numbers 0DFWHQ839T
Holomorphic function 0DG0Z72CQD
Cauchy's integral formula 0DG10TVYPN
Irrationality of the square root of 2 0DZGSDHD92
Number of nth roots of unity 0E021GF2B8
Liouville's theorem 0EHKVRF4J6
68–95–99.7 rule 0EYQ03XCR3
Cauchy's integral formula for derivatives 0F0H5P5DED
Inverse of a complex number 0FQRAV5SKH
The complex exponential is entire 0G2YJN0H5S
Skewness 0GQ3H7VW3V
Modulus is multiplicative 0HYNZE940T
Mean value property 0HYPR64JM2
Residue 0JFGKKWWFK
Cauchy's estimates 0JJRENWMP6
Fundamental theorem of algebra 0JP0W07Y9A
Isolated zeros theorem 0K83KEJ43P
Modulus of a complex number 0KW2X0TFBX
Quadratic formula 0KYZXYDGQZ
Schwarz lemma 0MB48XDBY3
exp(1/z) has an essential singularity at 0 0NB31CC4SN
Principal part 0NDV5R6Z6X
Meromorphic function 0NSD1TPHR0
Removable singularity 0P18JC72RE
Argument principle 0PN2BXRS8G
Holomorphic functions with nonzero derivative are conformal 0Q7M6K6VD7
Holomorphic functions are infinitely differentiable 0QEBN8DGVE
Branch of the logarithm 0SQ1F2BEDS
Principal value of the argument 0SQSQP748R
Hurwitz's theorem 0SSKBQN58M
Cauchy–Riemann equations 0T71SSYZ39
Isolated singularity 0TYB3HM9KE
Square root 0VB8BFRABH
Morera's theorem 0VDD7W0EKZ
Standard deviation 0VTN5RKNC5
Pole 0WPQYW8MTE
Complex logarithm 0X2FY491PF
The principal logarithm is holomorphic off the branch cut 0XVGJE7Q04
Identity theorem 0YBVKMYX0W
Irrationality of the square root of a prime 0YHFMXJJAZ
Order of a pole 0YK27TJ4WF
Essential singularity 0YKDJBV26S
Principal branch 0YKY4M3KRQ
Existence of nth roots of complex numbers 0YM6P6C206
Power series are holomorphic in the disc of convergence 0YMP521ZR5
Fundamental theorem of contour integration 0YQ458D7PF
The complex conjugate is not holomorphic 0Z8ATBPM5W
A complex number times its conjugate 0ZB7J071WQ
Complex power 0ZV9A7EV0F
Law of large numbers 0ZVEAYVRC3
Argument of a complex number 0ZZRSX91QR