Metamath Proof Explorer


Theorem fprodm1s

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

Ref Expression
Hypotheses fprodm1s.1 φ N M
fprodm1s.2 φ k M N A
Assertion fprodm1s φ k = M N A = k = M N 1 A N / k A

Proof

Step Hyp Ref Expression
1 fprodm1s.1 φ N M
2 fprodm1s.2 φ k M N A
3 2 ralrimiva φ k M N 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 k M N A m / k A
9 3 8 mpan9 φ m M N m / k A
10 csbeq1 m = N m / k A = N / k A
11 1 9 10 fprodm1 φ m = M N m / k A = m = M N 1 m / k A N / k A
12 nfcv _ m A
13 12 4 6 cbvprodi k = M N A = m = M N m / k A
14 12 4 6 cbvprodi k = M N 1 A = m = M N 1 m / k A
15 14 oveq1i k = M N 1 A N / k A = m = M N 1 m / k A N / k A
16 11 13 15 3eqtr4g φ k = M N A = k = M N 1 A N / k A