Theorem List for Intuitionistic Logic Explorer - 11401-11500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | efcllemp 11401* |
Lemma for efcl 11407. The series that defines the exponential
function
converges. The ratio test cvgratgt0 11334 is used to show convergence.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → (2 ·
(abs‘𝐴)) < 𝐾)
⇒ ⊢ (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ ) |
|
Theorem | efcllem 11402* |
Lemma for efcl 11407. The series that defines the exponential
function
converges. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → seq0( + , 𝐹) ∈ dom ⇝
) |
|
Theorem | ef0lem 11403* |
The series defining the exponential function converges in the (trivial)
case of a zero argument. (Contributed by Steve Rodriguez, 7-Jun-2006.)
(Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 = 0 → seq0( + , 𝐹) ⇝ 1) |
|
Theorem | efval 11404* |
Value of the exponential function. (Contributed by NM, 8-Jan-2006.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 ((𝐴↑𝑘) / (!‘𝑘))) |
|
Theorem | esum 11405 |
Value of Euler's constant e = 2.71828.... (Contributed
by Steve
Rodriguez, 5-Mar-2006.)
|
⊢ e = Σ𝑘 ∈ ℕ0 (1 /
(!‘𝑘)) |
|
Theorem | eff 11406 |
Domain and codomain of the exponential function. (Contributed by Paul
Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
⊢ exp:ℂ⟶ℂ |
|
Theorem | efcl 11407 |
Closure law for the exponential function. (Contributed by NM,
8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈
ℂ) |
|
Theorem | efval2 11408* |
Value of the exponential function. (Contributed by Mario Carneiro,
29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 (𝐹‘𝑘)) |
|
Theorem | efcvg 11409* |
The series that defines the exponential function converges to it.
(Contributed by NM, 9-Jan-2006.) (Revised by Mario Carneiro,
28-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → seq0( + , 𝐹) ⇝ (exp‘𝐴)) |
|
Theorem | efcvgfsum 11410* |
Exponential function convergence in terms of a sequence of partial
finite sums. (Contributed by NM, 10-Jan-2006.) (Revised by Mario
Carneiro, 28-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦
Σ𝑘 ∈ (0...𝑛)((𝐴↑𝑘) / (!‘𝑘))) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ (exp‘𝐴)) |
|
Theorem | reefcl 11411 |
The exponential function is real if its argument is real. (Contributed
by NM, 27-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈
ℝ) |
|
Theorem | reefcld 11412 |
The exponential function is real if its argument is real. (Contributed
by Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ) |
|
Theorem | ere 11413 |
Euler's constant e = 2.71828... is a real number.
(Contributed by
NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.)
|
⊢ e ∈ ℝ |
|
Theorem | ege2le3 11414 |
Euler's constant e = 2.71828... is bounded by 2 and 3.
(Contributed by NM, 20-Mar-2005.) (Proof shortened by Mario Carneiro,
28-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 /
2)↑𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 /
(!‘𝑛))) ⇒ ⊢ (2 ≤ e ∧ e ≤
3) |
|
Theorem | ef0 11415 |
Value of the exponential function at 0. Equation 2 of [Gleason] p. 308.
(Contributed by Steve Rodriguez, 27-Jun-2006.) (Revised by Mario
Carneiro, 28-Apr-2014.)
|
⊢ (exp‘0) = 1 |
|
Theorem | efcj 11416 |
The exponential of a complex conjugate. Equation 3 of [Gleason] p. 308.
(Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro,
28-Apr-2014.)
|
⊢ (𝐴 ∈ ℂ →
(exp‘(∗‘𝐴)) = (∗‘(exp‘𝐴))) |
|
Theorem | efaddlem 11417* |
Lemma for efadd 11418 (exponential function addition law).
(Contributed by
Mario Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛))) & ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵))) |
|
Theorem | efadd 11418 |
Sum of exponents law for exponential function. (Contributed by NM,
10-Jan-2006.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵))) |
|
Theorem | efcan 11419 |
Cancellation law for exponential function. Equation 27 of [Rudin] p. 164.
(Contributed by NM, 13-Jan-2006.)
|
⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) · (exp‘-𝐴)) = 1) |
|
Theorem | efap0 11420 |
The exponential of a complex number is apart from zero. (Contributed by
Jim Kingdon, 12-Dec-2022.)
|
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) # 0) |
|
Theorem | efne0 11421 |
The exponential of a complex number is nonzero. Corollary 15-4.3 of
[Gleason] p. 309. The same result also
holds with not equal replaced by
apart, as seen at efap0 11420 (which will be more useful in most
contexts).
(Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro,
29-Apr-2014.)
|
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ≠ 0) |
|
Theorem | efneg 11422 |
The exponential of the opposite is the inverse of the exponential.
(Contributed by Mario Carneiro, 10-May-2014.)
|
⊢ (𝐴 ∈ ℂ → (exp‘-𝐴) = (1 / (exp‘𝐴))) |
|
Theorem | eff2 11423 |
The exponential function maps the complex numbers to the nonzero complex
numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
|
⊢ exp:ℂ⟶(ℂ ∖
{0}) |
|
Theorem | efsub 11424 |
Difference of exponents law for exponential function. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵))) |
|
Theorem | efexp 11425 |
The exponential of an integer power. Corollary 15-4.4 of [Gleason]
p. 309, restricted to integers. (Contributed by NM, 13-Jan-2006.)
(Revised by Mario Carneiro, 5-Jun-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (exp‘(𝑁 · 𝐴)) = ((exp‘𝐴)↑𝑁)) |
|
Theorem | efzval 11426 |
Value of the exponential function for integers. Special case of efval 11404.
Equation 30 of [Rudin] p. 164. (Contributed
by Steve Rodriguez,
15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁)) |
|
Theorem | efgt0 11427 |
The exponential of a real number is greater than 0. (Contributed by Paul
Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ (𝐴 ∈ ℝ → 0 <
(exp‘𝐴)) |
|
Theorem | rpefcl 11428 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 10-Nov-2013.)
|
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈
ℝ+) |
|
Theorem | rpefcld 11429 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (exp‘𝐴) ∈
ℝ+) |
|
Theorem | eftlcvg 11430* |
The tail series of the exponential function are convergent.
(Contributed by Mario Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) →
seq𝑀( + , 𝐹) ∈ dom ⇝
) |
|
Theorem | eftlcl 11431* |
Closure of the sum of an infinite tail of the series defining the
exponential function. (Contributed by Paul Chapman, 17-Jan-2008.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) →
Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ) |
|
Theorem | reeftlcl 11432* |
Closure of the sum of an infinite tail of the series defining the
exponential function. (Contributed by Paul Chapman, 17-Jan-2008.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) →
Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℝ) |
|
Theorem | eftlub 11433* |
An upper bound on the absolute value of the infinite tail of the series
expansion of the exponential function on the closed unit disk.
(Contributed by Paul Chapman, 19-Jan-2008.) (Proof shortened by Mario
Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦
(((abs‘𝐴)↑𝑛) / (!‘𝑛))) & ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐴) ≤
1) ⇒ ⊢ (𝜑 → (abs‘Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) |
|
Theorem | efsep 11434* |
Separate out the next term of the power series expansion of the
exponential function. The last hypothesis allows the separated terms to
be rearranged as desired. (Contributed by Paul Chapman, 23-Nov-2007.)
(Revised by Mario Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ 𝑁 = (𝑀 + 1) & ⊢ 𝑀 ∈
ℕ0
& ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (exp‘𝐴) = (𝐵 + Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘))) & ⊢ (𝜑 → (𝐵 + ((𝐴↑𝑀) / (!‘𝑀))) = 𝐷) ⇒ ⊢ (𝜑 → (exp‘𝐴) = (𝐷 + Σ𝑘 ∈ (ℤ≥‘𝑁)(𝐹‘𝑘))) |
|
Theorem | effsumlt 11435* |
The partial sums of the series expansion of the exponential function at
a positive real number are bounded by the value of the function.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro,
29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈
ℕ0) ⇒ ⊢ (𝜑 → (seq0( + , 𝐹)‘𝑁) < (exp‘𝐴)) |
|
Theorem | eft0val 11436 |
The value of the first term of the series expansion of the exponential
function is 1. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by
Mario Carneiro, 29-Apr-2014.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴↑0) / (!‘0)) =
1) |
|
Theorem | ef4p 11437* |
Separate out the first four terms of the infinite series expansion of
the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.)
(Revised by Mario Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = ((((1 + 𝐴) + ((𝐴↑2) / 2)) + ((𝐴↑3) / 6)) + Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘))) |
|
Theorem | efgt1p2 11438 |
The exponential of a positive real number is greater than the sum of the
first three terms of the series expansion. (Contributed by Mario
Carneiro, 15-Sep-2014.)
|
⊢ (𝐴 ∈ ℝ+ → ((1 +
𝐴) + ((𝐴↑2) / 2)) < (exp‘𝐴)) |
|
Theorem | efgt1p 11439 |
The exponential of a positive real number is greater than 1 plus that
number. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by
Mario Carneiro, 30-Apr-2014.)
|
⊢ (𝐴 ∈ ℝ+ → (1 +
𝐴) < (exp‘𝐴)) |
|
Theorem | efgt1 11440 |
The exponential of a positive real number is greater than 1.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro,
30-Apr-2014.)
|
⊢ (𝐴 ∈ ℝ+ → 1 <
(exp‘𝐴)) |
|
Theorem | efltim 11441 |
The exponential function on the reals is strictly increasing.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
20-Dec-2022.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → (exp‘𝐴) < (exp‘𝐵))) |
|
Theorem | reef11 11442 |
The exponential function on real numbers is one-to-one. (Contributed by
NM, 21-Aug-2008.) (Revised by Jim Kingdon, 20-Dec-2022.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((exp‘𝐴) = (exp‘𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | reeff1 11443 |
The exponential function maps real arguments one-to-one to positive
reals. (Contributed by Steve Rodriguez, 25-Aug-2007.) (Revised by
Mario Carneiro, 10-Nov-2013.)
|
⊢ (exp ↾ ℝ):ℝ–1-1→ℝ+ |
|
Theorem | eflegeo 11444 |
The exponential function on the reals between 0 and 1 lies below the
comparable geometric series sum. (Contributed by Paul Chapman,
11-Sep-2007.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 𝐴 < 1) ⇒ ⊢ (𝜑 → (exp‘𝐴) ≤ (1 / (1 − 𝐴))) |
|
Theorem | sinval 11445 |
Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised
by Mario Carneiro, 10-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) = (((exp‘(i ·
𝐴)) − (exp‘(-i
· 𝐴))) / (2
· i))) |
|
Theorem | cosval 11446 |
Value of the cosine function. (Contributed by NM, 14-Mar-2005.)
(Revised by Mario Carneiro, 10-Nov-2013.)
|
⊢ (𝐴 ∈ ℂ → (cos‘𝐴) = (((exp‘(i ·
𝐴)) + (exp‘(-i
· 𝐴))) /
2)) |
|
Theorem | sinf 11447 |
Domain and codomain of the sine function. (Contributed by Paul Chapman,
22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ sin:ℂ⟶ℂ |
|
Theorem | cosf 11448 |
Domain and codomain of the cosine function. (Contributed by Paul Chapman,
22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ cos:ℂ⟶ℂ |
|
Theorem | sincl 11449 |
Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised
by Mario Carneiro, 30-Apr-2014.)
|
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈
ℂ) |
|
Theorem | coscl 11450 |
Closure of the cosine function with a complex argument. (Contributed by
NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈
ℂ) |
|
Theorem | tanvalap 11451 |
Value of the tangent function. (Contributed by Mario Carneiro,
14-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.)
|
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) # 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴))) |
|
Theorem | tanclap 11452 |
The closure of the tangent function with a complex argument. (Contributed
by David A. Wheeler, 15-Mar-2014.) (Revised by Jim Kingdon,
21-Dec-2022.)
|
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) # 0) → (tan‘𝐴) ∈
ℂ) |
|
Theorem | sincld 11453 |
Closure of the sine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ) |
|
Theorem | coscld 11454 |
Closure of the cosine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ) |
|
Theorem | tanclapd 11455 |
Closure of the tangent function. (Contributed by Mario Carneiro,
29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (cos‘𝐴) # 0)
⇒ ⊢ (𝜑 → (tan‘𝐴) ∈ ℂ) |
|
Theorem | tanval2ap 11456 |
Express the tangent function directly in terms of exp.
(Contributed
by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon,
22-Dec-2022.)
|
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) # 0) → (tan‘𝐴) = (((exp‘(i ·
𝐴)) − (exp‘(-i
· 𝐴))) / (i
· ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴)))))) |
|
Theorem | tanval3ap 11457 |
Express the tangent function directly in terms of exp.
(Contributed
by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon,
22-Dec-2022.)
|
⊢ ((𝐴 ∈ ℂ ∧ ((exp‘(2
· (i · 𝐴)))
+ 1) # 0) → (tan‘𝐴) = (((exp‘(2 · (i ·
𝐴))) − 1) / (i
· ((exp‘(2 · (i · 𝐴))) + 1)))) |
|
Theorem | resinval 11458 |
The sine of a real number in terms of the exponential function.
(Contributed by NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) =
(ℑ‘(exp‘(i · 𝐴)))) |
|
Theorem | recosval 11459 |
The cosine of a real number in terms of the exponential function.
(Contributed by NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = (ℜ‘(exp‘(i
· 𝐴)))) |
|
Theorem | efi4p 11460* |
Separate out the first four terms of the infinite series expansion of
the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → (exp‘(i
· 𝐴)) = (((1
− ((𝐴↑2) / 2))
+ (i · (𝐴 −
((𝐴↑3) / 6)))) +
Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘))) |
|
Theorem | resin4p 11461* |
Separate out the first four terms of the infinite series expansion of
the sine of a real number. (Contributed by Paul Chapman, 19-Jan-2008.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℝ → (sin‘𝐴) = ((𝐴 − ((𝐴↑3) / 6)) +
(ℑ‘Σ𝑘
∈ (ℤ≥‘4)(𝐹‘𝑘)))) |
|
Theorem | recos4p 11462* |
Separate out the first four terms of the infinite series expansion of
the cosine of a real number. (Contributed by Paul Chapman,
19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = ((1 − ((𝐴↑2) / 2)) +
(ℜ‘Σ𝑘
∈ (ℤ≥‘4)(𝐹‘𝑘)))) |
|
Theorem | resincl 11463 |
The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈
ℝ) |
|
Theorem | recoscl 11464 |
The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈
ℝ) |
|
Theorem | retanclap 11465 |
The closure of the tangent function with a real argument. (Contributed by
David A. Wheeler, 15-Mar-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ (cos‘𝐴) # 0) → (tan‘𝐴) ∈
ℝ) |
|
Theorem | resincld 11466 |
Closure of the sine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ) |
|
Theorem | recoscld 11467 |
Closure of the cosine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (cos‘𝐴) ∈ ℝ) |
|
Theorem | retanclapd 11468 |
Closure of the tangent function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (cos‘𝐴) # 0)
⇒ ⊢ (𝜑 → (tan‘𝐴) ∈ ℝ) |
|
Theorem | sinneg 11469 |
The sine of a negative is the negative of the sine. (Contributed by NM,
30-Apr-2005.)
|
⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴)) |
|
Theorem | cosneg 11470 |
The cosines of a number and its negative are the same. (Contributed by
NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴)) |
|
Theorem | tannegap 11471 |
The tangent of a negative is the negative of the tangent. (Contributed by
David A. Wheeler, 23-Mar-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) # 0) → (tan‘-𝐴) = -(tan‘𝐴)) |
|
Theorem | sin0 11472 |
Value of the sine function at 0. (Contributed by Steve Rodriguez,
14-Mar-2005.)
|
⊢ (sin‘0) = 0 |
|
Theorem | cos0 11473 |
Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
|
⊢ (cos‘0) = 1 |
|
Theorem | tan0 11474 |
The value of the tangent function at zero is zero. (Contributed by David
A. Wheeler, 16-Mar-2014.)
|
⊢ (tan‘0) = 0 |
|
Theorem | efival 11475 |
The exponential function in terms of sine and cosine. (Contributed by NM,
30-Apr-2005.)
|
⊢ (𝐴 ∈ ℂ → (exp‘(i
· 𝐴)) =
((cos‘𝐴) + (i
· (sin‘𝐴)))) |
|
Theorem | efmival 11476 |
The exponential function in terms of sine and cosine. (Contributed by NM,
14-Jan-2006.)
|
⊢ (𝐴 ∈ ℂ → (exp‘(-i
· 𝐴)) =
((cos‘𝐴) − (i
· (sin‘𝐴)))) |
|
Theorem | efeul 11477 |
Eulerian representation of the complex exponential. (Suggested by Jeff
Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.)
|
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) =
((exp‘(ℜ‘𝐴)) ·
((cos‘(ℑ‘𝐴)) + (i ·
(sin‘(ℑ‘𝐴)))))) |
|
Theorem | efieq 11478 |
The exponentials of two imaginary numbers are equal iff their sine and
cosine components are equal. (Contributed by Paul Chapman,
15-Mar-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((exp‘(i
· 𝐴)) =
(exp‘(i · 𝐵))
↔ ((cos‘𝐴) =
(cos‘𝐵) ∧
(sin‘𝐴) =
(sin‘𝐵)))) |
|
Theorem | sinadd 11479 |
Addition formula for sine. Equation 14 of [Gleason] p. 310. (Contributed
by Steve Rodriguez, 10-Nov-2006.) (Revised by Mario Carneiro,
30-Apr-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 + 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵)))) |
|
Theorem | cosadd 11480 |
Addition formula for cosine. Equation 15 of [Gleason] p. 310.
(Contributed by NM, 15-Jan-2006.) (Revised by Mario Carneiro,
30-Apr-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (cos‘(𝐴 + 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵)))) |
|
Theorem | tanaddaplem 11481 |
A useful intermediate step in tanaddap 11482 when showing that the addition of
tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.)
(Revised by Jim Kingdon, 25-Dec-2022.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((cos‘𝐴) # 0 ∧ (cos‘𝐵) # 0)) →
((cos‘(𝐴 + 𝐵)) # 0 ↔ ((tan‘𝐴) · (tan‘𝐵)) # 1)) |
|
Theorem | tanaddap 11482 |
Addition formula for tangent. (Contributed by Mario Carneiro,
4-Apr-2015.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((cos‘𝐴) # 0 ∧ (cos‘𝐵) # 0 ∧ (cos‘(𝐴 + 𝐵)) # 0)) → (tan‘(𝐴 + 𝐵)) = (((tan‘𝐴) + (tan‘𝐵)) / (1 − ((tan‘𝐴) · (tan‘𝐵))))) |
|
Theorem | sinsub 11483 |
Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 − 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) − ((cos‘𝐴) · (sin‘𝐵)))) |
|
Theorem | cossub 11484 |
Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (cos‘(𝐴 − 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) + ((sin‘𝐴) · (sin‘𝐵)))) |
|
Theorem | addsin 11485 |
Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) + (sin‘𝐵)) = (2 ·
((sin‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) /
2))))) |
|
Theorem | subsin 11486 |
Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) − (sin‘𝐵)) = (2 ·
((cos‘((𝐴 + 𝐵) / 2)) ·
(sin‘((𝐴 −
𝐵) /
2))))) |
|
Theorem | sinmul 11487 |
Product of sines can be rewritten as half the difference of certain
cosines. This follows from cosadd 11480 and cossub 11484. (Contributed by David
A. Wheeler, 26-May-2015.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (sin‘𝐵)) = (((cos‘(𝐴 − 𝐵)) − (cos‘(𝐴 + 𝐵))) / 2)) |
|
Theorem | cosmul 11488 |
Product of cosines can be rewritten as half the sum of certain cosines.
This follows from cosadd 11480 and cossub 11484. (Contributed by David A.
Wheeler, 26-May-2015.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) · (cos‘𝐵)) = (((cos‘(𝐴 − 𝐵)) + (cos‘(𝐴 + 𝐵))) / 2)) |
|
Theorem | addcos 11489 |
Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) + (cos‘𝐵)) = (2 ·
((cos‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) /
2))))) |
|
Theorem | subcos 11490 |
Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
(Revised by Mario Carneiro, 10-May-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐵) − (cos‘𝐴)) = (2 ·
((sin‘((𝐴 + 𝐵) / 2)) ·
(sin‘((𝐴 −
𝐵) /
2))))) |
|
Theorem | sincossq 11491 |
Sine squared plus cosine squared is 1. Equation 17 of [Gleason] p. 311.
Note that this holds for non-real arguments, even though individually each
term is unbounded. (Contributed by NM, 15-Jan-2006.)
|
⊢ (𝐴 ∈ ℂ → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) =
1) |
|
Theorem | sin2t 11492 |
Double-angle formula for sine. (Contributed by Paul Chapman,
17-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘(2
· 𝐴)) = (2 ·
((sin‘𝐴) ·
(cos‘𝐴)))) |
|
Theorem | cos2t 11493 |
Double-angle formula for cosine. (Contributed by Paul Chapman,
24-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘(2
· 𝐴)) = ((2
· ((cos‘𝐴)↑2)) − 1)) |
|
Theorem | cos2tsin 11494 |
Double-angle formula for cosine in terms of sine. (Contributed by NM,
12-Sep-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘(2
· 𝐴)) = (1 −
(2 · ((sin‘𝐴)↑2)))) |
|
Theorem | sinbnd 11495 |
The sine of a real number lies between -1 and 1. Equation 18 of [Gleason]
p. 311. (Contributed by NM, 16-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ → (-1 ≤
(sin‘𝐴) ∧
(sin‘𝐴) ≤
1)) |
|
Theorem | cosbnd 11496 |
The cosine of a real number lies between -1 and 1. Equation 18 of
[Gleason] p. 311. (Contributed by NM,
16-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ → (-1 ≤
(cos‘𝐴) ∧
(cos‘𝐴) ≤
1)) |
|
Theorem | sinbnd2 11497 |
The sine of a real number is in the closed interval from -1 to 1.
(Contributed by Mario Carneiro, 12-May-2014.)
|
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈
(-1[,]1)) |
|
Theorem | cosbnd2 11498 |
The cosine of a real number is in the closed interval from -1 to 1.
(Contributed by Mario Carneiro, 12-May-2014.)
|
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈
(-1[,]1)) |
|
Theorem | ef01bndlem 11499* |
Lemma for sin01bnd 11500 and cos01bnd 11501. (Contributed by Paul Chapman,
19-Jan-2008.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) < ((𝐴↑4) / 6)) |
|
Theorem | sin01bnd 11500 |
Bounds on the sine of a positive real number less than or equal to 1.
(Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro,
30-Apr-2014.)
|
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴)) |