![]() |
Metamath
Proof Explorer Theorem List (p. 268 of 481) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30606) |
![]() (30607-32129) |
![]() (32130-48006) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | quart1cl 26701 | Closure lemmas for quart 26708. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) & ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) & ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) ⇒ ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ)) | ||
Theorem | quart1lem 26702 | Lemma for quart1 26703. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) & ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) & ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑌 = (𝑋 + (𝐴 / 4))) ⇒ ⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅))) | ||
Theorem | quart1 26703 | Depress a quartic equation. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) & ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) & ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑌 = (𝑋 + (𝐴 / 4))) ⇒ ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅))) | ||
Theorem | quartlem1 26704 | Lemma for quart 26708. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝜑 → 𝑃 ∈ ℂ) & ⊢ (𝜑 → 𝑄 ∈ ℂ) & ⊢ (𝜑 → 𝑅 ∈ ℂ) & ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅))) & ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅)))) ⇒ ⊢ (𝜑 → (𝑈 = (((2 · 𝑃)↑2) − (3 · ((𝑃↑2) − (4 · 𝑅)))) ∧ 𝑉 = (((2 · ((2 · 𝑃)↑3)) − (9 · ((2 · 𝑃) · ((𝑃↑2) − (4 · 𝑅))))) + (;27 · -(𝑄↑2))))) | ||
Theorem | quartlem2 26705 | Closure lemmas for quart 26708. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐸 = -(𝐴 / 4)) & ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) & ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) & ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) & ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅))) & ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅)))) & ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3))))) ⇒ ⊢ (𝜑 → (𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ)) | ||
Theorem | quartlem3 26706 | Closure lemmas for quart 26708. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐸 = -(𝐴 / 4)) & ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) & ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) & ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) & ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅))) & ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅)))) & ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3))))) & ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2)) & ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3)) & ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))) & ⊢ (𝜑 → 𝑇 ≠ 0) ⇒ ⊢ (𝜑 → (𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ)) | ||
Theorem | quartlem4 26707 | Closure lemmas for quart 26708. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐸 = -(𝐴 / 4)) & ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) & ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) & ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) & ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅))) & ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅)))) & ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3))))) & ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2)) & ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3)) & ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))) & ⊢ (𝜑 → 𝑇 ≠ 0) & ⊢ (𝜑 → 𝑀 ≠ 0) & ⊢ (𝜑 → 𝐼 = (√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))) & ⊢ (𝜑 → 𝐽 = (√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))) ⇒ ⊢ (𝜑 → (𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ)) | ||
Theorem | quart 26708 | The quartic equation, writing out all roots using square and cube root functions so that only direct substitutions remain, and we can actually claim to have a "quartic equation". Naturally, this theorem is ridiculously long (see quartfull 34611) if all the substitutions are performed. This is Metamath 100 proof #46. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐸 = -(𝐴 / 4)) & ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) & ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) & ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) & ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅))) & ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅)))) & ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3))))) & ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2)) & ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3)) & ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))) & ⊢ (𝜑 → 𝑇 ≠ 0) & ⊢ (𝜑 → 𝑀 ≠ 0) & ⊢ (𝜑 → 𝐼 = (√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))) & ⊢ (𝜑 → 𝐽 = (√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))) ⇒ ⊢ (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((𝑋 = ((𝐸 − 𝑆) + 𝐼) ∨ 𝑋 = ((𝐸 − 𝑆) − 𝐼)) ∨ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽))))) | ||
Syntax | casin 26709 | The arcsine function. |
class arcsin | ||
Syntax | cacos 26710 | The arccosine function. |
class arccos | ||
Syntax | catan 26711 | The arctangent function. |
class arctan | ||
Definition | df-asin 26712 | Define the arcsine function. Because sin is not a one-to-one function, the literal inverse ◡sin is not a function. Rather than attempt to find the right domain on which to restrict sin in order to get a total function, we just define it in terms of log, which we already know is total (except at 0). There are branch points at -1 and 1 (at which the function is defined), and branch cuts along the real line not between -1 and 1, which is to say (-∞, -1) ∪ (1, +∞). (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) | ||
Definition | df-acos 26713 | Define the arccosine function. See also remarks for df-asin 26712. Since we define arccos in terms of arcsin, it shares the same branch points and cuts, namely (-∞, -1) ∪ (1, +∞). (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arccos = (𝑥 ∈ ℂ ↦ ((π / 2) − (arcsin‘𝑥))) | ||
Definition | df-atan 26714 | Define the arctangent function. See also remarks for df-asin 26712. Unlike arcsin and arccos, this function is not defined everywhere, because tan(𝑧) ≠ ±i for all 𝑧 ∈ ℂ. For all other 𝑧, there is a formula for arctan(𝑧) in terms of log, and we take that as the definition. Branch points are at ±i; branch cuts are on the pure imaginary axis not between -i and i, which is to say {𝑧 ∈ ℂ ∣ (i · 𝑧) ∈ (-∞, -1) ∪ (1, +∞)}. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arctan = (𝑥 ∈ (ℂ ∖ {-i, i}) ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥)))))) | ||
Theorem | asinlem 26715 | The argument to the logarithm in df-asin 26712 is always nonzero. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → ((i · 𝐴) + (√‘(1 − (𝐴↑2)))) ≠ 0) | ||
Theorem | asinlem2 26716 | The argument to the logarithm in df-asin 26712 has the property that replacing 𝐴 with -𝐴 in the expression gives the reciprocal. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (((i · 𝐴) + (√‘(1 − (𝐴↑2)))) · ((i · -𝐴) + (√‘(1 − (-𝐴↑2))))) = 1) | ||
Theorem | asinlem3a 26717 | Lemma for asinlem3 26718. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≤ 0) → 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) | ||
Theorem | asinlem3 26718 | The argument to the logarithm in df-asin 26712 has nonnegative real part. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) | ||
Theorem | asinf 26719 | Domain and codomain of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arcsin:ℂ⟶ℂ | ||
Theorem | asincl 26720 | Closure for the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘𝐴) ∈ ℂ) | ||
Theorem | acosf 26721 | Domain and codoamin of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arccos:ℂ⟶ℂ | ||
Theorem | acoscl 26722 | Closure for the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘𝐴) ∈ ℂ) | ||
Theorem | atandm 26723 | Since the property is a little lengthy, we abbreviate 𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i as 𝐴 ∈ dom arctan. This is the necessary precondition for the definition of arctan to make sense. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i)) | ||
Theorem | atandm2 26724 | This form of atandm 26723 is a bit more useful for showing that the logarithms in df-atan 26714 are well-defined. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0)) | ||
Theorem | atandm3 26725 | A compact form of atandm 26723. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (𝐴↑2) ≠ -1)) | ||
Theorem | atandm4 26726 | A compact form of atandm 26723. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ≠ 0)) | ||
Theorem | atanf 26727 | Domain and codoamin of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arctan:(ℂ ∖ {-i, i})⟶ℂ | ||
Theorem | atancl 26728 | Closure for the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan → (arctan‘𝐴) ∈ ℂ) | ||
Theorem | asinval 26729 | Value of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘𝐴) = (-i · (log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) | ||
Theorem | acosval 26730 | Value of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘𝐴) = ((π / 2) − (arcsin‘𝐴))) | ||
Theorem | atanval 26731 | Value of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan → (arctan‘𝐴) = ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))) | ||
Theorem | atanre 26732 | A real number is in the domain of the arctangent function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ dom arctan) | ||
Theorem | asinneg 26733 | The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘-𝐴) = -(arcsin‘𝐴)) | ||
Theorem | acosneg 26734 | The negative symmetry relation of the arccosine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘-𝐴) = (π − (arccos‘𝐴))) | ||
Theorem | efiasin 26735 | The exponential of the arcsine function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (exp‘(i · (arcsin‘𝐴))) = ((i · 𝐴) + (√‘(1 − (𝐴↑2))))) | ||
Theorem | sinasin 26736 | The arcsine function is an inverse to sin. This is the main property that justifies the notation arcsin or sin↑-1. Because sin is not an injection, the other converse identity asinsin 26739 is only true under limited circumstances. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (sin‘(arcsin‘𝐴)) = 𝐴) | ||
Theorem | cosacos 26737 | The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (cos‘(arccos‘𝐴)) = 𝐴) | ||
Theorem | asinsinlem 26738 | Lemma for asinsin 26739. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · 𝐴)))) | ||
Theorem | asinsin 26739 | The arcsine function composed with sin is equal to the identity. This plus sinasin 26736 allow to view sin and arcsin as inverse operations to each other. For ease of use, we have not defined precisely the correct domain of correctness of this identity; in addition to the main region described here it is also true for some points on the branch cuts, namely when 𝐴 = (π / 2) − i𝑦 for nonnegative real 𝑦 and also symmetrically at 𝐴 = i𝑦 − (π / 2). In particular, when restricted to reals this identity extends to the closed interval [-(π / 2), (π / 2)], not just the open interval (see reasinsin 26743). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = 𝐴) | ||
Theorem | acoscos 26740 | The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (0(,)π)) → (arccos‘(cos‘𝐴)) = 𝐴) | ||
Theorem | asin1 26741 | The arcsine of 1 is π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arcsin‘1) = (π / 2) | ||
Theorem | acos1 26742 | The arccosine of 1 is 0. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arccos‘1) = 0 | ||
Theorem | reasinsin 26743 | The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → (arcsin‘(sin‘𝐴)) = 𝐴) | ||
Theorem | asinsinb 26744 | Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arcsin‘𝐴) = 𝐵 ↔ (sin‘𝐵) = 𝐴)) | ||
Theorem | acoscosb 26745 | Relationship between cosine and arccosine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (0(,)π)) → ((arccos‘𝐴) = 𝐵 ↔ (cos‘𝐵) = 𝐴)) | ||
Theorem | asinbnd 26746 | The arcsine function has range within a vertical strip of the complex plane with real part between -π / 2 and π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘(arcsin‘𝐴)) ∈ (-(π / 2)[,](π / 2))) | ||
Theorem | acosbnd 26747 | The arccosine function has range within a vertical strip of the complex plane with real part between 0 and π. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘(arccos‘𝐴)) ∈ (0[,]π)) | ||
Theorem | asinrebnd 26748 | Bounds on the arcsine function. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arcsin‘𝐴) ∈ (-(π / 2)[,](π / 2))) | ||
Theorem | asinrecl 26749 | The arcsine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arcsin‘𝐴) ∈ ℝ) | ||
Theorem | acosrecl 26750 | The arccosine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arccos‘𝐴) ∈ ℝ) | ||
Theorem | cosasin 26751 | The cosine of the arcsine of 𝐴 is √(1 − 𝐴↑2). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (cos‘(arcsin‘𝐴)) = (√‘(1 − (𝐴↑2)))) | ||
Theorem | sinacos 26752 | The sine of the arccosine of 𝐴 is √(1 − 𝐴↑2). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (sin‘(arccos‘𝐴)) = (√‘(1 − (𝐴↑2)))) | ||
Theorem | atandmneg 26753 | The domain of the arctangent function is closed under negatives. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → -𝐴 ∈ dom arctan) | ||
Theorem | atanneg 26754 | The arctangent function is odd. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (arctan‘-𝐴) = -(arctan‘𝐴)) | ||
Theorem | atan0 26755 | The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (arctan‘0) = 0 | ||
Theorem | atandmcj 26756 | The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan → (∗‘𝐴) ∈ dom arctan) | ||
Theorem | atancj 26757 | The arctangent function distributes under conjugation. (The condition that ℜ(𝐴) ≠ 0 is necessary because the branch cuts are chosen so that the negative imaginary line "agrees with" neighboring values with negative real part, while the positive imaginary line agrees with values with positive real part. This makes atanneg 26754 true unconditionally but messes up conjugation symmetry, and it is impossible to have both in a single-valued function. The claim is true on the imaginary line between -1 and 1, though.) (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (𝐴 ∈ dom arctan ∧ (∗‘(arctan‘𝐴)) = (arctan‘(∗‘𝐴)))) | ||
Theorem | atanrecl 26758 | The arctangent function is real for all real inputs. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ ℝ) | ||
Theorem | efiatan 26759 | Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (exp‘(i · (arctan‘𝐴))) = ((√‘(1 + (i · 𝐴))) / (√‘(1 − (i · 𝐴))))) | ||
Theorem | atanlogaddlem 26760 | Lemma for atanlogadd 26761. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 0 ≤ (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log) | ||
Theorem | atanlogadd 26761 | The rule √(𝑧𝑤) = (√𝑧)(√𝑤) is not always true on the complex numbers, but it is true when the arguments of 𝑧 and 𝑤 sum to within the interval (-π, π], so there are some cases such as this one with 𝑧 = 1 + i𝐴 and 𝑤 = 1 − i𝐴 which are true unconditionally. This result can also be stated as "√(1 + 𝑧) + √(1 − 𝑧) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log) | ||
Theorem | atanlogsublem 26762 | Lemma for atanlogsub 26763. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴))))) ∈ (-π(,)π)) | ||
Theorem | atanlogsub 26763 | A variation on atanlogadd 26761, to show that √(1 + i𝑧) / √(1 − i𝑧) = √((1 + i𝑧) / (1 − i𝑧)) under more limited conditions. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ (ℜ‘𝐴) ≠ 0) → ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴)))) ∈ ran log) | ||
Theorem | efiatan2 26764 | Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (exp‘(i · (arctan‘𝐴))) = ((1 + (i · 𝐴)) / (√‘(1 + (𝐴↑2))))) | ||
Theorem | 2efiatan 26765 | Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (exp‘(2 · (i · (arctan‘𝐴)))) = (((2 · i) / (𝐴 + i)) − 1)) | ||
Theorem | tanatan 26766 | The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (tan‘(arctan‘𝐴)) = 𝐴) | ||
Theorem | atandmtan 26767 | The tangent function has range contained in the domain of the arctangent. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ dom arctan) | ||
Theorem | cosatan 26768 | The cosine of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) = (1 / (√‘(1 + (𝐴↑2))))) | ||
Theorem | cosatanne0 26769 | The arctangent function has range contained in the domain of the tangent. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) ≠ 0) | ||
Theorem | atantan 26770 | The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴) | ||
Theorem | atantanb 26771 | Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arctan‘𝐴) = 𝐵 ↔ (tan‘𝐵) = 𝐴)) | ||
Theorem | atanbndlem 26772 | Lemma for atanbnd 26773. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ (𝐴 ∈ ℝ+ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2))) | ||
Theorem | atanbnd 26773 | The arctangent function is bounded by π / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2))) | ||
Theorem | atanord 26774 | The arctangent function is strictly increasing. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (arctan‘𝐴) < (arctan‘𝐵))) | ||
Theorem | atan1 26775 | The arctangent of 1 is π / 4. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arctan‘1) = (π / 4) | ||
Theorem | bndatandm 26776 | A point in the open unit disk is in the domain of the arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ dom arctan) | ||
Theorem | atans 26777* | The "domain of continuity" of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ∈ 𝐷)) | ||
Theorem | atans2 26778* | It suffices to show that 1 − i𝐴 and 1 + i𝐴 are in the continuity domain of log to show that 𝐴 is in the continuity domain of arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ∈ 𝐷 ∧ (1 + (i · 𝐴)) ∈ 𝐷)) | ||
Theorem | atansopn 26779* | The domain of continuity of the arctangent is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ 𝑆 ∈ (TopOpen‘ℂfld) | ||
Theorem | atansssdm 26780* | The domain of continuity of the arctangent is a subset of the actual domain of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ 𝑆 ⊆ dom arctan | ||
Theorem | ressatans 26781* | The real number line is a subset of the domain of continuity of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ ℝ ⊆ 𝑆 | ||
Theorem | dvatan 26782* | The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (ℂ D (arctan ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / (1 + (𝑥↑2)))) | ||
Theorem | atancn 26783* | The arctangent is a continuous function. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (arctan ↾ 𝑆) ∈ (𝑆–cn→ℂ) | ||
Theorem | atantayl 26784* | The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴)) | ||
Theorem | atantayl2 26785* | The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, ((-1↑((𝑛 − 1) / 2)) · ((𝐴↑𝑛) / 𝑛)))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴)) | ||
Theorem | atantayl3 26786* | The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , 𝐹) ⇝ (arctan‘𝐴)) | ||
Theorem | leibpilem1 26787 | Lemma for leibpi 26789. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by Steven Nguyen, 23-Mar-2023.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (¬ 𝑁 = 0 ∧ ¬ 2 ∥ 𝑁)) → (𝑁 ∈ ℕ ∧ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | leibpilem2 26788* | The Leibniz formula for π. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))) & ⊢ 𝐺 = (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘))) & ⊢ 𝐴 ∈ V ⇒ ⊢ (seq0( + , 𝐹) ⇝ 𝐴 ↔ seq0( + , 𝐺) ⇝ 𝐴) | ||
Theorem | leibpi 26789 | The Leibniz formula for π. This proof depends on three main facts: (1) the series 𝐹 is convergent, because it is an alternating series (iseralt 15627). (2) Using leibpilem2 26788 to rewrite the series as a power series, it is the 𝑥 = 1 special case of the Taylor series for arctan (atantayl2 26785). (3) Although we cannot directly plug 𝑥 = 1 into atantayl2 26785, Abel's theorem (abelth2 26295) says that the limit along any sequence converging to 1, such as 1 − 1 / 𝑛, of the power series converges to the power series extended to 1, and then since arctan is continuous at 1 (atancn 26783) we get the desired result. This is Metamath 100 proof #26. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))) ⇒ ⊢ seq0( + , 𝐹) ⇝ (π / 4) | ||
Theorem | leibpisum 26790 | The Leibniz formula for π. This version of leibpi 26789 looks nicer but does not assert that the series is convergent so is not as practically useful. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ Σ𝑛 ∈ ℕ0 ((-1↑𝑛) / ((2 · 𝑛) + 1)) = (π / 4) | ||
Theorem | log2cnv 26791 | Using the Taylor series for arctan(i / 3), produce a rapidly convergent series for log2. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ⇒ ⊢ seq0( + , 𝐹) ⇝ (log‘2) | ||
Theorem | log2tlbnd 26792* | Bound the error term in the series of log2cnv 26791. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))) | ||
Theorem | log2ublem1 26793 | Lemma for log2ub 26796. The proof of log2ub 26796, which is simply the evaluation of log2tlbnd 26792 for 𝑁 = 4, takes the form of the addition of five fractions and showing this is less than another fraction. We could just perform exact arithmetic on these fractions, get a large rational number, and just multiply everything to verify the claim, but as anyone who uses decimal numbers for this task knows, it is often better to pick a common denominator 𝑑 (usually a large power of 10) and work with the closest approximations of the form 𝑛 / 𝑑 for some integer 𝑛 instead. It turns out that for our purposes it is sufficient to take 𝑑 = (3↑7) · 5 · 7, which is also nice because it shares many factors in common with the fractions in question. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ (((3↑7) · (5 · 7)) · 𝐴) ≤ 𝐵 & ⊢ 𝐴 ∈ ℝ & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐶 = (𝐴 + (𝐷 / 𝐸)) & ⊢ (𝐵 + 𝐹) = 𝐺 & ⊢ (((3↑7) · (5 · 7)) · 𝐷) ≤ (𝐸 · 𝐹) ⇒ ⊢ (((3↑7) · (5 · 7)) · 𝐶) ≤ 𝐺 | ||
Theorem | log2ublem2 26794* | Lemma for log2ub 26796. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐵) & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ (𝑁 − 1) = 𝐾 & ⊢ (𝐵 + 𝐹) = 𝐺 & ⊢ 𝑀 ∈ ℕ0 & ⊢ (𝑀 + 𝑁) = 3 & ⊢ ((5 · 7) · (9↑𝑀)) = (((2 · 𝑁) + 1) · 𝐹) ⇒ ⊢ (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐺) | ||
Theorem | log2ublem3 26795 | Lemma for log2ub 26796. In decimal, this is a proof that the first four terms of the series for log2 is less than 53056 / 76545. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.) |
⊢ (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ ;;;;53056 | ||
Theorem | log2ub 26796 | log2 is less than 253 / 365. If written in decimal, this is because log2 = 0.693147... is less than 253/365 = 0.693151... , so this is a very tight bound, at five decimal places. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.) |
⊢ (log‘2) < (;;253 / ;;365) | ||
Theorem | log2le1 26797 | log2 is less than 1. This is just a weaker form of log2ub 26796 when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ (log‘2) < 1 | ||
Theorem | birthdaylem1 26798* | Lemma for birthday 26801. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} & ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} ⇒ ⊢ (𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ (𝑁 ∈ ℕ → 𝑆 ≠ ∅)) | ||
Theorem | birthdaylem2 26799* | For general 𝑁 and 𝐾, count the fraction of injective functions from 1...𝐾 to 1...𝑁. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} & ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘𝑇) / (♯‘𝑆)) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁))))) | ||
Theorem | birthdaylem3 26800* | For general 𝑁 and 𝐾, upper-bound the fraction of injective functions from 1...𝐾 to 1...𝑁. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} & ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} ⇒ ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → ((♯‘𝑇) / (♯‘𝑆)) ≤ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |