Proof of Theorem fmtnorec4
Step | Hyp | Ref
| Expression |
1 | | eluz2nn 12369 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) |
2 | | nnm1nn0 12020 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈
ℕ0) |
4 | | fmtno 44545 |
. . . . . 6
⊢ ((𝑁 − 1) ∈
ℕ0 → (FermatNo‘(𝑁 − 1)) = ((2↑(2↑(𝑁 − 1))) +
1)) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘(𝑁 − 1)) = ((2↑(2↑(𝑁 − 1))) +
1)) |
6 | 5 | oveq1d 7188 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1))↑2) =
(((2↑(2↑(𝑁
− 1))) + 1)↑2)) |
7 | | 2nn 11792 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℕ) |
9 | | 2nn0 11996 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
10 | 9 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈
ℕ0) |
11 | 10, 3 | nn0expcld 13702 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 − 1)) ∈
ℕ0) |
12 | 8, 11 | nnexpcld 13701 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(2↑(𝑁 − 1))) ∈
ℕ) |
13 | 12 | nncnd 11735 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(2↑(𝑁 − 1))) ∈
ℂ) |
14 | | binom21 13675 |
. . . . 5
⊢
((2↑(2↑(𝑁
− 1))) ∈ ℂ → (((2↑(2↑(𝑁 − 1))) + 1)↑2) =
((((2↑(2↑(𝑁
− 1)))↑2) + (2 · (2↑(2↑(𝑁 − 1))))) + 1)) |
15 | 13, 14 | syl 17 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2↑(2↑(𝑁 − 1))) + 1)↑2) =
((((2↑(2↑(𝑁
− 1)))↑2) + (2 · (2↑(2↑(𝑁 − 1))))) + 1)) |
16 | | 2cn 11794 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℂ) |
18 | 17, 10, 11 | expmuld 13608 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑((2↑(𝑁 − 1)) · 2)) =
((2↑(2↑(𝑁 −
1)))↑2)) |
19 | 17, 3 | expp1d 13606 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑((𝑁 − 1) + 1)) = ((2↑(𝑁 − 1)) ·
2)) |
20 | 1 | nncnd 11735 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) |
21 | | npcan1 11146 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 1) + 1) = 𝑁) |
23 | 22 | oveq2d 7189 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑((𝑁 − 1) + 1)) = (2↑𝑁)) |
24 | 19, 23 | eqtr3d 2776 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(𝑁 − 1)) · 2) = (2↑𝑁)) |
25 | 24 | oveq2d 7189 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑((2↑(𝑁 − 1)) · 2)) =
(2↑(2↑𝑁))) |
26 | 18, 25 | eqtr3d 2776 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 1)))↑2) =
(2↑(2↑𝑁))) |
27 | 26 | oveq1d 7188 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2↑(2↑(𝑁 − 1)))↑2) + (2 ·
(2↑(2↑(𝑁 −
1))))) = ((2↑(2↑𝑁)) + (2 · (2↑(2↑(𝑁 −
1)))))) |
28 | 27 | oveq1d 7188 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2↑(2↑(𝑁 − 1)))↑2) + (2 ·
(2↑(2↑(𝑁 −
1))))) + 1) = (((2↑(2↑𝑁)) + (2 · (2↑(2↑(𝑁 − 1))))) +
1)) |
29 | 6, 15, 28 | 3eqtrd 2778 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1))↑2) =
(((2↑(2↑𝑁)) + (2
· (2↑(2↑(𝑁
− 1))))) + 1)) |
30 | | uznn0sub 12362 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
31 | | fmtno 44545 |
. . . . . . . 8
⊢ ((𝑁 − 2) ∈
ℕ0 → (FermatNo‘(𝑁 − 2)) = ((2↑(2↑(𝑁 − 2))) +
1)) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘(𝑁 − 2)) = ((2↑(2↑(𝑁 − 2))) +
1)) |
33 | 32 | oveq1d 7188 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 2)) − 1) =
(((2↑(2↑(𝑁
− 2))) + 1) − 1)) |
34 | 33 | oveq1d 7188 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 2)) − 1)↑2) =
((((2↑(2↑(𝑁
− 2))) + 1) − 1)↑2)) |
35 | 10, 30 | nn0expcld 13702 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 − 2)) ∈
ℕ0) |
36 | 8, 35 | nnexpcld 13701 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(2↑(𝑁 − 2))) ∈
ℕ) |
37 | 36 | nncnd 11735 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(2↑(𝑁 − 2))) ∈
ℂ) |
38 | | peano2cn 10893 |
. . . . . . 7
⊢
((2↑(2↑(𝑁
− 2))) ∈ ℂ → ((2↑(2↑(𝑁 − 2))) + 1) ∈
ℂ) |
39 | 37, 38 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 2))) + 1) ∈
ℂ) |
40 | | binom2sub1 13677 |
. . . . . 6
⊢
(((2↑(2↑(𝑁
− 2))) + 1) ∈ ℂ → ((((2↑(2↑(𝑁 − 2))) + 1) − 1)↑2) =
(((((2↑(2↑(𝑁
− 2))) + 1)↑2) − (2 · ((2↑(2↑(𝑁 − 2))) + 1))) +
1)) |
41 | 39, 40 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2↑(2↑(𝑁 − 2))) + 1) − 1)↑2) =
(((((2↑(2↑(𝑁
− 2))) + 1)↑2) − (2 · ((2↑(2↑(𝑁 − 2))) + 1))) +
1)) |
42 | | binom21 13675 |
. . . . . . . 8
⊢
((2↑(2↑(𝑁
− 2))) ∈ ℂ → (((2↑(2↑(𝑁 − 2))) + 1)↑2) =
((((2↑(2↑(𝑁
− 2)))↑2) + (2 · (2↑(2↑(𝑁 − 2))))) + 1)) |
43 | 37, 42 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2↑(2↑(𝑁 − 2))) + 1)↑2) =
((((2↑(2↑(𝑁
− 2)))↑2) + (2 · (2↑(2↑(𝑁 − 2))))) + 1)) |
44 | 43 | oveq1d 7188 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2↑(2↑(𝑁 − 2))) + 1)↑2) − (2
· ((2↑(2↑(𝑁 − 2))) + 1))) =
(((((2↑(2↑(𝑁
− 2)))↑2) + (2 · (2↑(2↑(𝑁 − 2))))) + 1) − (2 ·
((2↑(2↑(𝑁 −
2))) + 1)))) |
45 | 44 | oveq1d 7188 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (((((2↑(2↑(𝑁 − 2))) + 1)↑2) − (2
· ((2↑(2↑(𝑁 − 2))) + 1))) + 1) =
((((((2↑(2↑(𝑁
− 2)))↑2) + (2 · (2↑(2↑(𝑁 − 2))))) + 1) − (2 ·
((2↑(2↑(𝑁 −
2))) + 1))) + 1)) |
46 | 34, 41, 45 | 3eqtrd 2778 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 2)) − 1)↑2) =
((((((2↑(2↑(𝑁
− 2)))↑2) + (2 · (2↑(2↑(𝑁 − 2))))) + 1) − (2 ·
((2↑(2↑(𝑁 −
2))) + 1))) + 1)) |
47 | 46 | oveq2d 7189 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (((FermatNo‘(𝑁 − 2)) − 1)↑2))
= (2 · ((((((2↑(2↑(𝑁 − 2)))↑2) + (2 ·
(2↑(2↑(𝑁 −
2))))) + 1) − (2 · ((2↑(2↑(𝑁 − 2))) + 1))) + 1))) |
48 | 29, 47 | oveq12d 7191 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(((FermatNo‘(𝑁
− 2)) − 1)↑2))) = ((((2↑(2↑𝑁)) + (2 · (2↑(2↑(𝑁 − 1))))) + 1) − (2
· ((((((2↑(2↑(𝑁 − 2)))↑2) + (2 ·
(2↑(2↑(𝑁 −
2))))) + 1) − (2 · ((2↑(2↑(𝑁 − 2))) + 1))) +
1)))) |
49 | 36, 10 | nnexpcld 13701 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 2)))↑2) ∈
ℕ) |
50 | 49 | nncnd 11735 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 2)))↑2) ∈
ℂ) |
51 | 17, 37 | mulcld 10742 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (2↑(2↑(𝑁 − 2)))) ∈
ℂ) |
52 | 50, 51 | addcld 10741 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2↑(2↑(𝑁 − 2)))↑2) + (2 ·
(2↑(2↑(𝑁 −
2))))) ∈ ℂ) |
53 | | peano2cn 10893 |
. . . . . . 7
⊢
((((2↑(2↑(𝑁 − 2)))↑2) + (2 ·
(2↑(2↑(𝑁 −
2))))) ∈ ℂ → ((((2↑(2↑(𝑁 − 2)))↑2) + (2 ·
(2↑(2↑(𝑁 −
2))))) + 1) ∈ ℂ) |
54 | 52, 53 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2↑(2↑(𝑁 − 2)))↑2) + (2 ·
(2↑(2↑(𝑁 −
2))))) + 1) ∈ ℂ) |
55 | 17, 39 | mulcld 10742 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · ((2↑(2↑(𝑁 − 2))) + 1)) ∈
ℂ) |
56 | 54, 55 | subcld 11078 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (((((2↑(2↑(𝑁 − 2)))↑2) + (2 ·
(2↑(2↑(𝑁 −
2))))) + 1) − (2 · ((2↑(2↑(𝑁 − 2))) + 1))) ∈
ℂ) |
57 | | 1cnd 10717 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℂ) |
58 | 17, 56, 57 | adddid 10746 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · ((((((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2))))) + 1) − (2 · ((2↑(2↑(𝑁 − 2))) + 1))) + 1)) = ((2 ·
(((((2↑(2↑(𝑁
− 2)))↑2) + (2 · (2↑(2↑(𝑁 − 2))))) + 1) − (2 ·
((2↑(2↑(𝑁 −
2))) + 1)))) + (2 · 1))) |
59 | 52, 57 | addcld 10741 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2↑(2↑(𝑁 − 2)))↑2) + (2 ·
(2↑(2↑(𝑁 −
2))))) + 1) ∈ ℂ) |
60 | 17, 59, 55 | subdid 11177 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (((((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2))))) + 1) − (2 · ((2↑(2↑(𝑁 − 2))) + 1)))) = ((2 ·
((((2↑(2↑(𝑁
− 2)))↑2) + (2 · (2↑(2↑(𝑁 − 2))))) + 1)) − (2 · (2
· ((2↑(2↑(𝑁 − 2))) + 1))))) |
61 | 17, 52, 57 | adddid 10746 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · ((((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2))))) + 1)) = ((2 · (((2↑(2↑(𝑁 − 2)))↑2) + (2 ·
(2↑(2↑(𝑁 −
2)))))) + (2 · 1))) |
62 | 17, 50, 51 | adddid 10746 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2)))))) = ((2 · ((2↑(2↑(𝑁 − 2)))↑2)) + (2 · (2
· (2↑(2↑(𝑁
− 2))))))) |
63 | 17, 10, 35 | expmuld 13608 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑((2↑(𝑁 − 2)) · 2)) =
((2↑(2↑(𝑁 −
2)))↑2)) |
64 | 17, 30 | expp1d 13606 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑((𝑁 − 2) + 1)) = ((2↑(𝑁 − 2)) ·
2)) |
65 | 20, 17, 57 | subsubd 11106 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − (2 − 1)) = ((𝑁 − 2) +
1)) |
66 | 65 | eqcomd 2745 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 2) + 1) = (𝑁 − (2 − 1))) |
67 | 66 | oveq2d 7189 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑((𝑁 − 2) + 1)) = (2↑(𝑁 − (2 −
1)))) |
68 | 64, 67 | eqtr3d 2776 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(𝑁 − 2)) · 2) = (2↑(𝑁 − (2 −
1)))) |
69 | 68 | oveq2d 7189 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑((2↑(𝑁 − 2)) · 2)) =
(2↑(2↑(𝑁 −
(2 − 1))))) |
70 | 63, 69 | eqtr3d 2776 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 2)))↑2) =
(2↑(2↑(𝑁 −
(2 − 1))))) |
71 | 70 | oveq2d 7189 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · ((2↑(2↑(𝑁 − 2)))↑2)) = (2
· (2↑(2↑(𝑁
− (2 − 1)))))) |
72 | | 2m1e1 11845 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 − 1) = 1) |
74 | 73 | oveq2d 7189 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − (2 − 1)) = (𝑁 − 1)) |
75 | 74 | oveq2d 7189 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 − (2 − 1))) = (2↑(𝑁 − 1))) |
76 | 75 | oveq2d 7189 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(2↑(𝑁 − (2 − 1)))) =
(2↑(2↑(𝑁 −
1)))) |
77 | 76 | oveq2d 7189 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (2↑(2↑(𝑁 − (2 − 1))))) = (2
· (2↑(2↑(𝑁
− 1))))) |
78 | 71, 77 | eqtrd 2774 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · ((2↑(2↑(𝑁 − 2)))↑2)) = (2
· (2↑(2↑(𝑁
− 1))))) |
79 | 17, 17, 37 | mulassd 10745 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · 2) ·
(2↑(2↑(𝑁 −
2)))) = (2 · (2 · (2↑(2↑(𝑁 − 2)))))) |
80 | 79 | eqcomd 2745 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (2 ·
(2↑(2↑(𝑁 −
2))))) = ((2 · 2) · (2↑(2↑(𝑁 − 2))))) |
81 | 78, 80 | oveq12d 7191 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · ((2↑(2↑(𝑁 − 2)))↑2)) + (2
· (2 · (2↑(2↑(𝑁 − 2)))))) = ((2 ·
(2↑(2↑(𝑁 −
1)))) + ((2 · 2) · (2↑(2↑(𝑁 − 2)))))) |
82 | 62, 81 | eqtrd 2774 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2)))))) = ((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2)))))) |
83 | | 2t1e2 11882 |
. . . . . . . . . 10
⊢ (2
· 1) = 2 |
84 | 83 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · 1) = 2) |
85 | 82, 84 | oveq12d 7191 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · (((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2)))))) + (2 · 1)) = (((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + 2)) |
86 | 61, 85 | eqtrd 2774 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · ((((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2))))) + 1)) = (((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 2)) |
87 | 17, 37, 57 | adddid 10746 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · ((2↑(2↑(𝑁 − 2))) + 1)) = ((2
· (2↑(2↑(𝑁
− 2)))) + (2 · 1))) |
88 | 84 | oveq2d 7189 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · (2↑(2↑(𝑁 − 2)))) + (2 · 1))
= ((2 · (2↑(2↑(𝑁 − 2)))) + 2)) |
89 | 87, 88 | eqtrd 2774 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · ((2↑(2↑(𝑁 − 2))) + 1)) = ((2
· (2↑(2↑(𝑁
− 2)))) + 2)) |
90 | 89 | oveq2d 7189 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (2 ·
((2↑(2↑(𝑁 −
2))) + 1))) = (2 · ((2 · (2↑(2↑(𝑁 − 2)))) + 2))) |
91 | 17, 51, 17 | adddid 10746 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · ((2 ·
(2↑(2↑(𝑁 −
2)))) + 2)) = ((2 · (2 · (2↑(2↑(𝑁 − 2))))) + (2 ·
2))) |
92 | | 2t2e4 11883 |
. . . . . . . . . 10
⊢ (2
· 2) = 4 |
93 | 92 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · 2) = 4) |
94 | 80, 93 | oveq12d 7191 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · (2 ·
(2↑(2↑(𝑁 −
2))))) + (2 · 2)) = (((2 · 2) · (2↑(2↑(𝑁 − 2)))) +
4)) |
95 | 90, 91, 94 | 3eqtrd 2778 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (2 ·
((2↑(2↑(𝑁 −
2))) + 1))) = (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) |
96 | 86, 95 | oveq12d 7191 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · ((((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2))))) + 1)) − (2 · (2 · ((2↑(2↑(𝑁 − 2))) + 1)))) = ((((2
· (2↑(2↑(𝑁
− 1)))) + ((2 · 2) · (2↑(2↑(𝑁 − 2))))) + 2) − (((2 ·
2) · (2↑(2↑(𝑁 − 2)))) + 4))) |
97 | 60, 96 | eqtrd 2774 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (((((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2))))) + 1) − (2 · ((2↑(2↑(𝑁 − 2))) + 1)))) = ((((2 ·
(2↑(2↑(𝑁 −
1)))) + ((2 · 2) · (2↑(2↑(𝑁 − 2))))) + 2) − (((2 ·
2) · (2↑(2↑(𝑁 − 2)))) + 4))) |
98 | 97, 84 | oveq12d 7191 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · (((((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2))))) + 1) − (2 · ((2↑(2↑(𝑁 − 2))) + 1)))) + (2 · 1)) =
(((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) +
2)) |
99 | 58, 98 | eqtrd 2774 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · ((((((2↑(2↑(𝑁 − 2)))↑2) + (2
· (2↑(2↑(𝑁
− 2))))) + 1) − (2 · ((2↑(2↑(𝑁 − 2))) + 1))) + 1)) = (((((2 ·
(2↑(2↑(𝑁 −
1)))) + ((2 · 2) · (2↑(2↑(𝑁 − 2))))) + 2) − (((2 ·
2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2)) |
100 | 99 | oveq2d 7189 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2↑(2↑𝑁)) + (2 · (2↑(2↑(𝑁 − 1))))) + 1) − (2
· ((((((2↑(2↑(𝑁 − 2)))↑2) + (2 ·
(2↑(2↑(𝑁 −
2))))) + 1) − (2 · ((2↑(2↑(𝑁 − 2))) + 1))) + 1))) =
((((2↑(2↑𝑁)) + (2
· (2↑(2↑(𝑁
− 1))))) + 1) − (((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) +
2))) |
101 | 17, 13 | mulcld 10742 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (2↑(2↑(𝑁 − 1)))) ∈
ℂ) |
102 | 16, 16 | mulcli 10729 |
. . . . . . . . . . . . 13
⊢ (2
· 2) ∈ ℂ |
103 | 102 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · 2) ∈
ℂ) |
104 | 103, 37 | mulcld 10742 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · 2) ·
(2↑(2↑(𝑁 −
2)))) ∈ ℂ) |
105 | 101, 104 | addcld 10741 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) ∈ ℂ) |
106 | 105, 17 | addcld 10741 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + 2) ∈ ℂ) |
107 | | 4cn 11804 |
. . . . . . . . . . 11
⊢ 4 ∈
ℂ |
108 | 107 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → 4 ∈ ℂ) |
109 | 104, 108 | addcld 10741 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2 · 2) ·
(2↑(2↑(𝑁 −
2)))) + 4) ∈ ℂ) |
110 | 105, 17, 17 | addassd 10744 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + 2) + 2) = (((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + (2 + 2))) |
111 | | 2p2e4 11854 |
. . . . . . . . . . . 12
⊢ (2 + 2) =
4 |
112 | 111 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 + 2) = 4) |
113 | 112 | oveq2d 7189 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + (2 + 2)) = (((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 4)) |
114 | 101, 104,
108 | addassd 10744 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + 4) = ((2 · (2↑(2↑(𝑁 − 1)))) + (((2 · 2) ·
(2↑(2↑(𝑁 −
2)))) + 4))) |
115 | 110, 113,
114 | 3eqtrd 2778 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + 2) + 2) = ((2 · (2↑(2↑(𝑁 − 1)))) + (((2 · 2) ·
(2↑(2↑(𝑁 −
2)))) + 4))) |
116 | 106, 17, 101, 109, 115 | subaddeqd 11136 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) = ((2
· (2↑(2↑(𝑁
− 1)))) − 2)) |
117 | 116 | eqcomd 2745 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · (2↑(2↑(𝑁 − 1)))) − 2) =
((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) +
4))) |
118 | 106, 109 | subcld 11078 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) ∈
ℂ) |
119 | 101, 17, 118 | subadd2d 11097 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2 · (2↑(2↑(𝑁 − 1)))) − 2) =
((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) ↔
(((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2) = (2
· (2↑(2↑(𝑁
− 1)))))) |
120 | 117, 119 | mpbid 235 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2) = (2
· (2↑(2↑(𝑁
− 1))))) |
121 | 120 | oveq2d 7189 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑𝑁)) + (((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2)) =
((2↑(2↑𝑁)) + (2
· (2↑(2↑(𝑁
− 1)))))) |
122 | | eluzge2nn0 12372 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
ℕ0) |
123 | 10, 122 | nn0expcld 13702 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑𝑁) ∈
ℕ0) |
124 | 8, 123 | nnexpcld 13701 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(2↑𝑁)) ∈ ℕ) |
125 | 124 | nncnd 11735 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(2↑𝑁)) ∈ ℂ) |
126 | 125, 101 | addcld 10741 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑𝑁)) + (2 · (2↑(2↑(𝑁 − 1))))) ∈
ℂ) |
127 | 118, 17 | addcld 10741 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2)
· (2↑(2↑(𝑁
− 2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2) ∈
ℂ) |
128 | 126, 127,
125 | subadd2d 11097 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2↑(2↑𝑁)) + (2 · (2↑(2↑(𝑁 − 1))))) − (((((2
· (2↑(2↑(𝑁
− 1)))) + ((2 · 2) · (2↑(2↑(𝑁 − 2))))) + 2) − (((2 ·
2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2)) =
(2↑(2↑𝑁)) ↔
((2↑(2↑𝑁)) +
(((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2)) =
((2↑(2↑𝑁)) + (2
· (2↑(2↑(𝑁
− 1))))))) |
129 | 121, 128 | mpbird 260 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2↑(2↑𝑁)) + (2 · (2↑(2↑(𝑁 − 1))))) − (((((2
· (2↑(2↑(𝑁
− 1)))) + ((2 · 2) · (2↑(2↑(𝑁 − 2))))) + 2) − (((2 ·
2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2)) =
(2↑(2↑𝑁))) |
130 | 129 | oveq1d 7188 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2↑(2↑𝑁)) + (2 · (2↑(2↑(𝑁 − 1))))) − (((((2
· (2↑(2↑(𝑁
− 1)))) + ((2 · 2) · (2↑(2↑(𝑁 − 2))))) + 2) − (((2 ·
2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2)) + 1) =
((2↑(2↑𝑁)) +
1)) |
131 | 126, 57, 127 | addsubd 11099 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2↑(2↑𝑁)) + (2 · (2↑(2↑(𝑁 − 1))))) + 1) −
(((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2)) =
((((2↑(2↑𝑁)) + (2
· (2↑(2↑(𝑁
− 1))))) − (((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2)) +
1)) |
132 | | fmtno 44545 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (FermatNo‘𝑁) =
((2↑(2↑𝑁)) +
1)) |
133 | 122, 132 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1)) |
134 | 130, 131,
133 | 3eqtr4d 2784 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((2↑(2↑𝑁)) + (2 · (2↑(2↑(𝑁 − 1))))) + 1) −
(((((2 · (2↑(2↑(𝑁 − 1)))) + ((2 · 2) ·
(2↑(2↑(𝑁 −
2))))) + 2) − (((2 · 2) · (2↑(2↑(𝑁 − 2)))) + 4)) + 2)) =
(FermatNo‘𝑁)) |
135 | 48, 100, 134 | 3eqtrrd 2779 |
1
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘𝑁) = (((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(((FermatNo‘(𝑁
− 2)) − 1)↑2)))) |