P. 124 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12301-12400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pwm1geoserap1 12301*	The n-th power of a number decreased by 1 expressed by the finite geometric series 1 + 𝐴↑1 + 𝐴↑2 +... + 𝐴↑(𝑁 − 1). (Contributed by AV, 14-Aug-2021.) (Revised by Jim Kingdon, 24-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 # 1)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))
Theorem	absltap 12302	Less-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐴) < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 # 𝐵)
Theorem	absgtap 12303	Greater-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 < (abs‘𝐴))    ⇒   ⊢ (𝜑 → 𝐴 # 𝐵)
Theorem	geolim 12304*	The partial sums in the infinite series 1 + 𝐴↑1 + 𝐴↑2... converge to (1 / (1 − 𝐴)). (Contributed by NM, 15-May-2006.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝐴) < 1)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = (𝐴↑𝑘))    ⇒   ⊢ (𝜑 → seq0( + , 𝐹) ⇝ (1 / (1 − 𝐴)))
Theorem	geolim2 12305*	The partial sums in the geometric series 𝐴↑𝑀 + 𝐴↑(𝑀 + 1)... converge to ((𝐴↑𝑀) / (1 − 𝐴)). (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 26-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝐴) < 1)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐴↑𝑘))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ ((𝐴↑𝑀) / (1 − 𝐴)))
Theorem	georeclim 12306*	The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 1 < (abs‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = ((1 / 𝐴)↑𝑘))    ⇒   ⊢ (𝜑 → seq0( + , 𝐹) ⇝ (𝐴 / (𝐴 − 1)))
Theorem	geo2sum 12307*	The value of the finite geometric series 2↑ -1 + 2↑ -2 +... + 2↑ -𝑁, multiplied by a constant. (Contributed by Mario Carneiro, 17-Mar-2014.) (Revised by Mario Carneiro, 26-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)(𝐴 / (2↑𝑘)) = (𝐴 − (𝐴 / (2↑𝑁))))
Theorem	geo2sum2 12308*	The value of the finite geometric series 1 + 2 + 4 + 8 +... + 2↑(𝑁 − 1). (Contributed by Mario Carneiro, 7-Sep-2016.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (0..^𝑁)(2↑𝑘) = ((2↑𝑁) − 1))
Theorem	geo2lim 12309*	The value of the infinite geometric series 2↑ -1 + 2↑ -2 +... , multiplied by a constant. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘)))    ⇒   ⊢ (𝐴 ∈ ℂ → seq1( + , 𝐹) ⇝ 𝐴)
Theorem	geoisum 12310*	The infinite sum of 1 + 𝐴↑1 + 𝐴↑2... is (1 / (1 − 𝐴)). (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 26-Apr-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ0 (𝐴↑𝑘) = (1 / (1 − 𝐴)))
Theorem	geoisumr 12311*	The infinite sum of reciprocals 1 + (1 / 𝐴)↑1 + (1 / 𝐴)↑2... is 𝐴 / (𝐴 − 1). (Contributed by rpenner, 3-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 1 < (abs‘𝐴)) → Σ𝑘 ∈ ℕ0 ((1 / 𝐴)↑𝑘) = (𝐴 / (𝐴 − 1)))
Theorem	geoisum1 12312*	The infinite sum of 𝐴↑1 + 𝐴↑2... is (𝐴 / (1 − 𝐴)). (Contributed by NM, 1-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → Σ𝑘 ∈ ℕ (𝐴↑𝑘) = (𝐴 / (1 − 𝐴)))
Theorem	geoisum1c 12313*	The infinite sum of 𝐴 · (𝑅↑1) + 𝐴 · (𝑅↑2)... is (𝐴 · 𝑅) / (1 − 𝑅). (Contributed by NM, 2-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ (abs‘𝑅) < 1) → Σ𝑘 ∈ ℕ (𝐴 · (𝑅↑𝑘)) = ((𝐴 · 𝑅) / (1 − 𝑅)))
Theorem	0.999... 12314	The recurring decimal 0.999..., which is defined as the infinite sum 0.9 + 0.09 + 0.009 + ... i.e. 9 / 10↑1 + 9 / 10↑2 + 9 / 10↑3 + ..., is exactly equal to 1. (Contributed by NM, 2-Nov-2007.) (Revised by AV, 8-Sep-2021.)
⊢ Σ𝑘 ∈ ℕ (9 / (;10↑𝑘)) = 1
Theorem	geoihalfsum 12315	Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 12312. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 12314 proves a similar claim for .999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.) (Proof shortened by AV, 9-Jul-2022.)
⊢ Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1
4.9.8  Ratio test for infinite series convergence
Theorem	cvgratnnlembern 12316	Lemma for cvgratnn 12324. Upper bound for a geometric progression of positive ratio less than one. (Contributed by Jim Kingdon, 24-Nov-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑀) < ((1 / ((1 / 𝐴) − 1)) / 𝑀))
Theorem	cvgratnnlemnexp 12317*	Lemma for cvgratnn 12324. (Contributed by Jim Kingdon, 15-Nov-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (abs‘(𝐹‘𝑁)) ≤ ((abs‘(𝐹‘1)) · (𝐴↑(𝑁 − 1))))
Theorem	cvgratnnlemmn 12318*	Lemma for cvgratnn 12324. (Contributed by Jim Kingdon, 15-Nov-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘))))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (abs‘(𝐹‘𝑁)) ≤ ((abs‘(𝐹‘𝑀)) · (𝐴↑(𝑁 − 𝑀))))
Theorem	cvgratnnlemseq 12319*	Lemma for cvgratnn 12324. (Contributed by Jim Kingdon, 21-Nov-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘))))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → ((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀)) = Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖))
Theorem	cvgratnnlemabsle 12320*	Lemma for cvgratnn 12324. (Contributed by Jim Kingdon, 21-Nov-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘))))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖)) ≤ ((abs‘(𝐹‘𝑀)) · Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀))))
Theorem	cvgratnnlemsumlt 12321*	Lemma for cvgratnn 12324. (Contributed by Jim Kingdon, 23-Nov-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘))))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀)) < (𝐴 / (1 − 𝐴)))
Theorem	cvgratnnlemfm 12322*	Lemma for cvgratnn 12324. (Contributed by Jim Kingdon, 23-Nov-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘))))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    ⇒   ⊢ (𝜑 → (abs‘(𝐹‘𝑀)) < ((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) / 𝑀))
Theorem	cvgratnnlemrate 12323*	Lemma for cvgratnn 12324. (Contributed by Jim Kingdon, 21-Nov-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘))))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (abs‘((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀))) < (((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) · (𝐴 / (1 − 𝐴))) / 𝑀))
Theorem	cvgratnn 12324*	Ratio test for convergence of a complex infinite series. If the ratio 𝐴 of the absolute values of successive terms in an infinite sequence 𝐹 is less than 1 for all terms, then the infinite sum of the terms of 𝐹 converges to a complex number. Although this theorem is similar to cvgratz 12325 and cvgratgt0 12326, the decision to index starting at one is not merely cosmetic, as proving convergence using climcvg1n 12142 is sensitive to how a sequence is indexed. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 12-Nov-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘))))    ⇒   ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
Theorem	cvgratz 12325*	Ratio test for convergence of a complex infinite series. If the ratio 𝐴 of the absolute values of successive terms in an infinite sequence 𝐹 is less than 1 for all terms, then the infinite sum of the terms of 𝐹 converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘))))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Theorem	cvgratgt0 12326*	Ratio test for convergence of a complex infinite series. If the ratio 𝐴 of the absolute values of successive terms in an infinite sequence 𝐹 is less than 1 for all terms beyond some index 𝐵, then the infinite sum of the terms of 𝐹 converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑊 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 0 < 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘))))    ⇒   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
4.9.9  Mertens' theorem
Theorem	mertenslemub 12327*	Lemma for mertensabs 12330. An upper bound for 𝑇. (Contributed by Jim Kingdon, 3-Dec-2022.)
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )    &   ⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑆 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))}    &   ⊢ (𝜑 → 𝑋 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝑋 ≤ Σ𝑛 ∈ (0...(𝑆 − 1))(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
Theorem	mertenslemi1 12328*	Lemma for mertensabs 12330. (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))    &   ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )    &   ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))}    &   ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))    &   ⊢ (𝜑 → 𝑃 ∈ ℝ)    &   ⊢ (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (𝑃 + 1)))))    &   ⊢ (𝜑 → 0 ≤ 𝑃)    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑃)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
Theorem	mertenslem2 12329*	Lemma for mertensabs 12330. (Contributed by Mario Carneiro, 28-Apr-2014.)
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))    &   ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )    &   ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))}    &   ⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)
Theorem	mertensabs 12330*	Mertens' theorem. If 𝐴(𝑗) is an absolutely convergent series and 𝐵(𝑘) is convergent, then (Σ𝑗 ∈ ℕ0𝐴(𝑗) · Σ𝑘 ∈ ℕ0𝐵(𝑘)) = Σ𝑘 ∈ ℕ0Σ𝑗 ∈ (0...𝑘)(𝐴(𝑗) · 𝐵(𝑘 − 𝑗)) (and this latter series is convergent). This latter sum is commonly known as the Cauchy product of the sequences. The proof follows the outline at http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem. (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon, 8-Dec-2022.)
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))    &   ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )    &   ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )    &   ⊢ (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
4.9.10  Finite and infinite products
4.9.10.1  Product sequences
Theorem	prodf 12331*	An infinite product of complex terms is a function from an upper set of integers to ℂ. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    ⇒   ⊢ (𝜑 → seq𝑀( · , 𝐹):𝑍⟶ℂ)
Theorem	clim2prod 12332*	The limit of an infinite product with an initial segment added. (Contributed by Scott Fenton, 18-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ 𝐴)    ⇒   ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘𝑁) · 𝐴))
Theorem	clim2divap 12333*	The limit of an infinite product with an initial segment removed. (Contributed by Scott Fenton, 20-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝐴)    &   ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) # 0)    ⇒   ⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ (𝐴 / (seq𝑀( · , 𝐹)‘𝑁)))
Theorem	prod3fmul 12334*	The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) · (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq𝑀( · , 𝐺)‘𝑁)))
Theorem	prodf1 12335	The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑁 ∈ 𝑍 → (seq𝑀( · , (𝑍 × {1}))‘𝑁) = 1)
Theorem	prodf1f 12336	A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) = (𝑍 × {1}))
Theorem	prodfclim1 12337	The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → seq𝑀( · , (𝑍 × {1})) ⇝ 1)
Theorem	prodfap0 12338*	The product of finitely many terms apart from zero is apart from zero. (Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon, 23-Mar-2024.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) # 0)    ⇒   ⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) # 0)
Theorem	prodfrecap 12339*	The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) # 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) = (1 / (𝐹‘𝑘)))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ)    ⇒   ⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) = (1 / (seq𝑀( · , 𝐹)‘𝑁)))
Theorem	prodfdivap 12340*	The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) # 0)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘) / (𝐺‘𝑘)))    ⇒   ⊢ (𝜑 → (seq𝑀( · , 𝐻)‘𝑁) = ((seq𝑀( · , 𝐹)‘𝑁) / (seq𝑀( · , 𝐺)‘𝑁)))
4.9.10.2  Non-trivial convergence
Theorem	ntrivcvgap 12341*	A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)    ⇒   ⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ dom ⇝ )
Theorem	ntrivcvgap0 12342*	A product that converges to a value apart from zero converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋)    &   ⊢ (𝜑 → 𝑋 # 0)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
4.9.10.3  Complex products
Syntax	cprod 12343	Extend class notation to include complex products.
class ∏𝑘 ∈ 𝐴 𝐵
Definition	df-proddc 12344*	Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sumdc 12146 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 21-Mar-2024.)
⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
Theorem	prodeq1f 12345	Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑘𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)
Theorem	prodeq1 12346*	Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)
Theorem	nfcprod1 12347*	Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ Ⅎ𝑘𝐴    ⇒   ⊢ Ⅎ𝑘∏𝑘 ∈ 𝐴 𝐵
Theorem	nfcprod 12348*	Bound-variable hypothesis builder for product: if 𝑥 is (effectively) not free in 𝐴 and 𝐵, it is not free in ∏𝑘 ∈ 𝐴𝐵. (Contributed by Scott Fenton, 1-Dec-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥∏𝑘 ∈ 𝐴 𝐵
Theorem	prodeq2w 12349*	Equality theorem for product, when the class expressions 𝐵 and 𝐶 are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (∀𝑘 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	prodeq2 12350*	Equality theorem for product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	cbvprod 12351*	Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑘𝐴    &   ⊢ Ⅎ𝑗𝐴    &   ⊢ Ⅎ𝑘𝐵    &   ⊢ Ⅎ𝑗𝐶    ⇒   ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶
Theorem	cbvprodv 12352*	Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    ⇒   ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶
Theorem	cbvprodi 12353*	Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ Ⅎ𝑘𝐵    &   ⊢ Ⅎ𝑗𝐶    &   ⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶)    ⇒   ⊢ ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶
Theorem	prodeq1i 12354*	Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶
Theorem	prodeq2i 12355*	Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝑘 ∈ 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶
Theorem	prodeq12i 12356*	Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑘 ∈ 𝐴 → 𝐶 = 𝐷)    ⇒   ⊢ ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷
Theorem	prodeq1d 12357*	Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)
Theorem	prodeq2d 12358*	Equality deduction for product. Note that unlike prodeq2dv 12359, 𝑘 may occur in 𝜑. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	prodeq2dv 12359*	Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	prodeq2sdv 12360*	Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	2cprodeq2dv 12361*	Equality deduction for double product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐶 = ∏𝑗 ∈ 𝐴 ∏𝑘 ∈ 𝐵 𝐷)
Theorem	prodeq12dv 12362*	Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷)
Theorem	prodeq12rdv 12363*	Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷)
Theorem	prodrbdclem 12364*	Lemma for prodrbdc 12367. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ⊆ (ℤ≥‘𝑁)) → (seq𝑀( · , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( · , 𝐹))
Theorem	fproddccvg 12365*	The sequence of partial products of a finite product converges to the whole product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq𝑀( · , 𝐹)‘𝑁))
Theorem	prodrbdclem2 12366*	Lemma for prodrbdc 12367. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑁))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → DECID 𝑘 ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (seq𝑀( · , 𝐹) ⇝ 𝐶 ↔ seq𝑁( · , 𝐹) ⇝ 𝐶))
Theorem	prodrbdc 12367*	Rebase the starting point of a product. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑁))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → DECID 𝑘 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (seq𝑀( · , 𝐹) ⇝ 𝐶 ↔ seq𝑁( · , 𝐹) ⇝ 𝐶))
Theorem	prodmodclem3 12368*	Lemma for prodmodc 12371. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))    &   ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1))    &   ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ))    &   ⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)    ⇒   ⊢ (𝜑 → (seq1( · , 𝐺)‘𝑀) = (seq1( · , 𝐻)‘𝑁))
Theorem	prodmodclem2a 12369*	Lemma for prodmodc 12371. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))    &   ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝐾‘𝑗) / 𝑘⦌𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))    ⇒   ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ (seq1( · , 𝐺)‘𝑁))
Theorem	prodmodclem2 12370*	Lemma for prodmodc 12371. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 13-Apr-2024.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))    ⇒   ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑧 = (seq1( · , 𝐺)‘𝑚)) → 𝑥 = 𝑧))
Theorem	prodmodc 12371*	A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017.) (Modified by Jim Kingdon, 14-Apr-2024.)
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))    ⇒   ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ∧ seq𝑚( · , 𝐹) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , 𝐺)‘𝑚))))
Theorem	zproddc 12372*	Series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 5-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑍)    &   ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))
Theorem	iprodap 12373*	Series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 5-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝑍 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))
Theorem	zprodap0 12374*	Nonzero series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 6-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑋 # 0)    &   ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋)    &   ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 𝑋)
Theorem	iprodap0 12375*	Nonzero series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 6-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑋 # 0)    &   ⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝑍 𝐵 = 𝑋)
4.9.10.4  Finite products
Theorem	fprodseq 12376*	The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))
Theorem	fprodntrivap 12377*	A non-triviality lemma for finite sequences. (Contributed by Scott Fenton, 16-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑀...𝑁))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ 𝑍 ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
Theorem	prod0 12378	A product over the empty set is one. (Contributed by Scott Fenton, 5-Dec-2017.)
⊢ ∏𝑘 ∈ ∅ 𝐴 = 1
Theorem	prod1dc 12379*	Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.)
⊢ (((𝑀 ∈ ℤ ∧ 𝐴 ⊆ (ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∨ 𝐴 ∈ Fin) → ∏𝑘 ∈ 𝐴 1 = 1)
Theorem	prodfct 12380*	A lemma to facilitate conversions from the function form to the class-variable form of a product. (Contributed by Scott Fenton, 7-Dec-2017.)
⊢ (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ∏𝑗 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑗) = ∏𝑘 ∈ 𝐴 𝐵)
Theorem	fprodf1o 12381*	Re-index a finite product using a bijection. (Contributed by Scott Fenton, 7-Dec-2017.)
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑛 ∈ 𝐶 𝐷)
Theorem	prodssdc 12382*	Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.) (Revised by Jim Kingdon, 6-Aug-2024.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦))    &   ⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 1)    &   ⊢ (𝜑 → 𝐵 ⊆ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)
Theorem	fprodssdc 12383*	Change the index set to a subset in a finite sum. (Contributed by Scott Fenton, 16-Dec-2017.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 1)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)
Theorem	fprodmul 12384*	The product of two finite products. (Contributed by Scott Fenton, 14-Dec-2017.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (𝐵 · 𝐶) = (∏𝑘 ∈ 𝐴 𝐵 · ∏𝑘 ∈ 𝐴 𝐶))
Theorem	prodsnf 12385*	A product of a singleton is the term. A version of prodsn 12386 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑘𝐵    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	prodsn 12386*	A product of a singleton is the term. (Contributed by Scott Fenton, 14-Dec-2017.)
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵)    ⇒   ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	fprod1 12387*	A finite product of only one term is the term itself. (Contributed by Scott Fenton, 14-Dec-2017.)
⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ (𝑀...𝑀)𝐴 = 𝐵)
Theorem	climprod1 12388	The limit of a product over one. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → seq𝑀( · , (𝑍 × {1})) ⇝ 1)
Theorem	fprodsplitdc 12389*	Split a finite product into two parts. New proofs should use fprodsplit 12390 which is the same but with one fewer hypothesis. (Contributed by Scott Fenton, 16-Dec-2017.) (New usage is discouraged.)
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑗 ∈ 𝑈 DECID 𝑗 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝑈 𝐶 = (∏𝑘 ∈ 𝐴 𝐶 · ∏𝑘 ∈ 𝐵 𝐶))
Theorem	fprodsplit 12390*	Split a finite product into two parts. (Contributed by Scott Fenton, 16-Dec-2017.)
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝑈 𝐶 = (∏𝑘 ∈ 𝐴 𝐶 · ∏𝑘 ∈ 𝐵 𝐶))
Theorem	fprodm1 12391*	Separate out the last term in a finite product. (Contributed by Scott Fenton, 16-Dec-2017.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = (∏𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 · 𝐵))
Theorem	fprod1p 12392*	Separate out the first term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = (𝐵 · ∏𝑘 ∈ ((𝑀 + 1)...𝑁)𝐴))
Theorem	fprodp1 12393*	Multiply in the last term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ ℂ)    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 = (∏𝑘 ∈ (𝑀...𝑁)𝐴 · 𝐵))
Theorem	fprodm1s 12394*	Separate out the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = (∏𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 · ⦋𝑁 / 𝑘⦌𝐴))
Theorem	fprodp1s 12395*	Multiply in the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 = (∏𝑘 ∈ (𝑀...𝑁)𝐴 · ⦋(𝑁 + 1) / 𝑘⦌𝐴))
Theorem	prodsns 12396*	A product of the singleton is the term. (Contributed by Scott Fenton, 25-Dec-2017.)
⊢ ((𝑀 ∈ 𝑉 ∧ ⦋𝑀 / 𝑘⦌𝐴 ∈ ℂ) → ∏𝑘 ∈ {𝑀}𝐴 = ⦋𝑀 / 𝑘⦌𝐴)
Theorem	fprodunsn 12397*	Multiply in an additional term in a finite product. See also fprodsplitsn 12426 which is the same but with a Ⅎ𝑘𝜑 hypothesis in place of the distinct variable condition between 𝜑 and 𝑘. (Contributed by Jim Kingdon, 16-Aug-2024.)
⊢ Ⅎ𝑘𝐷    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (𝐴 ∪ {𝐵})𝐶 = (∏𝑘 ∈ 𝐴 𝐶 · 𝐷))
Theorem	fprodcl2lem 12398*	Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	fprodcllem 12399*	Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 1 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	fprodcl 12400*	Closure of a finite product of complex numbers. (Contributed by Scott Fenton, 14-Dec-2017.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ ℂ)