Proof of Theorem itcovalt2lem2lem2
Step | Hyp | Ref
| Expression |
1 | | 2cnd 11737 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 2 ∈
ℂ) |
2 | | simpr 489 |
. . . . . . 7
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
3 | | simpr 489 |
. . . . . . . 8
⊢ ((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 𝐶 ∈
ℕ0) |
4 | 3 | adantr 485 |
. . . . . . 7
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝐶 ∈
ℕ0) |
5 | 2, 4 | nn0addcld 11983 |
. . . . . 6
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 𝐶) ∈
ℕ0) |
6 | 5 | nn0cnd 11981 |
. . . . 5
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 𝐶) ∈ ℂ) |
7 | | 2nn0 11936 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝑌 ∈ ℕ0
→ 2 ∈ ℕ0) |
9 | | id 22 |
. . . . . . . 8
⊢ (𝑌 ∈ ℕ0
→ 𝑌 ∈
ℕ0) |
10 | 8, 9 | nn0expcld 13642 |
. . . . . . 7
⊢ (𝑌 ∈ ℕ0
→ (2↑𝑌) ∈
ℕ0) |
11 | 10 | nn0cnd 11981 |
. . . . . 6
⊢ (𝑌 ∈ ℕ0
→ (2↑𝑌) ∈
ℂ) |
12 | 11 | ad2antrr 726 |
. . . . 5
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) →
(2↑𝑌) ∈
ℂ) |
13 | 6, 12 | mulcld 10684 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 𝐶) · (2↑𝑌)) ∈ ℂ) |
14 | | nn0cn 11929 |
. . . . 5
⊢ (𝐶 ∈ ℕ0
→ 𝐶 ∈
ℂ) |
15 | 14 | ad2antlr 727 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝐶 ∈
ℂ) |
16 | 1, 13, 15 | subdid 11119 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) = ((2 · ((𝑁 + 𝐶) · (2↑𝑌))) − (2 · 𝐶))) |
17 | 16 | oveq1d 7158 |
. 2
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2
· (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((2 · ((𝑁 + 𝐶) · (2↑𝑌))) − (2 · 𝐶)) + 𝐶)) |
18 | 7 | a1i 11 |
. . . . 5
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 2 ∈
ℕ0) |
19 | 10 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) →
(2↑𝑌) ∈
ℕ0) |
20 | 5, 19 | nn0mulcld 11984 |
. . . . 5
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 𝐶) · (2↑𝑌)) ∈
ℕ0) |
21 | 18, 20 | nn0mulcld 11984 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· ((𝑁 + 𝐶) · (2↑𝑌))) ∈
ℕ0) |
22 | 21 | nn0cnd 11981 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· ((𝑁 + 𝐶) · (2↑𝑌))) ∈
ℂ) |
23 | 7 | a1i 11 |
. . . . . 6
⊢ ((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 2 ∈ ℕ0) |
24 | 23, 3 | nn0mulcld 11984 |
. . . . 5
⊢ ((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (2 · 𝐶) ∈
ℕ0) |
25 | 24 | adantr 485 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· 𝐶) ∈
ℕ0) |
26 | 25 | nn0cnd 11981 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· 𝐶) ∈
ℂ) |
27 | 4 | nn0cnd 11981 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝐶 ∈
ℂ) |
28 | 22, 26, 27 | subsubd 11048 |
. 2
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2
· ((𝑁 + 𝐶) · (2↑𝑌))) − ((2 · 𝐶) − 𝐶)) = (((2 · ((𝑁 + 𝐶) · (2↑𝑌))) − (2 · 𝐶)) + 𝐶)) |
29 | 1, 6, 12 | mul12d 10872 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· ((𝑁 + 𝐶) · (2↑𝑌))) = ((𝑁 + 𝐶) · (2 · (2↑𝑌)))) |
30 | | 2cnd 11737 |
. . . . . . . 8
⊢ (𝑌 ∈ ℕ0
→ 2 ∈ ℂ) |
31 | 30, 11 | mulcomd 10685 |
. . . . . . 7
⊢ (𝑌 ∈ ℕ0
→ (2 · (2↑𝑌)) = ((2↑𝑌) · 2)) |
32 | 30, 9 | expp1d 13546 |
. . . . . . 7
⊢ (𝑌 ∈ ℕ0
→ (2↑(𝑌 + 1)) =
((2↑𝑌) ·
2)) |
33 | 31, 32 | eqtr4d 2797 |
. . . . . 6
⊢ (𝑌 ∈ ℕ0
→ (2 · (2↑𝑌)) = (2↑(𝑌 + 1))) |
34 | 33 | ad2antrr 726 |
. . . . 5
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· (2↑𝑌)) =
(2↑(𝑌 +
1))) |
35 | 34 | oveq2d 7159 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 𝐶) · (2 · (2↑𝑌))) = ((𝑁 + 𝐶) · (2↑(𝑌 + 1)))) |
36 | 29, 35 | eqtrd 2794 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· ((𝑁 + 𝐶) · (2↑𝑌))) = ((𝑁 + 𝐶) · (2↑(𝑌 + 1)))) |
37 | | 2txmxeqx 11799 |
. . . . 5
⊢ (𝐶 ∈ ℂ → ((2
· 𝐶) − 𝐶) = 𝐶) |
38 | 14, 37 | syl 17 |
. . . 4
⊢ (𝐶 ∈ ℕ0
→ ((2 · 𝐶)
− 𝐶) = 𝐶) |
39 | 38 | ad2antlr 727 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2
· 𝐶) − 𝐶) = 𝐶) |
40 | 36, 39 | oveq12d 7161 |
. 2
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2
· ((𝑁 + 𝐶) · (2↑𝑌))) − ((2 · 𝐶) − 𝐶)) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶)) |
41 | 17, 28, 40 | 3eqtr2d 2800 |
1
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2
· (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶)) |