| 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 ) ) |