Step | Hyp | Ref
| Expression |
1 | | oveq2 7167 |
. . . 4
⊢ (𝑘 = 0 → (4↑𝑘) = (4↑0)) |
2 | 1 | oveq1d 7174 |
. . 3
⊢ (𝑘 = 0 → ((4↑𝑘) + 2) = ((4↑0) +
2)) |
3 | 2 | breq2d 5081 |
. 2
⊢ (𝑘 = 0 → (3 ∥
((4↑𝑘) + 2) ↔ 3
∥ ((4↑0) + 2))) |
4 | | oveq2 7167 |
. . . 4
⊢ (𝑘 = 𝑛 → (4↑𝑘) = (4↑𝑛)) |
5 | 4 | oveq1d 7174 |
. . 3
⊢ (𝑘 = 𝑛 → ((4↑𝑘) + 2) = ((4↑𝑛) + 2)) |
6 | 5 | breq2d 5081 |
. 2
⊢ (𝑘 = 𝑛 → (3 ∥ ((4↑𝑘) + 2) ↔ 3 ∥
((4↑𝑛) +
2))) |
7 | | oveq2 7167 |
. . . 4
⊢ (𝑘 = (𝑛 + 1) → (4↑𝑘) = (4↑(𝑛 + 1))) |
8 | 7 | oveq1d 7174 |
. . 3
⊢ (𝑘 = (𝑛 + 1) → ((4↑𝑘) + 2) = ((4↑(𝑛 + 1)) + 2)) |
9 | 8 | breq2d 5081 |
. 2
⊢ (𝑘 = (𝑛 + 1) → (3 ∥ ((4↑𝑘) + 2) ↔ 3 ∥
((4↑(𝑛 + 1)) +
2))) |
10 | | oveq2 7167 |
. . . 4
⊢ (𝑘 = 𝑁 → (4↑𝑘) = (4↑𝑁)) |
11 | 10 | oveq1d 7174 |
. . 3
⊢ (𝑘 = 𝑁 → ((4↑𝑘) + 2) = ((4↑𝑁) + 2)) |
12 | 11 | breq2d 5081 |
. 2
⊢ (𝑘 = 𝑁 → (3 ∥ ((4↑𝑘) + 2) ↔ 3 ∥
((4↑𝑁) +
2))) |
13 | | 3z 12018 |
. . . 4
⊢ 3 ∈
ℤ |
14 | | iddvds 15626 |
. . . 4
⊢ (3 ∈
ℤ → 3 ∥ 3) |
15 | 13, 14 | ax-mp 5 |
. . 3
⊢ 3 ∥
3 |
16 | | 4nn0 11919 |
. . . . . 6
⊢ 4 ∈
ℕ0 |
17 | 16 | numexp0 16415 |
. . . . 5
⊢
(4↑0) = 1 |
18 | 17 | oveq1i 7169 |
. . . 4
⊢
((4↑0) + 2) = (1 + 2) |
19 | | 1p2e3 11783 |
. . . 4
⊢ (1 + 2) =
3 |
20 | 18, 19 | eqtri 2847 |
. . 3
⊢
((4↑0) + 2) = 3 |
21 | 15, 20 | breqtrri 5096 |
. 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 13610 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (4↑𝑛) ∈
ℕ0) |
26 | 25 | nn0zd 12088 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (4↑𝑛) ∈
ℤ) |
27 | 26 | adantr 483 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → (4↑𝑛)
∈ ℤ) |
28 | | 2z 12017 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 2 ∈ ℤ) |
30 | 27, 29 | zaddcld 12094 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → ((4↑𝑛) +
2) ∈ ℤ) |
31 | | 4z 12019 |
. . . . . . 7
⊢ 4 ∈
ℤ |
32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 4 ∈ ℤ) |
33 | | simpr 487 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 3 ∥ ((4↑𝑛) + 2)) |
34 | 22, 30, 32, 33 | dvdsmultr1d 15651 |
. . . . 5
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 3 ∥ (((4↑𝑛) + 2) · 4)) |
35 | | dvdsmul1 15634 |
. . . . . . 7
⊢ ((3
∈ ℤ ∧ 2 ∈ ℤ) → 3 ∥ (3 ·
2)) |
36 | 13, 28, 35 | mp2an 690 |
. . . . . 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 485 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 𝑛 ∈
ℕ0) |
40 | 38, 39 | nn0expcld 13610 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → (4↑𝑛)
∈ ℕ0) |
41 | 40 | nn0zd 12088 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → (4↑𝑛)
∈ ℤ) |
42 | 41, 29 | zaddcld 12094 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → ((4↑𝑛) +
2) ∈ ℤ) |
43 | 42, 32 | zmulcld 12096 |
. . . . 5
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → (((4↑𝑛) +
2) · 4) ∈ ℤ) |
44 | 22, 29 | zmulcld 12096 |
. . . . 5
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → (3 · 2) ∈ ℤ) |
45 | 22, 34, 37, 43, 44 | dvds2subd 15648 |
. . . 4
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 3 ∥ ((((4↑𝑛) + 2) · 4) − (3 ·
2))) |
46 | 25 | nn0cnd 11960 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (4↑𝑛) ∈
ℂ) |
47 | | 2cnd 11718 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 2 ∈ ℂ) |
48 | | 4cn 11725 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
49 | 48 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 4 ∈ ℂ) |
50 | 46, 47, 49 | adddird 10669 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ (((4↑𝑛) + 2)
· 4) = (((4↑𝑛)
· 4) + (2 · 4))) |
51 | 50 | oveq1d 7174 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((((4↑𝑛) + 2)
· 4) − (2 · 3)) = ((((4↑𝑛) · 4) + (2 · 4)) − (2
· 3))) |
52 | | 3cn 11721 |
. . . . . . . . 9
⊢ 3 ∈
ℂ |
53 | | 2cn 11715 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
54 | 52, 53 | mulcomi 10652 |
. . . . . . . 8
⊢ (3
· 2) = (2 · 3) |
55 | 54 | a1i 11 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ (3 · 2) = (2 · 3)) |
56 | 55 | oveq2d 7175 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((((4↑𝑛) + 2)
· 4) − (3 · 2)) = ((((4↑𝑛) + 2) · 4) − (2 ·
3))) |
57 | 49, 24 | expp1d 13514 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (4↑(𝑛 + 1)) =
((4↑𝑛) ·
4)) |
58 | | ax-1cn 10598 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
59 | | 3p1e4 11785 |
. . . . . . . . . . . . . 14
⊢ (3 + 1) =
4 |
60 | 52, 58, 59 | addcomli 10835 |
. . . . . . . . . . . . 13
⊢ (1 + 3) =
4 |
61 | 60 | eqcomi 2833 |
. . . . . . . . . . . 12
⊢ 4 = (1 +
3) |
62 | 58, 52, 61 | mvrraddi 10906 |
. . . . . . . . . . 11
⊢ (4
− 3) = 1 |
63 | 62 | oveq2i 7170 |
. . . . . . . . . 10
⊢ (2
· (4 − 3)) = (2 · 1) |
64 | 53, 48, 52 | subdii 11092 |
. . . . . . . . . 10
⊢ (2
· (4 − 3)) = ((2 · 4) − (2 ·
3)) |
65 | | 2t1e2 11803 |
. . . . . . . . . 10
⊢ (2
· 1) = 2 |
66 | 63, 64, 65 | 3eqtr3ri 2856 |
. . . . . . . . 9
⊢ 2 = ((2
· 4) − (2 · 3)) |
67 | 66 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ 2 = ((2 · 4) − (2 · 3))) |
68 | 57, 67 | oveq12d 7177 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((4↑(𝑛 + 1)) +
2) = (((4↑𝑛) ·
4) + ((2 · 4) − (2 · 3)))) |
69 | 46, 49 | mulcld 10664 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ ((4↑𝑛) ·
4) ∈ ℂ) |
70 | 47, 49 | mulcld 10664 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (2 · 4) ∈ ℂ) |
71 | 52 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ 3 ∈ ℂ) |
72 | 47, 71 | mulcld 10664 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (2 · 3) ∈ ℂ) |
73 | 69, 70, 72 | addsubassd 11020 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((((4↑𝑛)
· 4) + (2 · 4)) − (2 · 3)) = (((4↑𝑛) · 4) + ((2 · 4)
− (2 · 3)))) |
74 | 68, 73 | eqtr4d 2862 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((4↑(𝑛 + 1)) +
2) = ((((4↑𝑛) ·
4) + (2 · 4)) − (2 · 3))) |
75 | 51, 56, 74 | 3eqtr4rd 2870 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ ((4↑(𝑛 + 1)) +
2) = ((((4↑𝑛) + 2)
· 4) − (3 · 2))) |
76 | 75 | adantr 483 |
. . . 4
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → ((4↑(𝑛 +
1)) + 2) = ((((4↑𝑛) +
2) · 4) − (3 · 2))) |
77 | 45, 76 | breqtrrd 5097 |
. . 3
⊢ ((𝑛 ∈ ℕ0
∧ 3 ∥ ((4↑𝑛)
+ 2)) → 3 ∥ ((4↑(𝑛 + 1)) + 2)) |
78 | 77 | ex 415 |
. 2
⊢ (𝑛 ∈ ℕ0
→ (3 ∥ ((4↑𝑛) + 2) → 3 ∥ ((4↑(𝑛 + 1)) + 2))) |
79 | 3, 6, 9, 12, 21, 78 | nn0ind 12080 |
1
⊢ (𝑁 ∈ ℕ0
→ 3 ∥ ((4↑𝑁) + 2)) |