Metamath Proof Explorer

Theorem itcovalt2lem2lem2

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

Ref Expression
Assertion itcovalt2lem2lem2 ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 · ( ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) − 𝐶 ) ) + 𝐶 ) = ( ( ( 𝑁 + 𝐶 ) · ( 2 ↑ ( 𝑌 + 1 ) ) ) − 𝐶 ) )

Proof

Step Hyp Ref Expression
1 2cnd ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℂ )
2 simpr ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
3 simpr ⊢ ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
4 3 adantr ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
5 2 4 nn0addcld ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 𝐶 ) ∈ ℕ0 )
6 5 nn0cnd ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 𝐶 ) ∈ ℂ )
7 2nn0 ⊢ 2 ∈ ℕ0
8 7 a1i ⊢ ( 𝑌 ∈ ℕ0 → 2 ∈ ℕ0 )
9 id ⊢ ( 𝑌 ∈ ℕ0 → 𝑌 ∈ ℕ0 )
10 8 9 nn0expcld ⊢ ( 𝑌 ∈ ℕ0 → ( 2 ↑ 𝑌 ) ∈ ℕ0 )
11 10 nn0cnd ⊢ ( 𝑌 ∈ ℕ0 → ( 2 ↑ 𝑌 ) ∈ ℂ )
12 11 ad2antrr ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑌 ) ∈ ℂ )
13 6 12 mulcld ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ∈ ℂ )
14 nn0cn ⊢ ( 𝐶 ∈ ℕ0 → 𝐶 ∈ ℂ )
15 14 ad2antlr ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
16 1 13 15 subdid ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) − 𝐶 ) ) = ( ( 2 · ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ) − ( 2 · 𝐶 ) ) )
17 16 oveq1d ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 · ( ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) − 𝐶 ) ) + 𝐶 ) = ( ( ( 2 · ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ) − ( 2 · 𝐶 ) ) + 𝐶 ) )
18 7 a1i ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℕ0 )
19 10 ad2antrr ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑌 ) ∈ ℕ0 )
20 5 19 nn0mulcld ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ∈ ℕ0 )
21 18 20 nn0mulcld ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ) ∈ ℕ0 )
22 21 nn0cnd ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ) ∈ ℂ )
23 7 a1i ⊢ ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → 2 ∈ ℕ0 )
24 23 3 nn0mulcld ⊢ ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 2 · 𝐶 ) ∈ ℕ0 )
25 24 adantr ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 · 𝐶 ) ∈ ℕ0 )
26 25 nn0cnd ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 · 𝐶 ) ∈ ℂ )
27 4 nn0cnd ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
28 22 26 27 subsubd ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 · ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ) − ( ( 2 · 𝐶 ) − 𝐶 ) ) = ( ( ( 2 · ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ) − ( 2 · 𝐶 ) ) + 𝐶 ) )
29 1 6 12 mul12d ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ) = ( ( 𝑁 + 𝐶 ) · ( 2 · ( 2 ↑ 𝑌 ) ) ) )
30 2cnd ⊢ ( 𝑌 ∈ ℕ0 → 2 ∈ ℂ )
31 30 11 mulcomd ⊢ ( 𝑌 ∈ ℕ0 → ( 2 · ( 2 ↑ 𝑌 ) ) = ( ( 2 ↑ 𝑌 ) · 2 ) )
32 30 9 expp1d ⊢ ( 𝑌 ∈ ℕ0 → ( 2 ↑ ( 𝑌 + 1 ) ) = ( ( 2 ↑ 𝑌 ) · 2 ) )
33 31 32 eqtr4d ⊢ ( 𝑌 ∈ ℕ0 → ( 2 · ( 2 ↑ 𝑌 ) ) = ( 2 ↑ ( 𝑌 + 1 ) ) )
34 33 ad2antrr ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑌 ) ) = ( 2 ↑ ( 𝑌 + 1 ) ) )
35 34 oveq2d ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 𝐶 ) · ( 2 · ( 2 ↑ 𝑌 ) ) ) = ( ( 𝑁 + 𝐶 ) · ( 2 ↑ ( 𝑌 + 1 ) ) ) )
36 29 35 eqtrd ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ) = ( ( 𝑁 + 𝐶 ) · ( 2 ↑ ( 𝑌 + 1 ) ) ) )
37 2txmxeqx ⊢ ( 𝐶 ∈ ℂ → ( ( 2 · 𝐶 ) − 𝐶 ) = 𝐶 )
38 14 37 syl ⊢ ( 𝐶 ∈ ℕ0 → ( ( 2 · 𝐶 ) − 𝐶 ) = 𝐶 )
39 38 ad2antlr ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 · 𝐶 ) − 𝐶 ) = 𝐶 )
40 36 39 oveq12d ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 · ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) ) − ( ( 2 · 𝐶 ) − 𝐶 ) ) = ( ( ( 𝑁 + 𝐶 ) · ( 2 ↑ ( 𝑌 + 1 ) ) ) − 𝐶 ) )
41 17 28 40 3eqtr2d ⊢ ( ( ( 𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 · ( ( ( 𝑁 + 𝐶 ) · ( 2 ↑ 𝑌 ) ) − 𝐶 ) ) + 𝐶 ) = ( ( ( 𝑁 + 𝐶 ) · ( 2 ↑ ( 𝑌 + 1 ) ) ) − 𝐶 ) )