P. 150 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14901-15000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	coscl 14901	Closure of the cosine function with a complex argument. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
Theorem	tanval 14902	Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
Theorem	tancl 14903	The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℂ)
Theorem	sincld 14904	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ)
Theorem	coscld 14905	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ)
Theorem	tancld 14906	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (cos‘𝐴) ≠ 0)    ⇒   ⊢ (𝜑 → (tan‘𝐴) ∈ ℂ)
Theorem	tanval2 14907	Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (i · ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))))))
Theorem	tanval3 14908	Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℂ ∧ ((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (tan‘𝐴) = (((exp‘(2 · (i · 𝐴))) − 1) / (i · ((exp‘(2 · (i · 𝐴))) + 1))))
Theorem	resinval 14909	The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) = (ℑ‘(exp‘(i · 𝐴))))
Theorem	recosval 14910	The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = (ℜ‘(exp‘(i · 𝐴))))
Theorem	efi4p 14911*	Separate out the first four terms of the infinite series expansion of the exponential function of an imaginary number. (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 14912*	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 14913*	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 14914	The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈ ℝ)
Theorem	recoscl 14915	The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ ℝ)
Theorem	retancl 14916	The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℝ)
Theorem	resincld 14917	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ)
Theorem	recoscld 14918	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℝ)
Theorem	retancld 14919	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (cos‘𝐴) ≠ 0)    ⇒   ⊢ (𝜑 → (tan‘𝐴) ∈ ℝ)
Theorem	sinneg 14920	The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴))
Theorem	cosneg 14921	The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴))
Theorem	tanneg 14922	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 14923	Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)
⊢ (sin‘0) = 0
Theorem	cos0 14924	Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
⊢ (cos‘0) = 1
Theorem	tan0 14925	The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)
⊢ (tan‘0) = 0
Theorem	efival 14926	The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
Theorem	efmival 14927	The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.)
⊢ (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴))))
Theorem	sinhval 14928	Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℂ → ((sin‘(i · 𝐴)) / i) = (((exp‘𝐴) − (exp‘-𝐴)) / 2))
Theorem	coshval 14929	Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (cos‘(i · 𝐴)) = (((exp‘𝐴) + (exp‘-𝐴)) / 2))
Theorem	resinhcl 14930	The hyperbolic sine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → ((sin‘(i · 𝐴)) / i) ∈ ℝ)
Theorem	rpcoshcl 14931	The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → (cos‘(i · 𝐴)) ∈ ℝ+)
Theorem	recoshcl 14932	The hyperbolic cosine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → (cos‘(i · 𝐴)) ∈ ℝ)
Theorem	retanhcl 14933	The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) ∈ ℝ)
Theorem	tanhlt1 14934	The hyperbolic tangent of a real number is upper bounded by 1. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) < 1)
Theorem	tanhbnd 14935	The hyperbolic tangent of a real number is bounded by 1. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) ∈ (-1(,)1))
Theorem	efeul 14936	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 14937	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 14938	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 14939	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	tanaddlem 14940	A useful intermediate step in tanadd 14941 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((cos‘𝐴) ≠ 0 ∧ (cos‘𝐵) ≠ 0)) → ((cos‘(𝐴 + 𝐵)) ≠ 0 ↔ ((tan‘𝐴) · (tan‘𝐵)) ≠ 1))
Theorem	tanadd 14941	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 14942	Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 − 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) − ((cos‘𝐴) · (sin‘𝐵))))
Theorem	cossub 14943	Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (cos‘(𝐴 − 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) + ((sin‘𝐴) · (sin‘𝐵))))
Theorem	addsin 14944	Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) + (sin‘𝐵)) = (2 · ((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2)))))
Theorem	subsin 14945	Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) − (sin‘𝐵)) = (2 · ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2)))))
Theorem	sinmul 14946	Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 14939 and cossub 14943. (Contributed by David A. Wheeler, 26-May-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (sin‘𝐵)) = (((cos‘(𝐴 − 𝐵)) − (cos‘(𝐴 + 𝐵))) / 2))
Theorem	cosmul 14947	Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 14939 and cossub 14943. (Contributed by David A. Wheeler, 26-May-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) · (cos‘𝐵)) = (((cos‘(𝐴 − 𝐵)) + (cos‘(𝐴 + 𝐵))) / 2))
Theorem	addcos 14948	Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) + (cos‘𝐵)) = (2 · ((cos‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2)))))
Theorem	subcos 14949	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 14950	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 14951	Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(2 · 𝐴)) = (2 · ((sin‘𝐴) · (cos‘𝐴))))
Theorem	cos2t 14952	Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(2 · 𝐴)) = ((2 · ((cos‘𝐴)↑2)) − 1))
Theorem	cos2tsin 14953	Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(2 · 𝐴)) = (1 − (2 · ((sin‘𝐴)↑2))))
Theorem	sinbnd 14954	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 14955	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 14956	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 14957	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 14958*	Lemma for sin01bnd 14959 and cos01bnd 14960. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ (0(,]1) → (abs‘Σ𝑘 ∈ (ℤ≥‘4)(𝐹‘𝑘)) < ((𝐴↑4) / 6))
Theorem	sin01bnd 14959	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 14960	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 14961	Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ ((1 / 3) < (cos‘1) ∧ (cos‘1) < (2 / 3))
Theorem	cos2bnd 14962	Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (-(7 / 9) < (cos‘2) ∧ (cos‘2) < -(1 / 9))
Theorem	sinltx 14963	The sine of a positive real number is less than its argument. (Contributed by Mario Carneiro, 29-Jul-2014.)
⊢ (𝐴 ∈ ℝ+ → (sin‘𝐴) < 𝐴)
Theorem	sin01gt0 14964	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 14965	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 14966	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 14967	The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (0 < (sin‘1) ∧ 0 < (cos‘1))
Theorem	sincos2sgn 14968	The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (0 < (sin‘2) ∧ (cos‘2) < 0)
Theorem	sin4lt0 14969	The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (sin‘4) < 0
Theorem	absefi 14970	The absolute value of the exponential function 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 14971	The absolute value of the exponential function is the exponential function of the real part. (Contributed by Paul Chapman, 13-Sep-2007.)
⊢ (𝐴 ∈ ℂ → (abs‘(exp‘𝐴)) = (exp‘(ℜ‘𝐴)))
Theorem	absefib 14972	A number is real iff its imaginary exponential has absolute value one. (Contributed by NM, 21-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (abs‘(exp‘(i · 𝐴))) = 1))
Theorem	efieq1re 14973	A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.)
⊢ ((𝐴 ∈ ℂ ∧ (exp‘(i · 𝐴)) = 1) → 𝐴 ∈ ℝ)
Theorem	demoivre 14974	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 14975 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
Theorem	demoivreALT 14975	Alternate proof of demoivre 14974. 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‘(𝑁 · 𝐴)))))
5.11.2  _e is irrational
Theorem	eirrlem 14976*	Lemma for eirr 14977. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))    &   ⊢ (𝜑 → 𝑃 ∈ ℤ)    &   ⊢ (𝜑 → 𝑄 ∈ ℕ)    &   ⊢ (𝜑 → e = (𝑃 / 𝑄))    ⇒   ⊢ ¬ 𝜑
Theorem	eirr 14977	e is irrational. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
⊢ e ∉ ℚ
Theorem	egt2lt3 14978	Euler's constant e = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
⊢ (2 < e ∧ e < 3)
Theorem	epos 14979	Euler's constant e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.)
⊢ 0 < e
Theorem	epr 14980	Euler's constant e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.)
⊢ e ∈ ℝ+
Theorem	ene0 14981	e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.)
⊢ e ≠ 0
Theorem	ene1 14982	e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.)
⊢ e ≠ 1
5.12  Cardinality of real and complex number subsets
5.12.1  Countability of integers and rationals
Theorem	xpnnen 14983	The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 9-Mar-2013.)
⊢ (ℕ × ℕ) ≈ ℕ
Theorem	znnenlem 14984	Lemma for znnen 14985. (Contributed by NM, 31-Jul-2004.)
⊢ (((0 ≤ 𝑥 ∧ ¬ 0 ≤ 𝑦) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 = 𝑦 ↔ (2 · 𝑥) = ((-2 · 𝑦) + 1)))
Theorem	znnen 14985	The set of integers and the set of positive integers are equinumerous. Exercise 1 of [Gleason] p. 140. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 13-Jun-2014.)
⊢ ℤ ≈ ℕ
Theorem	qnnen 14986	The rational numbers are countable. This proof does not use the Axiom of Choice, even though it uses an onto function, because the base set (ℤ × ℕ) is numerable. Exercise 2 of [Enderton] p. 133. For purposes of the Metamath 100 list, we are considering Mario Carneiro's revision as the date this proof was completed. This is Metamath 100 proof #3. (Contributed by NM, 31-Jul-2004.) (Revised by Mario Carneiro, 3-Mar-2013.)
⊢ ℚ ≈ ℕ
5.12.2  The reals are uncountable
Theorem	rpnnen2lem1 14987*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐹‘𝐴)‘𝑁) = if(𝑁 ∈ 𝐴, ((1 / 3)↑𝑁), 0))
Theorem	rpnnen2lem2 14988*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ (𝐴 ⊆ ℕ → (𝐹‘𝐴):ℕ⟶ℝ)
Theorem	rpnnen2lem3 14989*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ seq1( + , (𝐹‘ℕ)) ⇝ (1 / 2)
Theorem	rpnnen2lem4 14990*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 31-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ) → (0 ≤ ((𝐹‘𝐴)‘𝑘) ∧ ((𝐹‘𝐴)‘𝑘) ≤ ((𝐹‘𝐵)‘𝑘)))
Theorem	rpnnen2lem5 14991*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → seq𝑀( + , (𝐹‘𝐴)) ∈ dom ⇝ )
Theorem	rpnnen2lem6 14992*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐴)‘𝑘) ∈ ℝ)
Theorem	rpnnen2lem7 14993*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐴)‘𝑘) ≤ Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐵)‘𝑘))
Theorem	rpnnen2lem8 14994*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → Σ𝑘 ∈ ℕ ((𝐹‘𝐴)‘𝑘) = (Σ𝑘 ∈ (1...(𝑀 − 1))((𝐹‘𝐴)‘𝑘) + Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐴)‘𝑘)))
Theorem	rpnnen2lem9 14995*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = (0 + (((1 / 3)↑(𝑀 + 1)) / (1 − (1 / 3)))))
Theorem	rpnnen2lem10 14996*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑚 ∈ (𝐴 ∖ 𝐵))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵)))    &   ⊢ (𝜓 ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝐵)‘𝑘))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘))
Theorem	rpnnen2lem11 14997*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑚 ∈ (𝐴 ∖ 𝐵))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵)))    &   ⊢ (𝜓 ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝐵)‘𝑘))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	rpnnen2lem12 14998*	Lemma for rpnnen2 14999. (Contributed by Mario Carneiro, 13-May-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ 𝒫 ℕ ≼ (0[,]1)
Theorem	rpnnen2 14999	The other half of rpnnen 15000, where we show an injection from sets of positive integers to real numbers. The obvious choice for this is binary expansion, but it has the unfortunate property that it does not produce an injection on numbers which end with all 0's or all 1's (the more well-known decimal version of this is 0.999... 14656). Instead, we opt for a ternary expansion, which produces (a scaled version of) the Cantor set. Since the Cantor set is riddled with gaps, we can show that any two sequences that are not equal must differ somewhere, and when they do, they are placed a finite distance apart, thus ensuring that the map is injective. Our map assigns to each subset 𝐴 of the positive integers the number Σ𝑘 ∈ 𝐴(3↑-𝑘) = Σ𝑘 ∈ ℕ((𝐹‘𝐴)‘𝑘), where ((𝐹‘𝐴)‘𝑘) = if(𝑘 ∈ 𝐴, (3↑-𝑘), 0)) (rpnnen2lem1 14987). This is an infinite sum of real numbers (rpnnen2lem2 14988), and since 𝐴 ⊆ 𝐵 implies (𝐹‘𝐴) ≤ (𝐹‘𝐵) (rpnnen2lem4 14990) and (𝐹‘ℕ) converges to 1 / 2 (rpnnen2lem3 14989) by geoisum1 14654, the sum is convergent to some real (rpnnen2lem5 14991 and rpnnen2lem6 14992) by the comparison test for convergence cvgcmp 14592. The comparison test also tells us that 𝐴 ⊆ 𝐵 implies Σ(𝐹‘𝐴) ≤ Σ(𝐹‘𝐵) (rpnnen2lem7 14993). Putting it all together, if we have two sets 𝑥 ≠ 𝑦, there must differ somewhere, and so there must be an 𝑚 such that ∀𝑛 < 𝑚(𝑛 ∈ 𝑥 ↔ 𝑛 ∈ 𝑦) but 𝑚 ∈ (𝑥 ∖ 𝑦) or vice versa. In this case, we split off the first 𝑚 − 1 terms (rpnnen2lem8 14994) and cancel them (rpnnen2lem10 14996), since these are the same for both sets. For the remaining terms, we use the subset property to establish that Σ(𝐹‘𝑦) ≤ Σ(𝐹‘(ℕ ∖ {𝑚})) and Σ(𝐹‘{𝑚}) ≤ Σ(𝐹‘𝑥) (where these sums are only over (ℤ≥‘𝑚)), and since Σ(𝐹‘(ℕ ∖ {𝑚})) = (3↑-𝑚) / 2 (rpnnen2lem9 14995) and Σ(𝐹‘{𝑚}) = (3↑-𝑚), we establish that Σ(𝐹‘𝑦) < Σ(𝐹‘𝑥) (rpnnen2lem11 14997) so that they must be different. By contraposition (rpnnen2lem12 14998), we find that this map is an injection. (Contributed by Mario Carneiro, 13-May-2013.) (Proof shortened by Mario Carneiro, 30-Apr-2014.) (Revised by NM, 17-Aug-2021.)
⊢ 𝒫 ℕ ≼ (0[,]1)
Theorem	rpnnen 15000	The cardinality of the continuum is the same as the powerset of ω. This is a stronger statement than ruc 15016, which only asserts that ℝ is uncountable, i.e. has a cardinality larger than ω. The main proof is in two parts, rpnnen1 11858 and rpnnen2 14999, each showing an injection in one direction, and this last part uses sbth 8121 to prove that the sets are equinumerous. By constructing explicit injections, we avoid the use of AC. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ℝ ≈ 𝒫 ℕ