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 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 )