Metamath Proof Explorer

Theorem fprodsubrecnncnvlem

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 fprodsubrecnncnvlem.k 
|- F/ k ph
fprodsubrecnncnvlem.a 
|- ( ph -> A e. Fin )
fprodsubrecnncnvlem.b 
|- ( ( ph /\ k e. A ) -> B e. CC )
fprodsubrecnncnvlem.s 
|- S = ( n e. NN |-> prod_ k e. A ( B - ( 1 / n ) ) )
fprodsubrecnncnvlem.f 
|- F = ( x e. CC |-> prod_ k e. A ( B - x ) )
fprodsubrecnncnvlem.g 
|- G = ( n e. NN |-> ( 1 / n ) )
Assertion fprodsubrecnncnvlem 
|- ( ph -> S ~~> prod_ k e. A B )

Proof

Step Hyp Ref Expression
1 fprodsubrecnncnvlem.k 
 |-  F/ k ph
2 fprodsubrecnncnvlem.a 
 |-  ( ph -> A e. Fin )
3 fprodsubrecnncnvlem.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 fprodsubrecnncnvlem.s 
 |-  S = ( n e. NN |-> prod_ k e. A ( B - ( 1 / n ) ) )
5 fprodsubrecnncnvlem.f 
 |-  F = ( x e. CC |-> prod_ k e. A ( B - x ) )
6 fprodsubrecnncnvlem.g 
 |-  G = ( n e. NN |-> ( 1 / n ) )
7 nnuz 
 |-  NN = ( ZZ>= ` 1 )
8 1zzd 
 |-  ( ph -> 1 e. ZZ )
9 1 2 3 5 fprodsub2cncf 
 |-  ( ph -> F e. ( CC -cn-> CC ) )
10 1rp 
 |-  1 e. RR+
11 10 a1i 
 |-  ( n e. NN -> 1 e. RR+ )
12 nnrp 
 |-  ( n e. NN -> n e. RR+ )
13 11 12 rpdivcld 
 |-  ( n e. NN -> ( 1 / n ) e. RR+ )
14 13 rpcnd 
 |-  ( n e. NN -> ( 1 / n ) e. CC )
15 14 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / n ) e. CC )
16 15 6 fmptd 
 |-  ( ph -> G : NN --> CC )
17 1cnd 
 |-  ( ph -> 1 e. CC )
18 divcnv 
 |-  ( 1 e. CC -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 )
19 17 18 syl 
 |-  ( ph -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 )
20 6 a1i 
 |-  ( ph -> G = ( n e. NN |-> ( 1 / n ) ) )
21 20 breq1d 
 |-  ( ph -> ( G ~~> 0 <-> ( n e. NN |-> ( 1 / n ) ) ~~> 0 ) )
22 19 21 mpbird 
 |-  ( ph -> G ~~> 0 )
23 0cnd 
 |-  ( ph -> 0 e. CC )
24 7 8 9 16 22 23 climcncf 
 |-  ( ph -> ( F o. G ) ~~> ( F ` 0 ) )
25 nfv 
 |-  F/ k x e. CC
26 1 25 nfan 
 |-  F/ k ( ph /\ x e. CC )
27 2 adantr 
 |-  ( ( ph /\ x e. CC ) -> A e. Fin )
28 3 adantlr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. A ) -> B e. CC )
29 simplr 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. A ) -> x e. CC )
30 28 29 subcld 
 |-  ( ( ( ph /\ x e. CC ) /\ k e. A ) -> ( B - x ) e. CC )
31 26 27 30 fprodclf 
 |-  ( ( ph /\ x e. CC ) -> prod_ k e. A ( B - x ) e. CC )
32 31 5 fmptd 
 |-  ( ph -> F : CC --> CC )
33 fcompt 
 |-  ( ( F : CC --> CC /\ G : NN --> CC ) -> ( F o. G ) = ( n e. NN |-> ( F ` ( G ` n ) ) ) )
34 32 16 33 syl2anc 
 |-  ( ph -> ( F o. G ) = ( n e. NN |-> ( F ` ( G ` n ) ) ) )
35 4 a1i 
 |-  ( ph -> S = ( n e. NN |-> prod_ k e. A ( B - ( 1 / n ) ) ) )
36 id 
 |-  ( n e. NN -> n e. NN )
37 6 fvmpt2 
 |-  ( ( n e. NN /\ ( 1 / n ) e. CC ) -> ( G ` n ) = ( 1 / n ) )
38 36 14 37 syl2anc 
 |-  ( n e. NN -> ( G ` n ) = ( 1 / n ) )
39 38 fveq2d 
 |-  ( n e. NN -> ( F ` ( G ` n ) ) = ( F ` ( 1 / n ) ) )
40 39 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( F ` ( G ` n ) ) = ( F ` ( 1 / n ) ) )
41 oveq2 
 |-  ( x = ( 1 / n ) -> ( B - x ) = ( B - ( 1 / n ) ) )
42 41 prodeq2ad 
 |-  ( x = ( 1 / n ) -> prod_ k e. A ( B - x ) = prod_ k e. A ( B - ( 1 / n ) ) )
43 prodex 
 |-  prod_ k e. A ( B - ( 1 / n ) ) e. _V
44 43 a1i 
 |-  ( ( ph /\ n e. NN ) -> prod_ k e. A ( B - ( 1 / n ) ) e. _V )
45 5 42 15 44 fvmptd3 
 |-  ( ( ph /\ n e. NN ) -> ( F ` ( 1 / n ) ) = prod_ k e. A ( B - ( 1 / n ) ) )
46 40 45 eqtr2d 
 |-  ( ( ph /\ n e. NN ) -> prod_ k e. A ( B - ( 1 / n ) ) = ( F ` ( G ` n ) ) )
47 46 mpteq2dva 
 |-  ( ph -> ( n e. NN |-> prod_ k e. A ( B - ( 1 / n ) ) ) = ( n e. NN |-> ( F ` ( G ` n ) ) ) )
48 35 47 eqtrd 
 |-  ( ph -> S = ( n e. NN |-> ( F ` ( G ` n ) ) ) )
49 34 48 eqtr4d 
 |-  ( ph -> ( F o. G ) = S )
50 5 a1i 
 |-  ( ph -> F = ( x e. CC |-> prod_ k e. A ( B - x ) ) )
51 nfv 
 |-  F/ k x = 0
52 1 51 nfan 
 |-  F/ k ( ph /\ x = 0 )
53 oveq2 
 |-  ( x = 0 -> ( B - x ) = ( B - 0 ) )
54 53 ad2antlr 
 |-  ( ( ( ph /\ x = 0 ) /\ k e. A ) -> ( B - x ) = ( B - 0 ) )
55 3 subid1d 
 |-  ( ( ph /\ k e. A ) -> ( B - 0 ) = B )
56 55 adantlr 
 |-  ( ( ( ph /\ x = 0 ) /\ k e. A ) -> ( B - 0 ) = B )
57 54 56 eqtrd 
 |-  ( ( ( ph /\ x = 0 ) /\ k e. A ) -> ( B - x ) = B )
58 57 ex 
 |-  ( ( ph /\ x = 0 ) -> ( k e. A -> ( B - x ) = B ) )
59 52 58 ralrimi 
 |-  ( ( ph /\ x = 0 ) -> A. k e. A ( B - x ) = B )
60 59 prodeq2d 
 |-  ( ( ph /\ x = 0 ) -> prod_ k e. A ( B - x ) = prod_ k e. A B )
61 prodex 
 |-  prod_ k e. A B e. _V
62 61 a1i 
 |-  ( ph -> prod_ k e. A B e. _V )
63 50 60 23 62 fvmptd 
 |-  ( ph -> ( F ` 0 ) = prod_ k e. A B )
64 49 63 breq12d 
 |-  ( ph -> ( ( F o. G ) ~~> ( F ` 0 ) <-> S ~~> prod_ k e. A B ) )
65 24 64 mpbid 
 |-  ( ph -> S ~~> prod_ k e. A B )