This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fprodp1s

Description: Multiply in the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017)

Ref Expression
Hypotheses fprodp1s.1 ⊢ φ → N ∈ ℤ ≥ M
fprodp1s.2 ⊢ φ ∧ k ∈ M … N + 1 → A ∈ ℂ
Assertion fprodp1s ⊢ φ → ∏ k = M N + 1 A = ∏ k = M N A ⁢ ⦋ N + 1 / k⦌ A

Proof

Step Hyp Ref Expression
1 fprodp1s.1 ⊢ φ → N ∈ ℤ ≥ M
2 fprodp1s.2 ⊢ φ ∧ k ∈ M … N + 1 → A ∈ ℂ
3 2 ralrimiva ⊢ φ → ∀ k ∈ M … N + 1 A ∈ ℂ
4 nfcsb1v ⊢ Ⅎ _ k ⦋ m / k⦌ A
5 4 nfel1 ⊢ Ⅎ k ⦋ m / k⦌ A ∈ ℂ
6 csbeq1a ⊢ k = m → A = ⦋ m / k⦌ A
7 6 eleq1d ⊢ k = m → A ∈ ℂ ↔ ⦋ m / k⦌ A ∈ ℂ
8 5 7 rspc ⊢ m ∈ M … N + 1 → ∀ k ∈ M … N + 1 A ∈ ℂ → ⦋ m / k⦌ A ∈ ℂ
9 3 8 mpan9 ⊢ φ ∧ m ∈ M … N + 1 → ⦋ m / k⦌ A ∈ ℂ
10 csbeq1 ⊢ m = N + 1 → ⦋ m / k⦌ A = ⦋ N + 1 / k⦌ A
11 1 9 10 fprodp1 ⊢ φ → ∏ m = M N + 1 ⦋ m / k⦌ A = ∏ m = M N ⦋ m / k⦌ A ⁢ ⦋ N + 1 / k⦌ A
12 nfcv ⊢ Ⅎ _ m A
13 12 4 6 cbvprodi ⊢ ∏ k = M N + 1 A = ∏ m = M N + 1 ⦋ m / k⦌ A
14 12 4 6 cbvprodi ⊢ ∏ k = M N A = ∏ m = M N ⦋ m / k⦌ A
15 14 oveq1i ⊢ ∏ k = M N A ⁢ ⦋ N + 1 / k⦌ A = ∏ m = M N ⦋ m / k⦌ A ⁢ ⦋ N + 1 / k⦌ A
16 11 13 15 3eqtr4g ⊢ φ → ∏ k = M N + 1 A = ∏ k = M N A ⁢ ⦋ N + 1 / k⦌ A