2lgslem1a1

		Ref	Expression
	Assertion	2lgslem1a1	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to \forall i \in (1 \dots \frac{P - 1}{2}) i \cdot 2 = i \cdot 2 \mod P$

Proof

Step	Hyp	Ref	Expression
1		nnrp	$⊢ P \in ℕ \to P \in ℝ^{+}$
2	1	adantr	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to P \in ℝ^{+}$
3		elfzelz	$⊢ i \in (1 \dots \frac{P - 1}{2}) \to i \in ℤ$
4		zre	$⊢ i \in ℤ \to i \in ℝ$
5		2re	$⊢ 2 \in ℝ$
6	5	a1i	$⊢ i \in ℤ \to 2 \in ℝ$
7	4 6	remulcld	$⊢ i \in ℤ \to i \cdot 2 \in ℝ$
8	3 7	syl	$⊢ i \in (1 \dots \frac{P - 1}{2}) \to i \cdot 2 \in ℝ$
9	2 8	anim12ci	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land i \in (1 \dots \frac{P - 1}{2})) \to (i \cdot 2 \in ℝ \land P \in ℝ^{+})$
10		elfznn	$⊢ i \in (1 \dots \frac{P - 1}{2}) \to i \in ℕ$
11		nnre	$⊢ i \in ℕ \to i \in ℝ$
12		nnnn0	$⊢ i \in ℕ \to i \in ℕ_{0}$
13	12	nn0ge0d	$⊢ i \in ℕ \to 0 \leq i$
14		0le2	$⊢ 0 \leq 2$
15	5 14	pm3.2i	$⊢ (2 \in ℝ \land 0 \leq 2)$
16	15	a1i	$⊢ i \in ℕ \to (2 \in ℝ \land 0 \leq 2)$
17		mulge0	$⊢ ((i \in ℝ \land 0 \leq i) \land (2 \in ℝ \land 0 \leq 2)) \to 0 \leq i \cdot 2$
18	11 13 16 17	syl21anc	$⊢ i \in ℕ \to 0 \leq i \cdot 2$
19	10 18	syl	$⊢ i \in (1 \dots \frac{P - 1}{2}) \to 0 \leq i \cdot 2$
20	19	adantl	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land i \in (1 \dots \frac{P - 1}{2})) \to 0 \leq i \cdot 2$
21		elfz2	$⊢ i \in (1 \dots \frac{P - 1}{2}) \leftrightarrow ((1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \land (1 \leq i \land i \leq \frac{P - 1}{2}))$
22	4	3ad2ant3	$⊢ (1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \to i \in ℝ$
23		zre	$⊢ \frac{P - 1}{2} \in ℤ \to \frac{P - 1}{2} \in ℝ$
24	23	3ad2ant2	$⊢ (1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \to \frac{P - 1}{2} \in ℝ$
25		2pos	$⊢ 0 < 2$
26	5 25	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
27	26	a1i	$⊢ (1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \to (2 \in ℝ \land 0 < 2)$
28		lemul1	$⊢ (i \in ℝ \land \frac{P - 1}{2} \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (i \leq \frac{P - 1}{2} \leftrightarrow i \cdot 2 \leq (\frac{P - 1}{2}) \cdot 2)$
29	22 24 27 28	syl3anc	$⊢ (1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \to (i \leq \frac{P - 1}{2} \leftrightarrow i \cdot 2 \leq (\frac{P - 1}{2}) \cdot 2)$
30		nncn	$⊢ P \in ℕ \to P \in ℂ$
31		peano2cnm	$⊢ P \in ℂ \to P - 1 \in ℂ$
32	30 31	syl	$⊢ P \in ℕ \to P - 1 \in ℂ$
33		2cnd	$⊢ P \in ℕ \to 2 \in ℂ$
34		2ne0	$⊢ 2 \neq 0$
35	34	a1i	$⊢ P \in ℕ \to 2 \neq 0$
36	32 33 35	divcan1d	$⊢ P \in ℕ \to (\frac{P - 1}{2}) \cdot 2 = P - 1$
37	36	adantr	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to (\frac{P - 1}{2}) \cdot 2 = P - 1$
38	37	adantl	$⊢ ((1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \land (P \in ℕ \land \neg 2 ∥ P)) \to (\frac{P - 1}{2}) \cdot 2 = P - 1$
39	38	breq2d	$⊢ ((1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \land (P \in ℕ \land \neg 2 ∥ P)) \to (i \cdot 2 \leq (\frac{P - 1}{2}) \cdot 2 \leftrightarrow i \cdot 2 \leq P - 1)$
40		id	$⊢ i \in ℤ \to i \in ℤ$
41		2z	$⊢ 2 \in ℤ$
42	41	a1i	$⊢ i \in ℤ \to 2 \in ℤ$
43	40 42	zmulcld	$⊢ i \in ℤ \to i \cdot 2 \in ℤ$
44	43	3ad2ant3	$⊢ (1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \to i \cdot 2 \in ℤ$
45		nnz	$⊢ P \in ℕ \to P \in ℤ$
46	45	adantr	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to P \in ℤ$
47		zltlem1	$⊢ (i \cdot 2 \in ℤ \land P \in ℤ) \to (i \cdot 2 < P \leftrightarrow i \cdot 2 \leq P - 1)$
48	44 46 47	syl2an	$⊢ ((1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \land (P \in ℕ \land \neg 2 ∥ P)) \to (i \cdot 2 < P \leftrightarrow i \cdot 2 \leq P - 1)$
49	48	biimprd	$⊢ ((1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \land (P \in ℕ \land \neg 2 ∥ P)) \to (i \cdot 2 \leq P - 1 \to i \cdot 2 < P)$
50	39 49	sylbid	$⊢ ((1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \land (P \in ℕ \land \neg 2 ∥ P)) \to (i \cdot 2 \leq (\frac{P - 1}{2}) \cdot 2 \to i \cdot 2 < P)$
51	50	ex	$⊢ (1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \to ((P \in ℕ \land \neg 2 ∥ P) \to (i \cdot 2 \leq (\frac{P - 1}{2}) \cdot 2 \to i \cdot 2 < P))$
52	51	com23	$⊢ (1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \to (i \cdot 2 \leq (\frac{P - 1}{2}) \cdot 2 \to ((P \in ℕ \land \neg 2 ∥ P) \to i \cdot 2 < P))$
53	29 52	sylbid	$⊢ (1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \to (i \leq \frac{P - 1}{2} \to ((P \in ℕ \land \neg 2 ∥ P) \to i \cdot 2 < P))$
54	53	a1d	$⊢ (1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \to (1 \leq i \to (i \leq \frac{P - 1}{2} \to ((P \in ℕ \land \neg 2 ∥ P) \to i \cdot 2 < P)))$
55	54	imp32	$⊢ ((1 \in ℤ \land \frac{P - 1}{2} \in ℤ \land i \in ℤ) \land (1 \leq i \land i \leq \frac{P - 1}{2})) \to ((P \in ℕ \land \neg 2 ∥ P) \to i \cdot 2 < P)$
56	21 55	sylbi	$⊢ i \in (1 \dots \frac{P - 1}{2}) \to ((P \in ℕ \land \neg 2 ∥ P) \to i \cdot 2 < P)$
57	56	impcom	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land i \in (1 \dots \frac{P - 1}{2})) \to i \cdot 2 < P$
58		modid	$⊢ ((i \cdot 2 \in ℝ \land P \in ℝ^{+}) \land (0 \leq i \cdot 2 \land i \cdot 2 < P)) \to i \cdot 2 \mod P = i \cdot 2$
59	9 20 57 58	syl12anc	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land i \in (1 \dots \frac{P - 1}{2})) \to i \cdot 2 \mod P = i \cdot 2$
60	59	eqcomd	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land i \in (1 \dots \frac{P - 1}{2})) \to i \cdot 2 = i \cdot 2 \mod P$
61	60	ralrimiva	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to \forall i \in (1 \dots \frac{P - 1}{2}) i \cdot 2 = i \cdot 2 \mod P$

Metamath Proof Explorer

Theorem 2lgslem1a1

Proof