P. 118 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11701-11800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sinval 11701	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 11702	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 11703	Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ sin:ℂ⟶ℂ
Theorem	cosf 11704	Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ cos:ℂ⟶ℂ
Theorem	sincl 11705	Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
Theorem	coscl 11706	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 11707	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 11708	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 11709	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ)
Theorem	coscld 11710	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ)
Theorem	tanclapd 11711	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (cos‘𝐴) # 0)    ⇒   ⊢ (𝜑 → (tan‘𝐴) ∈ ℂ)
Theorem	tanval2ap 11712	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 11713	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 11714	The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) = (ℑ‘(exp‘(i · 𝐴))))
Theorem	recosval 11715	The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = (ℜ‘(exp‘(i · 𝐴))))
Theorem	efi4p 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, 30-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = (((1 − ((𝐴↑2) / 2)) + (i · (𝐴 − ((𝐴↑3) / 6)))) + Σ𝑘 ∈ (ℤ≥‘4)(𝐹‘𝑘)))
Theorem	resin4p 11717*	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 11718*	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 11719	The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈ ℝ)
Theorem	recoscl 11720	The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ ℝ)
Theorem	retanclap 11721	The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ (cos‘𝐴) # 0) → (tan‘𝐴) ∈ ℝ)
Theorem	resincld 11722	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ)
Theorem	recoscld 11723	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℝ)
Theorem	retanclapd 11724	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (cos‘𝐴) # 0)    ⇒   ⊢ (𝜑 → (tan‘𝐴) ∈ ℝ)
Theorem	sinneg 11725	The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴))
Theorem	cosneg 11726	The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴))
Theorem	tannegap 11727	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 11728	Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)
⊢ (sin‘0) = 0
Theorem	cos0 11729	Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
⊢ (cos‘0) = 1
Theorem	tan0 11730	The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)
⊢ (tan‘0) = 0
Theorem	efival 11731	The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
Theorem	efmival 11732	The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.)
⊢ (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴))))
Theorem	efeul 11733	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 11734	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 11735	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 11736	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 11737	A useful intermediate step in tanaddap 11738 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 11738	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 11739	Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 − 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) − ((cos‘𝐴) · (sin‘𝐵))))
Theorem	cossub 11740	Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (cos‘(𝐴 − 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) + ((sin‘𝐴) · (sin‘𝐵))))
Theorem	addsin 11741	Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) + (sin‘𝐵)) = (2 · ((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2)))))
Theorem	subsin 11742	Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) − (sin‘𝐵)) = (2 · ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2)))))
Theorem	sinmul 11743	Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 11736 and cossub 11740. (Contributed by David A. Wheeler, 26-May-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (sin‘𝐵)) = (((cos‘(𝐴 − 𝐵)) − (cos‘(𝐴 + 𝐵))) / 2))
Theorem	cosmul 11744	Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 11736 and cossub 11740. (Contributed by David A. Wheeler, 26-May-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) · (cos‘𝐵)) = (((cos‘(𝐴 − 𝐵)) + (cos‘(𝐴 + 𝐵))) / 2))
Theorem	addcos 11745	Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) + (cos‘𝐵)) = (2 · ((cos‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2)))))
Theorem	subcos 11746	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 11747	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 11748	Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(2 · 𝐴)) = (2 · ((sin‘𝐴) · (cos‘𝐴))))
Theorem	cos2t 11749	Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(2 · 𝐴)) = ((2 · ((cos‘𝐴)↑2)) − 1))
Theorem	cos2tsin 11750	Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(2 · 𝐴)) = (1 − (2 · ((sin‘𝐴)↑2))))
Theorem	sinbnd 11751	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 11752	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 11753	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 11754	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 11755*	Lemma for sin01bnd 11756 and cos01bnd 11757. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ (0(,]1) → (abs‘Σ𝑘 ∈ (ℤ≥‘4)(𝐹‘𝑘)) < ((𝐴↑4) / 6))
Theorem	sin01bnd 11756	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 11757	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 11758	Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ ((1 / 3) < (cos‘1) ∧ (cos‘1) < (2 / 3))
Theorem	cos2bnd 11759	Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (-(7 / 9) < (cos‘2) ∧ (cos‘2) < -(1 / 9))
Theorem	sin01gt0 11760	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 11761	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 11762	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 11763	The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (0 < (sin‘1) ∧ 0 < (cos‘1))
Theorem	sincos2sgn 11764	The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (0 < (sin‘2) ∧ (cos‘2) < 0)
Theorem	sin4lt0 11765	The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (sin‘4) < 0
Theorem	cos12dec 11766	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 11767	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 11768	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 11769	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 11770	A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.)
⊢ ((𝐴 ∈ ℂ ∧ (exp‘(i · 𝐴)) = 1) → 𝐴 ∈ ℝ)
Theorem	demoivre 11771	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 11772 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
Theorem	demoivreALT 11772	Alternate proof of demoivre 11771. 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 11773	Extend class notation to include the constant tau, τ = 6.28318....
class τ
Definition	df-tau 11774	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 11775*	Lemma for eirrap 11776. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 5-Jan-2022.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))    &   ⊢ (𝜑 → 𝑃 ∈ ℤ)    &   ⊢ (𝜑 → 𝑄 ∈ ℕ)    ⇒   ⊢ (𝜑 → e # (𝑃 / 𝑄))
Theorem	eirrap 11776	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 11777. (Contributed by Jim Kingdon, 6-Jan-2023.)
⊢ (𝑄 ∈ ℚ → e # 𝑄)
Theorem	eirr 11777	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 11776. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 6-Jan-2023.)
⊢ e ∉ ℚ
Theorem	egt2lt3 11778	Euler's constant e = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Jim Kingdon, 7-Jan-2023.)
⊢ (2 < e ∧ e < 3)
Theorem	epos 11779	Euler's constant e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.)
⊢ 0 < e
Theorem	epr 11780	Euler's constant e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.)
⊢ e ∈ ℝ+
Theorem	ene0 11781	e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.)
⊢ e ≠ 0
Theorem	eap0 11782	e is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.)
⊢ e # 0
Theorem	ene1 11783	e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.)
⊢ e ≠ 1
Theorem	eap1 11784	e is apart from 1. (Contributed by Jim Kingdon, 7-Jan-2023.)
⊢ e # 1
PART 5  ELEMENTARY NUMBER THEORY This part introduces elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory.
5.1  Elementary properties of divisibility
5.1.1  The divides relation
Syntax	cdvds 11785	Extend the definition of a class to include the divides relation. See df-dvds 11786.
class ∥
Definition	df-dvds 11786*	Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
Theorem	divides 11787*	Define the divides relation. 𝑀 ∥ 𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 14253). As proven in dvdsval3 11789, 𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 11787 and dvdsval2 11788 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
Theorem	dvdsval2 11788	One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
Theorem	dvdsval3 11789	One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 15-Jul-2014.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0))
Theorem	dvdszrcl 11790	Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ (𝑋 ∥ 𝑌 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ))
Theorem	dvdsmod0 11791	If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑀 ∥ 𝑁) → (𝑁 mod 𝑀) = 0)
Theorem	p1modz1 11792	If a number greater than 1 divides another number, the second number increased by 1 is 1 modulo the first number. (Contributed by AV, 19-Mar-2022.)
⊢ ((𝑀 ∥ 𝐴 ∧ 1 < 𝑀) → ((𝐴 + 1) mod 𝑀) = 1)
Theorem	dvdsmodexp 11793	If a positive integer divides another integer, this other integer is equal to its positive powers modulo the positive integer. (Formerly part of the proof for fermltl 12224). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by AV, 19-Mar-2022.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∥ 𝐴) → ((𝐴↑𝐵) mod 𝑁) = (𝐴 mod 𝑁))
Theorem	nndivdvds 11794	Strong form of dvdsval2 11788 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵 ∥ 𝐴 ↔ (𝐴 / 𝐵) ∈ ℕ))
Theorem	nndivides 11795*	Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (𝑛 · 𝑀) = 𝑁))
Theorem	dvdsdc 11796	Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → DECID 𝑀 ∥ 𝑁)
Theorem	moddvds 11797	Two ways to say 𝐴≡𝐵 (mod 𝑁), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝐵)))
Theorem	modm1div 11798	An integer greater than one divides another integer minus one iff the second integer modulo the first integer is one. (Contributed by AV, 30-May-2023.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ) → ((𝐴 mod 𝑁) = 1 ↔ 𝑁 ∥ (𝐴 − 1)))
Theorem	dvds0lem 11799	A lemma to assist theorems of ∥ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 · 𝑀) = 𝑁) → 𝑀 ∥ 𝑁)
Theorem	dvds1lem 11800*	A lemma to assist theorems of ∥ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ))    &   ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑍 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝐽) = 𝐾 → (𝑍 · 𝑀) = 𝑁))    ⇒   ⊢ (𝜑 → (𝐽 ∥ 𝐾 → 𝑀 ∥ 𝑁))