Mathematica has a flexible system for specifying arbitrary symbolic assumptions about variables. It uses a wide range of sophisticated algorithms to infer the consequences of assumptions—often in the process automatically proving a sequence of necessary mathematical theorems.
Element () — specify membership in a domain (entered as EscelemEsc)
NotElement () — specify exclusion from a domain (Esc!elemEsc)
ForAll () — universal quantifier (entered as EscfaEsc)
Exists () — existential quantifier (entered as EscexEsc)
Refine — evaluate an expression using assumptions
FunctionExpand — expand in terms of simpler functions, using assumptions
Assuming — set up assumptions to be used by functions inside