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		1zzd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 1 \in ℤ$
7	1	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in (ℙ ∖ \{2\})$
8		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
9	7 8	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{P - 1}{2} \in ℕ$
10	9	nnzd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{P - 1}{2} \in ℤ$
11		neg1cn	$⊢ - 1 \in ℂ$
12	11	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to - 1 \in ℂ$
13		neg1ne0	$⊢ - 1 \neq 0$
14	13	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to - 1 \neq 0$
15		2z	$⊢ 2 \in ℤ$
16	15	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 2 \in ℤ$
17		simpr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to \frac{R}{2} \in ℤ$
18		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}}$
19	12 14 16 17 18	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}}$
20	2	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in (ℙ ∖ \{2\})$
21	20	eldifad	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in ℙ$
22		prmz	$⊢ Q \in ℙ \to Q \in ℤ$
23	21 22	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q \in ℤ$
24		elfzelz	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℤ$
25	24	adantl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \in ℤ$
26		zmulcl	$⊢ (2 \in ℤ \land x \in ℤ) \to 2 x \in ℤ$
27	15 25 26	sylancr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℤ$
28	23 27	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \in ℤ$
29	7	eldifad	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℙ$
30		prmnn	$⊢ P \in ℙ \to P \in ℕ$
31	29 30	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℕ$
32		zmodfz	$⊢ (Q 2 x \in ℤ \land P \in ℕ) \to Q 2 x \mod P \in (0 \dots P - 1)$
33	28 31 32	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \mod P \in (0 \dots P - 1)$
34	4 33	eqeltrid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in (0 \dots P - 1)$
35		elfznn0	$⊢ R \in (0 \dots P - 1) \to R \in ℕ_{0}$
36	34 35	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℕ_{0}$
37	36	nn0zd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℤ$
38	37	zcnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℂ$
39	38	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to R \in ℂ$
40		2cnd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 2 \in ℂ$
41		2ne0	$⊢ 2 \neq 0$
42	41	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 2 \neq 0$
43	39 40 42	divcan2d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 2 (\frac{R}{2}) = R$
44	43	oveq2d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{2 (\frac{R}{2})} = {(- 1)}^{R}$
45		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
46	45	oveq1i	$⊢ {({-1}^{2})}^{\frac{R}{2}} = 1^{\frac{R}{2}}$
47		1exp	$⊢ \frac{R}{2} \in ℤ \to 1^{\frac{R}{2}} = 1$
48	47	adantl	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 1^{\frac{R}{2}} = 1$
49	46 48	eqtrid	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {({-1}^{2})}^{\frac{R}{2}} = 1$
50	19 44 49	3eqtr3d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{R} = 1$
51	50	oveq1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{R} R = 1 R$
52	39	mulid2d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to 1 R = R$
53	51 52	eqtrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{R} R = R$
54	53	oveq1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{R} R \mod P = R \mod P$
55	36	nn0red	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℝ$
56	31	nnrpd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℝ^{+}$
57	36	nn0ge0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 0 \leq R$
58	28	zred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \in ℝ$
59		modlt	$⊢ (Q 2 x \in ℝ \land P \in ℝ^{+}) \to Q 2 x \mod P < P$
60	58 56 59	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to Q 2 x \mod P < P$
61	4 60	eqbrtrid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R < P$
62		modid	$⊢ ((R \in ℝ \land P \in ℝ^{+}) \land (0 \leq R \land R < P)) \to R \mod P = R$
63	55 56 57 61 62	syl22anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \mod P = R$
64	63	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to R \mod P = R$
65	54 64	eqtrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to {(- 1)}^{R} R \mod P = R$
66	65	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}$
67	66 17	eqeltrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R}{2} \in ℤ) \to \frac{{(- 1)}^{R} R \mod P}{2} \in ℤ$
68	31	nncnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℂ$
69	68	mulid2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 1 P = P$
70	69	oveq2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - R + 1 P = - R + P$
71	55	renegcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - R \in ℝ$
72	71	recnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - R \in ℂ$
73	68 72	addcomd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P + (- R) = - R + P$
74	68 38	negsubd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P + (- R) = P - R$
75	70 73 74	3eqtr2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - R + 1 P = P - R$
76	75	oveq1d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (- R + 1 P) \mod P = (P - R) \mod P$
77		modcyc	$⊢ (- R \in ℝ \land P \in ℝ^{+} \land 1 \in ℤ) \to (- R + 1 P) \mod P = (- R) \mod P$
78	71 56 6 77	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (- R + 1 P) \mod P = (- R) \mod P$
79	31	nnred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℝ$
80	79 55	resubcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - R \in ℝ$
81	55 79 61	ltled	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \leq P$
82	79 55	subge0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (0 \leq P - R \leftrightarrow R \leq P)$
83	81 82	mpbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 0 \leq P - R$
84		2nn	$⊢ 2 \in ℕ$
85		elfznn	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℕ$
86	85	adantl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \in ℕ$
87		nnmulcl	$⊢ (2 \in ℕ \land x \in ℕ) \to 2 x \in ℕ$
88	84 86 87	sylancr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in ℕ$
89		elfzle2	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \leq \frac{P - 1}{2}$
90	89	adantl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \leq \frac{P - 1}{2}$
91	86	nnred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to x \in ℝ$
92		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
93		uz2m1nn	$⊢ P \in ℤ_{\geq 2} \to P - 1 \in ℕ$
94	29 92 93	3syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℕ$
95	94	nnred	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℝ$
96		2re	$⊢ 2 \in ℝ$
97	96	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 \in ℝ$
98		2pos	$⊢ 0 < 2$
99	98	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 0 < 2$
100		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})$
101	91 95 97 99 100	syl112anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (2 x \leq P - 1 \leftrightarrow x \leq \frac{P - 1}{2})$
102	90 101	mpbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \leq P - 1$
103		prmz	$⊢ P \in ℙ \to P \in ℤ$
104	29 103	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \in ℤ$
105		peano2zm	$⊢ P \in ℤ \to P - 1 \in ℤ$
106		fznn	$⊢ P - 1 \in ℤ \to (2 x \in (1 \dots P - 1) \leftrightarrow (2 x \in ℕ \land 2 x \leq P - 1))$
107	104 105 106	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))$
108	88 102 107	mpbir2and	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to 2 x \in (1 \dots P - 1)$
109		fzm1ndvds	$⊢ (P \in ℕ \land 2 x \in (1 \dots P - 1)) \to \neg P ∥ 2 x$
110	31 108 109	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg P ∥ 2 x$
111	3	adantr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \neq Q$
112		prmrp	$⊢ (P \in ℙ \land Q \in ℙ) \to (P \gcd Q = 1 \leftrightarrow P \neq Q)$
113	29 21 112	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P \gcd Q = 1 \leftrightarrow P \neq Q)$
114	111 113	mpbird	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P \gcd Q = 1$
115		coprmdvds	$⊢ (P \in ℤ \land Q \in ℤ \land 2 x \in ℤ) \to ((P ∥ Q 2 x \land P \gcd Q = 1) \to P ∥ 2 x)$
116	104 23 27 115	syl3anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to ((P ∥ Q 2 x \land P \gcd Q = 1) \to P ∥ 2 x)$
117	114 116	mpan2d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P ∥ Q 2 x \to P ∥ 2 x)$
118	110 117	mtod	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg P ∥ Q 2 x$
119		dvdsval3	$⊢ (P \in ℕ \land Q 2 x \in ℤ) \to (P ∥ Q 2 x \leftrightarrow Q 2 x \mod P = 0)$
120	31 28 119	syl2anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P ∥ Q 2 x \leftrightarrow Q 2 x \mod P = 0)$
121	118 120	mtbid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg Q 2 x \mod P = 0$
122	4	eqeq1i	$⊢ R = 0 \leftrightarrow Q 2 x \mod P = 0$
123	121 122	sylnibr	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \neg R = 0$
124	94	nnnn0d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℕ_{0}$
125		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
126	124 125	eleqtrdi	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℤ_{\geq 0}$
127		elfzp12	$⊢ P - 1 \in ℤ_{\geq 0} \to (R \in (0 \dots P - 1) \leftrightarrow (R = 0 \lor R \in (0 + 1 \dots P - 1)))$
128	126 127	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)))$
129	34 128	mpbid	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (R = 0 \lor R \in (0 + 1 \dots P - 1))$
130	129	ord	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (\neg R = 0 \to R \in (0 + 1 \dots P - 1))$
131	123 130	mpd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in (0 + 1 \dots P - 1)$
132		1e0p1	$⊢ 1 = 0 + 1$
133	132	oveq1i	$⊢ (1 \dots P - 1) = (0 + 1 \dots P - 1)$
134	131 133	eleqtrrdi	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in (1 \dots P - 1)$
135		elfznn	$⊢ R \in (1 \dots P - 1) \to R \in ℕ$
136	134 135	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℕ$
137	136	nnrpd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R \in ℝ^{+}$
138	79 137	ltsubrpd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - R < P$
139		modid	$⊢ ((P - R \in ℝ \land P \in ℝ^{+}) \land (0 \leq P - R \land P - R < P)) \to (P - R) \mod P = P - R$
140	80 56 83 138 139	syl22anc	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (P - R) \mod P = P - R$
141	76 78 140	3eqtr3d	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (- R) \mod P = P - R$
142	141	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to (- R) \mod P = P - R$
143		ax-1cn	$⊢ 1 \in ℂ$
144	143	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 1 \in ℂ$
145	136	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to R \in ℕ$
146	37	peano2zd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to R + 1 \in ℤ$
147		dvdsval2	$⊢ (2 \in ℤ \land 2 \neq 0 \land R + 1 \in ℤ) \to (2 ∥ (R + 1) \leftrightarrow \frac{R + 1}{2} \in ℤ)$
148	15 41 146 147	mp3an12i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (2 ∥ (R + 1) \leftrightarrow \frac{R + 1}{2} \in ℤ)$
149	148	biimpar	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 2 ∥ (R + 1)$
150	37	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to R \in ℤ$
151	84	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 2 \in ℕ$
152		1lt2	$⊢ 1 < 2$
153	152	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 1 < 2$
154		ndvdsp1	$⊢ (R \in ℤ \land 2 \in ℕ \land 1 < 2) \to (2 ∥ R \to \neg 2 ∥ (R + 1))$
155	150 151 153 154	syl3anc	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to (2 ∥ R \to \neg 2 ∥ (R + 1))$
156	149 155	mt2d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to \neg 2 ∥ R$
157		oexpneg	$⊢ (1 \in ℂ \land R \in ℕ \land \neg 2 ∥ R) \to {(- 1)}^{R} = - 1^{R}$
158	144 145 156 157	syl3anc	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to {(- 1)}^{R} = - 1^{R}$
159		1exp	$⊢ R \in ℤ \to 1^{R} = 1$
160	150 159	syl	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 1^{R} = 1$
161	160	negeqd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to - 1^{R} = - 1$
162	158 161	eqtrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to {(- 1)}^{R} = - 1$
163	162	oveq1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to {(- 1)}^{R} R = -1 R$
164	38	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to R \in ℂ$
165	164	mulm1d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to -1 R = - R$
166	163 165	eqtrd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to {(- 1)}^{R} R = - R$
167	166	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$
168	68	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P \in ℂ$
169	168 164 144	pnpcan2d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P + 1 - (R + 1) = P - R$
170	142 167 169	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)$
171	170	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}$
172		peano2cn	$⊢ P \in ℂ \to P + 1 \in ℂ$
173	168 172	syl	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P + 1 \in ℂ$
174		peano2cn	$⊢ R \in ℂ \to R + 1 \in ℂ$
175	164 174	syl	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to R + 1 \in ℂ$
176		2cnd	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 2 \in ℂ$
177	41	a1i	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to 2 \neq 0$
178	173 175 176 177	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})$
179	171 178	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})$
180	168 144 176	subadd23d	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P - 1 + 2 = P + 2 - 1$
181		2m1e1	$⊢ 2 - 1 = 1$
182	181	oveq2i	$⊢ P + 2 - 1 = P + 1$
183	180 182	eqtr2di	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P + 1 = P - 1 + 2$
184	183	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}$
185	94	nncnd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to P - 1 \in ℂ$
186	185	adantr	$⊢ ((φ \land x \in (1 \dots \frac{P - 1}{2})) \land \frac{R + 1}{2} \in ℤ) \to P - 1 \in ℂ$
187	186 176 176 177	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})$
188		2div2e1	$⊢ \frac{2}{2} = 1$
189	188	oveq2i	$⊢ (\frac{P - 1}{2}) + (\frac{2}{2}) = (\frac{P - 1}{2}) + 1$
190	187 189	eqtrdi	$⊢ ((φ \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$
191	184 190	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$
192	10	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	191 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	179 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	37 198	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to (\frac{R}{2} \in ℤ \lor \frac{R + 1}{2} \in ℤ)$
200	67 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	37 201	syl	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} \in ℤ$
203	202 37	zmulcld	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} R \in ℤ$
204	203 31	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	31 134 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	143 143 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	11	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - 1 \in ℂ$
216	13	a1i	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to - 1 \neq 0$
217	215 216 37	exprecd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(\frac{1}{- 1})}^{R} = \frac{1}{{(- 1)}^{R}}$
218	214 217	eqtr3id	$⊢ (φ \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 37	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 38	mulassd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to {(- 1)}^{R} {(- 1)}^{R} R = {(- 1)}^{R} {(- 1)}^{R} R$
226	38	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	104 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	31 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 97 240 99	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 31 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 95 97 99 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	6 10 200 244 251	elfzd	$⊢ (φ \land x \in (1 \dots \frac{P - 1}{2})) \to \frac{{(- 1)}^{R} R \mod P}{2} \in (1 \dots \frac{P - 1}{2})$
253	252 5	fmptd	$⊢ φ \to M : (1 \dots \frac{P - 1}{2}) ⟶ (1 \dots \frac{P - 1}{2})$

Metamath Proof Explorer

Theorem lgseisenlem1

Proof