lgseisenlem2

Description: Lemma for lgseisen . The function M is an injection (and hence a bijection by the pigeonhole principle). (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})$
	lgseisen.6	$⊢ S = Q 2 y \mod P$
Assertion	lgseisenlem2	$⊢ φ \to M : (1 \dots \frac{P - 1}{2}) \underset{1-1 onto}{⟶} (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		lgseisen.6	$⊢ S = Q 2 y \mod P$
7	1 2 3 4 5	lgseisenlem1	$⊢ φ \to M : (1 \dots \frac{P - 1}{2}) ⟶ (1 \dots \frac{P - 1}{2})$
8		oveq2	$⊢ x = y \to 2 x = 2 y$
9	8	oveq2d	$⊢ x = y \to Q 2 x = Q 2 y$
10	9	oveq1d	$⊢ x = y \to Q 2 x \mod P = Q 2 y \mod P$
11	10 4 6	3eqtr4g	$⊢ x = y \to R = S$
12	11	oveq2d	$⊢ x = y \to {(- 1)}^{R} = {(- 1)}^{S}$
13	12 11	oveq12d	$⊢ x = y \to {(- 1)}^{R} R = {(- 1)}^{S} S$
14	13	oveq1d	$⊢ x = y \to {(- 1)}^{R} R \mod P = {(- 1)}^{S} S \mod P$
15	14	oveq1d	$⊢ x = y \to \frac{{(- 1)}^{R} R \mod P}{2} = \frac{{(- 1)}^{S} S \mod P}{2}$
16		ovex	$⊢ \frac{{(- 1)}^{S} S \mod P}{2} \in V$
17	15 5 16	fvmpt	$⊢ y \in (1 \dots \frac{P - 1}{2}) \to M (y) = \frac{{(- 1)}^{S} S \mod P}{2}$
18	17	ad2antrl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to M (y) = \frac{{(- 1)}^{S} S \mod P}{2}$
19		ovex	$⊢ \frac{{(- 1)}^{R} R \mod P}{2} \in V$
20	5	fvmpt2	$⊢ (x \in (1 \dots \frac{P - 1}{2}) \land \frac{{(- 1)}^{R} R \mod P}{2} \in V) \to M (x) = \frac{{(- 1)}^{R} R \mod P}{2}$
21	19 20	mpan2	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to M (x) = \frac{{(- 1)}^{R} R \mod P}{2}$
22	21	ad2antll	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to M (x) = \frac{{(- 1)}^{R} R \mod P}{2}$
23	18 22	eqeq12d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (M (y) = M (x) \leftrightarrow \frac{{(- 1)}^{S} S \mod P}{2} = \frac{{(- 1)}^{R} R \mod P}{2})$
24	2	adantr	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q \in (ℙ ∖ \{2\})$
25	24	eldifad	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q \in ℙ$
26		prmz	$⊢ Q \in ℙ \to Q \in ℤ$
27	25 26	syl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q \in ℤ$
28		2z	$⊢ 2 \in ℤ$
29		elfzelz	$⊢ y \in (1 \dots \frac{P - 1}{2}) \to y \in ℤ$
30	29	ad2antrl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to y \in ℤ$
31		zmulcl	$⊢ (2 \in ℤ \land y \in ℤ) \to 2 y \in ℤ$
32	28 30 31	sylancr	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 y \in ℤ$
33	27 32	zmulcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q 2 y \in ℤ$
34	1	adantr	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P \in (ℙ ∖ \{2\})$
35	34	eldifad	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P \in ℙ$
36		prmnn	$⊢ P \in ℙ \to P \in ℕ$
37	35 36	syl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P \in ℕ$
38	33 37	zmodcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q 2 y \mod P \in ℕ_{0}$
39	6 38	eqeltrid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to S \in ℕ_{0}$
40	39	nn0zd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to S \in ℤ$
41		m1expcl	$⊢ S \in ℤ \to {(- 1)}^{S} \in ℤ$
42	40 41	syl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} \in ℤ$
43	42 40	zmulcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} S \in ℤ$
44	43 37	zmodcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} S \mod P \in ℕ_{0}$
45	44	nn0cnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} S \mod P \in ℂ$
46		elfzelz	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℤ$
47	46	ad2antll	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to x \in ℤ$
48		zmulcl	$⊢ (2 \in ℤ \land x \in ℤ) \to 2 x \in ℤ$
49	28 47 48	sylancr	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 x \in ℤ$
50	27 49	zmulcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q 2 x \in ℤ$
51	50 37	zmodcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q 2 x \mod P \in ℕ_{0}$
52	4 51	eqeltrid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to R \in ℕ_{0}$
53	52	nn0zd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to R \in ℤ$
54		m1expcl	$⊢ R \in ℤ \to {(- 1)}^{R} \in ℤ$
55	53 54	syl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} \in ℤ$
56	55 53	zmulcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} R \in ℤ$
57	56 37	zmodcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} R \mod P \in ℕ_{0}$
58	57	nn0cnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} R \mod P \in ℂ$
59		2cnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 \in ℂ$
60		2ne0	$⊢ 2 \neq 0$
61	60	a1i	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 \neq 0$
62		div11	$⊢ ({(- 1)}^{S} S \mod P \in ℂ \land {(- 1)}^{R} R \mod P \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to (\frac{{(- 1)}^{S} S \mod P}{2} = \frac{{(- 1)}^{R} R \mod P}{2} \leftrightarrow {(- 1)}^{S} S \mod P = {(- 1)}^{R} R \mod P)$
63	45 58 59 61 62	syl112anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (\frac{{(- 1)}^{S} S \mod P}{2} = \frac{{(- 1)}^{R} R \mod P}{2} \leftrightarrow {(- 1)}^{S} S \mod P = {(- 1)}^{R} R \mod P)$
64	37	nnrpd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P \in ℝ^{+}$
65		eqidd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} \mod P = {(- 1)}^{S} \mod P$
66	6	oveq1i	$⊢ S \mod P = (Q 2 y \mod P) \mod P$
67	33	zred	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q 2 y \in ℝ$
68		modabs2	$⊢ (Q 2 y \in ℝ \land P \in ℝ^{+}) \to (Q 2 y \mod P) \mod P = Q 2 y \mod P$
69	67 64 68	syl2anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (Q 2 y \mod P) \mod P = Q 2 y \mod P$
70	66 69	eqtrid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to S \mod P = Q 2 y \mod P$
71	42 42 40 33 64 65 70	modmul12d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} S \mod P = {(- 1)}^{S} Q 2 y \mod P$
72		eqidd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} \mod P = {(- 1)}^{R} \mod P$
73	4	oveq1i	$⊢ R \mod P = (Q 2 x \mod P) \mod P$
74	50	zred	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q 2 x \in ℝ$
75		modabs2	$⊢ (Q 2 x \in ℝ \land P \in ℝ^{+}) \to (Q 2 x \mod P) \mod P = Q 2 x \mod P$
76	74 64 75	syl2anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (Q 2 x \mod P) \mod P = Q 2 x \mod P$
77	73 76	eqtrid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to R \mod P = Q 2 x \mod P$
78	55 55 53 50 64 72 77	modmul12d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} R \mod P = {(- 1)}^{R} Q 2 x \mod P$
79	71 78	eqeq12d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ({(- 1)}^{S} S \mod P = {(- 1)}^{R} R \mod P \leftrightarrow {(- 1)}^{S} Q 2 y \mod P = {(- 1)}^{R} Q 2 x \mod P)$
80	42 33	zmulcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} Q 2 y \in ℤ$
81	55 50	zmulcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} Q 2 x \in ℤ$
82		moddvds	$⊢ (P \in ℕ \land {(- 1)}^{S} Q 2 y \in ℤ \land {(- 1)}^{R} Q 2 x \in ℤ) \to ({(- 1)}^{S} Q 2 y \mod P = {(- 1)}^{R} Q 2 x \mod P \leftrightarrow P ∥ ({(- 1)}^{S} Q 2 y - {(- 1)}^{R} Q 2 x))$
83	37 80 81 82	syl3anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ({(- 1)}^{S} Q 2 y \mod P = {(- 1)}^{R} Q 2 x \mod P \leftrightarrow P ∥ ({(- 1)}^{S} Q 2 y - {(- 1)}^{R} Q 2 x))$
84	27	zcnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q \in ℂ$
85	42 32	zmulcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} 2 y \in ℤ$
86	85	zcnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} 2 y \in ℂ$
87	55 49	zmulcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} 2 x \in ℤ$
88	87	zcnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} 2 x \in ℂ$
89	84 86 88	subdid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) = Q {(- 1)}^{S} 2 y - Q {(- 1)}^{R} 2 x$
90	42	zcnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} \in ℂ$
91	32	zcnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 y \in ℂ$
92	84 90 91	mul12d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q {(- 1)}^{S} 2 y = {(- 1)}^{S} Q 2 y$
93	55	zcnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} \in ℂ$
94	49	zcnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 x \in ℂ$
95	84 93 94	mul12d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q {(- 1)}^{R} 2 x = {(- 1)}^{R} Q 2 x$
96	92 95	oveq12d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q {(- 1)}^{S} 2 y - Q {(- 1)}^{R} 2 x = {(- 1)}^{S} Q 2 y - {(- 1)}^{R} Q 2 x$
97	89 96	eqtrd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to Q ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) = {(- 1)}^{S} Q 2 y - {(- 1)}^{R} Q 2 x$
98	97	breq2d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ Q ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) \leftrightarrow P ∥ ({(- 1)}^{S} Q 2 y - {(- 1)}^{R} Q 2 x))$
99	3	adantr	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P \neq Q$
100		prmrp	$⊢ (P \in ℙ \land Q \in ℙ) \to (P \gcd Q = 1 \leftrightarrow P \neq Q)$
101	35 25 100	syl2anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P \gcd Q = 1 \leftrightarrow P \neq Q)$
102	99 101	mpbird	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P \gcd Q = 1$
103		prmz	$⊢ P \in ℙ \to P \in ℤ$
104	35 103	syl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P \in ℤ$
105	85 87	zsubcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x \in ℤ$
106		coprmdvds	$⊢ (P \in ℤ \land Q \in ℤ \land {(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x \in ℤ) \to ((P ∥ Q ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) \land P \gcd Q = 1) \to P ∥ ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x))$
107	104 27 105 106	syl3anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ((P ∥ Q ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) \land P \gcd Q = 1) \to P ∥ ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x))$
108	102 107	mpan2d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ Q ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) \to P ∥ ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x))$
109		dvdsmultr2	$⊢ (P \in ℤ \land {(- 1)}^{R} \in ℤ \land {(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x \in ℤ) \to (P ∥ ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) \to P ∥ {(- 1)}^{R} ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x))$
110	104 55 105 109	syl3anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) \to P ∥ {(- 1)}^{R} ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x))$
111	93 86 88	subdid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) = {(- 1)}^{R} {(- 1)}^{S} 2 y - {(- 1)}^{R} {(- 1)}^{R} 2 x$
112		neg1cn	$⊢ - 1 \in ℂ$
113	112	a1i	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to - 1 \in ℂ$
114	113 39 52	expaddd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R + S} = {(- 1)}^{R} {(- 1)}^{S}$
115	114	oveq1d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R + S} 2 y = {(- 1)}^{R} {(- 1)}^{S} 2 y$
116	93 90 91	mulassd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} {(- 1)}^{S} 2 y = {(- 1)}^{R} {(- 1)}^{S} 2 y$
117	115 116	eqtr2d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} {(- 1)}^{S} 2 y = {(- 1)}^{R + S} 2 y$
118		ax-1cn	$⊢ 1 \in ℂ$
119		ax-1ne0	$⊢ 1 \neq 0$
120		divneg2	$⊢ (1 \in ℂ \land 1 \in ℂ \land 1 \neq 0) \to - \frac{1}{1} = \frac{1}{- 1}$
121	118 118 119 120	mp3an	$⊢ - \frac{1}{1} = \frac{1}{- 1}$
122		1div1e1	$⊢ \frac{1}{1} = 1$
123	122	negeqi	$⊢ - \frac{1}{1} = - 1$
124	121 123	eqtr3i	$⊢ \frac{1}{- 1} = - 1$
125	124	oveq1i	$⊢ {(\frac{1}{- 1})}^{R} = {(- 1)}^{R}$
126		neg1ne0	$⊢ - 1 \neq 0$
127	126	a1i	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to - 1 \neq 0$
128	113 127 53	exprecd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(\frac{1}{- 1})}^{R} = \frac{1}{{(- 1)}^{R}}$
129	125 128	eqtr3id	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} = \frac{1}{{(- 1)}^{R}}$
130	129	oveq2d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} {(- 1)}^{R} = {(- 1)}^{R} (\frac{1}{{(- 1)}^{R}})$
131	113 127 53	expne0d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} \neq 0$
132	93 131	recidd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} (\frac{1}{{(- 1)}^{R}}) = 1$
133	130 132	eqtrd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} {(- 1)}^{R} = 1$
134	133	oveq1d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} {(- 1)}^{R} 2 x = 1 2 x$
135	93 93 94	mulassd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} {(- 1)}^{R} 2 x = {(- 1)}^{R} {(- 1)}^{R} 2 x$
136	94	mullidd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 1 2 x = 2 x$
137	134 135 136	3eqtr3d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} {(- 1)}^{R} 2 x = 2 x$
138	117 137	oveq12d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} {(- 1)}^{S} 2 y - {(- 1)}^{R} {(- 1)}^{R} 2 x = {(- 1)}^{R + S} 2 y - 2 x$
139	111 138	eqtrd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R} ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) = {(- 1)}^{R + S} 2 y - 2 x$
140	139	breq2d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ {(- 1)}^{R} ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) \leftrightarrow P ∥ ({(- 1)}^{R + S} 2 y - 2 x))$
141		eqcom	$⊢ -1 2 y \mod P = 2 x \mod P \leftrightarrow 2 x \mod P = -1 2 y \mod P$
142	91	mulm1d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to -1 2 y = - 2 y$
143	142	oveq1d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to -1 2 y \mod P = (- 2 y) \mod P$
144	143	eqeq2d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (2 x \mod P = -1 2 y \mod P \leftrightarrow 2 x \mod P = (- 2 y) \mod P)$
145	141 144	bitrid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (-1 2 y \mod P = 2 x \mod P \leftrightarrow 2 x \mod P = (- 2 y) \mod P)$
146	32	znegcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to - 2 y \in ℤ$
147		moddvds	$⊢ (P \in ℕ \land 2 x \in ℤ \land - 2 y \in ℤ) \to (2 x \mod P = (- 2 y) \mod P \leftrightarrow P ∥ (2 x - (- 2 y)))$
148	37 49 146 147	syl3anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (2 x \mod P = (- 2 y) \mod P \leftrightarrow P ∥ (2 x - (- 2 y)))$
149		elfznn	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℕ$
150	149	ad2antll	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to x \in ℕ$
151		elfznn	$⊢ y \in (1 \dots \frac{P - 1}{2}) \to y \in ℕ$
152	151	ad2antrl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to y \in ℕ$
153	150 152	nnaddcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to x + y \in ℕ$
154	150	nnred	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to x \in ℝ$
155	30	zred	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to y \in ℝ$
156		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
157	34 156	syl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to \frac{P - 1}{2} \in ℕ$
158	157	nnred	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to \frac{P - 1}{2} \in ℝ$
159		elfzle2	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \leq \frac{P - 1}{2}$
160	159	ad2antll	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to x \leq \frac{P - 1}{2}$
161		elfzle2	$⊢ y \in (1 \dots \frac{P - 1}{2}) \to y \leq \frac{P - 1}{2}$
162	161	ad2antrl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to y \leq \frac{P - 1}{2}$
163	154 155 158 158 160 162	le2addd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to x + y \leq (\frac{P - 1}{2}) + (\frac{P - 1}{2})$
164	37	nnred	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P \in ℝ$
165		peano2rem	$⊢ P \in ℝ \to P - 1 \in ℝ$
166	164 165	syl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P - 1 \in ℝ$
167	166	recnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P - 1 \in ℂ$
168	167	2halvesd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (\frac{P - 1}{2}) + (\frac{P - 1}{2}) = P - 1$
169	163 168	breqtrd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to x + y \leq P - 1$
170		peano2zm	$⊢ P \in ℤ \to P - 1 \in ℤ$
171		fznn	$⊢ P - 1 \in ℤ \to (x + y \in (1 \dots P - 1) \leftrightarrow (x + y \in ℕ \land x + y \leq P - 1))$
172	104 170 171	3syl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (x + y \in (1 \dots P - 1) \leftrightarrow (x + y \in ℕ \land x + y \leq P - 1))$
173	153 169 172	mpbir2and	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to x + y \in (1 \dots P - 1)$
174		fzm1ndvds	$⊢ (P \in ℕ \land x + y \in (1 \dots P - 1)) \to \neg P ∥ (x + y)$
175	37 173 174	syl2anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to \neg P ∥ (x + y)$
176		eldifsni	$⊢ P \in (ℙ ∖ \{2\}) \to P \neq 2$
177	34 176	syl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P \neq 2$
178		2prm	$⊢ 2 \in ℙ$
179		prmrp	$⊢ (P \in ℙ \land 2 \in ℙ) \to (P \gcd 2 = 1 \leftrightarrow P \neq 2)$
180	35 178 179	sylancl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P \gcd 2 = 1 \leftrightarrow P \neq 2)$
181	177 180	mpbird	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to P \gcd 2 = 1$
182	28	a1i	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 \in ℤ$
183	153	nnzd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to x + y \in ℤ$
184		coprmdvds	$⊢ (P \in ℤ \land 2 \in ℤ \land x + y \in ℤ) \to ((P ∥ 2 (x + y) \land P \gcd 2 = 1) \to P ∥ (x + y))$
185	104 182 183 184	syl3anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ((P ∥ 2 (x + y) \land P \gcd 2 = 1) \to P ∥ (x + y))$
186	181 185	mpan2d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ 2 (x + y) \to P ∥ (x + y))$
187	175 186	mtod	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to \neg P ∥ 2 (x + y)$
188	94 91	subnegd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 x - (- 2 y) = 2 x + 2 y$
189	47	zcnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to x \in ℂ$
190	30	zcnd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to y \in ℂ$
191	59 189 190	adddid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 (x + y) = 2 x + 2 y$
192	188 191	eqtr4d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 x - (- 2 y) = 2 (x + y)$
193	192	breq2d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ (2 x - (- 2 y)) \leftrightarrow P ∥ 2 (x + y))$
194	187 193	mtbird	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to \neg P ∥ (2 x - (- 2 y))$
195	194	pm2.21d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ (2 x - (- 2 y)) \to 2 y = 2 x)$
196	148 195	sylbid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (2 x \mod P = (- 2 y) \mod P \to 2 y = 2 x)$
197	145 196	sylbid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (-1 2 y \mod P = 2 x \mod P \to 2 y = 2 x)$
198		oveq1	$⊢ {(- 1)}^{R + S} = - 1 \to {(- 1)}^{R + S} 2 y = -1 2 y$
199	198	oveq1d	$⊢ {(- 1)}^{R + S} = - 1 \to {(- 1)}^{R + S} 2 y \mod P = -1 2 y \mod P$
200	199	eqeq1d	$⊢ {(- 1)}^{R + S} = - 1 \to ({(- 1)}^{R + S} 2 y \mod P = 2 x \mod P \leftrightarrow -1 2 y \mod P = 2 x \mod P)$
201	200	imbi1d	$⊢ {(- 1)}^{R + S} = - 1 \to (({(- 1)}^{R + S} 2 y \mod P = 2 x \mod P \to 2 y = 2 x) \leftrightarrow (-1 2 y \mod P = 2 x \mod P \to 2 y = 2 x))$
202	197 201	syl5ibrcom	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ({(- 1)}^{R + S} = - 1 \to ({(- 1)}^{R + S} 2 y \mod P = 2 x \mod P \to 2 y = 2 x))$
203	91	mullidd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 1 2 y = 2 y$
204	203	oveq1d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 1 2 y \mod P = 2 y \mod P$
205	32	zred	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 y \in ℝ$
206		2nn	$⊢ 2 \in ℕ$
207		nnmulcl	$⊢ (2 \in ℕ \land y \in ℕ) \to 2 y \in ℕ$
208	206 152 207	sylancr	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 y \in ℕ$
209	208	nnnn0d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 y \in ℕ_{0}$
210	209	nn0ge0d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 0 \leq 2 y$
211		2re	$⊢ 2 \in ℝ$
212	211	a1i	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 \in ℝ$
213		2pos	$⊢ 0 < 2$
214	213	a1i	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 0 < 2$
215		lemuldiv2	$⊢ (y \in ℝ \land P - 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 y \leq P - 1 \leftrightarrow y \leq \frac{P - 1}{2})$
216	155 166 212 214 215	syl112anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (2 y \leq P - 1 \leftrightarrow y \leq \frac{P - 1}{2})$
217	162 216	mpbird	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 y \leq P - 1$
218		zltlem1	$⊢ (2 y \in ℤ \land P \in ℤ) \to (2 y < P \leftrightarrow 2 y \leq P - 1)$
219	32 104 218	syl2anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (2 y < P \leftrightarrow 2 y \leq P - 1)$
220	217 219	mpbird	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 y < P$
221		modid	$⊢ ((2 y \in ℝ \land P \in ℝ^{+}) \land (0 \leq 2 y \land 2 y < P)) \to 2 y \mod P = 2 y$
222	205 64 210 220 221	syl22anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 y \mod P = 2 y$
223	204 222	eqtrd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 1 2 y \mod P = 2 y$
224	49	zred	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 x \in ℝ$
225		nnmulcl	$⊢ (2 \in ℕ \land x \in ℕ) \to 2 x \in ℕ$
226	206 150 225	sylancr	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 x \in ℕ$
227	226	nnnn0d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 x \in ℕ_{0}$
228	227	nn0ge0d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 0 \leq 2 x$
229		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})$
230	154 166 212 214 229	syl112anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (2 x \leq P - 1 \leftrightarrow x \leq \frac{P - 1}{2})$
231	160 230	mpbird	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 x \leq P - 1$
232		zltlem1	$⊢ (2 x \in ℤ \land P \in ℤ) \to (2 x < P \leftrightarrow 2 x \leq P - 1)$
233	49 104 232	syl2anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (2 x < P \leftrightarrow 2 x \leq P - 1)$
234	231 233	mpbird	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 x < P$
235		modid	$⊢ ((2 x \in ℝ \land P \in ℝ^{+}) \land (0 \leq 2 x \land 2 x < P)) \to 2 x \mod P = 2 x$
236	224 64 228 234 235	syl22anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to 2 x \mod P = 2 x$
237	223 236	eqeq12d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (1 2 y \mod P = 2 x \mod P \leftrightarrow 2 y = 2 x)$
238	237	biimpd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (1 2 y \mod P = 2 x \mod P \to 2 y = 2 x)$
239		oveq1	$⊢ {(- 1)}^{R + S} = 1 \to {(- 1)}^{R + S} 2 y = 1 2 y$
240	239	oveq1d	$⊢ {(- 1)}^{R + S} = 1 \to {(- 1)}^{R + S} 2 y \mod P = 1 2 y \mod P$
241	240	eqeq1d	$⊢ {(- 1)}^{R + S} = 1 \to ({(- 1)}^{R + S} 2 y \mod P = 2 x \mod P \leftrightarrow 1 2 y \mod P = 2 x \mod P)$
242	241	imbi1d	$⊢ {(- 1)}^{R + S} = 1 \to (({(- 1)}^{R + S} 2 y \mod P = 2 x \mod P \to 2 y = 2 x) \leftrightarrow (1 2 y \mod P = 2 x \mod P \to 2 y = 2 x))$
243	238 242	syl5ibrcom	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ({(- 1)}^{R + S} = 1 \to ({(- 1)}^{R + S} 2 y \mod P = 2 x \mod P \to 2 y = 2 x))$
244	52 39	nn0addcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to R + S \in ℕ_{0}$
245	244	nn0zd	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to R + S \in ℤ$
246		m1expcl2	$⊢ R + S \in ℤ \to {(- 1)}^{R + S} \in \{- 1, 1\}$
247		elpri	$⊢ {(- 1)}^{R + S} \in \{- 1, 1\} \to ({(- 1)}^{R + S} = - 1 \lor {(- 1)}^{R + S} = 1)$
248	245 246 247	3syl	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ({(- 1)}^{R + S} = - 1 \lor {(- 1)}^{R + S} = 1)$
249	202 243 248	mpjaod	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ({(- 1)}^{R + S} 2 y \mod P = 2 x \mod P \to 2 y = 2 x)$
250		neg1z	$⊢ - 1 \in ℤ$
251		zexpcl	$⊢ (- 1 \in ℤ \land R + S \in ℕ_{0}) \to {(- 1)}^{R + S} \in ℤ$
252	250 244 251	sylancr	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R + S} \in ℤ$
253	252 32	zmulcld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to {(- 1)}^{R + S} 2 y \in ℤ$
254		moddvds	$⊢ (P \in ℕ \land {(- 1)}^{R + S} 2 y \in ℤ \land 2 x \in ℤ) \to ({(- 1)}^{R + S} 2 y \mod P = 2 x \mod P \leftrightarrow P ∥ ({(- 1)}^{R + S} 2 y - 2 x))$
255	37 253 49 254	syl3anc	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ({(- 1)}^{R + S} 2 y \mod P = 2 x \mod P \leftrightarrow P ∥ ({(- 1)}^{R + S} 2 y - 2 x))$
256	190 189 59 61	mulcand	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (2 y = 2 x \leftrightarrow y = x)$
257	249 255 256	3imtr3d	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ ({(- 1)}^{R + S} 2 y - 2 x) \to y = x)$
258	140 257	sylbid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ {(- 1)}^{R} ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) \to y = x)$
259	108 110 258	3syld	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ Q ({(- 1)}^{S} 2 y - {(- 1)}^{R} 2 x) \to y = x)$
260	98 259	sylbird	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ ({(- 1)}^{S} Q 2 y - {(- 1)}^{R} Q 2 x) \to y = x)$
261	83 260	sylbid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ({(- 1)}^{S} Q 2 y \mod P = {(- 1)}^{R} Q 2 x \mod P \to y = x)$
262	79 261	sylbid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to ({(- 1)}^{S} S \mod P = {(- 1)}^{R} R \mod P \to y = x)$
263	63 262	sylbid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (\frac{{(- 1)}^{S} S \mod P}{2} = \frac{{(- 1)}^{R} R \mod P}{2} \to y = x)$
264	23 263	sylbid	$⊢ (φ \land (y \in (1 \dots \frac{P - 1}{2}) \land x \in (1 \dots \frac{P - 1}{2}))) \to (M (y) = M (x) \to y = x)$
265	264	ralrimivva	$⊢ φ \to \forall y \in (1 \dots \frac{P - 1}{2}) \forall x \in (1 \dots \frac{P - 1}{2}) (M (y) = M (x) \to y = x)$
266		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (1 \dots \frac{P - 1}{2}) ⟼ \frac{{(- 1)}^{R} R \mod P}{2})$
267	5 266	nfcxfr	$⊢ \underline{Ⅎ} x M$
268		nfcv	$⊢ \underline{Ⅎ} x y$
269	267 268	nffv	$⊢ \underline{Ⅎ} x M (y)$
270		nfcv	$⊢ \underline{Ⅎ} x z$
271	267 270	nffv	$⊢ \underline{Ⅎ} x M (z)$
272	269 271	nfeq	$⊢ Ⅎ x M (y) = M (z)$
273		nfv	$⊢ Ⅎ x y = z$
274	272 273	nfim	$⊢ Ⅎ x (M (y) = M (z) \to y = z)$
275		nfv	$⊢ Ⅎ z (M (y) = M (x) \to y = x)$
276		fveq2	$⊢ z = x \to M (z) = M (x)$
277	276	eqeq2d	$⊢ z = x \to (M (y) = M (z) \leftrightarrow M (y) = M (x))$
278		equequ2	$⊢ z = x \to (y = z \leftrightarrow y = x)$
279	277 278	imbi12d	$⊢ z = x \to ((M (y) = M (z) \to y = z) \leftrightarrow (M (y) = M (x) \to y = x))$
280	274 275 279	cbvralw	$⊢ \forall z \in (1 \dots \frac{P - 1}{2}) (M (y) = M (z) \to y = z) \leftrightarrow \forall x \in (1 \dots \frac{P - 1}{2}) (M (y) = M (x) \to y = x)$
281	280	ralbii	$⊢ \forall y \in (1 \dots \frac{P - 1}{2}) \forall z \in (1 \dots \frac{P - 1}{2}) (M (y) = M (z) \to y = z) \leftrightarrow \forall y \in (1 \dots \frac{P - 1}{2}) \forall x \in (1 \dots \frac{P - 1}{2}) (M (y) = M (x) \to y = x)$
282	265 281	sylibr	$⊢ φ \to \forall y \in (1 \dots \frac{P - 1}{2}) \forall z \in (1 \dots \frac{P - 1}{2}) (M (y) = M (z) \to y = z)$
283		dff13	$⊢ M : (1 \dots \frac{P - 1}{2}) \underset{1-1}{⟶} (1 \dots \frac{P - 1}{2}) \leftrightarrow (M : (1 \dots \frac{P - 1}{2}) ⟶ (1 \dots \frac{P - 1}{2}) \land \forall y \in (1 \dots \frac{P - 1}{2}) \forall z \in (1 \dots \frac{P - 1}{2}) (M (y) = M (z) \to y = z))$
284	7 282 283	sylanbrc	$⊢ φ \to M : (1 \dots \frac{P - 1}{2}) \underset{1-1}{⟶} (1 \dots \frac{P - 1}{2})$
285		ovex	$⊢ (1 \dots \frac{P - 1}{2}) \in V$
286	285	enref	$⊢ (1 \dots \frac{P - 1}{2}) \approx (1 \dots \frac{P - 1}{2})$
287		fzfi	$⊢ (1 \dots \frac{P - 1}{2}) \in Fin$
288		f1finf1o	$⊢ ((1 \dots \frac{P - 1}{2}) \approx (1 \dots \frac{P - 1}{2}) \land (1 \dots \frac{P - 1}{2}) \in Fin) \to (M : (1 \dots \frac{P - 1}{2}) \underset{1-1}{⟶} (1 \dots \frac{P - 1}{2}) \leftrightarrow M : (1 \dots \frac{P - 1}{2}) \underset{1-1 onto}{⟶} (1 \dots \frac{P - 1}{2}))$
289	286 287 288	mp2an	$⊢ M : (1 \dots \frac{P - 1}{2}) \underset{1-1}{⟶} (1 \dots \frac{P - 1}{2}) \leftrightarrow M : (1 \dots \frac{P - 1}{2}) \underset{1-1 onto}{⟶} (1 \dots \frac{P - 1}{2})$
290	284 289	sylib	$⊢ φ \to M : (1 \dots \frac{P - 1}{2}) \underset{1-1 onto}{⟶} (1 \dots \frac{P - 1}{2})$

Metamath Proof Explorer

Theorem lgseisenlem2

Proof