Step | Hyp | Ref
| Expression |
1 | | oveq2 6918 |
. . . 4
⊢ (𝑘 = 0 → (4↑𝑘) = (4↑0)) |
2 | 1 | oveq1d 6925 |
. . 3
⊢ (𝑘 = 0 → ((4↑𝑘) + 2) = ((4↑0) +
2)) |
3 | 2 | breq2d 4887 |
. 2
⊢ (𝑘 = 0 → (3 ∥
((4↑𝑘) + 2) ↔ 3
∥ ((4↑0) + 2))) |
4 | | oveq2 6918 |
. . . 4
⊢ (𝑘 = 𝑛 → (4↑𝑘) = (4↑𝑛)) |
5 | 4 | oveq1d 6925 |
. . 3
⊢ (𝑘 = 𝑛 → ((4↑𝑘) + 2) = ((4↑𝑛) + 2)) |
6 | 5 | breq2d 4887 |
. 2
⊢ (𝑘 = 𝑛 → (3 ∥ ((4↑𝑘) + 2) ↔ 3 ∥
((4↑𝑛) +
2))) |
7 | | oveq2 6918 |
. . . 4
⊢ (𝑘 = (𝑛 + 1) → (4↑𝑘) = (4↑(𝑛 + 1))) |
8 | 7 | oveq1d 6925 |
. . 3
⊢ (𝑘 = (𝑛 + 1) → ((4↑𝑘) + 2) = ((4↑(𝑛 + 1)) + 2)) |
9 | 8 | breq2d 4887 |
. 2
⊢ (𝑘 = (𝑛 + 1) → (3 ∥ ((4↑𝑘) + 2) ↔ 3 ∥
((4↑(𝑛 + 1)) +
2))) |
10 | | oveq2 6918 |
. . . 4
⊢ (𝑘 = 𝑁 → (4↑𝑘) = (4↑𝑁)) |
11 | 10 | oveq1d 6925 |
. . 3
⊢ (𝑘 = 𝑁 → ((4↑𝑘) + 2) = ((4↑𝑁) + 2)) |
12 | 11 | breq2d 4887 |
. 2
⊢ (𝑘 = 𝑁 → (3 ∥ ((4↑𝑘) + 2) ↔ 3 ∥
((4↑𝑁) +
2))) |
13 | | 3z 11745 |
. . . 4
⊢ 3 ∈
ℤ |
14 | | iddvds 15379 |
. . . 4
⊢ (3 ∈
ℤ → 3 ∥ 3) |
15 | 13, 14 | ax-mp 5 |
. . 3
⊢ 3 ∥
3 |
16 | | 4nn0 11646 |
. . . . . 6
⊢ 4 ∈
ℕ0 |
17 | 16 | numexp0 16158 |
. . . . 5
⊢
(4↑0) = 1 |
18 | 17 | oveq1i 6920 |
. . . 4
⊢
((4↑0) + 2) = (1 + 2) |
19 | | 1p2e3 11508 |
. . . 4
⊢ (1 + 2) =
3 |
20 | 18, 19 | eqtri 2849 |
. . 3
⊢
((4↑0) + 2) = 3 |
21 | 15, 20 | breqtrri 4902 |
. 2
⊢ 3 ∥
((4↑0) + 2) |
22 | 13 | a1i 11 |
. . . . 5
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 3 ∈ ℤ) |
23 | 16 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ 4 ∈ ℕ0) |
24 | | id 22 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℕ0) |
25 | 23, 24 | nn0expcld 13334 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (4↑𝑛) ∈
ℕ0) |
26 | 25 | nn0zd 11815 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (4↑𝑛) ∈
ℤ) |
27 | 26 | adantr 474 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → (4↑𝑛)
∈ ℤ) |
28 | | 2z 11744 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 2 ∈ ℤ) |
30 | 27, 29 | zaddcld 11821 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → ((4↑𝑛) +
2) ∈ ℤ) |
31 | | 4z 11746 |
. . . . . . 7
⊢ 4 ∈
ℤ |
32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 4 ∈ ℤ) |
33 | | simpr 479 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 3 ∥ ((4↑𝑛) + 2)) |
34 | 22, 30, 32, 33 | dvdsmultr1d 15404 |
. . . . 5
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 3 ∥ (((4↑𝑛) + 2) · 4)) |
35 | | dvdsmul1 15387 |
. . . . . . 7
⊢ ((3
∈ ℤ ∧ 2 ∈ ℤ) → 3 ∥ (3 ·
2)) |
36 | 13, 28, 35 | mp2an 683 |
. . . . . 6
⊢ 3 ∥
(3 · 2) |
37 | 36 | a1i 11 |
. . . . 5
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 3 ∥ (3 · 2)) |
38 | 16 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 4 ∈ ℕ0) |
39 | | simpl 476 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 𝑛 ∈
ℕ0) |
40 | 38, 39 | nn0expcld 13334 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → (4↑𝑛)
∈ ℕ0) |
41 | 40 | nn0zd 11815 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → (4↑𝑛)
∈ ℤ) |
42 | 41, 29 | zaddcld 11821 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → ((4↑𝑛) +
2) ∈ ℤ) |
43 | 42, 32 | zmulcld 11823 |
. . . . 5
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → (((4↑𝑛) +
2) · 4) ∈ ℤ) |
44 | 22, 29 | zmulcld 11823 |
. . . . 5
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → (3 · 2) ∈ ℤ) |
45 | 22, 34, 37, 43, 44 | dvds2subd 15401 |
. . . 4
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 3 ∥ ((((4↑𝑛) + 2) · 4) − (3 ·
2))) |
46 | 25 | nn0cnd 11687 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (4↑𝑛) ∈
ℂ) |
47 | | 2cnd 11436 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 2 ∈ ℂ) |
48 | | 4cn 11444 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
49 | 48 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 4 ∈ ℂ) |
50 | 46, 47, 49 | adddird 10389 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ (((4↑𝑛) + 2)
· 4) = (((4↑𝑛)
· 4) + (2 · 4))) |
51 | 50 | oveq1d 6925 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((((4↑𝑛) + 2)
· 4) − (2 · 3)) = ((((4↑𝑛) · 4) + (2 · 4)) − (2
· 3))) |
52 | | 3cn 11439 |
. . . . . . . . 9
⊢ 3 ∈
ℂ |
53 | | 2cn 11433 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
54 | 52, 53 | mulcomi 10372 |
. . . . . . . 8
⊢ (3
· 2) = (2 · 3) |
55 | 54 | a1i 11 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ (3 · 2) = (2 · 3)) |
56 | 55 | oveq2d 6926 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((((4↑𝑛) + 2)
· 4) − (3 · 2)) = ((((4↑𝑛) + 2) · 4) − (2 ·
3))) |
57 | 49, 24 | expp1d 13310 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (4↑(𝑛 + 1)) =
((4↑𝑛) ·
4)) |
58 | | ax-1cn 10317 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
59 | | 3p1e4 11510 |
. . . . . . . . . . . . . . 15
⊢ (3 + 1) =
4 |
60 | 52, 58, 59 | addcomli 10554 |
. . . . . . . . . . . . . 14
⊢ (1 + 3) =
4 |
61 | 60 | eqcomi 2834 |
. . . . . . . . . . . . 13
⊢ 4 = (1 +
3) |
62 | 61 | oveq1i 6920 |
. . . . . . . . . . . 12
⊢ (4
− 3) = ((1 + 3) − 3) |
63 | 58, 52 | pncan3oi 10625 |
. . . . . . . . . . . 12
⊢ ((1 + 3)
− 3) = 1 |
64 | 62, 63 | eqtri 2849 |
. . . . . . . . . . 11
⊢ (4
− 3) = 1 |
65 | 64 | oveq2i 6921 |
. . . . . . . . . 10
⊢ (2
· (4 − 3)) = (2 · 1) |
66 | 53, 48, 52 | subdii 10810 |
. . . . . . . . . 10
⊢ (2
· (4 − 3)) = ((2 · 4) − (2 ·
3)) |
67 | | 2t1e2 11528 |
. . . . . . . . . 10
⊢ (2
· 1) = 2 |
68 | 65, 66, 67 | 3eqtr3ri 2858 |
. . . . . . . . 9
⊢ 2 = ((2
· 4) − (2 · 3)) |
69 | 68 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 2 = ((2 · 4) − (2 · 3))) |
70 | 57, 69 | oveq12d 6928 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((4↑(𝑛 + 1)) +
2) = (((4↑𝑛) ·
4) + ((2 · 4) − (2 · 3)))) |
71 | 46, 49 | mulcld 10384 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ ((4↑𝑛) ·
4) ∈ ℂ) |
72 | 47, 49 | mulcld 10384 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (2 · 4) ∈ ℂ) |
73 | 52 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ 3 ∈ ℂ) |
74 | 47, 73 | mulcld 10384 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (2 · 3) ∈ ℂ) |
75 | 71, 72, 74 | addsubassd 10740 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((((4↑𝑛)
· 4) + (2 · 4)) − (2 · 3)) = (((4↑𝑛) · 4) + ((2 · 4)
− (2 · 3)))) |
76 | 70, 75 | eqtr4d 2864 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((4↑(𝑛 + 1)) +
2) = ((((4↑𝑛) ·
4) + (2 · 4)) − (2 · 3))) |
77 | 51, 56, 76 | 3eqtr4rd 2872 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ ((4↑(𝑛 + 1)) +
2) = ((((4↑𝑛) + 2)
· 4) − (3 · 2))) |
78 | 77 | adantr 474 |
. . . 4
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → ((4↑(𝑛 +
1)) + 2) = ((((4↑𝑛) +
2) · 4) − (3 · 2))) |
79 | 45, 78 | breqtrrd 4903 |
. . 3
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 3 ∥ ((4↑(𝑛 + 1)) + 2)) |
80 | 79 | ex 403 |
. 2
⊢ (𝑛 ∈ ℕ0
→ (3 ∥ ((4↑𝑛) + 2) → 3 ∥ ((4↑(𝑛 + 1)) + 2))) |
81 | 3, 6, 9, 12, 21, 80 | nn0ind 11807 |
1
⊢ (𝑁 ∈ ℕ0
→ 3 ∥ ((4↑𝑁) + 2)) |