Proof of Theorem itcovalt2lem2lem2
| Step | Hyp | Ref
| Expression |
| 1 | | 2cnd 12344 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 2 ∈
ℂ) |
| 2 | | simpr 484 |
. . . . . . 7
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
| 3 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 𝐶 ∈
ℕ0) |
| 4 | 3 | adantr 480 |
. . . . . . 7
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝐶 ∈
ℕ0) |
| 5 | 2, 4 | nn0addcld 12591 |
. . . . . 6
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 𝐶) ∈
ℕ0) |
| 6 | 5 | nn0cnd 12589 |
. . . . 5
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 𝐶) ∈ ℂ) |
| 7 | | 2nn0 12543 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
| 8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝑌 ∈ ℕ0
→ 2 ∈ ℕ0) |
| 9 | | id 22 |
. . . . . . . 8
⊢ (𝑌 ∈ ℕ0
→ 𝑌 ∈
ℕ0) |
| 10 | 8, 9 | nn0expcld 14285 |
. . . . . . 7
⊢ (𝑌 ∈ ℕ0
→ (2↑𝑌) ∈
ℕ0) |
| 11 | 10 | nn0cnd 12589 |
. . . . . 6
⊢ (𝑌 ∈ ℕ0
→ (2↑𝑌) ∈
ℂ) |
| 12 | 11 | ad2antrr 726 |
. . . . 5
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) →
(2↑𝑌) ∈
ℂ) |
| 13 | 6, 12 | mulcld 11281 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 𝐶) · (2↑𝑌)) ∈ ℂ) |
| 14 | | nn0cn 12536 |
. . . . 5
⊢ (𝐶 ∈ ℕ0
→ 𝐶 ∈
ℂ) |
| 15 | 14 | ad2antlr 727 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝐶 ∈
ℂ) |
| 16 | 1, 13, 15 | subdid 11719 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) = ((2 · ((𝑁 + 𝐶) · (2↑𝑌))) − (2 · 𝐶))) |
| 17 | 16 | oveq1d 7446 |
. 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 12592 |
. . . . 5
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 𝐶) · (2↑𝑌)) ∈
ℕ0) |
| 21 | 18, 20 | nn0mulcld 12592 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· ((𝑁 + 𝐶) · (2↑𝑌))) ∈
ℕ0) |
| 22 | 21 | nn0cnd 12589 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· ((𝑁 + 𝐶) · (2↑𝑌))) ∈
ℂ) |
| 23 | 7 | a1i 11 |
. . . . . 6
⊢ ((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → 2 ∈ ℕ0) |
| 24 | 23, 3 | nn0mulcld 12592 |
. . . . 5
⊢ ((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) → (2 · 𝐶) ∈
ℕ0) |
| 25 | 24 | adantr 480 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· 𝐶) ∈
ℕ0) |
| 26 | 25 | nn0cnd 12589 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· 𝐶) ∈
ℂ) |
| 27 | 4 | nn0cnd 12589 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝐶 ∈
ℂ) |
| 28 | 22, 26, 27 | subsubd 11648 |
. 2
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2
· ((𝑁 + 𝐶) · (2↑𝑌))) − ((2 · 𝐶) − 𝐶)) = (((2 · ((𝑁 + 𝐶) · (2↑𝑌))) − (2 · 𝐶)) + 𝐶)) |
| 29 | 1, 6, 12 | mul12d 11470 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· ((𝑁 + 𝐶) · (2↑𝑌))) = ((𝑁 + 𝐶) · (2 · (2↑𝑌)))) |
| 30 | | 2cnd 12344 |
. . . . . . . 8
⊢ (𝑌 ∈ ℕ0
→ 2 ∈ ℂ) |
| 31 | 30, 11 | mulcomd 11282 |
. . . . . . 7
⊢ (𝑌 ∈ ℕ0
→ (2 · (2↑𝑌)) = ((2↑𝑌) · 2)) |
| 32 | 30, 9 | expp1d 14187 |
. . . . . . 7
⊢ (𝑌 ∈ ℕ0
→ (2↑(𝑌 + 1)) =
((2↑𝑌) ·
2)) |
| 33 | 31, 32 | eqtr4d 2780 |
. . . . . 6
⊢ (𝑌 ∈ ℕ0
→ (2 · (2↑𝑌)) = (2↑(𝑌 + 1))) |
| 34 | 33 | ad2antrr 726 |
. . . . 5
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· (2↑𝑌)) =
(2↑(𝑌 +
1))) |
| 35 | 34 | oveq2d 7447 |
. . . 4
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 𝐶) · (2 · (2↑𝑌))) = ((𝑁 + 𝐶) · (2↑(𝑌 + 1)))) |
| 36 | 29, 35 | eqtrd 2777 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → (2
· ((𝑁 + 𝐶) · (2↑𝑌))) = ((𝑁 + 𝐶) · (2↑(𝑌 + 1)))) |
| 37 | | 2txmxeqx 12406 |
. . . . 5
⊢ (𝐶 ∈ ℂ → ((2
· 𝐶) − 𝐶) = 𝐶) |
| 38 | 14, 37 | syl 17 |
. . . 4
⊢ (𝐶 ∈ ℕ0
→ ((2 · 𝐶)
− 𝐶) = 𝐶) |
| 39 | 38 | ad2antlr 727 |
. . 3
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2
· 𝐶) − 𝐶) = 𝐶) |
| 40 | 36, 39 | oveq12d 7449 |
. 2
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2
· ((𝑁 + 𝐶) · (2↑𝑌))) − ((2 · 𝐶) − 𝐶)) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶)) |
| 41 | 17, 28, 40 | 3eqtr2d 2783 |
1
⊢ (((𝑌 ∈ ℕ0
∧ 𝐶 ∈
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2
· (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶)) |