Step |
Hyp |
Ref |
Expression |
1 |
|
eluz2nn |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ ) |
2 |
|
eldifi |
⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ ) |
3 |
|
id |
⊢ ( 𝑃 ∥ ( FermatNo ‘ 𝑁 ) → 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) |
4 |
|
fmtnoprmfac1 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) |
5 |
1 2 3 4
|
syl3an |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) |
6 |
|
2z |
⊢ 2 ∈ ℤ |
7 |
|
simp2 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) ) |
8 |
|
lgsvalmod |
⊢ ( ( 2 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) ) |
9 |
8
|
eqcomd |
⊢ ( ( 2 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( 2 /L 𝑃 ) mod 𝑃 ) ) |
10 |
6 7 9
|
sylancr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( 2 /L 𝑃 ) mod 𝑃 ) ) |
11 |
10
|
ad2antrr |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( 2 /L 𝑃 ) mod 𝑃 ) ) |
12 |
|
nncn |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ ) |
13 |
12
|
adantl |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ ) |
14 |
|
2nn |
⊢ 2 ∈ ℕ |
15 |
14
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℕ ) |
16 |
|
eluzge2nn0 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 ) |
17 |
|
peano2nn0 |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 ) |
18 |
16 17
|
syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 + 1 ) ∈ ℕ0 ) |
19 |
15 18
|
nnexpcld |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ ) |
20 |
19
|
nncnd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℂ ) |
21 |
20
|
adantr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℂ ) |
22 |
13 21
|
mulcomd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 2 ↑ ( 𝑁 + 1 ) ) · 𝑛 ) ) |
23 |
|
8cn |
⊢ 8 ∈ ℂ |
24 |
23
|
a1i |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → 8 ∈ ℂ ) |
25 |
|
0re |
⊢ 0 ∈ ℝ |
26 |
|
8pos |
⊢ 0 < 8 |
27 |
25 26
|
gtneii |
⊢ 8 ≠ 0 |
28 |
27
|
a1i |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → 8 ≠ 0 ) |
29 |
21 24 28
|
divcan2d |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( 8 · ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) |
30 |
29
|
eqcomd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ ( 𝑁 + 1 ) ) = ( 8 · ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) ) ) |
31 |
30
|
oveq1d |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) · 𝑛 ) = ( ( 8 · ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) ) · 𝑛 ) ) |
32 |
23
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 8 ∈ ℂ ) |
33 |
27
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 8 ≠ 0 ) |
34 |
20 32 33
|
divcld |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) ∈ ℂ ) |
35 |
34
|
adantr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) ∈ ℂ ) |
36 |
24 35 13
|
mulassd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( ( 8 · ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) ) · 𝑛 ) = ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) ) |
37 |
22 31 36
|
3eqtrd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) ) |
38 |
37
|
oveq1d |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) = ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) ) |
39 |
38
|
eqeq2d |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ↔ 𝑃 = ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) ) ) |
40 |
|
oveq1 |
⊢ ( 𝑃 = ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) → ( 𝑃 mod 8 ) = ( ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) mod 8 ) ) |
41 |
40
|
adantl |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) ) → ( 𝑃 mod 8 ) = ( ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) mod 8 ) ) |
42 |
|
3m1e2 |
⊢ ( 3 − 1 ) = 2 |
43 |
|
eluzle |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑁 ) |
44 |
42 43
|
eqbrtrid |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 3 − 1 ) ≤ 𝑁 ) |
45 |
|
3re |
⊢ 3 ∈ ℝ |
46 |
45
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 3 ∈ ℝ ) |
47 |
|
1red |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℝ ) |
48 |
|
eluzelre |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℝ ) |
49 |
46 47 48
|
lesubaddd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 3 − 1 ) ≤ 𝑁 ↔ 3 ≤ ( 𝑁 + 1 ) ) ) |
50 |
44 49
|
mpbid |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 3 ≤ ( 𝑁 + 1 ) ) |
51 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
52 |
|
nn0sub |
⊢ ( ( 3 ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( 3 ≤ ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) − 3 ) ∈ ℕ0 ) ) |
53 |
51 18 52
|
sylancr |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 3 ≤ ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) − 3 ) ∈ ℕ0 ) ) |
54 |
50 53
|
mpbid |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 + 1 ) − 3 ) ∈ ℕ0 ) |
55 |
15 54
|
nnexpcld |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) ∈ ℕ ) |
56 |
55
|
nnzd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) ∈ ℤ ) |
57 |
|
oveq2 |
⊢ ( 𝑘 = ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) → ( 8 · 𝑘 ) = ( 8 · ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) ) ) |
58 |
57
|
eqeq1d |
⊢ ( 𝑘 = ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) → ( ( 8 · 𝑘 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ↔ ( 8 · ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) |
59 |
58
|
adantl |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 = ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) ) → ( ( 8 · 𝑘 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ↔ ( 8 · ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) ) |
60 |
|
cu2 |
⊢ ( 2 ↑ 3 ) = 8 |
61 |
60
|
eqcomi |
⊢ 8 = ( 2 ↑ 3 ) |
62 |
61
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 8 = ( 2 ↑ 3 ) ) |
63 |
|
2cnne0 |
⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) |
64 |
63
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) |
65 |
|
eluzelz |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℤ ) |
66 |
65
|
peano2zd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 + 1 ) ∈ ℤ ) |
67 |
|
3z |
⊢ 3 ∈ ℤ |
68 |
67
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 3 ∈ ℤ ) |
69 |
|
expsub |
⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( 𝑁 + 1 ) ∈ ℤ ∧ 3 ∈ ℤ ) ) → ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) = ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 3 ) ) ) |
70 |
64 66 68 69
|
syl12anc |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) = ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 3 ) ) ) |
71 |
62 70
|
oveq12d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 8 · ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) ) = ( ( 2 ↑ 3 ) · ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 3 ) ) ) ) |
72 |
|
nnexpcl |
⊢ ( ( 2 ∈ ℕ ∧ 3 ∈ ℕ0 ) → ( 2 ↑ 3 ) ∈ ℕ ) |
73 |
14 51 72
|
mp2an |
⊢ ( 2 ↑ 3 ) ∈ ℕ |
74 |
73
|
nncni |
⊢ ( 2 ↑ 3 ) ∈ ℂ |
75 |
74
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ 3 ) ∈ ℂ ) |
76 |
|
2cn |
⊢ 2 ∈ ℂ |
77 |
|
2ne0 |
⊢ 2 ≠ 0 |
78 |
|
expne0i |
⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 3 ∈ ℤ ) → ( 2 ↑ 3 ) ≠ 0 ) |
79 |
76 77 67 78
|
mp3an |
⊢ ( 2 ↑ 3 ) ≠ 0 |
80 |
79
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ 3 ) ≠ 0 ) |
81 |
20 75 80
|
divcan2d |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ 3 ) · ( ( 2 ↑ ( 𝑁 + 1 ) ) / ( 2 ↑ 3 ) ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) |
82 |
71 81
|
eqtrd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 8 · ( 2 ↑ ( ( 𝑁 + 1 ) − 3 ) ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) |
83 |
56 59 82
|
rspcedvd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑘 ∈ ℤ ( 8 · 𝑘 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ) |
84 |
|
8nn |
⊢ 8 ∈ ℕ |
85 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
86 |
85
|
a1i |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℕ0 ) |
87 |
86 18
|
nn0expcld |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ0 ) |
88 |
87
|
nn0zd |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℤ ) |
89 |
|
zdiv |
⊢ ( ( 8 ∈ ℕ ∧ ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℤ ) → ( ∃ 𝑘 ∈ ℤ ( 8 · 𝑘 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ↔ ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) ∈ ℤ ) ) |
90 |
84 88 89
|
sylancr |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ∃ 𝑘 ∈ ℤ ( 8 · 𝑘 ) = ( 2 ↑ ( 𝑁 + 1 ) ) ↔ ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) ∈ ℤ ) ) |
91 |
83 90
|
mpbid |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) ∈ ℤ ) |
92 |
91
|
adantr |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) ∈ ℤ ) |
93 |
|
nnz |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ ) |
94 |
93
|
adantl |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℤ ) |
95 |
92 94
|
zmulcld |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ∈ ℤ ) |
96 |
84
|
nnzi |
⊢ 8 ∈ ℤ |
97 |
|
2re |
⊢ 2 ∈ ℝ |
98 |
|
8re |
⊢ 8 ∈ ℝ |
99 |
|
2lt8 |
⊢ 2 < 8 |
100 |
97 98 99
|
ltleii |
⊢ 2 ≤ 8 |
101 |
|
eluz2 |
⊢ ( 8 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 8 ∈ ℤ ∧ 2 ≤ 8 ) ) |
102 |
6 96 100 101
|
mpbir3an |
⊢ 8 ∈ ( ℤ≥ ‘ 2 ) |
103 |
|
mulp1mod1 |
⊢ ( ( ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ∈ ℤ ∧ 8 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) mod 8 ) = 1 ) |
104 |
95 102 103
|
sylancl |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) mod 8 ) = 1 ) |
105 |
|
1nn |
⊢ 1 ∈ ℕ |
106 |
|
prid1g |
⊢ ( 1 ∈ ℕ → 1 ∈ { 1 , 7 } ) |
107 |
105 106
|
mp1i |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → 1 ∈ { 1 , 7 } ) |
108 |
104 107
|
eqeltrd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) mod 8 ) ∈ { 1 , 7 } ) |
109 |
108
|
adantr |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) ) → ( ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) mod 8 ) ∈ { 1 , 7 } ) |
110 |
41 109
|
eqeltrd |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) ) → ( 𝑃 mod 8 ) ∈ { 1 , 7 } ) |
111 |
110
|
ex |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 = ( ( 8 · ( ( ( 2 ↑ ( 𝑁 + 1 ) ) / 8 ) · 𝑛 ) ) + 1 ) → ( 𝑃 mod 8 ) ∈ { 1 , 7 } ) ) |
112 |
39 111
|
sylbid |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) → ( 𝑃 mod 8 ) ∈ { 1 , 7 } ) ) |
113 |
112
|
3ad2antl1 |
⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) → ( 𝑃 mod 8 ) ∈ { 1 , 7 } ) ) |
114 |
113
|
imp |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) → ( 𝑃 mod 8 ) ∈ { 1 , 7 } ) |
115 |
|
2lgs |
⊢ ( 𝑃 ∈ ℙ → ( ( 2 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 8 ) ∈ { 1 , 7 } ) ) |
116 |
2 115
|
syl |
⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 2 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 8 ) ∈ { 1 , 7 } ) ) |
117 |
116
|
3ad2ant2 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( 2 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 8 ) ∈ { 1 , 7 } ) ) |
118 |
117
|
ad2antrr |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) → ( ( 2 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 8 ) ∈ { 1 , 7 } ) ) |
119 |
114 118
|
mpbird |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) → ( 2 /L 𝑃 ) = 1 ) |
120 |
119
|
oveq1d |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) → ( ( 2 /L 𝑃 ) mod 𝑃 ) = ( 1 mod 𝑃 ) ) |
121 |
|
prmuz2 |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) ) |
122 |
|
eluzelre |
⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℝ ) |
123 |
|
eluz2gt1 |
⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑃 ) |
124 |
122 123
|
jca |
⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) ) |
125 |
121 124
|
syl |
⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) ) |
126 |
|
1mod |
⊢ ( ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 ) |
127 |
2 125 126
|
3syl |
⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 1 mod 𝑃 ) = 1 ) |
128 |
127
|
3ad2ant2 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( 1 mod 𝑃 ) = 1 ) |
129 |
128
|
ad2antrr |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) → ( 1 mod 𝑃 ) = 1 ) |
130 |
11 120 129
|
3eqtrd |
⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 ) |
131 |
130
|
rexlimdva2 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ∃ 𝑛 ∈ ℕ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 ) ) |
132 |
5 131
|
mpd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 ) |