Description: The sequence S of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fprodsubrecnncnv.1 | ||
fprodsubrecnncnv.2 | |||
fprodsubrecnncnv.3 | |||
fprodsubrecnncnv.4 | |||
Assertion | fprodsubrecnncnv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fprodsubrecnncnv.1 | ||
2 | fprodsubrecnncnv.2 | ||
3 | fprodsubrecnncnv.3 | ||
4 | fprodsubrecnncnv.4 | ||
5 | eqid | ||
6 | oveq2 | ||
7 | 6 | cbvmptv | |
8 | 1 2 3 4 5 7 | fprodsubrecnncnvlem |