Home | Metamath
Proof Explorer Theorem List (p. 376 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | int-mulcomd 37501 | MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) = (𝐶 · 𝐴)) | ||
Theorem | int-mulassocd 37502 | MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · 𝐷)) | ||
Theorem | int-mulsimpd 37503 | MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → 1 = (𝐴 / 𝐵)) | ||
Theorem | int-leftdistd 37504 | AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ((𝐶 + 𝐷) · 𝐵) = ((𝐶 · 𝐴) + (𝐷 · 𝐴))) | ||
Theorem | int-rightdistd 37505 | AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐵 · (𝐶 + 𝐷)) = ((𝐴 · 𝐶) + (𝐴 · 𝐷))) | ||
Theorem | int-sqdefd 37506 | SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐴↑2)) | ||
Theorem | int-mul11d 37507 | First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 · 1) = 𝐵) | ||
Theorem | int-mul12d 37508 | Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (1 · 𝐴) = 𝐵) | ||
Theorem | int-add01d 37509 | First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐵) | ||
Theorem | int-add02d 37510 | Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐵) | ||
Theorem | int-sqgeq0d 37511 | SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵)) | ||
Theorem | int-eqprincd 37512 | PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐷)) | ||
Theorem | int-eqtransd 37513 | EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | int-eqmvtd 37514 | EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐵 − 𝐷)) | ||
Theorem | int-eqineqd 37515 | EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝐴) | ||
Theorem | int-ineqmvtd 37516 | IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → (𝐵 − 𝐷) ≤ 𝐶) | ||
Theorem | int-ineq1stprincd 37517 | FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐷 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 + 𝐷) ≤ (𝐴 + 𝐶)) | ||
Theorem | int-ineq2ndprincd 37518 | SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐵 · 𝐶) ≤ (𝐴 · 𝐶)) | ||
Theorem | int-ineqtransd 37519 | InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ≤ 𝐴) | ||
This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 11388 addcomli 10107 00id 10090 addid1i 10102 addid2i 10103 eqid 2610 dec0h 11398 decadd 11446 decaddc 11448. | ||
Theorem | unitadd 37520 | Theorem used in conjunction with decaddc 11448 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.) |
⊢ (𝐴 + 𝐵) = 𝐹 & ⊢ (𝐶 + 1) = 𝐵 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ ((𝐴 + 𝐶) + 1) = 𝐹 | ||
Theorem | gsumws3 37521 | Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵))) → (𝐺 Σg 〈“𝑆𝑇𝑈”〉) = (𝑆 + (𝑇 + 𝑈))) | ||
Theorem | gsumws4 37522 | Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑆 ∈ 𝐵 ∧ (𝑇 ∈ 𝐵 ∧ (𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)))) → (𝐺 Σg 〈“𝑆𝑇𝑈𝑉”〉) = (𝑆 + (𝑇 + (𝑈 + 𝑉)))) | ||
Theorem | amgm2d 37523 | Arithmetic-geometric mean inequality for 𝑛 = 2, derived from amgmlem 24516. (Contributed by Stanislas Polu, 8-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑐(1 / 2)) ≤ ((𝐴 + 𝐵) / 2)) | ||
Theorem | amgm3d 37524 | Arithmetic-geometric mean inequality for 𝑛 = 3. (Contributed by Stanislas Polu, 11-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · 𝐶))↑𝑐(1 / 3)) ≤ ((𝐴 + (𝐵 + 𝐶)) / 3)) | ||
Theorem | amgm4d 37525 | Arithmetic-geometric mean inequality for 𝑛 = 4. (Contributed by Stanislas Polu, 11-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · (𝐵 · (𝐶 · 𝐷)))↑𝑐(1 / 4)) ≤ ((𝐴 + (𝐵 + (𝐶 + 𝐷))) / 4)) | ||
Theorem | nanorxor 37526 | 'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ⊻ 𝜓))) | ||
Theorem | undisjrab 37527 | Union of two disjoint restricted class abstractions; compare unrab 3857. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ∅ ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ⊻ 𝜓)}) | ||
Theorem | iso0 37528 | The empty set is an 𝑅, 𝑆 isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
⊢ ∅ Isom 𝑅, 𝑆 (∅, ∅) | ||
Theorem | ssrecnpr 37529 | ℝ is a subset of both ℝ and ℂ. (Contributed by Steve Rodriguez, 22-Nov-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → ℝ ⊆ 𝑆) | ||
Theorem | seff 37530 | Let set 𝑆 be the real or complex numbers. Then the exponential function restricted to 𝑆 is a mapping from 𝑆 to 𝑆. (Contributed by Steve Rodriguez, 6-Nov-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) ⇒ ⊢ (𝜑 → (exp ↾ 𝑆):𝑆⟶𝑆) | ||
Theorem | sblpnf 37531 | The infinity ball in the absolute value metric is just the whole space. 𝑆 analogue of blpnf 22012. (Contributed by Steve Rodriguez, 8-Nov-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆) | ||
Theorem | prmunb2 37532* | The primes are unbounded. This generalizes prmunb 15456 to real 𝐴 with arch 11166 and lttrd 10077: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝐴 ∈ ℝ → ∃𝑝 ∈ ℙ 𝐴 < 𝑝) | ||
Theorem | dvgrat 37533* | Ratio test for divergence of a complex infinite series. See e.g. remark "if (abs‘((𝑎‘(𝑛 + 1)) / (𝑎‘𝑛))) ≥ 1 for all large n..." in https://en.wikipedia.org/wiki/Ratio_test#The_test. (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘(𝐹‘𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1)))) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) ∉ dom ⇝ ) | ||
Theorem | cvgdvgrat 37534* |
Ratio test for convergence and divergence of a complex infinite series.
If the ratio 𝑅 of the absolute values of successive
terms in an
infinite sequence 𝐹 converges to less than one, then the
infinite
sum of the terms of 𝐹 converges to a complex number; and
if 𝑅
converges greater then the sum diverges. This combined form of
cvgrat 14454 and dvgrat 37533 directly uses the limit of the ratio.
(It also demonstrates how to use climi2 14090 and absltd 14016 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191, and how to use r19.29a 3060 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3013 at https://groups.google.com/forum/#!topic/metamath/2RPikOiXLMo.) (Contributed by Steve Rodriguez, 28-Feb-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0) & ⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) & ⊢ (𝜑 → 𝑅 ⇝ 𝐿) & ⊢ (𝜑 → 𝐿 ≠ 1) ⇒ ⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ )) | ||
Theorem | radcnvrat 37535* | Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 37534) as 𝑘 increases. Then the radius of convergence of power series Σ𝑛 ∈ ℕ0((𝐴‘𝑛) · (𝑥↑𝑛)) is (1 / 𝐿) if 𝐿 is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐷 = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0) & ⊢ (𝜑 → 𝐷 ⇝ 𝐿) & ⊢ (𝜑 → 𝐿 ≠ 0) ⇒ ⊢ (𝜑 → 𝑅 = (1 / 𝐿)) | ||
Theorem | reldvds 37536 | The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ Rel ∥ | ||
Theorem | nznngen 37537 | All positive integers in the set of multiples of n, nℤ, are the absolute value of n or greater. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑁}) ∩ ℕ) ⊆ (ℤ≥‘(abs‘𝑁))) | ||
Theorem | nzss 37538 | The set of multiples of m, mℤ, is a subset of those of n, nℤ, iff n divides m. Lemma 2.1(a) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑀}) ⊆ ( ∥ “ {𝑁}) ↔ 𝑁 ∥ 𝑀)) | ||
Theorem | nzin 37539 | The intersection of the set of multiples of m, mℤ, and those of n, nℤ, is the set of multiples of their least common multiple. Roughly Lemma 2.1(c) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5 and Problem 1(b) of https://people.math.binghamton.edu/mazur/teach/40107/40107h16sol.pdf p. 1, with mℤ and nℤ as images of the divides relation under m and n. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑀}) ∩ ( ∥ “ {𝑁})) = ( ∥ “ {(𝑀 lcm 𝑁)})) | ||
Theorem | nzprmdif 37540 | Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℙ) & ⊢ (𝜑 → 𝑀 ≠ 𝑁) ⇒ ⊢ (𝜑 → (( ∥ “ {𝑀}) ∖ ( ∥ “ {𝑁})) = (( ∥ “ {𝑀}) ∖ ( ∥ “ {(𝑀 · 𝑁)}))) | ||
Theorem | hashnzfz 37541 | Special case of hashdvds 15318: the count of multiples in nℤ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘(𝐽 − 1))) ⇒ ⊢ (𝜑 → (#‘(( ∥ “ {𝑁}) ∩ (𝐽...𝐾))) = ((⌊‘(𝐾 / 𝑁)) − (⌊‘((𝐽 − 1) / 𝑁)))) | ||
Theorem | hashnzfz2 37542 | Special case of hashnzfz 37541: the count of multiples in nℤ, n greater than one, restricted to an interval starting at two. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ ℕ) ⇒ ⊢ (𝜑 → (#‘(( ∥ “ {𝑁}) ∩ (2...𝐾))) = (⌊‘(𝐾 / 𝑁))) | ||
Theorem | hashnzfzclim 37543* | As the upper bound 𝐾 of the constraint interval (𝐽...𝐾) in hashnzfz 37541 increases, the resulting count of multiples tends to (𝐾 / 𝑀) —that is, there are approximately (𝐾 / 𝑀) multiples of 𝑀 in a finite interval of integers. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦ ((#‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘)) ⇝ (1 / 𝑀)) | ||
Theorem | caofcan 37544* | Transfer a cancellation law like mulcan 10543 to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑇) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦) = (𝑥𝑅𝑧) ↔ 𝑦 = 𝑧)) ⇒ ⊢ (𝜑 → ((𝐹 ∘𝑓 𝑅𝐺) = (𝐹 ∘𝑓 𝑅𝐻) ↔ 𝐺 = 𝐻)) | ||
Theorem | ofsubid 37545 | Function analogue of subid 10179. (Contributed by Steve Rodriguez, 5-Nov-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) → (𝐹 ∘𝑓 − 𝐹) = (𝐴 × {0})) | ||
Theorem | ofmul12 37546 | Function analogue of mul12 10081. (Contributed by Steve Rodriguez, 13-Nov-2015.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → (𝐹 ∘𝑓 · (𝐺 ∘𝑓 · 𝐻)) = (𝐺 ∘𝑓 · (𝐹 ∘𝑓 · 𝐻))) | ||
Theorem | ofdivrec 37547 | Function analogue of divrec 10580, a division analogue of ofnegsub 10895. (Contributed by Steve Rodriguez, 3-Nov-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → (𝐹 ∘𝑓 · ((𝐴 × {1}) ∘𝑓 / 𝐺)) = (𝐹 ∘𝑓 / 𝐺)) | ||
Theorem | ofdivcan4 37548 | Function analogue of divcan4 10591. (Contributed by Steve Rodriguez, 4-Nov-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → ((𝐹 ∘𝑓 · 𝐺) ∘𝑓 / 𝐺) = 𝐹) | ||
Theorem | ofdivdiv2 37549 | Function analogue of divdiv2 10616. (Contributed by Steve Rodriguez, 23-Nov-2015.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → (𝐹 ∘𝑓 / (𝐺 ∘𝑓 / 𝐻)) = ((𝐹 ∘𝑓 · 𝐻) ∘𝑓 / 𝐺)) | ||
Theorem | lhe4.4ex1a 37550 | Example of the Fundamental Theorem of Calculus, part two (ftc2 23611): ∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 23611 as simply the "Fundamental Theorem of Calculus", then ftc1 23609 as the "Second Fundamental Theorem of Calculus".) (Contributed by Steve Rodriguez, 28-Oct-2015.) (Revised by Steve Rodriguez, 31-Oct-2015.) |
⊢ ∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3) | ||
Theorem | dvsconst 37551 | Derivative of a constant function on the real or complex numbers. The function may return a complex 𝐴 even if 𝑆 is ℝ. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐴 ∈ ℂ) → (𝑆 D (𝑆 × {𝐴})) = (𝑆 × {0})) | ||
Theorem | dvsid 37552 | Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D ( I ↾ 𝑆)) = (𝑆 × {1})) | ||
Theorem | dvsef 37553 | Derivative of the exponential function on the real or complex numbers. (Contributed by Steve Rodriguez, 12-Nov-2015.) |
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D (exp ↾ 𝑆)) = (exp ↾ 𝑆)) | ||
Theorem | expgrowthi 37554* | Exponential growth and decay model. See expgrowth 37556 for more information. (Contributed by Steve Rodriguez, 4-Nov-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐾 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡)))) ⇒ ⊢ (𝜑 → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘𝑓 · 𝑌)) | ||
Theorem | dvconstbi 37555* | The derivative of a function on 𝑆 is zero iff it is a constant function. Roughly a biconditional 𝑆 analogue of dvconst 23486 and dveq0 23567. Corresponds to integration formula "∫0 d𝑥 = 𝐶 " in section 4.1 of [LarsonHostetlerEdwards] p. 278. (Contributed by Steve Rodriguez, 11-Nov-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝑌:𝑆⟶ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝑌) = 𝑆) ⇒ ⊢ (𝜑 → ((𝑆 D 𝑌) = (𝑆 × {0}) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑆 × {𝑐}))) | ||
Theorem | expgrowth 37556* |
Exponential growth and decay model. The derivative of a function y of
variable t equals a constant k times y itself, iff
y equals some
constant C times the exponential of kt. This theorem and
expgrowthi 37554 illustrate one of the simplest and most
crucial classes of
differential equations, equations that relate functions to their
derivatives.
Section 6.3 of [Strang] p. 242 calls y' = ky "the most important differential equation in applied mathematics". In the field of population ecology it is known as the Malthusian growth model or exponential law, and C, k, and t correspond to initial population size, growth rate, and time respectively (https://en.wikipedia.org/wiki/Malthusian_growth_model); and in finance, the model appears in a similar role in continuous compounding with C as the initial amount of money. In exponential decay models, k is often expressed as the negative of a positive constant λ. Here y' is given as (𝑆 D 𝑌), C as 𝑐, and ky as ((𝑆 × {𝐾}) ∘𝑓 · 𝑌). (𝑆 × {𝐾}) is the constant function that maps any real or complex input to k and ∘𝑓 · is multiplication as a function operation. The leftward direction of the biconditional is as given in http://www.saylor.org/site/wp-content/uploads/2011/06/MA221-2.1.1.pdf pp. 1-2, which also notes the reverse direction ("While we will not prove this here, it turns out that these are the only functions that satisfy this equation."). The rightward direction is Theorem 5.1 of [LarsonHostetlerEdwards] p. 375 (which notes " C is the initial value of y, and k is the proportionality constant. Exponential growth occurs when k > 0, and exponential decay occurs when k < 0."); its proof here closely follows the proof of y' = y in https://proofwiki.org/wiki/Exponential_Growth_Equation/Special_Case. Statements for this and expgrowthi 37554 formulated by Mario Carneiro. (Contributed by Steve Rodriguez, 24-Nov-2015.) |
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) & ⊢ (𝜑 → 𝐾 ∈ ℂ) & ⊢ (𝜑 → 𝑌:𝑆⟶ℂ) & ⊢ (𝜑 → dom (𝑆 D 𝑌) = 𝑆) ⇒ ⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘𝑓 · 𝑌) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡)))))) | ||
Syntax | cbcc 37557 | Extend class notation to include the generalized binomial coefficient operation. |
class C𝑐 | ||
Definition | df-bcc 37558* | Define a generalized binomial coefficient operation, which unlike df-bc 12952 allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ C𝑐 = (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘))) | ||
Theorem | bccval 37559 | Value of the generalized binomial coefficient, 𝐶 choose 𝐾. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶C𝑐𝐾) = ((𝐶 FallFac 𝐾) / (!‘𝐾))) | ||
Theorem | bcccl 37560 | Closure of the generalized binomial coefficient. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶C𝑐𝐾) ∈ ℂ) | ||
Theorem | bcc0 37561 | The generalized binomial coefficient 𝐶 choose 𝐾 is zero iff 𝐶 is an integer between zero and (𝐾 − 1) inclusive. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐶C𝑐𝐾) = 0 ↔ 𝐶 ∈ (0...(𝐾 − 1)))) | ||
Theorem | bccp1k 37562 | Generalized binomial coefficient: 𝐶 choose (𝐾 + 1). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐶C𝑐(𝐾 + 1)) = ((𝐶C𝑐𝐾) · ((𝐶 − 𝐾) / (𝐾 + 1)))) | ||
Theorem | bccm1k 37563 | Generalized binomial coefficient: 𝐶 choose (𝐾 − 1), when 𝐶 is not (𝐾 − 1). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ (ℂ ∖ {(𝐾 − 1)})) & ⊢ (𝜑 → 𝐾 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐶C𝑐(𝐾 − 1)) = ((𝐶C𝑐𝐾) / ((𝐶 − (𝐾 − 1)) / 𝐾))) | ||
Theorem | bccn0 37564 | Generalized binomial coefficient: 𝐶 choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶C𝑐0) = 1) | ||
Theorem | bccn1 37565 | Generalized binomial coefficient: 𝐶 choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐶C𝑐1) = 𝐶) | ||
Theorem | bccbc 37566 | The binomial coefficient and generalized binomial coefficient are equal when their arguments are nonnegative integers. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑁C𝑐𝐾) = (𝑁C𝐾)) | ||
Theorem | uzmptshftfval 37567* | When 𝐹 is a maps-to function on some set of upper integers 𝑍 that returns a set 𝐵, (𝐹 shift 𝑁) is another maps-to function on the shifted set of upper integers 𝑊. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝑍 ↦ 𝐵) & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = (𝑦 − 𝑁) → 𝐵 = 𝐶) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝑁)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹 shift 𝑁) = (𝑦 ∈ 𝑊 ↦ 𝐶)) | ||
Theorem | dvradcnv2 37568* | The radius of convergence of the (formal) derivative 𝐻 of the power series 𝐺 is (at least) as large as the radius of convergence of 𝐺. This version of dvradcnv 23979 uses a shifted version of 𝐻 to match the sum form of (ℂ D 𝐹) in pserdv2 23988 (and shows how to use uzmptshftfval 37567 to shift a maps-to function on a set of upper integers). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛 · (𝐴‘𝑛)) · (𝑋↑(𝑛 − 1)))) & ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝑋) < 𝑅) ⇒ ⊢ (𝜑 → seq1( + , 𝐻) ∈ dom ⇝ ) | ||
Theorem | binomcxplemwb 37569 | Lemma for binomcxp 37578. The lemma in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) ⇒ ⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = (𝐶 · (𝐶C𝑐𝐾))) | ||
Theorem | binomcxplemnn0 37570* | Lemma for binomcxp 37578. When 𝐶 is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom 14401 equals this generalized infinite sum: the generalized binomial coefficient and exponentiation operators give exactly the same values in the standard index set (0...𝐶), and when the index set is widened beyond 𝐶 the additional values are just zeroes. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | ||
Theorem | binomcxplemrat 37571* | Lemma for binomcxp 37578. As 𝑘 increases, this ratio's absolute value converges to one. Part of equation "Since continuity of the absolute value..." in the Wikibooks proof (proven for the inverse ratio, which we later show is no problem). (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))) ⇝ 1) | ||
Theorem | binomcxplemfrat 37572* | Lemma for binomcxp 37578. binomcxplemrat 37571 implies that when 𝐶 is not a nonnegative integer, the absolute value of the ratio ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) converges to one. The rest of equation "Since continuity of the absolute value..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) ⇝ 1) | ||
Theorem | binomcxplemradcnv 37573* | Lemma for binomcxp 37578. By binomcxplemfrat 37572 and radcnvrat 37535 the radius of convergence of power series Σ𝑘 ∈ ℕ0((𝐹‘𝑘) · (𝑏↑𝑘)) is one. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) & ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ⇒ ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 𝑅 = 1) | ||
Theorem | binomcxplemdvbinom 37574* | Lemma for binomcxp 37578. By the power and chain rules, calculate the derivative of ((1 + 𝑏)↑𝑐-𝐶), with respect to 𝑏 in the disk of convergence 𝐷. We later multiply the derivative in the later binomcxplemdvsum 37576 by this derivative to show that ((1 + 𝑏)↑𝑐𝐶) (with a non-negated 𝐶) and the later sum, since both at 𝑏 = 0 equal one, are the same. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) & ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) & ⊢ 𝐷 = (◡abs “ (0[,)𝑅)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑏 ∈ 𝐷 ↦ ((1 + 𝑏)↑𝑐-𝐶))) = (𝑏 ∈ 𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1))))) | ||
Theorem | binomcxplemcvg 37575* | Lemma for binomcxp 37578. The sum in binomcxplemnn0 37570 and its derivative (see the next theorem, binomcxplemdvsum 37576) converge, as long as their base 𝐽 is within the disk of convergence. Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) & ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) & ⊢ 𝐷 = (◡abs “ (0[,)𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ 𝐷) → (seq0( + , (𝑆‘𝐽)) ∈ dom ⇝ ∧ seq1( + , (𝐸‘𝐽)) ∈ dom ⇝ )) | ||
Theorem | binomcxplemdvsum 37576* | Lemma for binomcxp 37578. The derivative of the generalized sum in binomcxplemnn0 37570. Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) & ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) & ⊢ 𝐷 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑃 = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘)) ⇒ ⊢ (𝜑 → (ℂ D 𝑃) = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸‘𝑏)‘𝑘))) | ||
Theorem | binomcxplemnotnn0 37577* |
Lemma for binomcxp 37578. When 𝐶 is not a nonnegative integer, the
generalized sum in binomcxplemnn0 37570 —which we will call 𝑃
—is a convergent power series: its base 𝑏 is always of
smaller absolute value than the radius of convergence.
pserdv2 23988 gives the derivative of 𝑃, which by dvradcnv 23979 also converges in that radius. When 𝐴 is fixed at one, (𝐴 + 𝑏) times that derivative equals (𝐶 · 𝑃) and fraction (𝑃 / ((𝐴 + 𝑏)↑𝑐𝐶)) is always defined with derivative zero, so the fraction is a constant—specifically one, because ((1 + 0)↑𝑐𝐶) = 1. Thus ((1 + 𝑏)↑𝑐𝐶) = (𝑃‘𝑏). Finally, let 𝑏 be (𝐵 / 𝐴), and multiply both the binomial ((1 + (𝐵 / 𝐴))↑𝑐𝐶) and the sum (𝑃‘(𝐵 / 𝐴)) by (𝐴↑𝑐𝐶) to get the result. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) & ⊢ 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹‘𝑘) · (𝑏↑𝑘)))) & ⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) & ⊢ 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹‘𝑘)) · (𝑏↑(𝑘 − 1))))) & ⊢ 𝐷 = (◡abs “ (0[,)𝑅)) & ⊢ 𝑃 = (𝑏 ∈ 𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆‘𝑏)‘𝑘)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | ||
Theorem | binomcxp 37578* | Generalize the binomial theorem binom 14401 to positive real summand 𝐴, real summand 𝐵, and complex exponent 𝐶. Proof in https://en.wikibooks.org/wiki/Advanced_Calculus; see also https://en.wikipedia.org/wiki/Binomial_series, https://en.wikipedia.org/wiki/Binomial_theorem (sections "Newton's generalized binomial theorem" and "Future generalizations"), and proof "General Binomial Theorem" in https://proofwiki.org/wiki/Binomial_Theorem. (Contributed by Steve Rodriguez, 22-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘)))) | ||
Theorem | pm10.12 37579* | Theorem *10.12 in [WhiteheadRussell] p. 146. In *10, this is treated as an axiom, and the proofs in *10 are based on this theorem. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ (∀𝑥(𝜑 ∨ 𝜓) → (𝜑 ∨ ∀𝑥𝜓)) | ||
Theorem | pm10.14 37580 | Theorem *10.14 in [WhiteheadRussell] p. 146. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | ||
Theorem | pm10.251 37581 | Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑) | ||
Theorem | pm10.252 37582 | Theorem *10.252 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) (New usage is discouraged.) |
⊢ (¬ ∃𝑥𝜑 ↔ ∀𝑥 ¬ 𝜑) | ||
Theorem | pm10.253 37583 | Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ (¬ ∀𝑥𝜑 ↔ ∃𝑥 ¬ 𝜑) | ||
Theorem | albitr 37584 | Theorem *10.301 in [WhiteheadRussell] p. 151. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((∀𝑥(𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜓 ↔ 𝜒)) → ∀𝑥(𝜑 ↔ 𝜒)) | ||
Theorem | pm10.42 37585 | Theorem *10.42 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | pm10.52 37586* | Theorem *10.52 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ 𝜓)) | ||
Theorem | pm10.53 37587 | Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | pm10.541 37588* | Theorem *10.541 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥(𝜑 → (𝜒 ∨ 𝜓)) ↔ (𝜒 ∨ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | pm10.542 37589* | Theorem *10.542 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) ↔ (𝜒 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | pm10.55 37590 | Theorem *10.55 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∀𝑥(𝜑 → 𝜓)) ↔ (∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | pm10.56 37591 | Theorem *10.56 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥(𝜑 ∧ 𝜒)) → ∃𝑥(𝜓 ∧ 𝜒)) | ||
Theorem | pm10.57 37592 | Theorem *10.57 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥(𝜑 → (𝜓 ∨ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ∨ ∃𝑥(𝜑 ∧ 𝜒))) | ||
Theorem | 2alanimi 37593 | Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∀𝑥∀𝑦𝜒) | ||
Theorem | 2al2imi 37594 | Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒)) | ||
Theorem | pm11.11 37595 | Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑧∀𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 | ||
Theorem | pm11.12 37596* | Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 ∨ 𝜓) → (𝜑 ∨ ∀𝑥∀𝑦𝜓)) | ||
Theorem | 19.21vv 37597* | Compare Theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1855. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜓 → 𝜑) ↔ (𝜓 → ∀𝑥∀𝑦𝜑)) | ||
Theorem | 2alim 37598 | Theorem *11.32 in [WhiteheadRussell] p. 162. Theorem 19.20 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)) | ||
Theorem | 2albi 37599 | Theorem *11.33 in [WhiteheadRussell] p. 162. Theorem 19.15 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)) | ||
Theorem | 2exim 37600 | Theorem *11.34 in [WhiteheadRussell] p. 162. Theorem 19.22 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |