Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-rsqrt Unicode version

Definition df-rsqrt 10022
 Description: Define a function whose value is the square root of a nonnegative real number. Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.)
Assertion
Ref Expression
df-rsqrt
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-rsqrt
StepHypRef Expression
1 csqrt 10020 . 2
2 vx . . 3
3 cr 7042 . . 3
4 vy . . . . . . . 8
54cv 1284 . . . . . . 7
6 c2 8156 . . . . . . 7
7 cexp 9572 . . . . . . 7
85, 6, 7co 5543 . . . . . 6
92cv 1284 . . . . . 6
108, 9wceq 1285 . . . . 5
11 cc0 7043 . . . . . 6
12 cle 7216 . . . . . 6
1311, 5, 12wbr 3793 . . . . 5
1410, 13wa 102 . . . 4
1514, 4, 3crio 5498 . . 3
162, 3, 15cmpt 3847 . 2
171, 16wceq 1285 1
 Colors of variables: wff set class This definition is referenced by:  sqrtrval  10024  absval  10025
 Copyright terms: Public domain W3C validator