statement theorem
Exponential of a sum
Statement
For all real numbers and ,
Remarks
Multiply the two series by the Cauchy product. The binomial theorem gives .
In particular, .
So is a group homomorphism from to the multiplicative group . Mathlib states the formula as Real.exp_add.
Explanations
L1 human
The exponential function turns addition into multiplication. This is the rule for powers.
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 28 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
What depends on this
29 nodes use this node, directly or through other nodes.
- Natural logarithm 0044CPHJBV
- Euler–Mascheroni constant 00C5P9JZBK
- The logarithm grows slower than any power 00DGYY10FV
- 1 + x is at most exp x 012C7GFF20
- Integral of exp(-x) over the half line 039JAF7ZAN
- log x is at most x - 1 04CBRA4JRK
- Inverse hyperbolic functions 04D7CHT5V1
- Harmonic numbers grow like log n 05S2GSPMGA
- Integral of the exponential function 06D0EWR2DV
- Power series of the exponential function 06JZGMYTYD
- Derivatives of the hyperbolic functions 07T2TKGZ4J
- Derivative of the logarithm 07X1QA6BRW
- The exponential function is convex 0D7GRZ2ADX
- The exponential function is its own derivative 0EX9GFJ0B3
- The gamma function extends the factorial 0FDCW77H44
- Addition formulas for hyperbolic functions 0GJZCE87WP
- 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
- The exponential function is positive 0P9BNBW2W3
- 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
Sources
- Web https://en.wikipedia.org/wiki/Exponential_function, Functional equation
What links here
Used by
- The exponential function is its own derivative 0EX9GFJ0B3
- Addition formulas for hyperbolic functions 0GJZCE87WP
- Logarithm of a product 0K2FNY6DYV
- The exponential function is positive 0P9BNBW2W3