2lgslem1a

		Ref	Expression
	Assertion	2lgslem1a	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to \{x \in ℤ \| \exists i \in (1 \dots \frac{P - 1}{2}) (x = i \cdot 2 \land \frac{P}{2} < x \mod P)\} = \{x \in ℤ \| \exists i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) x = i \cdot 2\}$

Proof

Step	Hyp	Ref	Expression
1		prmnn	$⊢ P \in ℙ \to P \in ℕ$
2	1	nnnn0d	$⊢ P \in ℙ \to P \in ℕ_{0}$
3	2	ad2antrr	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to P \in ℕ_{0}$
4		4nn	$⊢ 4 \in ℕ$
5	3 4	jctir	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to (P \in ℕ_{0} \land 4 \in ℕ)$
6		fldivnn0	$⊢ (P \in ℕ_{0} \land 4 \in ℕ) \to ⌊\frac{P}{4}⌋ \in ℕ_{0}$
7		nn0p1nn	$⊢ ⌊\frac{P}{4}⌋ \in ℕ_{0} \to ⌊\frac{P}{4}⌋ + 1 \in ℕ$
8	5 6 7	3syl	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to ⌊\frac{P}{4}⌋ + 1 \in ℕ$
9		elnnuz	$⊢ ⌊\frac{P}{4}⌋ + 1 \in ℕ \leftrightarrow ⌊\frac{P}{4}⌋ + 1 \in ℤ_{\geq 1}$
10	8 9	sylib	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to ⌊\frac{P}{4}⌋ + 1 \in ℤ_{\geq 1}$
11		fzss1	$⊢ ⌊\frac{P}{4}⌋ + 1 \in ℤ_{\geq 1} \to (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \subseteq (1 \dots \frac{P - 1}{2})$
12		rexss	$⊢ (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \subseteq (1 \dots \frac{P - 1}{2}) \to (\exists i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) x = i \cdot 2 \leftrightarrow \exists i \in (1 \dots \frac{P - 1}{2}) (i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \land x = i \cdot 2))$
13	10 11 12	3syl	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to (\exists i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) x = i \cdot 2 \leftrightarrow \exists i \in (1 \dots \frac{P - 1}{2}) (i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \land x = i \cdot 2))$
14		ancom	$⊢ (i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \land x = i \cdot 2) \leftrightarrow (x = i \cdot 2 \land i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}))$
15	2 4	jctir	$⊢ P \in ℙ \to (P \in ℕ_{0} \land 4 \in ℕ)$
16	15 6	syl	$⊢ P \in ℙ \to ⌊\frac{P}{4}⌋ \in ℕ_{0}$
17	16	nn0zd	$⊢ P \in ℙ \to ⌊\frac{P}{4}⌋ \in ℤ$
18	17	ad2antrr	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to ⌊\frac{P}{4}⌋ \in ℤ$
19		elfzelz	$⊢ i \in (1 \dots \frac{P - 1}{2}) \to i \in ℤ$
20		zltp1le	$⊢ (⌊\frac{P}{4}⌋ \in ℤ \land i \in ℤ) \to (⌊\frac{P}{4}⌋ < i \leftrightarrow ⌊\frac{P}{4}⌋ + 1 \leq i)$
21	18 19 20	syl2an	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to (⌊\frac{P}{4}⌋ < i \leftrightarrow ⌊\frac{P}{4}⌋ + 1 \leq i)$
22	21	bicomd	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to (⌊\frac{P}{4}⌋ + 1 \leq i \leftrightarrow ⌊\frac{P}{4}⌋ < i)$
23	22	anbi1d	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to ((⌊\frac{P}{4}⌋ + 1 \leq i \land i \leq \frac{P - 1}{2}) \leftrightarrow (⌊\frac{P}{4}⌋ < i \land i \leq \frac{P - 1}{2}))$
24	19	adantl	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to i \in ℤ$
25	17	peano2zd	$⊢ P \in ℙ \to ⌊\frac{P}{4}⌋ + 1 \in ℤ$
26	25	adantr	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to ⌊\frac{P}{4}⌋ + 1 \in ℤ$
27	26	ad2antrr	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to ⌊\frac{P}{4}⌋ + 1 \in ℤ$
28		prmz	$⊢ P \in ℙ \to P \in ℤ$
29		oddm1d2	$⊢ P \in ℤ \to (\neg 2 ∥ P \leftrightarrow \frac{P - 1}{2} \in ℤ)$
30	28 29	syl	$⊢ P \in ℙ \to (\neg 2 ∥ P \leftrightarrow \frac{P - 1}{2} \in ℤ)$
31	30	biimpa	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to \frac{P - 1}{2} \in ℤ$
32	31	ad2antrr	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to \frac{P - 1}{2} \in ℤ$
33		elfz	$⊢ (i \in ℤ \land ⌊\frac{P}{4}⌋ + 1 \in ℤ \land \frac{P - 1}{2} \in ℤ) \to (i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \leftrightarrow (⌊\frac{P}{4}⌋ + 1 \leq i \land i \leq \frac{P - 1}{2}))$
34	24 27 32 33	syl3anc	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to (i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \leftrightarrow (⌊\frac{P}{4}⌋ + 1 \leq i \land i \leq \frac{P - 1}{2}))$
35		elfzle2	$⊢ i \in (1 \dots \frac{P - 1}{2}) \to i \leq \frac{P - 1}{2}$
36	35	adantl	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to i \leq \frac{P - 1}{2}$
37	36	biantrud	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to (⌊\frac{P}{4}⌋ < i \leftrightarrow (⌊\frac{P}{4}⌋ < i \land i \leq \frac{P - 1}{2}))$
38	23 34 37	3bitr4d	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to (i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \leftrightarrow ⌊\frac{P}{4}⌋ < i)$
39	28	ad2antrr	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to P \in ℤ$
40		2lgslem1a2	$⊢ (P \in ℤ \land i \in ℤ) \to (⌊\frac{P}{4}⌋ < i \leftrightarrow \frac{P}{2} < i \cdot 2)$
41	39 19 40	syl2an	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to (⌊\frac{P}{4}⌋ < i \leftrightarrow \frac{P}{2} < i \cdot 2)$
42	38 41	bitrd	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to (i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \leftrightarrow \frac{P}{2} < i \cdot 2)$
43		2lgslem1a1	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to \forall k \in (1 \dots \frac{P - 1}{2}) k \cdot 2 = k \cdot 2 \mod P$
44	1 43	sylan	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to \forall k \in (1 \dots \frac{P - 1}{2}) k \cdot 2 = k \cdot 2 \mod P$
45	44	adantr	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to \forall k \in (1 \dots \frac{P - 1}{2}) k \cdot 2 = k \cdot 2 \mod P$
46		oveq1	$⊢ k = i \to k \cdot 2 = i \cdot 2$
47	46	oveq1d	$⊢ k = i \to k \cdot 2 \mod P = i \cdot 2 \mod P$
48	46 47	eqeq12d	$⊢ k = i \to (k \cdot 2 = k \cdot 2 \mod P \leftrightarrow i \cdot 2 = i \cdot 2 \mod P)$
49	48	rspccva	$⊢ (\forall k \in (1 \dots \frac{P - 1}{2}) k \cdot 2 = k \cdot 2 \mod P \land i \in (1 \dots \frac{P - 1}{2})) \to i \cdot 2 = i \cdot 2 \mod P$
50	45 49	sylan	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to i \cdot 2 = i \cdot 2 \mod P$
51	50	breq2d	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to (\frac{P}{2} < i \cdot 2 \leftrightarrow \frac{P}{2} < i \cdot 2 \mod P)$
52	42 51	bitrd	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to (i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \leftrightarrow \frac{P}{2} < i \cdot 2 \mod P)$
53		oveq1	$⊢ x = i \cdot 2 \to x \mod P = i \cdot 2 \mod P$
54	53	eqcomd	$⊢ x = i \cdot 2 \to i \cdot 2 \mod P = x \mod P$
55	54	breq2d	$⊢ x = i \cdot 2 \to (\frac{P}{2} < i \cdot 2 \mod P \leftrightarrow \frac{P}{2} < x \mod P)$
56	52 55	sylan9bb	$⊢ ((((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \land x = i \cdot 2) \to (i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \leftrightarrow \frac{P}{2} < x \mod P)$
57	56	pm5.32da	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to ((x = i \cdot 2 \land i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2})) \leftrightarrow (x = i \cdot 2 \land \frac{P}{2} < x \mod P))$
58	14 57	bitrid	$⊢ (((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \land i \in (1 \dots \frac{P - 1}{2})) \to ((i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \land x = i \cdot 2) \leftrightarrow (x = i \cdot 2 \land \frac{P}{2} < x \mod P))$
59	58	rexbidva	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to (\exists i \in (1 \dots \frac{P - 1}{2}) (i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) \land x = i \cdot 2) \leftrightarrow \exists i \in (1 \dots \frac{P - 1}{2}) (x = i \cdot 2 \land \frac{P}{2} < x \mod P))$
60	13 59	bitrd	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to (\exists i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) x = i \cdot 2 \leftrightarrow \exists i \in (1 \dots \frac{P - 1}{2}) (x = i \cdot 2 \land \frac{P}{2} < x \mod P))$
61	60	bicomd	$⊢ ((P \in ℙ \land \neg 2 ∥ P) \land x \in ℤ) \to (\exists i \in (1 \dots \frac{P - 1}{2}) (x = i \cdot 2 \land \frac{P}{2} < x \mod P) \leftrightarrow \exists i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) x = i \cdot 2)$
62	61	rabbidva	$⊢ (P \in ℙ \land \neg 2 ∥ P) \to \{x \in ℤ \| \exists i \in (1 \dots \frac{P - 1}{2}) (x = i \cdot 2 \land \frac{P}{2} < x \mod P)\} = \{x \in ℤ \| \exists i \in (⌊\frac{P}{4}⌋ + 1 \dots \frac{P - 1}{2}) x = i \cdot 2\}$

Metamath Proof Explorer

Theorem 2lgslem1a

Proof