Proof of Theorem fmtnoprmfac1lem
Step | Hyp | Ref
| Expression |
1 | | nnnn0 11176 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
2 | | fmtno 39979 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (FermatNo‘𝑁) =
((2↑(2↑𝑁)) +
1)) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(FermatNo‘𝑁) =
((2↑(2↑𝑁)) +
1)) |
4 | 3 | breq2d 4595 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑃 ∥ (FermatNo‘𝑁) ↔ 𝑃 ∥ ((2↑(2↑𝑁)) + 1))) |
5 | 4 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∥
(FermatNo‘𝑁) ↔
𝑃 ∥
((2↑(2↑𝑁)) +
1))) |
6 | | eldifi 3694 |
. . . . . 6
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
7 | | prmnn 15226 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℕ) |
9 | | 2nn 11062 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
10 | 9 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ) |
11 | | 2nn0 11186 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
12 | 11 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ0) |
13 | 12, 1 | nn0expcld 12893 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑𝑁) ∈
ℕ0) |
14 | 10, 13 | nnexpcld 12892 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(2↑(2↑𝑁)) ∈
ℕ) |
15 | 14 | peano2nnd 10914 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((2↑(2↑𝑁)) + 1)
∈ ℕ) |
16 | 15 | nnzd 11357 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((2↑(2↑𝑁)) + 1)
∈ ℤ) |
17 | | dvdsval3 14825 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧
((2↑(2↑𝑁)) + 1)
∈ ℤ) → (𝑃
∥ ((2↑(2↑𝑁)) + 1) ↔ (((2↑(2↑𝑁)) + 1) mod 𝑃) = 0)) |
18 | 8, 16, 17 | syl2anr 494 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∥
((2↑(2↑𝑁)) + 1)
↔ (((2↑(2↑𝑁)) + 1) mod 𝑃) = 0)) |
19 | 5, 18 | bitrd 267 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∥
(FermatNo‘𝑁) ↔
(((2↑(2↑𝑁)) + 1)
mod 𝑃) =
0)) |
20 | 19 | biimp3a 1424 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∥
(FermatNo‘𝑁)) →
(((2↑(2↑𝑁)) + 1)
mod 𝑃) =
0) |
21 | 14 | nnzd 11357 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(2↑(2↑𝑁)) ∈
ℤ) |
22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (2↑(2↑𝑁))
∈ ℤ) |
23 | | 1zzd 11285 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 1 ∈ ℤ) |
24 | 8 | adantl 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ∈
ℕ) |
25 | | summodnegmod 14850 |
. . . . . 6
⊢
(((2↑(2↑𝑁)) ∈ ℤ ∧ 1 ∈ ℤ
∧ 𝑃 ∈ ℕ)
→ ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 ↔ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃))) |
26 | 22, 23, 24, 25 | syl3anc 1318 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 ↔ ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃))) |
27 | | neg1z 11290 |
. . . . . . . . . 10
⊢ -1 ∈
ℤ |
28 | 22, 27 | jctir 559 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((2↑(2↑𝑁))
∈ ℤ ∧ -1 ∈ ℤ)) |
29 | 28 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑𝑁))
mod 𝑃) = (-1 mod 𝑃)) → ((2↑(2↑𝑁)) ∈ ℤ ∧ -1
∈ ℤ)) |
30 | 7 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ+) |
31 | 6, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℝ+) |
32 | 12, 31 | anim12i 588 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (2 ∈ ℕ0 ∧ 𝑃 ∈
ℝ+)) |
33 | 32 | adantr 480 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑𝑁))
mod 𝑃) = (-1 mod 𝑃)) → (2 ∈
ℕ0 ∧ 𝑃
∈ ℝ+)) |
34 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑𝑁))
mod 𝑃) = (-1 mod 𝑃)) → ((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃)) |
35 | | modexp 12861 |
. . . . . . . 8
⊢
((((2↑(2↑𝑁)) ∈ ℤ ∧ -1 ∈ ℤ)
∧ (2 ∈ ℕ0 ∧ 𝑃 ∈ ℝ+) ∧
((2↑(2↑𝑁)) mod
𝑃) = (-1 mod 𝑃)) →
(((2↑(2↑𝑁))↑2) mod 𝑃) = ((-1↑2) mod 𝑃)) |
36 | 29, 33, 34, 35 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑𝑁))
mod 𝑃) = (-1 mod 𝑃)) →
(((2↑(2↑𝑁))↑2) mod 𝑃) = ((-1↑2) mod 𝑃)) |
37 | 36 | ex 449 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃) → (((2↑(2↑𝑁))↑2) mod 𝑃) = ((-1↑2) mod 𝑃))) |
38 | | 2cnd 10970 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
39 | 38, 13, 12 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (2 ∈
ℂ ∧ (2↑𝑁)
∈ ℕ0 ∧ 2 ∈
ℕ0)) |
40 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (2 ∈ ℂ ∧ (2↑𝑁) ∈ ℕ0 ∧ 2 ∈
ℕ0)) |
41 | | expmul 12767 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ (2↑𝑁) ∈ ℕ0 ∧ 2 ∈
ℕ0) → (2↑((2↑𝑁) · 2)) = ((2↑(2↑𝑁))↑2)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (2↑((2↑𝑁)
· 2)) = ((2↑(2↑𝑁))↑2)) |
43 | | 2cnd 10970 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 2 ∈ ℂ) |
44 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑁 ∈
ℕ0) |
45 | 43, 44 | expp1d 12871 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (2↑(𝑁 + 1)) =
((2↑𝑁) ·
2)) |
46 | 45 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((2↑𝑁) ·
2) = (2↑(𝑁 +
1))) |
47 | 46 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (2↑((2↑𝑁)
· 2)) = (2↑(2↑(𝑁 + 1)))) |
48 | 42, 47 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((2↑(2↑𝑁))↑2) = (2↑(2↑(𝑁 + 1)))) |
49 | 48 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑𝑁))↑2) mod 𝑃) = ((2↑(2↑(𝑁 + 1))) mod 𝑃)) |
50 | | neg1sqe1 12821 |
. . . . . . . . . . 11
⊢
(-1↑2) = 1 |
51 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (-1↑2) = 1) |
52 | 51 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((-1↑2) mod 𝑃)
= (1 mod 𝑃)) |
53 | 8 | nnred 10912 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℝ) |
54 | | prmgt1 15247 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 1 <
𝑃) |
55 | 6, 54 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 1 < 𝑃) |
56 | | 1mod 12564 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (1 mod 𝑃) = 1) |
57 | 53, 55, 56 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (1 mod 𝑃) =
1) |
58 | 57 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (1 mod 𝑃) =
1) |
59 | 52, 58 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((-1↑2) mod 𝑃)
= 1) |
60 | 49, 59 | eqeq12d 2625 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((((2↑(2↑𝑁))↑2) mod 𝑃) = ((-1↑2) mod 𝑃) ↔ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1)) |
61 | | simpll 786 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) ∧
(((2↑(2↑𝑁)) + 1)
mod 𝑃) = 0) → (𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖
{2}))) |
62 | 21 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(2↑(2↑𝑁)) ∈
ℤ) |
63 | | 1zzd 11285 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 ∈
ℤ) |
64 | 7 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈
ℕ) |
65 | 62, 63, 64 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
((2↑(2↑𝑁)) ∈
ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ)) |
66 | 6, 65 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((2↑(2↑𝑁))
∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ)) |
67 | 66 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) →
((2↑(2↑𝑁)) ∈
ℤ ∧ 1 ∈ ℤ ∧ 𝑃 ∈ ℕ)) |
68 | 67, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) →
((((2↑(2↑𝑁)) + 1)
mod 𝑃) = 0 ↔
((2↑(2↑𝑁)) mod
𝑃) = (-1 mod 𝑃))) |
69 | | m1modnnsub1 12578 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℕ → (-1 mod
𝑃) = (𝑃 − 1)) |
70 | 24, 69 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (-1 mod 𝑃) = (𝑃 − 1)) |
71 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ≠
2) |
73 | 72 | necomd 2837 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 2 ≠ 𝑃) |
74 | 8 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℂ) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 𝑃 ∈
ℂ) |
76 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ 1 ∈ ℂ) |
77 | 75, 76, 76 | subadd2d 10290 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝑃 − 1) = 1
↔ (1 + 1) = 𝑃)) |
78 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 + 1) =
2 |
79 | 78 | eqeq1i 2615 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1 + 1)
= 𝑃 ↔ 2 = 𝑃) |
80 | 77, 79 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝑃 − 1) = 1
↔ 2 = 𝑃)) |
81 | 80 | necon3bid 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((𝑃 − 1) ≠
1 ↔ 2 ≠ 𝑃)) |
82 | 73, 81 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 − 1) ≠
1) |
83 | 70, 82 | eqnetrd 2849 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (-1 mod 𝑃) ≠
1) |
84 | 83 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) → (-1
mod 𝑃) ≠
1) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) ∧
((2↑(2↑𝑁)) mod
𝑃) = (-1 mod 𝑃)) → (-1 mod 𝑃) ≠ 1) |
86 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢
(((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃) → (((2↑(2↑𝑁)) mod 𝑃) = 1 ↔ (-1 mod 𝑃) = 1)) |
87 | 86 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) ∧
((2↑(2↑𝑁)) mod
𝑃) = (-1 mod 𝑃)) →
(((2↑(2↑𝑁)) mod
𝑃) = 1 ↔ (-1 mod 𝑃) = 1)) |
88 | 87 | necon3bid 2826 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) ∧
((2↑(2↑𝑁)) mod
𝑃) = (-1 mod 𝑃)) →
(((2↑(2↑𝑁)) mod
𝑃) ≠ 1 ↔ (-1 mod
𝑃) ≠
1)) |
89 | 85, 88 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) ∧
((2↑(2↑𝑁)) mod
𝑃) = (-1 mod 𝑃)) → ((2↑(2↑𝑁)) mod 𝑃) ≠ 1) |
90 | 89 | ex 449 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) →
(((2↑(2↑𝑁)) mod
𝑃) = (-1 mod 𝑃) → ((2↑(2↑𝑁)) mod 𝑃) ≠ 1)) |
91 | 68, 90 | sylbid 229 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) →
((((2↑(2↑𝑁)) + 1)
mod 𝑃) = 0 →
((2↑(2↑𝑁)) mod
𝑃) ≠
1)) |
92 | 91 | imp 444 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) ∧
(((2↑(2↑𝑁)) + 1)
mod 𝑃) = 0) →
((2↑(2↑𝑁)) mod
𝑃) ≠ 1) |
93 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) ∧
(((2↑(2↑𝑁)) + 1)
mod 𝑃) = 0) →
((2↑(2↑(𝑁 + 1)))
mod 𝑃) =
1) |
94 | | odz2prm2pw 40013 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ (((2↑(2↑𝑁))
mod 𝑃) ≠ 1 ∧
((2↑(2↑(𝑁 + 1)))
mod 𝑃) = 1)) →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) |
95 | 61, 92, 93, 94 | syl12anc 1316 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) ∧
(((2↑(2↑𝑁)) + 1)
mod 𝑃) = 0) →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) |
96 | 95 | ex 449 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
∧ ((2↑(2↑(𝑁 +
1))) mod 𝑃) = 1) →
((((2↑(2↑𝑁)) + 1)
mod 𝑃) = 0 →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))) |
97 | 96 | ex 449 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑(𝑁
+ 1))) mod 𝑃) = 1 →
((((2↑(2↑𝑁)) + 1)
mod 𝑃) = 0 →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
98 | 60, 97 | sylbid 229 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((((2↑(2↑𝑁))↑2) mod 𝑃) = ((-1↑2) mod 𝑃) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
99 | 37, 98 | syld 46 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (((2↑(2↑𝑁)) mod 𝑃) = (-1 mod 𝑃) → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
100 | 26, 99 | sylbid 229 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 → ((((2↑(2↑𝑁)) + 1) mod 𝑃) = 0 →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
101 | 19, 100 | sylbid 229 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}))
→ (𝑃 ∥
(FermatNo‘𝑁) →
((((2↑(2↑𝑁)) + 1)
mod 𝑃) = 0 →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))))) |
102 | 101 | 3impia 1253 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∥
(FermatNo‘𝑁)) →
((((2↑(2↑𝑁)) + 1)
mod 𝑃) = 0 →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))) |
103 | 20, 102 | mpd 15 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ 𝑃 ∥
(FermatNo‘𝑁)) →
((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1))) |