Metamath Proof Explorer

Theorem itcovalt2lem2lem2

Description: Lemma 2 for itcovalt2lem2 . (Contributed by AV, 7-May-2024)

Ref Expression
Assertion itcovalt2lem2lem2 
|- ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( 2 x. ( ( ( N + C ) x. ( 2 ^ Y ) ) - C ) ) + C ) = ( ( ( N + C ) x. ( 2 ^ ( Y + 1 ) ) ) - C ) )

Proof

Step Hyp Ref Expression
1 2cnd 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> 2 e. CC )
2 simpr 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> N e. NN0 )
3 simpr 
 |-  ( ( Y e. NN0 /\ C e. NN0 ) -> C e. NN0 )
4 3 adantr 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> C e. NN0 )
5 2 4 nn0addcld 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( N + C ) e. NN0 )
6 5 nn0cnd 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( N + C ) e. CC )
7 2nn0 
 |-  2 e. NN0
8 7 a1i 
 |-  ( Y e. NN0 -> 2 e. NN0 )
9 id 
 |-  ( Y e. NN0 -> Y e. NN0 )
10 8 9 nn0expcld 
 |-  ( Y e. NN0 -> ( 2 ^ Y ) e. NN0 )
11 10 nn0cnd 
 |-  ( Y e. NN0 -> ( 2 ^ Y ) e. CC )
12 11 ad2antrr 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( 2 ^ Y ) e. CC )
13 6 12 mulcld 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( N + C ) x. ( 2 ^ Y ) ) e. CC )
14 nn0cn 
 |-  ( C e. NN0 -> C e. CC )
15 14 ad2antlr 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> C e. CC )
16 1 13 15 subdid 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( 2 x. ( ( ( N + C ) x. ( 2 ^ Y ) ) - C ) ) = ( ( 2 x. ( ( N + C ) x. ( 2 ^ Y ) ) ) - ( 2 x. C ) ) )
17 16 oveq1d 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( 2 x. ( ( ( N + C ) x. ( 2 ^ Y ) ) - C ) ) + C ) = ( ( ( 2 x. ( ( N + C ) x. ( 2 ^ Y ) ) ) - ( 2 x. C ) ) + C ) )
18 7 a1i 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> 2 e. NN0 )
19 10 ad2antrr 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( 2 ^ Y ) e. NN0 )
20 5 19 nn0mulcld 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( N + C ) x. ( 2 ^ Y ) ) e. NN0 )
21 18 20 nn0mulcld 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( 2 x. ( ( N + C ) x. ( 2 ^ Y ) ) ) e. NN0 )
22 21 nn0cnd 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( 2 x. ( ( N + C ) x. ( 2 ^ Y ) ) ) e. CC )
23 7 a1i 
 |-  ( ( Y e. NN0 /\ C e. NN0 ) -> 2 e. NN0 )
24 23 3 nn0mulcld 
 |-  ( ( Y e. NN0 /\ C e. NN0 ) -> ( 2 x. C ) e. NN0 )
25 24 adantr 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( 2 x. C ) e. NN0 )
26 25 nn0cnd 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( 2 x. C ) e. CC )
27 4 nn0cnd 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> C e. CC )
28 22 26 27 subsubd 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( 2 x. ( ( N + C ) x. ( 2 ^ Y ) ) ) - ( ( 2 x. C ) - C ) ) = ( ( ( 2 x. ( ( N + C ) x. ( 2 ^ Y ) ) ) - ( 2 x. C ) ) + C ) )
29 1 6 12 mul12d 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( 2 x. ( ( N + C ) x. ( 2 ^ Y ) ) ) = ( ( N + C ) x. ( 2 x. ( 2 ^ Y ) ) ) )
30 2cnd 
 |-  ( Y e. NN0 -> 2 e. CC )
31 30 11 mulcomd 
 |-  ( Y e. NN0 -> ( 2 x. ( 2 ^ Y ) ) = ( ( 2 ^ Y ) x. 2 ) )
32 30 9 expp1d 
 |-  ( Y e. NN0 -> ( 2 ^ ( Y + 1 ) ) = ( ( 2 ^ Y ) x. 2 ) )
33 31 32 eqtr4d 
 |-  ( Y e. NN0 -> ( 2 x. ( 2 ^ Y ) ) = ( 2 ^ ( Y + 1 ) ) )
34 33 ad2antrr 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( 2 x. ( 2 ^ Y ) ) = ( 2 ^ ( Y + 1 ) ) )
35 34 oveq2d 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( N + C ) x. ( 2 x. ( 2 ^ Y ) ) ) = ( ( N + C ) x. ( 2 ^ ( Y + 1 ) ) ) )
36 29 35 eqtrd 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( 2 x. ( ( N + C ) x. ( 2 ^ Y ) ) ) = ( ( N + C ) x. ( 2 ^ ( Y + 1 ) ) ) )
37 2txmxeqx 
 |-  ( C e. CC -> ( ( 2 x. C ) - C ) = C )
38 14 37 syl 
 |-  ( C e. NN0 -> ( ( 2 x. C ) - C ) = C )
39 38 ad2antlr 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( 2 x. C ) - C ) = C )
40 36 39 oveq12d 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( 2 x. ( ( N + C ) x. ( 2 ^ Y ) ) ) - ( ( 2 x. C ) - C ) ) = ( ( ( N + C ) x. ( 2 ^ ( Y + 1 ) ) ) - C ) )
41 17 28 40 3eqtr2d 
 |-  ( ( ( Y e. NN0 /\ C e. NN0 ) /\ N e. NN0 ) -> ( ( 2 x. ( ( ( N + C ) x. ( 2 ^ Y ) ) - C ) ) + C ) = ( ( ( N + C ) x. ( 2 ^ ( Y + 1 ) ) ) - C ) )