Metamath Proof Explorer

Theorem fmtnoprmfac2lem1

Description: Lemma for fmtnoprmfac2 . (Contributed by AV, 26-Jul-2021)

Ref Expression
Assertion fmtnoprmfac2lem1 ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 )

Proof

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 1mod ⊢ ( ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 )
126 2 121 124 125 4syl ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 1 mod 𝑃 ) = 1 )
127 126 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( 1 mod 𝑃 ) = 1 )
128 127 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) → ( 1 mod 𝑃 ) = 1 )
129 11 120 128 3eqtrd ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 )
130 129 rexlimdva2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ∃ 𝑛 ∈ ℕ 𝑃 = ( ( 𝑛 · ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 ) )
131 5 130 mpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑃 ∥ ( FermatNo ‘ 𝑁 ) ) → ( ( 2 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = 1 )