Theorem List for Intuitionistic Logic Explorer - 11701-11800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | efneg 11701 |
The exponential of the opposite is the inverse of the exponential.
(Contributed by Mario Carneiro, 10-May-2014.)
|
⊢ (𝐴 ∈ ℂ → (exp‘-𝐴) = (1 / (exp‘𝐴))) |
|
Theorem | eff2 11702 |
The exponential function maps the complex numbers to the nonzero complex
numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
|
⊢ exp:ℂ⟶(ℂ ∖
{0}) |
|
Theorem | efsub 11703 |
Difference of exponents law for exponential function. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵))) |
|
Theorem | efexp 11704 |
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 11705 |
Value of the exponential function for integers. Special case of efval 11683.
Equation 30 of [Rudin] p. 164. (Contributed
by Steve Rodriguez,
15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁)) |
|
Theorem | efgt0 11706 |
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 11707 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 10-Nov-2013.)
|
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈
ℝ+) |
|
Theorem | rpefcld 11708 |
The exponential of a real number is a positive real. (Contributed by
Mario Carneiro, 29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (exp‘𝐴) ∈
ℝ+) |
|
Theorem | eftlcvg 11709* |
The tail series of the exponential function are convergent.
(Contributed by Mario Carneiro, 29-Apr-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) →
seq𝑀( + , 𝐹) ∈ dom ⇝
) |
|
Theorem | eftlcl 11710* |
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 11711* |
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 11712* |
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 11713* |
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 11714* |
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 11715 |
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 11716* |
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 11717 |
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 11718 |
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 11719 |
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 11720 |
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 11721 |
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 11722 |
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 11723 |
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 11724 |
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 11725 |
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 11726 |
Domain and codomain of the sine function. (Contributed by Paul Chapman,
22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ sin:ℂ⟶ℂ |
|
Theorem | cosf 11727 |
Domain and codomain of the cosine function. (Contributed by Paul Chapman,
22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ cos:ℂ⟶ℂ |
|
Theorem | sincl 11728 |
Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised
by Mario Carneiro, 30-Apr-2014.)
|
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈
ℂ) |
|
Theorem | coscl 11729 |
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 11730 |
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 11731 |
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 11732 |
Closure of the sine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ) |
|
Theorem | coscld 11733 |
Closure of the cosine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ) |
|
Theorem | tanclapd 11734 |
Closure of the tangent function. (Contributed by Mario Carneiro,
29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (cos‘𝐴) # 0)
⇒ ⊢ (𝜑 → (tan‘𝐴) ∈ ℂ) |
|
Theorem | tanval2ap 11735 |
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 11736 |
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 11737 |
The sine of a real number in terms of the exponential function.
(Contributed by NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) =
(ℑ‘(exp‘(i · 𝐴)))) |
|
Theorem | recosval 11738 |
The cosine of a real number in terms of the exponential function.
(Contributed by NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = (ℜ‘(exp‘(i
· 𝐴)))) |
|
Theorem | efi4p 11739* |
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 11740* |
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 11741* |
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 11742 |
The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈
ℝ) |
|
Theorem | recoscl 11743 |
The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈
ℝ) |
|
Theorem | retanclap 11744 |
The closure of the tangent function with a real argument. (Contributed by
David A. Wheeler, 15-Mar-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ (cos‘𝐴) # 0) → (tan‘𝐴) ∈
ℝ) |
|
Theorem | resincld 11745 |
Closure of the sine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ) |
|
Theorem | recoscld 11746 |
Closure of the cosine function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → (cos‘𝐴) ∈ ℝ) |
|
Theorem | retanclapd 11747 |
Closure of the tangent function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (cos‘𝐴) # 0)
⇒ ⊢ (𝜑 → (tan‘𝐴) ∈ ℝ) |
|
Theorem | sinneg 11748 |
The sine of a negative is the negative of the sine. (Contributed by NM,
30-Apr-2005.)
|
⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴)) |
|
Theorem | cosneg 11749 |
The cosines of a number and its negative are the same. (Contributed by
NM, 30-Apr-2005.)
|
⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴)) |
|
Theorem | tannegap 11750 |
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 11751 |
Value of the sine function at 0. (Contributed by Steve Rodriguez,
14-Mar-2005.)
|
⊢ (sin‘0) = 0 |
|
Theorem | cos0 11752 |
Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
|
⊢ (cos‘0) = 1 |
|
Theorem | tan0 11753 |
The value of the tangent function at zero is zero. (Contributed by David
A. Wheeler, 16-Mar-2014.)
|
⊢ (tan‘0) = 0 |
|
Theorem | efival 11754 |
The exponential function in terms of sine and cosine. (Contributed by NM,
30-Apr-2005.)
|
⊢ (𝐴 ∈ ℂ → (exp‘(i
· 𝐴)) =
((cos‘𝐴) + (i
· (sin‘𝐴)))) |
|
Theorem | efmival 11755 |
The exponential function in terms of sine and cosine. (Contributed by NM,
14-Jan-2006.)
|
⊢ (𝐴 ∈ ℂ → (exp‘(-i
· 𝐴)) =
((cos‘𝐴) − (i
· (sin‘𝐴)))) |
|
Theorem | efeul 11756 |
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 11757 |
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 11758 |
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 11759 |
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 11760 |
A useful intermediate step in tanaddap 11761 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 11761 |
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 11762 |
Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 − 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) − ((cos‘𝐴) · (sin‘𝐵)))) |
|
Theorem | cossub 11763 |
Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (cos‘(𝐴 − 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) + ((sin‘𝐴) · (sin‘𝐵)))) |
|
Theorem | addsin 11764 |
Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) + (sin‘𝐵)) = (2 ·
((sin‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) /
2))))) |
|
Theorem | subsin 11765 |
Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) − (sin‘𝐵)) = (2 ·
((cos‘((𝐴 + 𝐵) / 2)) ·
(sin‘((𝐴 −
𝐵) /
2))))) |
|
Theorem | sinmul 11766 |
Product of sines can be rewritten as half the difference of certain
cosines. This follows from cosadd 11759 and cossub 11763. (Contributed by David
A. Wheeler, 26-May-2015.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (sin‘𝐵)) = (((cos‘(𝐴 − 𝐵)) − (cos‘(𝐴 + 𝐵))) / 2)) |
|
Theorem | cosmul 11767 |
Product of cosines can be rewritten as half the sum of certain cosines.
This follows from cosadd 11759 and cossub 11763. (Contributed by David A.
Wheeler, 26-May-2015.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) · (cos‘𝐵)) = (((cos‘(𝐴 − 𝐵)) + (cos‘(𝐴 + 𝐵))) / 2)) |
|
Theorem | addcos 11768 |
Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) + (cos‘𝐵)) = (2 ·
((cos‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) /
2))))) |
|
Theorem | subcos 11769 |
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 11770 |
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 11771 |
Double-angle formula for sine. (Contributed by Paul Chapman,
17-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (sin‘(2
· 𝐴)) = (2 ·
((sin‘𝐴) ·
(cos‘𝐴)))) |
|
Theorem | cos2t 11772 |
Double-angle formula for cosine. (Contributed by Paul Chapman,
24-Jan-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘(2
· 𝐴)) = ((2
· ((cos‘𝐴)↑2)) − 1)) |
|
Theorem | cos2tsin 11773 |
Double-angle formula for cosine in terms of sine. (Contributed by NM,
12-Sep-2008.)
|
⊢ (𝐴 ∈ ℂ → (cos‘(2
· 𝐴)) = (1 −
(2 · ((sin‘𝐴)↑2)))) |
|
Theorem | sinbnd 11774 |
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 11775 |
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 11776 |
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 11777 |
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 11778* |
Lemma for sin01bnd 11779 and cos01bnd 11780. (Contributed by Paul Chapman,
19-Jan-2008.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i
· 𝐴)↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ (0(,]1) →
(abs‘Σ𝑘 ∈
(ℤ≥‘4)(𝐹‘𝑘)) < ((𝐴↑4) / 6)) |
|
Theorem | sin01bnd 11779 |
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‘𝐴) < 𝐴)) |
|
Theorem | cos01bnd 11780 |
Bounds on the cosine 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) → ((1 − (2
· ((𝐴↑2) /
3))) < (cos‘𝐴)
∧ (cos‘𝐴) <
(1 − ((𝐴↑2) /
3)))) |
|
Theorem | cos1bnd 11781 |
Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|
⊢ ((1 / 3) < (cos‘1) ∧
(cos‘1) < (2 / 3)) |
|
Theorem | cos2bnd 11782 |
Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
|
⊢ (-(7 / 9) < (cos‘2) ∧
(cos‘2) < -(1 / 9)) |
|
Theorem | sin01gt0 11783 |
The sine of a positive real number less than or equal to 1 is positive.
(Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Wolf Lammen,
25-Sep-2020.)
|
⊢ (𝐴 ∈ (0(,]1) → 0 <
(sin‘𝐴)) |
|
Theorem | cos01gt0 11784 |
The cosine of a positive real number less than or equal to 1 is positive.
(Contributed by Paul Chapman, 19-Jan-2008.)
|
⊢ (𝐴 ∈ (0(,]1) → 0 <
(cos‘𝐴)) |
|
Theorem | sin02gt0 11785 |
The sine of a positive real number less than or equal to 2 is positive.
(Contributed by Paul Chapman, 19-Jan-2008.)
|
⊢ (𝐴 ∈ (0(,]2) → 0 <
(sin‘𝐴)) |
|
Theorem | sincos1sgn 11786 |
The signs of the sine and cosine of 1. (Contributed by Paul Chapman,
19-Jan-2008.)
|
⊢ (0 < (sin‘1) ∧ 0 <
(cos‘1)) |
|
Theorem | sincos2sgn 11787 |
The signs of the sine and cosine of 2. (Contributed by Paul Chapman,
19-Jan-2008.)
|
⊢ (0 < (sin‘2) ∧ (cos‘2)
< 0) |
|
Theorem | sin4lt0 11788 |
The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.)
|
⊢ (sin‘4) < 0 |
|
Theorem | cos12dec 11789 |
Cosine is decreasing from one to two. (Contributed by Mario Carneiro and
Jim Kingdon, 6-Mar-2024.)
|
⊢ ((𝐴 ∈ (1[,]2) ∧ 𝐵 ∈ (1[,]2) ∧ 𝐴 < 𝐵) → (cos‘𝐵) < (cos‘𝐴)) |
|
Theorem | absefi 11790 |
The absolute value of the exponential of an imaginary number is one.
Equation 48 of [Rudin] p. 167. (Contributed
by Jason Orendorff,
9-Feb-2007.)
|
⊢ (𝐴 ∈ ℝ →
(abs‘(exp‘(i · 𝐴))) = 1) |
|
Theorem | absef 11791 |
The absolute value of the exponential is the exponential of the real part.
(Contributed by Paul Chapman, 13-Sep-2007.)
|
⊢ (𝐴 ∈ ℂ →
(abs‘(exp‘𝐴))
= (exp‘(ℜ‘𝐴))) |
|
Theorem | absefib 11792 |
A complex number is real iff the exponential of its product with i
has absolute value one. (Contributed by NM, 21-Aug-2008.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(abs‘(exp‘(i · 𝐴))) = 1)) |
|
Theorem | efieq1re 11793 |
A number whose imaginary exponential is one is real. (Contributed by NM,
21-Aug-2008.)
|
⊢ ((𝐴 ∈ ℂ ∧ (exp‘(i
· 𝐴)) = 1) →
𝐴 ∈
ℝ) |
|
Theorem | demoivre 11794 |
De Moivre's Formula. Proof by induction given at
http://en.wikipedia.org/wiki/De_Moivre's_formula,
but
restricted to nonnegative integer powers. See also demoivreALT 11795 for an
alternate longer proof not using the exponential function. (Contributed
by NM, 24-Jul-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i ·
(sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) |
|
Theorem | demoivreALT 11795 |
Alternate proof of demoivre 11794. It is longer but does not use the
exponential function. This is Metamath 100 proof #17. (Contributed by
Steve Rodriguez, 10-Nov-2006.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) →
(((cos‘𝐴) + (i
· (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) |
|
4.9.1.1 The circle constant (tau = 2
pi)
|
|
Syntax | ctau 11796 |
Extend class notation to include the constant tau, τ =
6.28318....
|
class τ |
|
Definition | df-tau 11797 |
Define the circle constant tau, τ = 6.28318...,
which is the
smallest positive real number whose cosine is one. Various notations have
been used or proposed for this number including τ, a three-legged
variant of π, or 2π.
Note the difference between this
constant τ and the formula variable 𝜏.
Following our
convention, the constant is displayed in upright font while the variable
is in italic font; furthermore, the colors are different. (Contributed by
Jim Kingdon, 9-Apr-2018.) (Revised by AV, 1-Oct-2020.)
|
⊢ τ = inf((ℝ+ ∩
(◡cos “ {1})), ℝ, <
) |
|
4.9.2 _e is irrational
|
|
Theorem | eirraplem 11798* |
Lemma for eirrap 11799. (Contributed by Paul Chapman, 9-Feb-2008.)
(Revised by Jim Kingdon, 5-Jan-2022.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (1 /
(!‘𝑛))) & ⊢ (𝜑 → 𝑃 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℕ)
⇒ ⊢ (𝜑 → e # (𝑃 / 𝑄)) |
|
Theorem | eirrap 11799 |
e is irrational. That is, for any rational number,
e is apart
from it. In the absence of excluded middle, we can distinguish between
this and saying that e is not rational, which is
eirr 11800.
(Contributed by Jim Kingdon, 6-Jan-2023.)
|
⊢ (𝑄 ∈ ℚ → e # 𝑄) |
|
Theorem | eirr 11800 |
e is not rational. In the absence of excluded middle,
we can
distinguish between this and saying that e is
irrational in the
sense of being apart from any rational number, which is eirrap 11799.
(Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon,
6-Jan-2023.)
|
⊢ e ∉ ℚ |