Home | Intuitionistic Logic Explorer Theorem List (p. 115 of 133) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cosf 11401 | Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ cos:ℂ⟶ℂ | ||
Theorem | sincl 11402 | Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ) | ||
Theorem | coscl 11403 | 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 11404 | 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 11405 | 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 11406 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ) | ||
Theorem | coscld 11407 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ) | ||
Theorem | tanclapd 11408 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (cos‘𝐴) # 0) ⇒ ⊢ (𝜑 → (tan‘𝐴) ∈ ℂ) | ||
Theorem | tanval2ap 11409 | 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 11410 | 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 11411 | The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) = (ℑ‘(exp‘(i · 𝐴)))) | ||
Theorem | recosval 11412 | The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = (ℜ‘(exp‘(i · 𝐴)))) | ||
Theorem | efi4p 11413* | 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 11414* | 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 11415* | 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 11416 | The sine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈ ℝ) | ||
Theorem | recoscl 11417 | The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ ℝ) | ||
Theorem | retanclap 11418 | The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ (cos‘𝐴) # 0) → (tan‘𝐴) ∈ ℝ) | ||
Theorem | resincld 11419 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ) | ||
Theorem | recoscld 11420 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (cos‘𝐴) ∈ ℝ) | ||
Theorem | retanclapd 11421 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (cos‘𝐴) # 0) ⇒ ⊢ (𝜑 → (tan‘𝐴) ∈ ℝ) | ||
Theorem | sinneg 11422 | The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴)) | ||
Theorem | cosneg 11423 | The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴)) | ||
Theorem | tannegap 11424 | 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 11425 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
⊢ (sin‘0) = 0 | ||
Theorem | cos0 11426 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
⊢ (cos‘0) = 1 | ||
Theorem | tan0 11427 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
⊢ (tan‘0) = 0 | ||
Theorem | efival 11428 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴)))) | ||
Theorem | efmival 11429 | The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴)))) | ||
Theorem | efeul 11430 | 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 11431 | 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 11432 | 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 11433 | 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 11434 | A useful intermediate step in tanaddap 11435 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 11435 | 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 11436 | Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 − 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) − ((cos‘𝐴) · (sin‘𝐵)))) | ||
Theorem | cossub 11437 | Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (cos‘(𝐴 − 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) + ((sin‘𝐴) · (sin‘𝐵)))) | ||
Theorem | addsin 11438 | Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) + (sin‘𝐵)) = (2 · ((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))))) | ||
Theorem | subsin 11439 | Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) − (sin‘𝐵)) = (2 · ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2))))) | ||
Theorem | sinmul 11440 | Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 11433 and cossub 11437. (Contributed by David A. Wheeler, 26-May-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (sin‘𝐵)) = (((cos‘(𝐴 − 𝐵)) − (cos‘(𝐴 + 𝐵))) / 2)) | ||
Theorem | cosmul 11441 | Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 11433 and cossub 11437. (Contributed by David A. Wheeler, 26-May-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) · (cos‘𝐵)) = (((cos‘(𝐴 − 𝐵)) + (cos‘(𝐴 + 𝐵))) / 2)) | ||
Theorem | addcos 11442 | Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) + (cos‘𝐵)) = (2 · ((cos‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))))) | ||
Theorem | subcos 11443 | 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 11444 | 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 11445 | Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘(2 · 𝐴)) = (2 · ((sin‘𝐴) · (cos‘𝐴)))) | ||
Theorem | cos2t 11446 | Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘(2 · 𝐴)) = ((2 · ((cos‘𝐴)↑2)) − 1)) | ||
Theorem | cos2tsin 11447 | Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘(2 · 𝐴)) = (1 − (2 · ((sin‘𝐴)↑2)))) | ||
Theorem | sinbnd 11448 | 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 11449 | 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 11450 | 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 11451 | 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 11452* | Lemma for sin01bnd 11453 and cos01bnd 11454. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ (0(,]1) → (abs‘Σ𝑘 ∈ (ℤ≥‘4)(𝐹‘𝑘)) < ((𝐴↑4) / 6)) | ||
Theorem | sin01bnd 11453 | 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 11454 | 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 11455 | Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ ((1 / 3) < (cos‘1) ∧ (cos‘1) < (2 / 3)) | ||
Theorem | cos2bnd 11456 | Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ (-(7 / 9) < (cos‘2) ∧ (cos‘2) < -(1 / 9)) | ||
Theorem | sin01gt0 11457 | 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 11458 | 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 11459 | 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 11460 | The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ (0 < (sin‘1) ∧ 0 < (cos‘1)) | ||
Theorem | sincos2sgn 11461 | The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ (0 < (sin‘2) ∧ (cos‘2) < 0) | ||
Theorem | sin4lt0 11462 | The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ (sin‘4) < 0 | ||
Theorem | cos12dec 11463 | 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 11464 | 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 11465 | 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 11466 | 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 11467 | A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ (exp‘(i · 𝐴)) = 1) → 𝐴 ∈ ℝ) | ||
Theorem | demoivre 11468 | 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 11469 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) | ||
Theorem | demoivreALT 11469 | Alternate proof of demoivre 11468. 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‘(𝑁 · 𝐴))))) | ||
Syntax | ctau 11470 | Extend class notation to include the constant tau, τ = 6.28318.... |
class τ | ||
Definition | df-tau 11471 | 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})), ℝ, < ) | ||
Theorem | eirraplem 11472* | Lemma for eirrap 11473. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 5-Jan-2022.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛))) & ⊢ (𝜑 → 𝑃 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℕ) ⇒ ⊢ (𝜑 → e # (𝑃 / 𝑄)) | ||
Theorem | eirrap 11473 | 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 11474. (Contributed by Jim Kingdon, 6-Jan-2023.) |
⊢ (𝑄 ∈ ℚ → e # 𝑄) | ||
Theorem | eirr 11474 | 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 11473. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 6-Jan-2023.) |
⊢ e ∉ ℚ | ||
Theorem | egt2lt3 11475 | 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 11476 | Euler's constant e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.) |
⊢ 0 < e | ||
Theorem | epr 11477 | Euler's constant e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.) |
⊢ e ∈ ℝ+ | ||
Theorem | ene0 11478 | e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.) |
⊢ e ≠ 0 | ||
Theorem | eap0 11479 | e is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.) |
⊢ e # 0 | ||
Theorem | ene1 11480 | e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.) |
⊢ e ≠ 1 | ||
Theorem | eap1 11481 | e is apart from 1. (Contributed by Jim Kingdon, 7-Jan-2023.) |
⊢ e # 1 | ||
Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory. | ||
Syntax | cdvds 11482 | Extend the definition of a class to include the divides relation. See df-dvds 11483. |
class ∥ | ||
Definition | df-dvds 11483* | Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ∥ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)} | ||
Theorem | divides 11484* | Define the divides relation. 𝑀 ∥ 𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 12931). As proven in dvdsval3 11486, 𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 11484 and dvdsval2 11485 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁)) | ||
Theorem | dvdsval2 11485 | 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 11486 | 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 11487 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ (𝑋 ∥ 𝑌 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) | ||
Theorem | nndivdvds 11488 | Strong form of dvdsval2 11485 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵 ∥ 𝐴 ↔ (𝐴 / 𝐵) ∈ ℕ)) | ||
Theorem | nndivides 11489* | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (𝑛 · 𝑀) = 𝑁)) | ||
Theorem | dvdsdc 11490 | Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → DECID 𝑀 ∥ 𝑁) | ||
Theorem | moddvds 11491 | Two ways to say 𝐴≡𝐵 (mod 𝑁), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝐵))) | ||
Theorem | dvds0lem 11492 | A lemma to assist theorems of ∥ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 · 𝑀) = 𝑁) → 𝑀 ∥ 𝑁) | ||
Theorem | dvds1lem 11493* | A lemma to assist theorems of ∥ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) & ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑍 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝐽) = 𝐾 → (𝑍 · 𝑀) = 𝑁)) ⇒ ⊢ (𝜑 → (𝐽 ∥ 𝐾 → 𝑀 ∥ 𝑁)) | ||
Theorem | dvds2lem 11494* | A lemma to assist theorems of ∥ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ)) & ⊢ (𝜑 → (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) & ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑍 ∈ ℤ) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑥 · 𝐼) = 𝐽 ∧ (𝑦 · 𝐾) = 𝐿) → (𝑍 · 𝑀) = 𝑁)) ⇒ ⊢ (𝜑 → ((𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿) → 𝑀 ∥ 𝑁)) | ||
Theorem | iddvds 11495 | An integer divides itself. Theorem 1.1(a) in [ApostolNT] p. 14 (reflexive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 𝑁) | ||
Theorem | 1dvds 11496 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → 1 ∥ 𝑁) | ||
Theorem | dvds0 11497 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 0) | ||
Theorem | negdvdsb 11498 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ -𝑀 ∥ 𝑁)) | ||
Theorem | dvdsnegb 11499 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ -𝑁)) | ||
Theorem | absdvdsb 11500 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ 𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |