P. 444 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44301-44400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	undisjrab 44301	Union of two disjoint restricted class abstractions; compare unrab 4320. (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ∅ ↔ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ⊻ 𝜓)})
Theorem	iso0 44302	The empty set is an 𝑅, 𝑆 isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.)
⊢ ∅ Isom 𝑅, 𝑆 (∅, ∅)
Theorem	ssrecnpr 44303	ℝ is a subset of both ℝ and ℂ. (Contributed by Steve Rodriguez, 22-Nov-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → ℝ ⊆ 𝑆)
Theorem	seff 44304	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 44305	The infinity ball in the absolute value metric is just the whole space. 𝑆 analogue of blpnf 24422. (Contributed by Steve Rodriguez, 8-Nov-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑆 × 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑆) → (𝑃(ball‘𝐷)+∞) = 𝑆)
Theorem	prmunb2 44306*	The primes are unbounded. This generalizes prmunb 16947 to real 𝐴 with arch 12520 and lttrd 11419: 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 44307*	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 44308*	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 15915 and dvgrat 44307 directly uses the limit of the ratio. (It also demonstrates how to use climi2 15543 and absltd 15464 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 15464, and how to use r19.29a 3159 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 3152 at https://groups.google.com/g/metamath/c/2RPikOiXLMo 3152.) (Contributed by Steve Rodriguez, 28-Feb-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ≠ 0)    &   ⊢ 𝑅 = (𝑘 ∈ 𝑊 ↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))))    &   ⊢ (𝜑 → 𝑅 ⇝ 𝐿)    &   ⊢ (𝜑 → 𝐿 ≠ 1)    ⇒   ⊢ (𝜑 → (𝐿 < 1 ↔ seq𝑀( + , 𝐹) ∈ dom ⇝ ))
Theorem	radcnvrat 44309*	Let 𝐿 be the limit, if one exists, of the ratio (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) (as in the ratio test cvgdvgrat 44308) 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 44308 —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 44310	The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ Rel ∥
Theorem	nznngen 44311	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 44312	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 44313	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 44314	Subtract one prime's multiples from an unequal prime's. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑀 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℙ)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑁)    ⇒   ⊢ (𝜑 → (( ∥ “ {𝑀}) ∖ ( ∥ “ {𝑁})) = (( ∥ “ {𝑀}) ∖ ( ∥ “ {(𝑀 · 𝑁)})))
Theorem	hashnzfz 44315	Special case of hashdvds 16808: the count of multiples in nℤ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘(𝐽 − 1)))    ⇒   ⊢ (𝜑 → (♯‘(( ∥ “ {𝑁}) ∩ (𝐽...𝐾))) = ((⌊‘(𝐾 / 𝑁)) − (⌊‘((𝐽 − 1) / 𝑁))))
Theorem	hashnzfz2 44316	Special case of hashnzfz 44315: 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 44317*	As the upper bound 𝐾 of the constraint interval (𝐽...𝐾) in hashnzfz 44315 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 44318*	Transfer a cancellation law like mulcan 11897 to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑇)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝑆)    &   ⊢ (𝜑 → 𝐻:𝐴⟶𝑆)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦) = (𝑥𝑅𝑧) ↔ 𝑦 = 𝑧))    ⇒   ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f 𝑅𝐻) ↔ 𝐺 = 𝐻))
Theorem	ofsubid 44319	Function analogue of subid 11525. (Contributed by Steve Rodriguez, 5-Nov-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) → (𝐹 ∘f − 𝐹) = (𝐴 × {0}))
Theorem	ofmul12 44320	Function analogue of mul12 11423. (Contributed by Steve Rodriguez, 13-Nov-2015.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → (𝐹 ∘f · (𝐺 ∘f · 𝐻)) = (𝐺 ∘f · (𝐹 ∘f · 𝐻)))
Theorem	ofdivrec 44321	Function analogue of divrec 11935, a division analogue of ofnegsub 12261. (Contributed by Steve Rodriguez, 3-Nov-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → (𝐹 ∘f · ((𝐴 × {1}) ∘f / 𝐺)) = (𝐹 ∘f / 𝐺))
Theorem	ofdivcan4 44322	Function analogue of divcan4 11946. (Contributed by Steve Rodriguez, 4-Nov-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → ((𝐹 ∘f · 𝐺) ∘f / 𝐺) = 𝐹)
Theorem	ofdivdiv2 44323	Function analogue of divdiv2 11976. (Contributed by Steve Rodriguez, 23-Nov-2015.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → (𝐹 ∘f / (𝐺 ∘f / 𝐻)) = ((𝐹 ∘f · 𝐻) ∘f / 𝐺))
21.39.5  Calculus
Theorem	lhe4.4ex1a 44324	Example of the Fundamental Theorem of Calculus, part two (ftc2 26099): ∫(1(,)2)((𝑥↑2) − 3) d𝑥 = -(2 / 3). Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 26099 as simply the "Fundamental Theorem of Calculus", then ftc1 26097 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 44325	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 44326	Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D ( I ↾ 𝑆)) = (𝑆 × {1}))
Theorem	dvsef 44327	Derivative of the exponential function on the real or complex numbers. (Contributed by Steve Rodriguez, 12-Nov-2015.)
⊢ (𝑆 ∈ {ℝ, ℂ} → (𝑆 D (exp ↾ 𝑆)) = (exp ↾ 𝑆))
Theorem	expgrowthi 44328*	Exponential growth and decay model. See expgrowth 44330 for more information. (Contributed by Steve Rodriguez, 4-Nov-2015.)
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   ⊢ (𝜑 → 𝐾 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝑌 = (𝑡 ∈ 𝑆 ↦ (𝐶 · (exp‘(𝐾 · 𝑡))))    ⇒   ⊢ (𝜑 → (𝑆 D 𝑌) = ((𝑆 × {𝐾}) ∘f · 𝑌))
Theorem	dvconstbi 44329*	The derivative of a function on 𝑆 is zero iff it is a constant function. Roughly a biconditional 𝑆 analogue of dvconst 25966 and dveq0 26053. 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 44330*	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 44328 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 44328); 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 44328 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 44328. Statements for this and expgrowthi 44328 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 44331	Extend class notation to include the generalized binomial coefficient operation.
class C𝑐
Definition	df-bcc 44332*	Define a generalized binomial coefficient operation, which unlike df-bc 14338 allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ C𝑐 = (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘)))
Theorem	bccval 44333	Value of the generalized binomial coefficient, 𝐶 choose 𝐾. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐶C𝑐𝐾) = ((𝐶 FallFac 𝐾) / (!‘𝐾)))
Theorem	bcccl 44334	Closure of the generalized binomial coefficient. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐶C𝑐𝐾) ∈ ℂ)
Theorem	bcc0 44335	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 44336	Generalized binomial coefficient: 𝐶 choose (𝐾 + 1). (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐶C𝑐(𝐾 + 1)) = ((𝐶C𝑐𝐾) · ((𝐶 − 𝐾) / (𝐾 + 1))))
Theorem	bccm1k 44337	Generalized binomial coefficient: 𝐶 choose (𝐾 − 1), when 𝐶 is not (𝐾 − 1). (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ (ℂ ∖ {(𝐾 − 1)}))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐶C𝑐(𝐾 − 1)) = ((𝐶C𝑐𝐾) / ((𝐶 − (𝐾 − 1)) / 𝐾)))
Theorem	bccn0 44338	Generalized binomial coefficient: 𝐶 choose 0. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶C𝑐0) = 1)
Theorem	bccn1 44339	Generalized binomial coefficient: 𝐶 choose 1. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶C𝑐1) = 𝐶)
Theorem	bccbc 44340	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 44341*	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 44342*	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 26478 uses a shifted version of 𝐻 to match the sum form of (ℂ D 𝐹) in pserdv2 26488 (and shows how to use uzmptshftfval 44341 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 44343	Lemma for binomcxp 44352. The lemma in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    ⇒   ⊢ (𝜑 → (((𝐶 − 𝐾) · (𝐶C𝑐𝐾)) + ((𝐶 − (𝐾 − 1)) · (𝐶C𝑐(𝐾 − 1)))) = (𝐶 · (𝐶C𝑐𝐾)))
Theorem	binomcxplemnn0 44344*	Lemma for binomcxp 44352. When 𝐶 is a nonnegative integer, the binomial's finite sum value by the standard binomial theorem binom 15862 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 44345*	Lemma for binomcxp 44352. 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 44346*	Lemma for binomcxp 44352. binomcxplemrat 44345 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 44347*	Lemma for binomcxp 44352. By binomcxplemfrat 44346 and radcnvrat 44309 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 44348*	Lemma for binomcxp 44352. 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 44350 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 44349*	Lemma for binomcxp 44352. The sum in binomcxplemnn0 44344 and its derivative (see the next theorem, binomcxplemdvsum 44350) 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 44350*	Lemma for binomcxp 44352. The derivative of the generalized sum in binomcxplemnn0 44344. 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 44351*	Lemma for binomcxp 44352. When 𝐶 is not a nonnegative integer, the generalized sum in binomcxplemnn0 44344 —which we will call 𝑃 —is a convergent power series: its base 𝑏 is always of smaller absolute value than the radius of convergence. pserdv2 26488 gives the derivative of 𝑃, which by dvradcnv 26478 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 44352*	Generalize the binomial theorem binom 15862 to positive real summand 𝐴, real summand 𝐵, and complex exponent 𝐶. Proof in https://en.wikibooks.org/wiki/Advanced_Calculus 15862; see also https://en.wikipedia.org/wiki/Binomial_series 15862, https://en.wikipedia.org/wiki/Binomial_theorem 15862 (sections "Newton's generalized binomial theorem" and "Future generalizations"), and proof "General Binomial Theorem" in https://proofwiki.org/wiki/Binomial_Theorem 15862. (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 44353*	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 44354	Theorem *10.14 in [WhiteheadRussell] p. 146. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Theorem	pm10.251 44355	Theorem *10.251 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)
Theorem	pm10.252 44356	Theorem *10.252 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.) (New usage is discouraged.)
⊢ (¬ ∃𝑥𝜑 ↔ ∀𝑥 ¬ 𝜑)
Theorem	pm10.253 44357	Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (¬ ∀𝑥𝜑 ↔ ∃𝑥 ¬ 𝜑)
Theorem	albitr 44358	Theorem *10.301 in [WhiteheadRussell] p. 151. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥(𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜓 ↔ 𝜒)) → ∀𝑥(𝜑 ↔ 𝜒))
Theorem	pm10.42 44359	Theorem *10.42 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∨ 𝜓))
Theorem	pm10.52 44360*	Theorem *10.52 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ 𝜓))
Theorem	pm10.53 44361	Theorem *10.53 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝜓))
Theorem	pm10.541 44362*	Theorem *10.541 in [WhiteheadRussell] p. 155. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥(𝜑 → (𝜒 ∨ 𝜓)) ↔ (𝜒 ∨ ∀𝑥(𝜑 → 𝜓)))
Theorem	pm10.542 44363*	Theorem *10.542 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) ↔ (𝜒 → ∀𝑥(𝜑 → 𝜓)))
Theorem	pm10.55 44364	Theorem *10.55 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∃𝑥(𝜑 ∧ 𝜓) ∧ ∀𝑥(𝜑 → 𝜓)) ↔ (∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)))
Theorem	pm10.56 44365	Theorem *10.56 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥(𝜑 ∧ 𝜒)) → ∃𝑥(𝜓 ∧ 𝜒))
Theorem	pm10.57 44366	Theorem *10.57 in [WhiteheadRussell] p. 156. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥(𝜑 → (𝜓 ∨ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ∨ ∃𝑥(𝜑 ∧ 𝜒)))
21.40.2  Principia Mathematica * 11
Theorem	2alanimi 44367	Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∀𝑥∀𝑦𝜒)
Theorem	2al2imi 44368	Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒))
Theorem	pm11.11 44369	Theorem *11.11 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ 𝜑    ⇒   ⊢ ∀𝑧∀𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
Theorem	pm11.12 44370*	Theorem *11.12 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
⊢ (∀𝑥∀𝑦(𝜑 ∨ 𝜓) → (𝜑 ∨ ∀𝑥∀𝑦𝜓))
Theorem	19.21vv 44371*	Compare Theorem *11.3 in [WhiteheadRussell] p. 161. Special case of theorem 19.21 of [Margaris] p. 90 with two quantifiers. See 19.21v 1936. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜓 → 𝜑) ↔ (𝜓 → ∀𝑥∀𝑦𝜑))
Theorem	2alim 44372	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 44373	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 44374	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 44375	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 44376	Theorem *11.36 in [WhiteheadRussell] p. 162. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑥∃𝑦𝜑)
Theorem	19.33-2 44377	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 44378*	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 44379*	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 44380*	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 44381*	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 44382	Theorem *11.52 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥∀𝑦(𝜑 → ¬ 𝜓))
Theorem	aaanv 44383*	Theorem *11.56 in [WhiteheadRussell] p. 165. Special case of aaan 2331. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∀𝑥𝜑 ∧ ∀𝑦𝜓) ↔ ∀𝑥∀𝑦(𝜑 ∧ 𝜓))
Theorem	pm11.57 44384*	Theorem *11.57 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))
Theorem	pm11.58 44385*	Theorem *11.58 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑦(𝜑 ∧ [𝑦 / 𝑥]𝜑))
Theorem	pm11.59 44386*	Theorem *11.59 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∀𝑥(𝜑 → 𝜓) → ∀𝑦∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝜓 ∧ [𝑦 / 𝑥]𝜓)))
Theorem	pm11.6 44387*	Theorem *11.6 in [WhiteheadRussell] p. 165. (Contributed by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ∃𝑦(∃𝑥(𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	pm11.61 44388*	Theorem *11.61 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝜓) → ∀𝑥(𝜑 → ∃𝑦𝜓))
Theorem	pm11.62 44389*	Theorem *11.62 in [WhiteheadRussell] p. 166. Importation combined with the rearrangement with quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝜒) ↔ ∀𝑥(𝜑 → ∀𝑦(𝜓 → 𝜒)))
Theorem	pm11.63 44390	Theorem *11.63 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥∃𝑦𝜑 → ∀𝑥∀𝑦(𝜑 → 𝜓))
Theorem	pm11.7 44391	Theorem *11.7 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜑) ↔ ∃𝑥∃𝑦𝜑)
Theorem	pm11.71 44392*	Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑦(𝜒 → 𝜃)) ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))))
21.40.3  Predicate Calculus
Theorem	sbeqal1 44393*	If 𝑥 = 𝑦 always implies 𝑥 = 𝑧, then 𝑦 = 𝑧. (Contributed by Andrew Salmon, 2-Jun-2011.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑧) → 𝑦 = 𝑧)
Theorem	sbeqal1i 44394*	Suppose you know 𝑥 = 𝑦 implies 𝑥 = 𝑧, assuming 𝑥 and 𝑧 are distinct. Then, 𝑦 = 𝑧. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧)    ⇒   ⊢ 𝑦 = 𝑧
Theorem	sbeqal2i 44395*	If 𝑥 = 𝑦 implies 𝑥 = 𝑧, then we can infer 𝑧 = 𝑦. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑧)    ⇒   ⊢ 𝑧 = 𝑦
Theorem	axc5c4c711 44396	Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1791 as the inference rule. This proof extends the idea of axc5c711 38899 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011.)
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦(∀𝑦𝜑 → 𝜓) → (𝜑 → ∀𝑦(∀𝑦𝜑 → 𝜓))) → (∀𝑦𝜑 → ∀𝑦𝜓))
Theorem	axc5c4c711toc5 44397	Rederivation of sp 2180 from axc5c4c711 44396. Note that ax6 2386 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) Revised to use ax6v 1965 instead of ax6 2386, so that this rederivation requires only ax6v 1965 and propositional calculus. (Revised by BJ, 14-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c4c711toc4 44398	Rederivation of axc4 2319 from axc5c4c711 44396. Note that only propositional calculus is required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	axc5c4c711toc7 44399	Rederivation of axc7 2315 from axc5c4c711 44396. Note that neither axc7 2315 nor ax-11 2154 are required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc5c4c711to11 44400	Rederivation of ax-11 2154 from axc5c4c711 44396. Note that ax-11 2154 is not required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)