gausslemma2dlem0i

Description: Auxiliary lemma 9 for gausslemma2d . (Contributed by AV, 14-Jul-2021)

	Ref	Expression
Hypotheses	gausslemma2dlem0.p	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	gausslemma2dlem0.m	$⊢ M = ⌊\frac{P}{4}⌋$
	gausslemma2dlem0.h	$⊢ H = \frac{P - 1}{2}$
	gausslemma2dlem0.n	$⊢ N = H - M$
Assertion	gausslemma2dlem0i	$⊢ φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N})$

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0.p	$⊢ φ \to P \in (ℙ ∖ \{2\})$
2		gausslemma2dlem0.m	$⊢ M = ⌊\frac{P}{4}⌋$
3		gausslemma2dlem0.h	$⊢ H = \frac{P - 1}{2}$
4		gausslemma2dlem0.n	$⊢ N = H - M$
5		2z	$⊢ 2 \in ℤ$
6		id	$⊢ P \in (ℙ ∖ \{2\}) \to P \in (ℙ ∖ \{2\})$
7	6	gausslemma2dlem0a	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℕ$
8	7	nnzd	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ$
9	1 8	syl	$⊢ φ \to P \in ℤ$
10		lgscl1	$⊢ (2 \in ℤ \land P \in ℤ) \to 2 /_{L} P \in \{- 1, 0, 1\}$
11	5 9 10	sylancr	$⊢ φ \to 2 /_{L} P \in \{- 1, 0, 1\}$
12		ovex	$⊢ 2 /_{L} P \in V$
13	12	eltp	$⊢ 2 /_{L} P \in \{- 1, 0, 1\} \leftrightarrow (2 /_{L} P = - 1 \lor 2 /_{L} P = 0 \lor 2 /_{L} P = 1)$
14	1 2 3 4	gausslemma2dlem0h	$⊢ φ \to N \in ℕ_{0}$
15	14	nn0zd	$⊢ φ \to N \in ℤ$
16		m1expcl2	$⊢ N \in ℤ \to {(- 1)}^{N} \in \{- 1, 1\}$
17	15 16	syl	$⊢ φ \to {(- 1)}^{N} \in \{- 1, 1\}$
18		ovex	$⊢ {(- 1)}^{N} \in V$
19	18	elpr	$⊢ {(- 1)}^{N} \in \{- 1, 1\} \leftrightarrow ({(- 1)}^{N} = - 1 \lor {(- 1)}^{N} = 1)$
20		eqcom	$⊢ {(- 1)}^{N} = - 1 \leftrightarrow - 1 = {(- 1)}^{N}$
21	20	biimpi	$⊢ {(- 1)}^{N} = - 1 \to - 1 = {(- 1)}^{N}$
22	21	2a1d	$⊢ {(- 1)}^{N} = - 1 \to (φ \to (-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N}))$
23		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
24		prmnn	$⊢ P \in ℙ \to P \in ℕ$
25	24	nnred	$⊢ P \in ℙ \to P \in ℝ$
26		prmgt1	$⊢ P \in ℙ \to 1 < P$
27	25 26	jca	$⊢ P \in ℙ \to (P \in ℝ \land 1 < P)$
28	23 27	syl	$⊢ P \in (ℙ ∖ \{2\}) \to (P \in ℝ \land 1 < P)$
29		1mod	$⊢ (P \in ℝ \land 1 < P) \to 1 \mod P = 1$
30	1 28 29	3syl	$⊢ φ \to 1 \mod P = 1$
31	30	eqeq2d	$⊢ φ \to (-1 \mod P = 1 \mod P \leftrightarrow -1 \mod P = 1)$
32		oddprmge3	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ_{\geq 3}$
33		m1modge3gt1	$⊢ P \in ℤ_{\geq 3} \to 1 < -1 \mod P$
34		breq2	$⊢ -1 \mod P = 1 \to (1 < -1 \mod P \leftrightarrow 1 < 1)$
35		1re	$⊢ 1 \in ℝ$
36	35	ltnri	$⊢ \neg 1 < 1$
37	36	pm2.21i	$⊢ 1 < 1 \to - 1 = 1$
38	34 37	syl6bi	$⊢ -1 \mod P = 1 \to (1 < -1 \mod P \to - 1 = 1)$
39	33 38	syl5com	$⊢ P \in ℤ_{\geq 3} \to (-1 \mod P = 1 \to - 1 = 1)$
40	1 32 39	3syl	$⊢ φ \to (-1 \mod P = 1 \to - 1 = 1)$
41	31 40	sylbid	$⊢ φ \to (-1 \mod P = 1 \mod P \to - 1 = 1)$
42		oveq1	$⊢ {(- 1)}^{N} = 1 \to {(- 1)}^{N} \mod P = 1 \mod P$
43	42	eqeq2d	$⊢ {(- 1)}^{N} = 1 \to (-1 \mod P = {(- 1)}^{N} \mod P \leftrightarrow -1 \mod P = 1 \mod P)$
44		eqeq2	$⊢ {(- 1)}^{N} = 1 \to (- 1 = {(- 1)}^{N} \leftrightarrow - 1 = 1)$
45	43 44	imbi12d	$⊢ {(- 1)}^{N} = 1 \to ((-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N}) \leftrightarrow (-1 \mod P = 1 \mod P \to - 1 = 1))$
46	41 45	syl5ibr	$⊢ {(- 1)}^{N} = 1 \to (φ \to (-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N}))$
47	22 46	jaoi	$⊢ ({(- 1)}^{N} = - 1 \lor {(- 1)}^{N} = 1) \to (φ \to (-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N}))$
48	19 47	sylbi	$⊢ {(- 1)}^{N} \in \{- 1, 1\} \to (φ \to (-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N}))$
49	17 48	mpcom	$⊢ φ \to (-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N})$
50		oveq1	$⊢ 2 /_{L} P = - 1 \to (2 /_{L} P) \mod P = -1 \mod P$
51	50	eqeq1d	$⊢ 2 /_{L} P = - 1 \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \leftrightarrow -1 \mod P = {(- 1)}^{N} \mod P)$
52		eqeq1	$⊢ 2 /_{L} P = - 1 \to (2 /_{L} P = {(- 1)}^{N} \leftrightarrow - 1 = {(- 1)}^{N})$
53	51 52	imbi12d	$⊢ 2 /_{L} P = - 1 \to (((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}) \leftrightarrow (-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N}))$
54	49 53	syl5ibr	$⊢ 2 /_{L} P = - 1 \to (φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}))$
55	1	gausslemma2dlem0a	$⊢ φ \to P \in ℕ$
56	55	nnrpd	$⊢ φ \to P \in ℝ^{+}$
57		0mod	$⊢ P \in ℝ^{+} \to 0 \mod P = 0$
58	56 57	syl	$⊢ φ \to 0 \mod P = 0$
59	58	eqeq1d	$⊢ φ \to (0 \mod P = {(- 1)}^{N} \mod P \leftrightarrow 0 = {(- 1)}^{N} \mod P)$
60		oveq1	$⊢ {(- 1)}^{N} = - 1 \to {(- 1)}^{N} \mod P = -1 \mod P$
61	60	eqeq2d	$⊢ {(- 1)}^{N} = - 1 \to (0 = {(- 1)}^{N} \mod P \leftrightarrow 0 = -1 \mod P)$
62	61	adantr	$⊢ ({(- 1)}^{N} = - 1 \land φ) \to (0 = {(- 1)}^{N} \mod P \leftrightarrow 0 = -1 \mod P)$
63		negmod0	$⊢ (1 \in ℝ \land P \in ℝ^{+}) \to (1 \mod P = 0 \leftrightarrow -1 \mod P = 0)$
64		eqcom	$⊢ -1 \mod P = 0 \leftrightarrow 0 = -1 \mod P$
65	63 64	bitrdi	$⊢ (1 \in ℝ \land P \in ℝ^{+}) \to (1 \mod P = 0 \leftrightarrow 0 = -1 \mod P)$
66	35 56 65	sylancr	$⊢ φ \to (1 \mod P = 0 \leftrightarrow 0 = -1 \mod P)$
67	30	eqeq1d	$⊢ φ \to (1 \mod P = 0 \leftrightarrow 1 = 0)$
68		ax-1ne0	$⊢ 1 \neq 0$
69		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to 0 = {(- 1)}^{N})$
70	68 69	mpi	$⊢ 1 = 0 \to 0 = {(- 1)}^{N}$
71	67 70	syl6bi	$⊢ φ \to (1 \mod P = 0 \to 0 = {(- 1)}^{N})$
72	66 71	sylbird	$⊢ φ \to (0 = -1 \mod P \to 0 = {(- 1)}^{N})$
73	72	adantl	$⊢ ({(- 1)}^{N} = - 1 \land φ) \to (0 = -1 \mod P \to 0 = {(- 1)}^{N})$
74	62 73	sylbid	$⊢ ({(- 1)}^{N} = - 1 \land φ) \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N})$
75	74	ex	$⊢ {(- 1)}^{N} = - 1 \to (φ \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N}))$
76	42	eqeq2d	$⊢ {(- 1)}^{N} = 1 \to (0 = {(- 1)}^{N} \mod P \leftrightarrow 0 = 1 \mod P)$
77	76	adantr	$⊢ ({(- 1)}^{N} = 1 \land φ) \to (0 = {(- 1)}^{N} \mod P \leftrightarrow 0 = 1 \mod P)$
78		eqcom	$⊢ 0 = 1 \mod P \leftrightarrow 1 \mod P = 0$
79	78 67	syl5bb	$⊢ φ \to (0 = 1 \mod P \leftrightarrow 1 = 0)$
80	79 70	syl6bi	$⊢ φ \to (0 = 1 \mod P \to 0 = {(- 1)}^{N})$
81	80	adantl	$⊢ ({(- 1)}^{N} = 1 \land φ) \to (0 = 1 \mod P \to 0 = {(- 1)}^{N})$
82	77 81	sylbid	$⊢ ({(- 1)}^{N} = 1 \land φ) \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N})$
83	82	ex	$⊢ {(- 1)}^{N} = 1 \to (φ \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N}))$
84	75 83	jaoi	$⊢ ({(- 1)}^{N} = - 1 \lor {(- 1)}^{N} = 1) \to (φ \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N}))$
85	19 84	sylbi	$⊢ {(- 1)}^{N} \in \{- 1, 1\} \to (φ \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N}))$
86	17 85	mpcom	$⊢ φ \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N})$
87	59 86	sylbid	$⊢ φ \to (0 \mod P = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N})$
88		oveq1	$⊢ 2 /_{L} P = 0 \to (2 /_{L} P) \mod P = 0 \mod P$
89	88	eqeq1d	$⊢ 2 /_{L} P = 0 \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \leftrightarrow 0 \mod P = {(- 1)}^{N} \mod P)$
90		eqeq1	$⊢ 2 /_{L} P = 0 \to (2 /_{L} P = {(- 1)}^{N} \leftrightarrow 0 = {(- 1)}^{N})$
91	89 90	imbi12d	$⊢ 2 /_{L} P = 0 \to (((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}) \leftrightarrow (0 \mod P = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N}))$
92	87 91	syl5ibr	$⊢ 2 /_{L} P = 0 \to (φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}))$
93	30	eqeq1d	$⊢ φ \to (1 \mod P = {(- 1)}^{N} \mod P \leftrightarrow 1 = {(- 1)}^{N} \mod P)$
94		eqcom	$⊢ 1 = -1 \mod P \leftrightarrow -1 \mod P = 1$
95		eqcom	$⊢ 1 = - 1 \leftrightarrow - 1 = 1$
96	40 94 95	3imtr4g	$⊢ φ \to (1 = -1 \mod P \to 1 = - 1)$
97	60	eqeq2d	$⊢ {(- 1)}^{N} = - 1 \to (1 = {(- 1)}^{N} \mod P \leftrightarrow 1 = -1 \mod P)$
98		eqeq2	$⊢ {(- 1)}^{N} = - 1 \to (1 = {(- 1)}^{N} \leftrightarrow 1 = - 1)$
99	97 98	imbi12d	$⊢ {(- 1)}^{N} = - 1 \to ((1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}) \leftrightarrow (1 = -1 \mod P \to 1 = - 1))$
100	96 99	syl5ibr	$⊢ {(- 1)}^{N} = - 1 \to (φ \to (1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}))$
101		eqcom	$⊢ {(- 1)}^{N} = 1 \leftrightarrow 1 = {(- 1)}^{N}$
102	101	biimpi	$⊢ {(- 1)}^{N} = 1 \to 1 = {(- 1)}^{N}$
103	102	2a1d	$⊢ {(- 1)}^{N} = 1 \to (φ \to (1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}))$
104	100 103	jaoi	$⊢ ({(- 1)}^{N} = - 1 \lor {(- 1)}^{N} = 1) \to (φ \to (1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}))$
105	19 104	sylbi	$⊢ {(- 1)}^{N} \in \{- 1, 1\} \to (φ \to (1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}))$
106	17 105	mpcom	$⊢ φ \to (1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N})$
107	93 106	sylbid	$⊢ φ \to (1 \mod P = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N})$
108		oveq1	$⊢ 2 /_{L} P = 1 \to (2 /_{L} P) \mod P = 1 \mod P$
109	108	eqeq1d	$⊢ 2 /_{L} P = 1 \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \leftrightarrow 1 \mod P = {(- 1)}^{N} \mod P)$
110		eqeq1	$⊢ 2 /_{L} P = 1 \to (2 /_{L} P = {(- 1)}^{N} \leftrightarrow 1 = {(- 1)}^{N})$
111	109 110	imbi12d	$⊢ 2 /_{L} P = 1 \to (((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}) \leftrightarrow (1 \mod P = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}))$
112	107 111	syl5ibr	$⊢ 2 /_{L} P = 1 \to (φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}))$
113	54 92 112	3jaoi	$⊢ (2 /_{L} P = - 1 \lor 2 /_{L} P = 0 \lor 2 /_{L} P = 1) \to (φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}))$
114	13 113	sylbi	$⊢ 2 /_{L} P \in \{- 1, 0, 1\} \to (φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}))$
115	11 114	mpcom	$⊢ φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N})$

Metamath Proof Explorer

Theorem gausslemma2dlem0i

Proof