P. 119 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11801-11900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fprodsplitsn 11801*	Separate out a term in a finite product. See also fprodunsn 11772 which is the same but with a distinct variable condition in place of Ⅎ𝑘𝜑. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝐷    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (𝐴 ∪ {𝐵})𝐶 = (∏𝑘 ∈ 𝐴 𝐶 · 𝐷))
Theorem	fprodsplit1f 11802*	Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → Ⅎ𝑘𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐶) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (𝐷 · ∏𝑘 ∈ (𝐴 ∖ {𝐶})𝐵))
Theorem	fprodclf 11803*	Closure of a finite product of complex numbers. A version of fprodcl 11775 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
Theorem	fprodap0f 11804*	A finite product of terms apart from zero is apart from zero. A version of fprodap0 11789 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 # 0)
Theorem	fprodge0 11805*	If all the terms of a finite product are nonnegative, so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ ∏𝑘 ∈ 𝐴 𝐵)
Theorem	fprodeq0g 11806*	Any finite product containing a zero term is itself zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐶) → 𝐵 = 0)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0)
Theorem	fprodge1 11807*	If all of the terms of a finite product are greater than or equal to 1, so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 1 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 1 ≤ ∏𝑘 ∈ 𝐴 𝐵)
Theorem	fprodle 11808*	If all the terms of two finite products are nonnegative and compare, so do the two products. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ≤ ∏𝑘 ∈ 𝐴 𝐶)
Theorem	fprodmodd 11809*	If all factors of two finite products are equal modulo 𝑀, the products are equal modulo 𝑀. (Contributed by AV, 7-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 mod 𝑀) = (𝐶 mod 𝑀))    ⇒   ⊢ (𝜑 → (∏𝑘 ∈ 𝐴 𝐵 mod 𝑀) = (∏𝑘 ∈ 𝐴 𝐶 mod 𝑀))
4.10  Elementary trigonometry
4.10.1  The exponential, sine, and cosine functions
Syntax	ce 11810	Extend class notation to include the exponential function.
class exp
Syntax	ceu 11811	Extend class notation to include Euler's constant e = 2.71828....
class e
Syntax	csin 11812	Extend class notation to include the sine function.
class sin
Syntax	ccos 11813	Extend class notation to include the cosine function.
class cos
Syntax	ctan 11814	Extend class notation to include the tangent function.
class tan
Syntax	cpi 11815	Extend class notation to include the constant pi, π = 3.14159....
class π
Definition	df-ef 11816*	Define the exponential function. Its value at the complex number 𝐴 is (exp‘𝐴) and is called the "exponential of 𝐴"; see efval 11829. (Contributed by NM, 14-Mar-2005.)
⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘)))
Definition	df-e 11817	Define Euler's constant e = 2.71828.... (Contributed by NM, 14-Mar-2005.)
⊢ e = (exp‘1)
Definition	df-sin 11818	Define the sine function. (Contributed by NM, 14-Mar-2005.)
⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
Definition	df-cos 11819	Define the cosine function. (Contributed by NM, 14-Mar-2005.)
⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2))
Definition	df-tan 11820	Define the tangent function. We define it this way for cmpt 4095, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥)))
Definition	df-pi 11821	Define the constant pi, π = 3.14159..., which is the smallest positive number whose sine is zero. Definition of π in [Gleason] p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV, 14-Sep-2020.)
⊢ π = inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < )
Theorem	eftcl 11822	Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℂ)
Theorem	reeftcl 11823	The terms of the series expansion of the exponential function at a real number are real. (Contributed by Paul Chapman, 15-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℝ)
Theorem	eftabs 11824	The absolute value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 23-Nov-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → (abs‘((𝐴↑𝐾) / (!‘𝐾))) = (((abs‘𝐴)↑𝐾) / (!‘𝐾)))
Theorem	eftvalcn 11825*	The value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 8-Dec-2022.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐹‘𝑁) = ((𝐴↑𝑁) / (!‘𝑁)))
Theorem	efcllemp 11826*	Lemma for efcl 11832. The series that defines the exponential function converges. The ratio test cvgratgt0 11701 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 11827*	Lemma for efcl 11832. 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 11828*	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 11829*	Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 ((𝐴↑𝑘) / (!‘𝑘)))
Theorem	esum 11830	Value of Euler's constant e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.)
⊢ e = Σ𝑘 ∈ ℕ0 (1 / (!‘𝑘))
Theorem	eff 11831	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 11832	Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ)
Theorem	efval2 11833*	Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 (𝐹‘𝑘))
Theorem	efcvg 11834*	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 11835*	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 11836	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 11837	The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ)
Theorem	ere 11838	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 11839	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 11840	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 11841	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 11842*	Lemma for efadd 11843 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛)))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
Theorem	efadd 11843	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 11844	Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.)
⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) · (exp‘-𝐴)) = 1)
Theorem	efap0 11845	The exponential of a complex number is apart from zero. (Contributed by Jim Kingdon, 12-Dec-2022.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) # 0)
Theorem	efne0 11846	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 11845 (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 11847	The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.)
⊢ (𝐴 ∈ ℂ → (exp‘-𝐴) = (1 / (exp‘𝐴)))
Theorem	eff2 11848	The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
⊢ exp:ℂ⟶(ℂ ∖ {0})
Theorem	efsub 11849	Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	efexp 11850	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 11851	Value of the exponential function for integers. Special case of efval 11829. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁))
Theorem	efgt0 11852	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 11853	The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈ ℝ+)
Theorem	rpefcld 11854	The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ+)
Theorem	eftlcvg 11855*	The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Theorem	eftlcl 11856*	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 11857*	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 11858*	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 11859*	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 11860*	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 11861	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 11862*	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 11863	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 11864	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 11865	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 11866	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 11867	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 11868	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 11869	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 11870	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 11871	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 11872	Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ sin:ℂ⟶ℂ
Theorem	cosf 11873	Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ cos:ℂ⟶ℂ
Theorem	sincl 11874	Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
Theorem	coscl 11875	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 11876	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 11877	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 11878	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ)
Theorem	coscld 11879	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ)
Theorem	tanclapd 11880	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (cos‘𝐴) # 0)    ⇒   ⊢ (𝜑 → (tan‘𝐴) ∈ ℂ)
Theorem	tanval2ap 11881	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 11882	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 11883	The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) = (ℑ‘(exp‘(i · 𝐴))))
Theorem	recosval 11884	The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = (ℜ‘(exp‘(i · 𝐴))))
Theorem	efi4p 11885*	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 11886*	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 11887*	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 11888	The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈ ℝ)
Theorem	recoscl 11889	The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ ℝ)
Theorem	retanclap 11890	The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ (cos‘𝐴) # 0) → (tan‘𝐴) ∈ ℝ)
Theorem	resincld 11891	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ)
Theorem	recoscld 11892	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℝ)
Theorem	retanclapd 11893	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (cos‘𝐴) # 0)    ⇒   ⊢ (𝜑 → (tan‘𝐴) ∈ ℝ)
Theorem	sinneg 11894	The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴))
Theorem	cosneg 11895	The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴))
Theorem	tannegap 11896	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 11897	Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)
⊢ (sin‘0) = 0
Theorem	cos0 11898	Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
⊢ (cos‘0) = 1
Theorem	tan0 11899	The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)
⊢ (tan‘0) = 0
Theorem	efival 11900	The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))