List of theorems referencing the symbol SQRT

(915) Theorem 760: [The square of the square root of any positive x is x] ((X in Re) & (R_is_nonneg(X))) •imp ((sqrt(X) in Re) & (R_is_nonneg(sqrt(X))) & ((sqrt(X) •R_TIMES sqrt(X)) = X))
(916) Theorem 761: [The positive square root is unique] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & ((Y •R_TIMES Y) = X)) •imp (Y = sqrt(X))
(917) Theorem 762: [The square root is monotone increasing for positive numbers] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y) & (X •R_GT Y)) •imp (sqrt(X) •R_GT sqrt(Y))
(918) Theorem 763: [The square root of a product is the product of the square roots] ((X in Re) & (Y in Re) & R_is_nonneg(X) & R_is_nonneg(Y)) •imp (sqrt(X •R_TIMES Y) = (sqrt(X) •R_TIMES sqrt(Y)))
(919) Theorem 763a: [The square of the square root of any real w=(x •R_TIMES x) •R_PLUS (y •R_TIMES y) is w] ((X in Re) & (Y in Re)) •imp (sqrt((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)) •R_TIMES sqrt((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)) = ((X •R_TIMES X) •R_PLUS (Y •R_TIMES Y)))