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 )