P. 445 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44401-44500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ismnuprim 44401*	Express the predicate on 𝑈 in ismnu 44368 using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ↔ ∀𝑧(𝑧 ∈ 𝑈 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑈 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑈 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤))))))))))))
Theorem	rr-grothprimbi 44402*	Express "every set is contained in a Grothendieck universe" using only primitives. The right side (without the outermost universal quantifier) is proven as rr-grothprim 44407. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (∀𝑥∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀𝑥 ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤)))))))))))))
Theorem	inagrud 44403	Inaccessible levels of the cumulative hierarchy are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝜑 → 𝐼 ∈ Inacc)    ⇒   ⊢ (𝜑 → (𝑅1‘𝐼) ∈ Univ)
Theorem	inaex 44404*	Assuming the Tarski-Grothendieck axiom, every ordinal is contained in an inaccessible ordinal. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ Inacc 𝐴 ∈ 𝑥)
Theorem	gruex 44405*	Assuming the Tarski-Grothendieck axiom, every set is contained in a Grothendieck universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ∃𝑦 ∈ Univ 𝑥 ∈ 𝑦
Theorem	rr-groth 44406*	An equivalent of ax-groth 10724 using only simple defined symbols. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∀𝑓∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑦 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
Theorem	rr-grothprim 44407*	An equivalent of ax-groth 10724 using only primitives. This uses only 123 symbols, which is significantly less than the previous record of 163 established by grothprim 10735 (which uses some defined symbols, and requires 229 symbols if expanded to primitives). (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ¬ ∀𝑦(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑦 → ∀𝑓 ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧) → ¬ (𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤)) → ¬ ∀𝑖(𝑖 ∈ 𝑧 → (𝑣 ∈ 𝑦 → (𝑖 ∈ 𝑣 → (𝑣 ∈ 𝑓 → ¬ ∀𝑢(𝑢 ∈ 𝑓 → (𝑖 ∈ 𝑢 → ¬ ∀𝑜(𝑜 ∈ 𝑢 → ∀𝑠(𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤))))))))))))
Theorem	ismnushort 44408*	Express the predicate on 𝑈 and 𝑧 in ismnu 44368 in a shorter form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 10-Oct-2024.)
⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
Theorem	dfuniv2 44409*	Alternative definition of Univ using only simple defined symbols. (Contributed by Rohan Ridenour, 10-Oct-2024.)
⊢ Univ = {𝑦 ∣ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))}
Theorem	rr-grothshortbi 44410*	Express "every set is contained in a Grothendieck universe" in a short form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 8-Oct-2024.)
⊢ (∀𝑥∃𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀𝑥∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
Theorem	rr-grothshort 44411*	A shorter equivalent of ax-groth 10724 than rr-groth 44406 using a few more simple defined symbols. (Contributed by Rohan Ridenour, 8-Oct-2024.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∀𝑓 ∈ 𝒫 𝑦∃𝑤 ∈ 𝑦 (𝒫 𝑧 ⊆ (𝑦 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
21.39  Mathbox for Steve Rodriguez
21.39.1  Miscellanea
Theorem	nanorxor 44412	'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ⊻ 𝜓)))
Theorem	undisjrab 44413	Union of two disjoint restricted class abstractions; compare unrab 4266. (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ∅ ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ⊻ 𝜓)})
Theorem	iso0 44414	The empty set is an 𝑅, 𝑆 isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.)
⊢ ∅ Isom 𝑅, 𝑆 (∅, ∅)
Theorem	ssrecnpr 44415	ℝ is a subset of both ℝ and ℂ. (Contributed by Steve Rodriguez, 22-Nov-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → ℝ ⊆ 𝑆)
Theorem	seff 44416	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 44417	The infinity ball in the absolute value metric is just the whole space. 𝑆 analogue of blpnf 24322. (Contributed by Steve Rodriguez, 8-Nov-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑆 × 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆)
Theorem	prmunb2 44418*	The primes are unbounded. This generalizes prmunb 16836 to real 𝐴 with arch 12388 and lttrd 11284: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝐴 ∈ ℝ → ∃𝑝 ∈ ℙ 𝐴 < 𝑝)
21.39.2  Ratio test for infinite series convergence and divergence
Theorem	dvgrat 44419*	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 44420*	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 15800 and dvgrat 44419 directly uses the limit of the ratio. (It also demonstrates how to use climi2 15428 and absltd 15349 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15349, and how to use r19.29a 3142 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3135 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3135.) (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0)    &   ⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))    &   ⊢ (𝜑 → 𝑅 ⇝ 𝐿)    &   ⊢ (𝜑 → 𝐿 ≠ 1)    ⇒   ⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
Theorem	radcnvrat 44421*	Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 44420) 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 44420 —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 / 𝐿))
21.39.3  Multiples
Theorem	reldvds 44422	The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ Rel ∥
Theorem	nznngen 44423	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 44424	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 44425	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 44426	Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑀 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℙ)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑁)    ⇒   ⊢ (𝜑 → (( ∥ “ {𝑀}) ∖ ( ∥ “ {𝑁})) = (( ∥ “ {𝑀}) ∖ ( ∥ “ {(𝑀 · 𝑁)})))
Theorem	hashnzfz 44427	Special case of hashdvds 16696: the count of multiples in nℤ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘(𝐽 − 1)))    ⇒   ⊢ (𝜑 → (♯‘(( ∥ “ {𝑁}) ∩ (𝐽...𝐾))) = ((⌊‘(𝐾 / 𝑁)) − (⌊‘((𝐽 − 1) / 𝑁))))
Theorem	hashnzfz2 44428	Special case of hashnzfz 44427: 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 44429*	As the upper bound 𝐾 of the constraint interval (𝐽...𝐾) in hashnzfz 44427 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 / 𝑀))
21.39.4  Function operations
Theorem	caofcan 44430*	Transfer a cancellation law like mulcan 11764 to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑇)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦) = (𝑥𝑅𝑧) ↔ 𝑦 = 𝑧))    ⇒   ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f 𝑅𝐻) ↔ 𝐺 = 𝐻))
Theorem	ofsubid 44431	Function analogue of subid 11390. (Contributed by Steve Rodriguez, 5-Nov-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) → (𝐹 ∘f − 𝐹) = (𝐴 × {0}))
Theorem	ofmul12 44432	Function analogue of mul12 11288. (Contributed by Steve Rodriguez, 13-Nov-2015.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → (𝐹 ∘f · (𝐺 ∘f · 𝐻)) = (𝐺 ∘f · (𝐹 ∘f · 𝐻)))
Theorem	ofdivrec 44433	Function analogue of divrec 11802, a division analogue of ofnegsub 12133. (Contributed by Steve Rodriguez, 3-Nov-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → (𝐹 ∘f · ((𝐴 × {1}) ∘f / 𝐺)) = (𝐹 ∘f / 𝐺))
Theorem	ofdivcan4 44434	Function analogue of divcan4 11813. (Contributed by Steve Rodriguez, 4-Nov-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → ((𝐹 ∘f · 𝐺) ∘f / 𝐺) = 𝐹)
Theorem	ofdivdiv2 44435	Function analogue of divdiv2 11843. (Contributed by Steve Rodriguez, 23-Nov-2015.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → (𝐹 ∘f / (𝐺 ∘f / 𝐻)) = ((𝐹 ∘f · 𝐻) ∘f / 𝐺))
21.39.5  Calculus
Theorem	lhe4.4ex1a 44436	Example of the Fundamental Theorem of Calculus, part two (ftc2 25988): ∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 25988 as simply the "Fundamental Theorem of Calculus", then ftc1 25986 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 44437	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 44438	Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D ( I ↾ 𝑆)) = (𝑆 × {1}))
Theorem	dvsef 44439	Derivative of the exponential function on the real or complex numbers. (Contributed by Steve Rodriguez, 12-Nov-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D (exp ↾ 𝑆)) = (exp ↾ 𝑆))
Theorem	expgrowthi 44440*	Exponential growth and decay model. See expgrowth 44442 for more information. (Contributed by Steve Rodriguez, 4-Nov-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐾 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡))))    ⇒   ⊢ (𝜑 → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌))
Theorem	dvconstbi 44441*	The derivative of a function on 𝑆 is zero iff it is a constant function. Roughly a biconditional 𝑆 analogue of dvconst 25855 and dveq0 25942. 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 44442*	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 44440 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 44440); 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 ((𝑆 × {𝐾}) ∘f · 𝑌). (𝑆 × {𝐾}) is the constant function that maps any real or complex input to k and ∘f · 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 44440 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 44440. Statements for this and expgrowthi 44440 formulated by Mario Carneiro. (Contributed by Steve Rodriguez, 24-Nov-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐾 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌:𝑆⟶ℂ)    &   ⊢ (𝜑 → dom (𝑆 D 𝑌) = 𝑆)    ⇒   ⊢ (𝜑 → ((𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌) ↔ ∃𝑐 ∈ ℂ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝑐 · (exp‘(𝐾 · 𝑡))))))
21.39.6  The generalized binomial coefficient operation
Syntax	cbcc 44443	Extend class notation to include the generalized binomial coefficient operation.
class C𝑐
Definition	df-bcc 44444*	Define a generalized binomial coefficient operation, which unlike df-bc 14220 allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ C𝑐 = (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘)))
Theorem	bccval 44445	Value of the generalized binomial coefficient, 𝐶 choose 𝐾. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐶C𝑐𝐾) = ((𝐶 FallFac 𝐾) / (!‘𝐾)))
Theorem	bcccl 44446	Closure of the generalized binomial coefficient. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐶C𝑐𝐾) ∈ ℂ)
Theorem	bcc0 44447	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 44448	Generalized binomial coefficient: 𝐶 choose (𝐾 + 1). (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐶C𝑐(𝐾 + 1)) = ((𝐶C𝑐𝐾) · ((𝐶 − 𝐾) / (𝐾 + 1))))
Theorem	bccm1k 44449	Generalized binomial coefficient: 𝐶 choose (𝐾 − 1), when 𝐶 is not (𝐾 − 1). (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ (ℂ ∖ {(𝐾 − 1)}))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐶C𝑐(𝐾 − 1)) = ((𝐶C𝑐𝐾) / ((𝐶 − (𝐾 − 1)) / 𝐾)))
Theorem	bccn0 44450	Generalized binomial coefficient: 𝐶 choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶C𝑐0) = 1)
Theorem	bccn1 44451	Generalized binomial coefficient: 𝐶 choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶C𝑐1) = 𝐶)
Theorem	bccbc 44452	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𝐾))
21.39.7  Binomial series
Theorem	uzmptshftfval 44453*	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 44454*	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 26367 uses a shifted version of 𝐻 to match the sum form of (ℂ D 𝐹) in pserdv2 26377 (and shows how to use uzmptshftfval 44453 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 44455	Lemma for binomcxp 44464. The lemma in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    ⇒   ⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = (𝐶 · (𝐶C𝑐𝐾)))
Theorem	binomcxplemnn0 44456*	Lemma for binomcxp 44464. When 𝐶 is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom 15747 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 44457*	Lemma for binomcxp 44464. 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 44458*	Lemma for binomcxp 44464. binomcxplemrat 44457 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 44459*	Lemma for binomcxp 44464. By binomcxplemfrat 44458 and radcnvrat 44421 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 44460*	Lemma for binomcxp 44464. 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 44462 by this derivative to show that ((1 + 𝑏)↑𝑐𝐶) (with a nonnegated 𝐶) 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 44461*	Lemma for binomcxp 44464. The sum in binomcxplemnn0 44456 and its derivative (see the next theorem, binomcxplemdvsum 44462) 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 44462*	Lemma for binomcxp 44464. The derivative of the generalized sum in binomcxplemnn0 44456. Part of remark "This convergence allows 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 44463*	Lemma for binomcxp 44464. When 𝐶 is not a nonnegative integer, the generalized sum in binomcxplemnn0 44456 —which we will call 𝑃 —is a convergent power series: its base 𝑏 is always of smaller absolute value than the radius of convergence. pserdv2 26377 gives the derivative of 𝑃, which by dvradcnv 26367 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 44464*	Generalize the binomial theorem binom 15747 to positive real summand 𝐴, real summand 𝐵, and complex exponent 𝐶. Proof in https://en.wikibooks.org/wiki/Advanced_Calculus 15747; see also https://en.wikipedia.org/wiki/Binomial_series 15747, https://en.wikipedia.org/wiki/Binomial_theorem 15747 (sections "Newton's generalized binomial theorem" and "Future generalizations"), and proof "General Binomial Theorem" in https://proofwiki.org/wiki/Binomial_Theorem 15747. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵)↑𝑐𝐶) = Σ𝑘 ∈ ℕ0 ((𝐶C𝑐𝑘) · ((𝐴↑𝑐(𝐶 − 𝑘)) · (𝐵↑𝑘))))
21.40  Mathbox for Andrew Salmon
21.40.1  Principia Mathematica * 10
Theorem	pm10.12 44465*	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 44466	Theorem *10.14 in [WhiteheadRussell] p. 146. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Theorem	pm10.251 44467	Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)
Theorem	pm10.252 44468	Theorem *10.252 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) (New usage is discouraged.)
⊢ (¬ ∃𝑥𝜑 ↔ ∀𝑥 ¬ 𝜑)
Theorem	pm10.253 44469	Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (¬ ∀𝑥𝜑 ↔ ∃𝑥 ¬ 𝜑)
Theorem	albitr 44470	Theorem *10.301 in [WhiteheadRussell] p. 151. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥(𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜓 ↔ 𝜒)) → ∀𝑥(𝜑 ↔ 𝜒))
Theorem	pm10.42 44471	Theorem *10.42 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∨ 𝜓))
Theorem	pm10.52 44472*	Theorem *10.52 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ 𝜓))
Theorem	pm10.53 44473	Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝜓))
Theorem	pm10.541 44474*	Theorem *10.541 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥(𝜑 → (𝜒 ∨ 𝜓)) ↔ (𝜒 ∨ ∀𝑥(𝜑 → 𝜓)))
Theorem	pm10.542 44475*	Theorem *10.542 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) ↔ (𝜒 → ∀𝑥(𝜑 → 𝜓)))
Theorem	pm10.55 44476	Theorem *10.55 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∀𝑥(𝜑 → 𝜓)) ↔ (∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)))
Theorem	pm10.56 44477	Theorem *10.56 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥(𝜑 ∧ 𝜒)) → ∃𝑥(𝜓 ∧ 𝜒))
Theorem	pm10.57 44478	Theorem *10.57 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥(𝜑 → (𝜓 ∨ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ∨ ∃𝑥(𝜑 ∧ 𝜒)))
21.40.2  Principia Mathematica * 11
Theorem	2alanimi 44479	Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∀𝑥∀𝑦𝜒)
Theorem	2al2imi 44480	Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒))
Theorem	pm11.11 44481	Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ 𝜑    ⇒   ⊢ ∀𝑧∀𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
Theorem	pm11.12 44482*	Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (∀𝑥∀𝑦(𝜑 ∨ 𝜓) → (𝜑 ∨ ∀𝑥∀𝑦𝜓))
Theorem	19.21vv 44483*	Compare Theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1940. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜓 → 𝜑) ↔ (𝜓 → ∀𝑥∀𝑦𝜑))
Theorem	2alim 44484	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 44485	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 44486	Theorem *11.34 in [WhiteheadRussell] p. 162. Theorem 19.22 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓))
Theorem	2exbi 44487	Theorem *11.341 in [WhiteheadRussell] p. 162. Theorem 19.18 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓))
Theorem	spsbce-2 44488	Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑥∃𝑦𝜑)
Theorem	19.33-2 44489	Theorem *11.421 in [WhiteheadRussell] p. 163. Theorem 19.33 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥∀𝑦𝜑 ∨ ∀𝑥∀𝑦𝜓) → ∀𝑥∀𝑦(𝜑 ∨ 𝜓))
Theorem	19.36vv 44490*	Theorem *11.43 in [WhiteheadRussell] p. 163. Theorem 19.36 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 → 𝜓) ↔ (∀𝑥∀𝑦𝜑 → 𝜓))
Theorem	19.31vv 44491*	Theorem *11.44 in [WhiteheadRussell] p. 163. Theorem 19.31 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 ∨ 𝜓) ↔ (∀𝑥∀𝑦𝜑 ∨ 𝜓))
Theorem	19.37vv 44492*	Theorem *11.46 in [WhiteheadRussell] p. 164. Theorem 19.37 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜓 → 𝜑) ↔ (𝜓 → ∃𝑥∃𝑦𝜑))
Theorem	19.28vv 44493*	Theorem *11.47 in [WhiteheadRussell] p. 164. Theorem 19.28 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜓 ∧ 𝜑) ↔ (𝜓 ∧ ∀𝑥∀𝑦𝜑))
Theorem	pm11.52 44494	Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥∀𝑦(𝜑 → ¬ 𝜓))
Theorem	aaanv 44495*	Theorem *11.56 in [WhiteheadRussell] p. 165. Special case of aaan 2335. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥𝜑 ∧ ∀𝑦𝜓) ↔ ∀𝑥∀𝑦(𝜑 ∧ 𝜓))
Theorem	pm11.57 44496*	Theorem *11.57 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))
Theorem	pm11.58 44497*	Theorem *11.58 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))
Theorem	pm11.59 44498*	Theorem *11.59 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∀𝑥(𝜑 → 𝜓) → ∀𝑦∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝜓 ∧ [𝑦 / 𝑥]𝜓)))
Theorem	pm11.6 44499*	Theorem *11.6 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ∃𝑦(∃𝑥(𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	pm11.61 44500*	Theorem *11.61 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝜓) → ∀𝑥(𝜑 → ∃𝑦𝜓))