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