lgseisenlem1

Description: Lemma for lgseisen . If R ( u ) = ( Q x. u ) mod P and M ( u ) = ( -u 1 ^ R ( u ) ) x. R ( u ) , then for any even 1 <_ u <_ P - 1 , M ( u ) is also an even integer 1 <_ M ( u ) <_ P - 1 . To simplify these statements, we divide all the even numbers by 2 , so that it becomes the statement that M ( x / 2 ) = ( -u 1 ^ R ( x / 2 ) ) x. R ( x / 2 ) / 2 is an integer between 1 and ( P - 1 ) / 2 . (Contributed by Mario Carneiro, 17-Jun-2015)

	Ref	Expression
Hypotheses	lgseisen.1	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	lgseisen.2	$⊢ φ \to Q \in (ℙ ∖ \{2\})$
	lgseisen.3	$⊢ φ \to P \neq Q$
	lgseisen.4	$⊢ R = Q 2 x \mod P$
	lgseisen.5	$⊢ M = (x \in (1 \dots \frac{P - 1}{2}) ⟼ \frac{{(- 1)}^{R} R \mod P}{2})$
Assertion	lgseisenlem1	$⊢ φ \to M : (1 \dots \frac{P - 1}{2}) ⟶ (1 \dots \frac{P - 1}{2})$

Proof

Step	Hyp	Ref	Expression
1		lgseisen.1	$⊢ φ \to P \in (ℙ ∖ \{2\})$
2		lgseisen.2	$⊢ φ \to Q \in (ℙ ∖ \{2\})$
3		lgseisen.3	$⊢ φ \to P \neq Q$
4		lgseisen.4	$⊢ R = Q 2 x \mod P$
5		lgseisen.5	$⊢ M = (x \in (1 \dots \frac{P - 1}{2}) ⟼ \frac{{(- 1)}^{R} R \mod P}{2})$
6		neg1cn	$⊢ - 1 \in ℂ$
7	6	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to - 1 \in ℂ$
8		neg1ne0	$⊢ - 1 \neq 0$
9	8	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to - 1 \neq 0$
10		2z	$⊢ 2 \in ℤ$
11	10	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 2 \in ℤ$
12		simpr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to \frac{R}{2} \in ℤ$
13		expmulz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (2 \in ℤ \land \frac{R}{2} \in ℤ)) \to {(- 1)}^{2 (\frac{R}{2})} = {({-1}^{2})}^{\frac{R}{2}}$
14	7 9 11 12 13	syl22anc	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{2 (\frac{R}{2})} = {({-1}^{2})}^{\frac{R}{2}}$
15	2	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in (ℙ ∖ \{2\})$
16	15	eldifad	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in ℙ$
17		prmz	$⊢ Q \in ℙ \to Q \in ℤ$
18	16 17	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in ℤ$
19		elfzelz	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℤ$
20	19	adantl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \in ℤ$
21		zmulcl	$⊢ (2 \in ℤ \land x \in ℤ) \to 2 x \in ℤ$
22	10 20 21	sylancr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℤ$
23	18 22	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \in ℤ$
24	1	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in (ℙ ∖ \{2\})$
25	24	eldifad	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℙ$
26		prmnn	$⊢ P \in ℙ \to P \in ℕ$
27	25 26	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℕ$
28		zmodfz	$⊢ (Q 2 x \in ℤ \land P \in ℕ) \to Q 2 x \mod P \in (0 \dots P - 1)$
29	23 27 28	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \mod P \in (0 \dots P - 1)$
30	4 29	eqeltrid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in (0 \dots P - 1)$
31		elfznn0	$⊢ R \in (0 \dots P - 1) \to R \in ℕ_{0}$
32	30 31	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℕ_{0}$
33	32	nn0zd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℤ$
34	33	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℂ$
35	34	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to R \in ℂ$
36		2cnd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 2 \in ℂ$
37		2ne0	$⊢ 2 \neq 0$
38	37	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 2 \neq 0$
39	35 36 38	divcan2d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 2 (\frac{R}{2}) = R$
40	39	oveq2d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{2 (\frac{R}{2})} = {(- 1)}^{R}$
41		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
42	41	oveq1i	$⊢ {({-1}^{2})}^{\frac{R}{2}} = 1^{\frac{R}{2}}$
43		1exp	$⊢ \frac{R}{2} \in ℤ \to 1^{\frac{R}{2}} = 1$
44	43	adantl	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 1^{\frac{R}{2}} = 1$
45	42 44	syl5eq	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {({-1}^{2})}^{\frac{R}{2}} = 1$
46	14 40 45	3eqtr3d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{R} = 1$
47	46	oveq1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{R} R = 1 R$
48	35	mulid2d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 1 R = R$
49	47 48	eqtrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{R} R = R$
50	49	oveq1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{R} R \mod P = R \mod P$
51	32	nn0red	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℝ$
52	27	nnrpd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℝ^{+}$
53	32	nn0ge0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 0 \leq R$
54	23	zred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \in ℝ$
55		modlt	$⊢ (Q 2 x \in ℝ \land P \in ℝ^{+}) \to Q 2 x \mod P < P$
56	54 52 55	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \mod P < P$
57	4 56	eqbrtrid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R < P$
58		modid	$⊢ ((R \in ℝ \land P \in ℝ^{+}) \land (0 \leq R \land R < P)) \to R \mod P = R$
59	51 52 53 57 58	syl22anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \mod P = R$
60	59	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to R \mod P = R$
61	50 60	eqtrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{R} R \mod P = R$
62	61	oveq1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to \frac{{(- 1)}^{R} R \mod P}{2} = \frac{R}{2}$
63	62 12	eqeltrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to \frac{{(- 1)}^{R} R \mod P}{2} \in ℤ$
64	27	nncnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℂ$
65	64	mulid2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 1 P = P$
66	65	oveq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - R + 1 P = - R + P$
67	51	renegcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - R \in ℝ$
68	67	recnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - R \in ℂ$
69	64 68	addcomd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P + (- R) = - R + P$
70	64 34	negsubd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P + (- R) = P - R$
71	66 69 70	3eqtr2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - R + 1 P = P - R$
72	71	oveq1d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (- R + 1 P) \mod P = (P - R) \mod P$
73		1zzd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 1 \in ℤ$
74		modcyc	$⊢ (- R \in ℝ \land P \in ℝ^{+} \land 1 \in ℤ) \to (- R + 1 P) \mod P = (- R) \mod P$
75	67 52 73 74	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (- R + 1 P) \mod P = (- R) \mod P$
76	27	nnred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℝ$
77	76 51	resubcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - R \in ℝ$
78	51 76 57	ltled	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \leq P$
79	76 51	subge0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (0 \leq P - R \leftrightarrow R \leq P)$
80	78 79	mpbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 0 \leq P - R$
81		2nn	$⊢ 2 \in ℕ$
82		elfznn	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℕ$
83	82	adantl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \in ℕ$
84		nnmulcl	$⊢ (2 \in ℕ \land x \in ℕ) \to 2 x \in ℕ$
85	81 83 84	sylancr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℕ$
86		elfzle2	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \leq \frac{P - 1}{2}$
87	86	adantl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \leq \frac{P - 1}{2}$
88	83	nnred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \in ℝ$
89		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
90		uz2m1nn	$⊢ P \in ℤ_{\geq 2} \to P - 1 \in ℕ$
91	25 89 90	3syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℕ$
92	91	nnred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℝ$
93		2re	$⊢ 2 \in ℝ$
94	93	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 \in ℝ$
95		2pos	$⊢ 0 < 2$
96	95	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 0 < 2$
97		lemuldiv2	$⊢ (x \in ℝ \land P - 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 x \leq P - 1 \leftrightarrow x \leq \frac{P - 1}{2})$
98	88 92 94 96 97	syl112anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (2 x \leq P - 1 \leftrightarrow x \leq \frac{P - 1}{2})$
99	87 98	mpbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \leq P - 1$
100		prmz	$⊢ P \in ℙ \to P \in ℤ$
101	25 100	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℤ$
102		peano2zm	$⊢ P \in ℤ \to P - 1 \in ℤ$
103		fznn	$⊢ P - 1 \in ℤ \to (2 x \in (1 \dots P - 1) \leftrightarrow (2 x \in ℕ \land 2 x \leq P - 1))$
104	101 102 103	3syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (2 x \in (1 \dots P - 1) \leftrightarrow (2 x \in ℕ \land 2 x \leq P - 1))$
105	85 99 104	mpbir2and	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in (1 \dots P - 1)$
106		fzm1ndvds	$⊢ (P \in ℕ \land 2 x \in (1 \dots P - 1)) \to \neg P ∥ 2 x$
107	27 105 106	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg P ∥ 2 x$
108	3	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \neq Q$
109		prmrp	$⊢ (P \in ℙ \land Q \in ℙ) \to (P \gcd Q = 1 \leftrightarrow P \neq Q)$
110	25 16 109	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P \gcd Q = 1 \leftrightarrow P \neq Q)$
111	108 110	mpbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \gcd Q = 1$
112		coprmdvds	$⊢ (P \in ℤ \land Q \in ℤ \land 2 x \in ℤ) \to ((P ∥ Q 2 x \land P \gcd Q = 1) \to P ∥ 2 x)$
113	101 18 22 112	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to ((P ∥ Q 2 x \land P \gcd Q = 1) \to P ∥ 2 x)$
114	111 113	mpan2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P ∥ Q 2 x \to P ∥ 2 x)$
115	107 114	mtod	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg P ∥ Q 2 x$
116		dvdsval3	$⊢ (P \in ℕ \land Q 2 x \in ℤ) \to (P ∥ Q 2 x \leftrightarrow Q 2 x \mod P = 0)$
117	27 23 116	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P ∥ Q 2 x \leftrightarrow Q 2 x \mod P = 0)$
118	115 117	mtbid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg Q 2 x \mod P = 0$
119	4	eqeq1i	$⊢ R = 0 \leftrightarrow Q 2 x \mod P = 0$
120	118 119	sylnibr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg R = 0$
121	91	nnnn0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℕ_{0}$
122		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
123	121 122	eleqtrdi	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℤ_{\geq 0}$
124		elfzp12	$⊢ P - 1 \in ℤ_{\geq 0} \to (R \in (0 \dots P - 1) \leftrightarrow (R = 0 \lor R \in (0 + 1 \dots P - 1)))$
125	123 124	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (R \in (0 \dots P - 1) \leftrightarrow (R = 0 \lor R \in (0 + 1 \dots P - 1)))$
126	30 125	mpbid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (R = 0 \lor R \in (0 + 1 \dots P - 1))$
127	126	ord	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (\neg R = 0 \to R \in (0 + 1 \dots P - 1))$
128	120 127	mpd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in (0 + 1 \dots P - 1)$
129		1e0p1	$⊢ 1 = 0 + 1$
130	129	oveq1i	$⊢ (1 \dots P - 1) = (0 + 1 \dots P - 1)$
131	128 130	eleqtrrdi	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in (1 \dots P - 1)$
132		elfznn	$⊢ R \in (1 \dots P - 1) \to R \in ℕ$
133	131 132	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℕ$
134	133	nnrpd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℝ^{+}$
135	76 134	ltsubrpd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - R < P$
136		modid	$⊢ ((P - R \in ℝ \land P \in ℝ^{+}) \land (0 \leq P - R \land P - R < P)) \to (P - R) \mod P = P - R$
137	77 52 80 135 136	syl22anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P - R) \mod P = P - R$
138	72 75 137	3eqtr3d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (- R) \mod P = P - R$
139	138	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to (- R) \mod P = P - R$
140		ax-1cn	$⊢ 1 \in ℂ$
141	140	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 1 \in ℂ$
142	133	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to R \in ℕ$
143	33	peano2zd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R + 1 \in ℤ$
144		dvdsval2	$⊢ (2 \in ℤ \land 2 \neq 0 \land R + 1 \in ℤ) \to (2 ∥ (R + 1) \leftrightarrow \frac{R + 1}{2} \in ℤ)$
145	10 37 143 144	mp3an12i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (2 ∥ (R + 1) \leftrightarrow \frac{R + 1}{2} \in ℤ)$
146	145	biimpar	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 2 ∥ (R + 1)$
147	33	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to R \in ℤ$
148	81	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 2 \in ℕ$
149		1lt2	$⊢ 1 < 2$
150	149	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 1 < 2$
151		ndvdsp1	$⊢ (R \in ℤ \land 2 \in ℕ \land 1 < 2) \to (2 ∥ R \to \neg 2 ∥ (R + 1))$
152	147 148 150 151	syl3anc	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to (2 ∥ R \to \neg 2 ∥ (R + 1))$
153	146 152	mt2d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \neg 2 ∥ R$
154		oexpneg	$⊢ (1 \in ℂ \land R \in ℕ \land \neg 2 ∥ R) \to {(- 1)}^{R} = - 1^{R}$
155	141 142 153 154	syl3anc	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to {(- 1)}^{R} = - 1^{R}$
156		1exp	$⊢ R \in ℤ \to 1^{R} = 1$
157	147 156	syl	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 1^{R} = 1$
158	157	negeqd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to - 1^{R} = - 1$
159	155 158	eqtrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to {(- 1)}^{R} = - 1$
160	159	oveq1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to {(- 1)}^{R} R = -1 R$
161	34	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to R \in ℂ$
162	161	mulm1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to -1 R = - R$
163	160 162	eqtrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to {(- 1)}^{R} R = - R$
164	163	oveq1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to {(- 1)}^{R} R \mod P = (- R) \mod P$
165	64	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P \in ℂ$
166	165 161 141	pnpcan2d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P + 1 - (R + 1) = P - R$
167	139 164 166	3eqtr4d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to {(- 1)}^{R} R \mod P = P + 1 - (R + 1)$
168	167	oveq1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{{(- 1)}^{R} R \mod P}{2} = \frac{P + 1 - (R + 1)}{2}$
169		peano2cn	$⊢ P \in ℂ \to P + 1 \in ℂ$
170	165 169	syl	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P + 1 \in ℂ$
171		peano2cn	$⊢ R \in ℂ \to R + 1 \in ℂ$
172	161 171	syl	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to R + 1 \in ℂ$
173		2cnd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 2 \in ℂ$
174	37	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 2 \neq 0$
175	170 172 173 174	divsubdird	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{P + 1 - (R + 1)}{2} = (\frac{P + 1}{2}) - (\frac{R + 1}{2})$
176	168 175	eqtrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{{(- 1)}^{R} R \mod P}{2} = (\frac{P + 1}{2}) - (\frac{R + 1}{2})$
177	165 141 173	subadd23d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P - 1 + 2 = P + 2 - 1$
178		2m1e1	$⊢ 2 - 1 = 1$
179	178	oveq2i	$⊢ P + 2 - 1 = P + 1$
180	177 179	syl6req	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P + 1 = P - 1 + 2$
181	180	oveq1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{P + 1}{2} = \frac{P - 1 + 2}{2}$
182	91	nncnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℂ$
183	182	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P - 1 \in ℂ$
184	183 173 173 174	divdird	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{P - 1 + 2}{2} = (\frac{P - 1}{2}) + (\frac{2}{2})$
185		2div2e1	$⊢ \frac{2}{2} = 1$
186	185	oveq2i	$⊢ (\frac{P - 1}{2}) + (\frac{2}{2}) = (\frac{P - 1}{2}) + 1$
187	184 186	syl6eq	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{P - 1 + 2}{2} = (\frac{P - 1}{2}) + 1$
188	181 187	eqtrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{P + 1}{2} = (\frac{P - 1}{2}) + 1$
189		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
190	24 189	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{P - 1}{2} \in ℕ$
191	190	nnzd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{P - 1}{2} \in ℤ$
192	191	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{P - 1}{2} \in ℤ$
193	192	peano2zd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to (\frac{P - 1}{2}) + 1 \in ℤ$
194	188 193	eqeltrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{P + 1}{2} \in ℤ$
195		simpr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{R + 1}{2} \in ℤ$
196	194 195	zsubcld	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to (\frac{P + 1}{2}) - (\frac{R + 1}{2}) \in ℤ$
197	176 196	eqeltrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \frac{{(- 1)}^{R} R \mod P}{2} \in ℤ$
198		zeo	$⊢ R \in ℤ \to (\frac{R}{2} \in ℤ \lor \frac{R + 1}{2} \in ℤ)$
199	33 198	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (\frac{R}{2} \in ℤ \lor \frac{R + 1}{2} \in ℤ)$
200	63 197 199	mpjaodan	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{{(- 1)}^{R} R \mod P}{2} \in ℤ$
201		m1expcl	$⊢ R \in ℤ \to {(- 1)}^{R} \in ℤ$
202	33 201	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} \in ℤ$
203	202 33	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \in ℤ$
204	203 27	zmodcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \mod P \in ℕ_{0}$
205	204	nn0red	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \mod P \in ℝ$
206		fzm1ndvds	$⊢ (P \in ℕ \land R \in (1 \dots P - 1)) \to \neg P ∥ R$
207	27 131 206	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg P ∥ R$
208		ax-1ne0	$⊢ 1 \neq 0$
209		divneg2	$⊢ (1 \in ℂ \land 1 \in ℂ \land 1 \neq 0) \to - \frac{1}{1} = \frac{1}{- 1}$
210	140 140 208 209	mp3an	$⊢ - \frac{1}{1} = \frac{1}{- 1}$
211		1div1e1	$⊢ \frac{1}{1} = 1$
212	211	negeqi	$⊢ - \frac{1}{1} = - 1$
213	210 212	eqtr3i	$⊢ \frac{1}{- 1} = - 1$
214	213	oveq1i	$⊢ {(\frac{1}{- 1})}^{R} = {(- 1)}^{R}$
215	6	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - 1 \in ℂ$
216	8	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - 1 \neq 0$
217	215 216 33	exprecd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(\frac{1}{- 1})}^{R} = \frac{1}{{(- 1)}^{R}}$
218	214 217	syl5eqr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} = \frac{1}{{(- 1)}^{R}}$
219	218	oveq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} {(- 1)}^{R} = {(- 1)}^{R} (\frac{1}{{(- 1)}^{R}})$
220	202	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} \in ℂ$
221	215 216 33	expne0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} \neq 0$
222	220 221	recidd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} (\frac{1}{{(- 1)}^{R}}) = 1$
223	219 222	eqtrd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} {(- 1)}^{R} = 1$
224	223	oveq1d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} {(- 1)}^{R} R = 1 R$
225	220 220 34	mulassd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} {(- 1)}^{R} R = {(- 1)}^{R} {(- 1)}^{R} R$
226	34	mulid2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 1 R = R$
227	224 225 226	3eqtr3d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} {(- 1)}^{R} R = R$
228	227	breq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P ∥ {(- 1)}^{R} {(- 1)}^{R} R \leftrightarrow P ∥ R)$
229	207 228	mtbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg P ∥ {(- 1)}^{R} {(- 1)}^{R} R$
230		dvdsmultr2	$⊢ (P \in ℤ \land {(- 1)}^{R} \in ℤ \land {(- 1)}^{R} R \in ℤ) \to (P ∥ {(- 1)}^{R} R \to P ∥ {(- 1)}^{R} {(- 1)}^{R} R)$
231	101 202 203 230	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P ∥ {(- 1)}^{R} R \to P ∥ {(- 1)}^{R} {(- 1)}^{R} R)$
232	229 231	mtod	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg P ∥ {(- 1)}^{R} R$
233		dvdsval3	$⊢ (P \in ℕ \land {(- 1)}^{R} R \in ℤ) \to (P ∥ {(- 1)}^{R} R \leftrightarrow {(- 1)}^{R} R \mod P = 0)$
234	27 203 233	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P ∥ {(- 1)}^{R} R \leftrightarrow {(- 1)}^{R} R \mod P = 0)$
235	232 234	mtbid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg {(- 1)}^{R} R \mod P = 0$
236		elnn0	$⊢ {(- 1)}^{R} R \mod P \in ℕ_{0} \leftrightarrow ({(- 1)}^{R} R \mod P \in ℕ \lor {(- 1)}^{R} R \mod P = 0)$
237	204 236	sylib	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to ({(- 1)}^{R} R \mod P \in ℕ \lor {(- 1)}^{R} R \mod P = 0)$
238	237	ord	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (\neg {(- 1)}^{R} R \mod P \in ℕ \to {(- 1)}^{R} R \mod P = 0)$
239	235 238	mt3d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \mod P \in ℕ$
240	239	nngt0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 0 < {(- 1)}^{R} R \mod P$
241	205 94 240 96	divgt0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 0 < \frac{{(- 1)}^{R} R \mod P}{2}$
242		elnnz	$⊢ \frac{{(- 1)}^{R} R \mod P}{2} \in ℕ \leftrightarrow (\frac{{(- 1)}^{R} R \mod P}{2} \in ℤ \land 0 < \frac{{(- 1)}^{R} R \mod P}{2})$
243	200 241 242	sylanbrc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{{(- 1)}^{R} R \mod P}{2} \in ℕ$
244	243	nnge1d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 1 \leq \frac{{(- 1)}^{R} R \mod P}{2}$
245		zmodfz	$⊢ ({(- 1)}^{R} R \in ℤ \land P \in ℕ) \to {(- 1)}^{R} R \mod P \in (0 \dots P - 1)$
246	203 27 245	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \mod P \in (0 \dots P - 1)$
247		elfzle2	$⊢ {(- 1)}^{R} R \mod P \in (0 \dots P - 1) \to {(- 1)}^{R} R \mod P \leq P - 1$
248	246 247	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \mod P \leq P - 1$
249		lediv1	$⊢ ({(- 1)}^{R} R \mod P \in ℝ \land P - 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to ({(- 1)}^{R} R \mod P \leq P - 1 \leftrightarrow \frac{{(- 1)}^{R} R \mod P}{2} \leq \frac{P - 1}{2})$
250	205 92 94 96 249	syl112anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to ({(- 1)}^{R} R \mod P \leq P - 1 \leftrightarrow \frac{{(- 1)}^{R} R \mod P}{2} \leq \frac{P - 1}{2})$
251	248 250	mpbid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{{(- 1)}^{R} R \mod P}{2} \leq \frac{P - 1}{2}$
252		elfz	$⊢ (\frac{{(- 1)}^{R} R \mod P}{2} \in ℤ \land 1 \in ℤ \land \frac{P - 1}{2} \in ℤ) \to (\frac{{(- 1)}^{R} R \mod P}{2} \in (1 \dots \frac{P - 1}{2}) \leftrightarrow (1 \leq \frac{{(- 1)}^{R} R \mod P}{2} \land \frac{{(- 1)}^{R} R \mod P}{2} \leq \frac{P - 1}{2}))$
253	200 73 191 252	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (\frac{{(- 1)}^{R} R \mod P}{2} \in (1 \dots \frac{P - 1}{2}) \leftrightarrow (1 \leq \frac{{(- 1)}^{R} R \mod P}{2} \land \frac{{(- 1)}^{R} R \mod P}{2} \leq \frac{P - 1}{2}))$
254	244 251 253	mpbir2and	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{{(- 1)}^{R} R \mod P}{2} \in (1 \dots \frac{P - 1}{2})$
255	254 5	fmptd	$⊢ φ \to M : (1 \dots \frac{P - 1}{2}) ⟶ (1 \dots \frac{P - 1}{2})$

Metamath Proof Explorer

Theorem lgseisenlem1

Proof