Metamath Proof Explorer

Theorem faclimlem3

Description: Lemma for faclim . Algebraic manipulation for the final induction. (Contributed by Scott Fenton, 15-Dec-2017)

Ref Expression
Assertion faclimlem3 
|- ( ( M e. NN0 /\ B e. NN ) -> ( ( ( 1 + ( 1 / B ) ) ^ ( M + 1 ) ) / ( 1 + ( ( M + 1 ) / B ) ) ) = ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( ( ( 1 + ( M / B ) ) x. ( 1 + ( 1 / B ) ) ) / ( 1 + ( ( M + 1 ) / B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 1rp 
 |-  1 e. RR+
2 1 a1i 
 |-  ( ( M e. NN0 /\ B e. NN ) -> 1 e. RR+ )
3 nnrp 
 |-  ( B e. NN -> B e. RR+ )
4 3 rpreccld 
 |-  ( B e. NN -> ( 1 / B ) e. RR+ )
5 4 adantl 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( 1 / B ) e. RR+ )
6 2 5 rpaddcld 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( 1 + ( 1 / B ) ) e. RR+ )
7 6 rpcnd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( 1 + ( 1 / B ) ) e. CC )
8 simpl 
 |-  ( ( M e. NN0 /\ B e. NN ) -> M e. NN0 )
9 7 8 expp1d 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( 1 + ( 1 / B ) ) ^ ( M + 1 ) ) = ( ( ( 1 + ( 1 / B ) ) ^ M ) x. ( 1 + ( 1 / B ) ) ) )
10 1 a1i 
 |-  ( B e. NN -> 1 e. RR+ )
11 10 4 rpaddcld 
 |-  ( B e. NN -> ( 1 + ( 1 / B ) ) e. RR+ )
12 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
13 rpexpcl 
 |-  ( ( ( 1 + ( 1 / B ) ) e. RR+ /\ M e. ZZ ) -> ( ( 1 + ( 1 / B ) ) ^ M ) e. RR+ )
14 11 12 13 syl2anr 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( 1 + ( 1 / B ) ) ^ M ) e. RR+ )
15 14 rpcnd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( 1 + ( 1 / B ) ) ^ M ) e. CC )
16 1cnd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> 1 e. CC )
17 nn0nndivcl 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( M / B ) e. RR )
18 17 recnd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( M / B ) e. CC )
19 16 18 addcomd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( 1 + ( M / B ) ) = ( ( M / B ) + 1 ) )
20 nn0ge0div 
 |-  ( ( M e. NN0 /\ B e. NN ) -> 0 <_ ( M / B ) )
21 17 20 ge0p1rpd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( M / B ) + 1 ) e. RR+ )
22 19 21 eqeltrd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( 1 + ( M / B ) ) e. RR+ )
23 22 rpcnd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( 1 + ( M / B ) ) e. CC )
24 22 rpne0d 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( 1 + ( M / B ) ) =/= 0 )
25 15 23 24 divcan1d 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( 1 + ( M / B ) ) ) = ( ( 1 + ( 1 / B ) ) ^ M ) )
26 25 oveq1d 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( 1 + ( M / B ) ) ) x. ( 1 + ( 1 / B ) ) ) = ( ( ( 1 + ( 1 / B ) ) ^ M ) x. ( 1 + ( 1 / B ) ) ) )
27 14 22 rpdivcld 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) e. RR+ )
28 27 rpcnd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) e. CC )
29 28 23 7 mulassd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( 1 + ( M / B ) ) ) x. ( 1 + ( 1 / B ) ) ) = ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( ( 1 + ( M / B ) ) x. ( 1 + ( 1 / B ) ) ) ) )
30 9 26 29 3eqtr2d 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( 1 + ( 1 / B ) ) ^ ( M + 1 ) ) = ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( ( 1 + ( M / B ) ) x. ( 1 + ( 1 / B ) ) ) ) )
31 30 oveq1d 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( ( 1 + ( 1 / B ) ) ^ ( M + 1 ) ) / ( 1 + ( ( M + 1 ) / B ) ) ) = ( ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( ( 1 + ( M / B ) ) x. ( 1 + ( 1 / B ) ) ) ) / ( 1 + ( ( M + 1 ) / B ) ) ) )
32 22 6 rpmulcld 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( 1 + ( M / B ) ) x. ( 1 + ( 1 / B ) ) ) e. RR+ )
33 32 rpcnd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( 1 + ( M / B ) ) x. ( 1 + ( 1 / B ) ) ) e. CC )
34 nn0p1nn 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN )
35 34 nnrpd 
 |-  ( M e. NN0 -> ( M + 1 ) e. RR+ )
36 35 adantr 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( M + 1 ) e. RR+ )
37 3 adantl 
 |-  ( ( M e. NN0 /\ B e. NN ) -> B e. RR+ )
38 36 37 rpdivcld 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( M + 1 ) / B ) e. RR+ )
39 2 38 rpaddcld 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( 1 + ( ( M + 1 ) / B ) ) e. RR+ )
40 39 rpcnd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( 1 + ( ( M + 1 ) / B ) ) e. CC )
41 39 rpne0d 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( 1 + ( ( M + 1 ) / B ) ) =/= 0 )
42 28 33 40 41 divassd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( ( 1 + ( M / B ) ) x. ( 1 + ( 1 / B ) ) ) ) / ( 1 + ( ( M + 1 ) / B ) ) ) = ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( ( ( 1 + ( M / B ) ) x. ( 1 + ( 1 / B ) ) ) / ( 1 + ( ( M + 1 ) / B ) ) ) ) )
43 31 42 eqtrd 
 |-  ( ( M e. NN0 /\ B e. NN ) -> ( ( ( 1 + ( 1 / B ) ) ^ ( M + 1 ) ) / ( 1 + ( ( M + 1 ) / B ) ) ) = ( ( ( ( 1 + ( 1 / B ) ) ^ M ) / ( 1 + ( M / B ) ) ) x. ( ( ( 1 + ( M / B ) ) x. ( 1 + ( 1 / B ) ) ) / ( 1 + ( ( M + 1 ) / B ) ) ) ) )