statement proposition
The exponential function is positive
Statement
For every real , .
Remarks
By the sum rule, . Also , so .
For , it also follows from the series, since all terms are nonnegative and the first is .
Mathlib states it as Real.exp_pos.
Explanations
L1 human
The graph of stays above the -axis. It comes close to as , but it never reaches .
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 29 nodes in this order. The foundations come first, and the list ends with this node.
- no evidence level
- Sequence definition
- Real sequence definition
- Bounded sequence definition
- Geometric sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Series definition
- Sum of a finite geometric series statement
- Monotone convergence theorem for sequences statement
- Convergent sequence definition
- Squeeze theorem statement
- Cauchy product definition
- Partial sum definition
- Power series definition
- The sequence r^n tends to zero for |r| < 1 example
- Radius of convergence definition
- Convergent series definition
- A series of nonnegative terms converges iff its partial sums are bounded statement
- Absolute convergence definition
- Sum of a series definition
- Comparison test statement
- Geometric series example
- Cauchy product of absolutely convergent series statement
- Ratio test statement
- Ratio formula for the radius of convergence statement
- The exponential series has infinite radius of convergence statement
- Exponential function definition
- Exponential of a sum statement
- The exponential function is positive statement
What depends on this
19 nodes use this node, directly or through other nodes.
- Natural logarithm 0044CPHJBV
- Euler–Mascheroni constant 00C5P9JZBK
- The logarithm grows slower than any power 00DGYY10FV
- log x is at most x - 1 04CBRA4JRK
- Inverse hyperbolic functions 04D7CHT5V1
- Harmonic numbers grow like log n 05S2GSPMGA
- Derivative of the logarithm 07X1QA6BRW
- Logarithm of a quotient 0J7PHRBNNS
- Integral of 1/x 0K1N1Y4EGZ
- Logarithm of a product 0K2FNY6DYV
- The exponential function is strictly increasing 0KN2V7840E
- Derivative of x^a 0KY08TWDMQ
- Logarithm is the inverse of the exponential 0RKW2X63YR
- Real exponentiation 0TV07AQT62
- Logarithm of a power 0V948DE5KA
- Improper integral of x^p on an unbounded interval 0VGKB2NC4T
- Integration by partial fractions 0WBTWFXJQG
- Mercator series 0YZXNE3HFR
- The logarithm is strictly concave 0ZS54B9GJF