Proof of Theorem fmtnorec3
Step | Hyp | Ref
| Expression |
1 | | fzfid 13546 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (0...(𝑁 − 2)) ∈ Fin) |
2 | | elfznn0 13205 |
. . . . . . . . 9
⊢ (𝑛 ∈ (0...(𝑁 − 2)) → 𝑛 ∈ ℕ0) |
3 | | fmtnonn 44656 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (FermatNo‘𝑛)
∈ ℕ) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝑛 ∈ (0...(𝑁 − 2)) → (FermatNo‘𝑛) ∈
ℕ) |
5 | 4 | nncnd 11846 |
. . . . . . 7
⊢ (𝑛 ∈ (0...(𝑁 − 2)) → (FermatNo‘𝑛) ∈
ℂ) |
6 | 5 | adantl 485 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑛 ∈ (0...(𝑁 − 2))) → (FermatNo‘𝑛) ∈
ℂ) |
7 | 1, 6 | fprodcl 15514 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ∏𝑛 ∈ (0...(𝑁 − 2))(FermatNo‘𝑛) ∈
ℂ) |
8 | | 2cn 11905 |
. . . . . 6
⊢ 2 ∈
ℂ |
9 | 8 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℂ) |
10 | | uznn0sub 12473 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
11 | | fmtnorec2 44668 |
. . . . . . 7
⊢ ((𝑁 − 2) ∈
ℕ0 → (FermatNo‘((𝑁 − 2) + 1)) = (∏𝑛 ∈ (0...(𝑁 − 2))(FermatNo‘𝑛) + 2)) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘((𝑁 − 2) + 1)) = (∏𝑛 ∈ (0...(𝑁 − 2))(FermatNo‘𝑛) + 2)) |
13 | 12 | eqcomd 2743 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (∏𝑛 ∈ (0...(𝑁 − 2))(FermatNo‘𝑛) + 2) = (FermatNo‘((𝑁 − 2) +
1))) |
14 | 7, 9, 13 | mvlraddd 11242 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ∏𝑛 ∈ (0...(𝑁 − 2))(FermatNo‘𝑛) = ((FermatNo‘((𝑁 − 2) + 1)) −
2)) |
15 | 14 | oveq2d 7229 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 1))) · ∏𝑛 ∈ (0...(𝑁 − 2))(FermatNo‘𝑛)) = ((2↑(2↑(𝑁 − 1))) ·
((FermatNo‘((𝑁
− 2) + 1)) − 2))) |
16 | 15 | oveq2d 7229 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1)) + ((2↑(2↑(𝑁 − 1))) ·
∏𝑛 ∈ (0...(𝑁 −
2))(FermatNo‘𝑛))) =
((FermatNo‘(𝑁 −
1)) + ((2↑(2↑(𝑁
− 1))) · ((FermatNo‘((𝑁 − 2) + 1)) −
2)))) |
17 | | 2nn0 12107 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈
ℕ0) |
19 | | eluz2nn 12480 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) |
20 | | nnm1nn0 12131 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 1) ∈
ℕ0) |
22 | 18, 21 | nn0expcld 13813 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(𝑁 − 1)) ∈
ℕ0) |
23 | 18, 22 | nn0expcld 13813 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(2↑(𝑁 − 1))) ∈
ℕ0) |
24 | 23 | nn0cnd 12152 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (2↑(2↑(𝑁 − 1))) ∈
ℂ) |
25 | | peano2nn0 12130 |
. . . . . . . 8
⊢ ((𝑁 − 2) ∈
ℕ0 → ((𝑁 − 2) + 1) ∈
ℕ0) |
26 | 10, 25 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 2) + 1) ∈
ℕ0) |
27 | | fmtnonn 44656 |
. . . . . . 7
⊢ (((𝑁 − 2) + 1) ∈
ℕ0 → (FermatNo‘((𝑁 − 2) + 1)) ∈
ℕ) |
28 | 26, 27 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘((𝑁 − 2) + 1)) ∈
ℕ) |
29 | 28 | nncnd 11846 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘((𝑁 − 2) + 1)) ∈
ℂ) |
30 | 24, 29, 9 | subdid 11288 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 1))) ·
((FermatNo‘((𝑁
− 2) + 1)) − 2)) = (((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘((𝑁 −
2) + 1))) − ((2↑(2↑(𝑁 − 1))) · 2))) |
31 | | eluzelcn 12450 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℂ) |
32 | | ax-1cn 10787 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
33 | 32 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℂ) |
34 | | subsub 11108 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → (𝑁 − (2 − 1)) = ((𝑁 − 2) +
1)) |
35 | 34 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 2) + 1) = (𝑁 − (2 − 1))) |
36 | 31, 9, 33, 35 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 2) + 1) = (𝑁 − (2 − 1))) |
37 | | 2m1e1 11956 |
. . . . . . . . 9
⊢ (2
− 1) = 1 |
38 | 37 | oveq2i 7224 |
. . . . . . . 8
⊢ (𝑁 − (2 − 1)) = (𝑁 − 1) |
39 | 36, 38 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
40 | 39 | fveq2d 6721 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘((𝑁 − 2) + 1)) = (FermatNo‘(𝑁 − 1))) |
41 | 40 | oveq2d 7229 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘((𝑁 −
2) + 1))) = ((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1)))) |
42 | 41 | oveq1d 7228 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘((𝑁 −
2) + 1))) − ((2↑(2↑(𝑁 − 1))) · 2)) =
(((2↑(2↑(𝑁
− 1))) · (FermatNo‘(𝑁 − 1))) −
((2↑(2↑(𝑁 −
1))) · 2))) |
43 | 30, 42 | eqtrd 2777 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 1))) ·
((FermatNo‘((𝑁
− 2) + 1)) − 2)) = (((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1))) − ((2↑(2↑(𝑁 − 1))) · 2))) |
44 | 43 | oveq2d 7229 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1)) + ((2↑(2↑(𝑁 − 1))) ·
((FermatNo‘((𝑁
− 2) + 1)) − 2))) = ((FermatNo‘(𝑁 − 1)) + (((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1))) − ((2↑(2↑(𝑁 − 1))) ·
2)))) |
45 | | fmtnonn 44656 |
. . . . . . . . . 10
⊢ ((𝑁 − 1) ∈
ℕ0 → (FermatNo‘(𝑁 − 1)) ∈
ℕ) |
46 | 21, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘(𝑁 − 1)) ∈
ℕ) |
47 | 46 | nncnd 11846 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘(𝑁 − 1)) ∈
ℂ) |
48 | 47 | mulid2d 10851 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 · (FermatNo‘(𝑁 − 1))) =
(FermatNo‘(𝑁 −
1))) |
49 | 48 | eqcomd 2743 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘(𝑁 − 1)) = (1 ·
(FermatNo‘(𝑁 −
1)))) |
50 | 49 | oveq1d 7228 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1)) + ((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1)))) = ((1 · (FermatNo‘(𝑁 − 1))) + ((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1))))) |
51 | 33, 24, 47 | adddird 10858 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((1 + (2↑(2↑(𝑁 − 1)))) ·
(FermatNo‘(𝑁 −
1))) = ((1 · (FermatNo‘(𝑁 − 1))) + ((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1))))) |
52 | 33, 24 | addcomd 11034 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 + (2↑(2↑(𝑁 − 1)))) = ((2↑(2↑(𝑁 − 1))) +
1)) |
53 | | fmtno 44654 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈
ℕ0 → (FermatNo‘(𝑁 − 1)) = ((2↑(2↑(𝑁 − 1))) +
1)) |
54 | 21, 53 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘(𝑁 − 1)) = ((2↑(2↑(𝑁 − 1))) +
1)) |
55 | 52, 54 | eqtr4d 2780 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 + (2↑(2↑(𝑁 − 1)))) = (FermatNo‘(𝑁 − 1))) |
56 | 55 | oveq1d 7228 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((1 + (2↑(2↑(𝑁 − 1)))) ·
(FermatNo‘(𝑁 −
1))) = ((FermatNo‘(𝑁
− 1)) · (FermatNo‘(𝑁 − 1)))) |
57 | 47 | sqvald 13713 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1))↑2) =
((FermatNo‘(𝑁 −
1)) · (FermatNo‘(𝑁 − 1)))) |
58 | 56, 57 | eqtr4d 2780 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((1 + (2↑(2↑(𝑁 − 1)))) ·
(FermatNo‘(𝑁 −
1))) = ((FermatNo‘(𝑁
− 1))↑2)) |
59 | 50, 51, 58 | 3eqtr2d 2783 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1)) + ((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1)))) = ((FermatNo‘(𝑁
− 1))↑2)) |
60 | 59 | oveq1d 7228 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1)) + ((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1)))) − ((2↑(2↑(𝑁 − 1))) · 2)) =
(((FermatNo‘(𝑁
− 1))↑2) − ((2↑(2↑(𝑁 − 1))) · 2))) |
61 | 24, 47 | mulcld 10853 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1))) ∈ ℂ) |
62 | 24, 9 | mulcld 10853 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2↑(2↑(𝑁 − 1))) · 2) ∈
ℂ) |
63 | 47, 61, 62 | addsubassd 11209 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1)) + ((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1)))) − ((2↑(2↑(𝑁 − 1))) · 2)) =
((FermatNo‘(𝑁 −
1)) + (((2↑(2↑(𝑁
− 1))) · (FermatNo‘(𝑁 − 1))) −
((2↑(2↑(𝑁 −
1))) · 2)))) |
64 | | npcan1 11257 |
. . . . . . 7
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
65 | 31, 64 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 − 1) + 1) = 𝑁) |
66 | 65 | eqcomd 2743 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 = ((𝑁 − 1) + 1)) |
67 | 66 | fveq2d 6721 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘𝑁) = (FermatNo‘((𝑁 − 1) + 1))) |
68 | | fmtnorec1 44662 |
. . . . 5
⊢ ((𝑁 − 1) ∈
ℕ0 → (FermatNo‘((𝑁 − 1) + 1)) =
((((FermatNo‘(𝑁
− 1)) − 1)↑2) + 1)) |
69 | 21, 68 | syl 17 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘((𝑁 − 1) + 1)) =
((((FermatNo‘(𝑁
− 1)) − 1)↑2) + 1)) |
70 | | binom2sub1 13788 |
. . . . . . 7
⊢
((FermatNo‘(𝑁
− 1)) ∈ ℂ → (((FermatNo‘(𝑁 − 1)) − 1)↑2) =
((((FermatNo‘(𝑁
− 1))↑2) − (2 · (FermatNo‘(𝑁 − 1)))) + 1)) |
71 | 47, 70 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1)) − 1)↑2) =
((((FermatNo‘(𝑁
− 1))↑2) − (2 · (FermatNo‘(𝑁 − 1)))) + 1)) |
72 | 71 | oveq1d 7228 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((FermatNo‘(𝑁 − 1)) − 1)↑2) + 1) =
(((((FermatNo‘(𝑁
− 1))↑2) − (2 · (FermatNo‘(𝑁 − 1)))) + 1) + 1)) |
73 | 46 | nnsqcld 13811 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1))↑2) ∈
ℕ) |
74 | 73 | nncnd 11846 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1))↑2) ∈
ℂ) |
75 | 9, 47 | mulcld 10853 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (FermatNo‘(𝑁 − 1))) ∈
ℂ) |
76 | 74, 75 | subcld 11189 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(FermatNo‘(𝑁 −
1)))) ∈ ℂ) |
77 | 76, 33, 33 | addassd 10855 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (((((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(FermatNo‘(𝑁 −
1)))) + 1) + 1) = ((((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(FermatNo‘(𝑁 −
1)))) + (1 + 1))) |
78 | 32 | 2timesi 11968 |
. . . . . . . . 9
⊢ (2
· 1) = (1 + 1) |
79 | 78 | eqcomi 2746 |
. . . . . . . 8
⊢ (1 + 1) =
(2 · 1) |
80 | 79 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 + 1) = (2 ·
1)) |
81 | 80 | oveq2d 7229 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(FermatNo‘(𝑁 −
1)))) + (1 + 1)) = ((((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(FermatNo‘(𝑁 −
1)))) + (2 · 1))) |
82 | 77, 81 | eqtrd 2777 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → (((((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(FermatNo‘(𝑁 −
1)))) + 1) + 1) = ((((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(FermatNo‘(𝑁 −
1)))) + (2 · 1))) |
83 | 8, 32 | mulcli 10840 |
. . . . . . . 8
⊢ (2
· 1) ∈ ℂ |
84 | 83 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · 1) ∈
ℂ) |
85 | 74, 75, 84 | subadd23d 11211 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(FermatNo‘(𝑁 −
1)))) + (2 · 1)) = (((FermatNo‘(𝑁 − 1))↑2) + ((2 · 1)
− (2 · (FermatNo‘(𝑁 − 1)))))) |
86 | 9, 33, 47 | subdid 11288 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (1 −
(FermatNo‘(𝑁 −
1)))) = ((2 · 1) − (2 · (FermatNo‘(𝑁 − 1))))) |
87 | 86 | eqcomd 2743 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → ((2 · 1) − (2 ·
(FermatNo‘(𝑁 −
1)))) = (2 · (1 − (FermatNo‘(𝑁 − 1))))) |
88 | 87 | oveq2d 7229 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1))↑2) + ((2 · 1)
− (2 · (FermatNo‘(𝑁 − 1))))) = (((FermatNo‘(𝑁 − 1))↑2) + (2
· (1 − (FermatNo‘(𝑁 − 1)))))) |
89 | 33, 47 | subcld 11189 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 − (FermatNo‘(𝑁 − 1))) ∈
ℂ) |
90 | 9, 89 | mulneg2d 11286 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · -(1 −
(FermatNo‘(𝑁 −
1)))) = -(2 · (1 − (FermatNo‘(𝑁 − 1))))) |
91 | 33, 47 | negsubdi2d 11205 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → -(1 − (FermatNo‘(𝑁 − 1))) =
((FermatNo‘(𝑁 −
1)) − 1)) |
92 | | fmtnom1nn 44657 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
ℕ0 → ((FermatNo‘(𝑁 − 1)) − 1) =
(2↑(2↑(𝑁 −
1)))) |
93 | 21, 92 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1)) − 1) =
(2↑(2↑(𝑁 −
1)))) |
94 | 91, 93 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → -(1 − (FermatNo‘(𝑁 − 1))) =
(2↑(2↑(𝑁 −
1)))) |
95 | 94 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · -(1 −
(FermatNo‘(𝑁 −
1)))) = (2 · (2↑(2↑(𝑁 − 1))))) |
96 | 90, 95 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → -(2 · (1 −
(FermatNo‘(𝑁 −
1)))) = (2 · (2↑(2↑(𝑁 − 1))))) |
97 | 96 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1))↑2) − -(2 · (1
− (FermatNo‘(𝑁
− 1))))) = (((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(2↑(2↑(𝑁 −
1)))))) |
98 | 9, 89 | mulcld 10853 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (1 −
(FermatNo‘(𝑁 −
1)))) ∈ ℂ) |
99 | 74, 98 | subnegd 11196 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1))↑2) − -(2 · (1
− (FermatNo‘(𝑁
− 1))))) = (((FermatNo‘(𝑁 − 1))↑2) + (2 · (1
− (FermatNo‘(𝑁
− 1)))))) |
100 | 9, 24 | mulcomd 10854 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (2 · (2↑(2↑(𝑁 − 1)))) =
((2↑(2↑(𝑁 −
1))) · 2)) |
101 | 100 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(2↑(2↑(𝑁 −
1))))) = (((FermatNo‘(𝑁 − 1))↑2) −
((2↑(2↑(𝑁 −
1))) · 2))) |
102 | 97, 99, 101 | 3eqtr3d 2785 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1))↑2) + (2 · (1
− (FermatNo‘(𝑁
− 1))))) = (((FermatNo‘(𝑁 − 1))↑2) −
((2↑(2↑(𝑁 −
1))) · 2))) |
103 | 85, 88, 102 | 3eqtrd 2781 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((FermatNo‘(𝑁 − 1))↑2) − (2 ·
(FermatNo‘(𝑁 −
1)))) + (2 · 1)) = (((FermatNo‘(𝑁 − 1))↑2) −
((2↑(2↑(𝑁 −
1))) · 2))) |
104 | 72, 82, 103 | 3eqtrd 2781 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((((FermatNo‘(𝑁 − 1)) − 1)↑2) + 1) =
(((FermatNo‘(𝑁
− 1))↑2) − ((2↑(2↑(𝑁 − 1))) · 2))) |
105 | 67, 69, 104 | 3eqtrrd 2782 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (((FermatNo‘(𝑁 − 1))↑2) −
((2↑(2↑(𝑁 −
1))) · 2)) = (FermatNo‘𝑁)) |
106 | 60, 63, 105 | 3eqtr3d 2785 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘2) → ((FermatNo‘(𝑁 − 1)) + (((2↑(2↑(𝑁 − 1))) ·
(FermatNo‘(𝑁 −
1))) − ((2↑(2↑(𝑁 − 1))) · 2))) =
(FermatNo‘𝑁)) |
107 | 16, 44, 106 | 3eqtrrd 2782 |
1
⊢ (𝑁 ∈
(ℤ≥‘2) → (FermatNo‘𝑁) = ((FermatNo‘(𝑁 − 1)) + ((2↑(2↑(𝑁 − 1))) ·
∏𝑛 ∈ (0...(𝑁 −
2))(FermatNo‘𝑛)))) |