fmtnoprmfac2lem1

		Ref	Expression
	Assertion	fmtnoprmfac2lem1	$⊢ (N \in ℤ_{\geq 2} \land P \in (ℙ ∖ \{2\}) \land P ∥ FermatNo (N)) \to 2^{\frac{P - 1}{2}} \mod P = 1$

Proof

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

Metamath Proof Explorer

Theorem fmtnoprmfac2lem1

Proof