Home | Metamath
Proof Explorer Theorem List (p. 247 of 426) | < 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | acosf 24601 | Domain and range of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arccos:ℂ⟶ℂ | ||
Theorem | acoscl 24602 | Closure for the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘𝐴) ∈ ℂ) | ||
Theorem | atandm 24603 | 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 24604 | This form of atandm 24603 is a bit more useful for showing that the logarithms in df-atan 24594 are well-defined. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0)) | ||
Theorem | atandm3 24605 | A compact form of atandm 24603. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (𝐴↑2) ≠ -1)) | ||
Theorem | atandm4 24606 | A compact form of atandm 24603. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ≠ 0)) | ||
Theorem | atanf 24607 | Domain and range of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arctan:(ℂ ∖ {-i, i})⟶ℂ | ||
Theorem | atancl 24608 | Closure for the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan → (arctan‘𝐴) ∈ ℂ) | ||
Theorem | asinval 24609 | Value of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘𝐴) = (-i · (log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) | ||
Theorem | acosval 24610 | Value of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘𝐴) = ((π / 2) − (arcsin‘𝐴))) | ||
Theorem | atanval 24611 | 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 24612 | A real number is in the domain of the arctangent function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ dom arctan) | ||
Theorem | asinneg 24613 | The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘-𝐴) = -(arcsin‘𝐴)) | ||
Theorem | acosneg 24614 | The negative symmetry relation of the arccosine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘-𝐴) = (π − (arccos‘𝐴))) | ||
Theorem | efiasin 24615 | The exponential of the arcsine function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (exp‘(i · (arcsin‘𝐴))) = ((i · 𝐴) + (√‘(1 − (𝐴↑2))))) | ||
Theorem | sinasin 24616 | 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 24619 is only true under limited circumstances. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (sin‘(arcsin‘𝐴)) = 𝐴) | ||
Theorem | cosacos 24617 | The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (cos‘(arccos‘𝐴)) = 𝐴) | ||
Theorem | asinsinlem 24618 | Lemma for asinsin 24619. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · 𝐴)))) | ||
Theorem | asinsin 24619 | The arcsine function composed with sin is equal to the identity. This plus sinasin 24616 allow us 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 24623). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = 𝐴) | ||
Theorem | acoscos 24620 | The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (0(,)π)) → (arccos‘(cos‘𝐴)) = 𝐴) | ||
Theorem | asin1 24621 | The arcsine of 1 is π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arcsin‘1) = (π / 2) | ||
Theorem | acos1 24622 | The arcsine of 1 is π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arccos‘1) = 0 | ||
Theorem | reasinsin 24623 | The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → (arcsin‘(sin‘𝐴)) = 𝐴) | ||
Theorem | asinsinb 24624 | Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arcsin‘𝐴) = 𝐵 ↔ (sin‘𝐵) = 𝐴)) | ||
Theorem | acoscosb 24625 | Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (0(,)π)) → ((arccos‘𝐴) = 𝐵 ↔ (cos‘𝐵) = 𝐴)) | ||
Theorem | asinbnd 24626 | 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 24627 | 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 24628 | Bounds on the arcsine function. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arcsin‘𝐴) ∈ (-(π / 2)[,](π / 2))) | ||
Theorem | asinrecl 24629 | The arcsine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arcsin‘𝐴) ∈ ℝ) | ||
Theorem | acosrecl 24630 | The arccosine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arccos‘𝐴) ∈ ℝ) | ||
Theorem | cosasin 24631 | The cosine of the arcsine of 𝐴 is √(1 − 𝐴↑2). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (cos‘(arcsin‘𝐴)) = (√‘(1 − (𝐴↑2)))) | ||
Theorem | sinacos 24632 | The sine of the arccosine of 𝐴 is √(1 − 𝐴↑2). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (sin‘(arccos‘𝐴)) = (√‘(1 − (𝐴↑2)))) | ||
Theorem | atandmneg 24633 | The domain of the arctangent function is closed under negatives. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → -𝐴 ∈ dom arctan) | ||
Theorem | atanneg 24634 | The arctangent function is odd. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (arctan‘-𝐴) = -(arctan‘𝐴)) | ||
Theorem | atan0 24635 | The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (arctan‘0) = 0 | ||
Theorem | atandmcj 24636 | The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan → (∗‘𝐴) ∈ dom arctan) | ||
Theorem | atancj 24637 | 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 24634 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 24638 | The arctangent function is real for all real inputs. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ ℝ) | ||
Theorem | efiatan 24639 | 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 24640 | Lemma for atanlogadd 24641. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 0 ≤ (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log) | ||
Theorem | atanlogadd 24641 | 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 24642 | Lemma for atanlogsub 24643. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴))))) ∈ (-π(,)π)) | ||
Theorem | atanlogsub 24643 | A variation on atanlogadd 24641, 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 24644 | 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 24645 | 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 24646 | The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (tan‘(arctan‘𝐴)) = 𝐴) | ||
Theorem | atandmtan 24647 | 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 24648 | The cosine of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) = (1 / (√‘(1 + (𝐴↑2))))) | ||
Theorem | cosatanne0 24649 | 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 24650 | The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴) | ||
Theorem | atantanb 24651 | Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arctan‘𝐴) = 𝐵 ↔ (tan‘𝐵) = 𝐴)) | ||
Theorem | atanbndlem 24652 | Lemma for atanbnd 24653. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ (𝐴 ∈ ℝ+ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2))) | ||
Theorem | atanbnd 24653 | The arctangent function is bounded by π / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2))) | ||
Theorem | atanord 24654 | The arctangent function is strictly increasing. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (arctan‘𝐴) < (arctan‘𝐵))) | ||
Theorem | atan1 24655 | The arctangent of 1 is π / 4. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arctan‘1) = (π / 4) | ||
Theorem | bndatandm 24656 | 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 24657* | The "domain of continuity" of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ∈ 𝐷)) | ||
Theorem | atans2 24658* | 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 24659* | 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 24660* | 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 24661* | 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 24662* | The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (ℂ D (arctan ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / (1 + (𝑥↑2)))) | ||
Theorem | atancn 24663* | The arctangent is a continuous function. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐷 = (ℂ ∖ (-∞(,]0)) & ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} ⇒ ⊢ (arctan ↾ 𝑆) ∈ (𝑆–cn→ℂ) | ||
Theorem | atantayl 24664* | The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴)) | ||
Theorem | atantayl2 24665* | The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, ((-1↑((𝑛 − 1) / 2)) · ((𝐴↑𝑛) / 𝑛)))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴)) | ||
Theorem | atantayl3 24666* | The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1)))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , 𝐹) ⇝ (arctan‘𝐴)) | ||
Theorem | leibpilem1 24667 | Lemma for leibpi 24669. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (¬ 𝑁 = 0 ∧ ¬ 2 ∥ 𝑁)) → (𝑁 ∈ ℕ ∧ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | leibpilem2 24668* | 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 24669 | The Leibniz formula for π. This proof depends on three main facts: (1) the series 𝐹 is convergent, because it is an alternating series (iseralt 14415). (2) Using leibpilem2 24668 to rewrite the series as a power series, it is the 𝑥 = 1 special case of the Taylor series for arctan (atantayl2 24665). (3) Although we cannot directly plug 𝑥 = 1 into atantayl2 24665, Abel's theorem (abelth2 24196) 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 24663) 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 24670 | The Leibniz formula for π. This version of leibpi 24669 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 24671 | 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 24672* | Bound the error term in the series of log2cnv 24671. (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 24673 | Lemma for log2ub 24676. The proof of log2ub 24676, which is simply the evaluation of log2tlbnd 24672 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 24674* | Lemma for log2ub 24676. (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 24675 | Lemma for log2ub 24676. 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 24676 | 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 24677 | log2 is less than 1. This is just a weaker form of log2ub 24676 when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ (log‘2) < 1 | ||
Theorem | birthdaylem1 24678* | Lemma for birthday 24681. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} & ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} ⇒ ⊢ (𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ (𝑁 ∈ ℕ → 𝑆 ≠ ∅)) | ||
Theorem | birthdaylem2 24679* | 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 24680* | 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) / 𝑁))) | ||
Theorem | birthday 24681* | The Birthday Problem. There is a more than even chance that out of 23 people in a room, at least two of them have the same birthday. Mathematically, this is asserting that for 𝐾 = 23 and 𝑁 = 365, fewer than half of the set of all functions from 1...𝐾 to 1...𝑁 are injective. This is Metamath 100 proof #93. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)} & ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)} & ⊢ 𝐾 = ;23 & ⊢ 𝑁 = ;;365 ⇒ ⊢ ((#‘𝑇) / (#‘𝑆)) < (1 / 2) | ||
Syntax | carea 24682 | Area of regions in the complex plane. |
class area | ||
Definition | df-area 24683* | Define the area of a subset of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ area = (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥) | ||
Theorem | dmarea 24684* | The domain of the area function is the set of finitely measurable subsets of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝐴 ∈ dom area ↔ (𝐴 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1)) | ||
Theorem | areambl 24685 | The fibers of a measurable region are finitely measurable subsets of ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ ((𝑆 ∈ dom area ∧ 𝐴 ∈ ℝ) → ((𝑆 “ {𝐴}) ∈ dom vol ∧ (vol‘(𝑆 “ {𝐴})) ∈ ℝ)) | ||
Theorem | areass 24686 | A measurable region is a subset of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝑆 ∈ dom area → 𝑆 ⊆ (ℝ × ℝ)) | ||
Theorem | dfarea 24687* | Rewrite df-area 24683 self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ area = (𝑠 ∈ dom area ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥) | ||
Theorem | areaf 24688 | Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ area:dom area⟶(0[,)+∞) | ||
Theorem | areacl 24689 | The area of a measurable region is a real number. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝑆 ∈ dom area → (area‘𝑆) ∈ ℝ) | ||
Theorem | areage0 24690 | The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝑆 ∈ dom area → 0 ≤ (area‘𝑆)) | ||
Theorem | areaval 24691* | The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥) | ||
Theorem | rlimcnp 24692* | Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞)) & ⊢ (𝜑 → 0 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ ℝ+) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) & ⊢ (𝑥 = 0 → 𝑅 = 𝐶) & ⊢ (𝑥 = (1 / 𝑦) → 𝑅 = 𝑆) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐴) ⇒ ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0))) | ||
Theorem | rlimcnp2 24693* | Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞)) & ⊢ (𝜑 → 0 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴)) & ⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐴) ⇒ ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) | ||
Theorem | rlimcnp3 24694* | Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑆 ∈ ℂ) & ⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t (0[,)+∞)) ⇒ ⊢ (𝜑 → ((𝑦 ∈ ℝ+ ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))) | ||
Theorem | xrlimcnp 24695* | Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +∞. Since any ⇝𝑟 limit can be written in the form on the left side of the implication, this shows that real limits are a special case of topological continuity at a point. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ (𝜑 → 𝐴 = (𝐵 ∪ {+∞})) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) & ⊢ (𝑥 = +∞ → 𝑅 = 𝐶) & ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = ((ordTop‘ ≤ ) ↾t 𝐴) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))) | ||
Theorem | efrlim 24696* | The limit of the sequence (1 + 𝐴 / 𝑘)↑𝑘 is the exponential function. This is often taken as an alternate definition of the exponential function (see also dfef2 24697). (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ 𝑆 = (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1))) ⇒ ⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℝ+ ↦ ((1 + (𝐴 / 𝑘))↑𝑐𝑘)) ⇝𝑟 (exp‘𝐴)) | ||
Theorem | dfef2 24697* | The limit of the sequence (1 + 𝐴 / 𝑘)↑𝑘 as 𝑘 goes to +∞ is (exp‘𝐴). This is another common definition of e. (Contributed by Mario Carneiro, 1-Mar-2015.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = ((1 + (𝐴 / 𝑘))↑𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ (exp‘𝐴)) | ||
Theorem | cxplim 24698* | A power to a negative exponent goes to zero as the base becomes large. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Mario Carneiro, 18-May-2016.) |
⊢ (𝐴 ∈ ℝ+ → (𝑛 ∈ ℝ+ ↦ (1 / (𝑛↑𝑐𝐴))) ⇝𝑟 0) | ||
Theorem | sqrtlim 24699 | The inverse square root function converges to zero. (Contributed by Mario Carneiro, 18-May-2016.) |
⊢ (𝑛 ∈ ℝ+ ↦ (1 / (√‘𝑛))) ⇝𝑟 0 | ||
Theorem | rlimcxp 24700* | Any power to a positive exponent of a converging sequence also converges. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ⇝𝑟 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |