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		1mod	$⊢ (P \in ℝ \land 1 < P) \to 1 \mod P = 1$
29	1 23 27 28	4syl	$⊢ φ \to 1 \mod P = 1$
30	29	eqeq2d	$⊢ φ \to (-1 \mod P = 1 \mod P \leftrightarrow -1 \mod P = 1)$
31		oddprmge3	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ_{\geq 3}$
32		m1modge3gt1	$⊢ P \in ℤ_{\geq 3} \to 1 < -1 \mod P$
33		breq2	$⊢ -1 \mod P = 1 \to (1 < -1 \mod P \leftrightarrow 1 < 1)$
34		1re	$⊢ 1 \in ℝ$
35	34	ltnri	$⊢ \neg 1 < 1$
36	35	pm2.21i	$⊢ 1 < 1 \to - 1 = 1$
37	33 36	biimtrdi	$⊢ -1 \mod P = 1 \to (1 < -1 \mod P \to - 1 = 1)$
38	32 37	syl5com	$⊢ P \in ℤ_{\geq 3} \to (-1 \mod P = 1 \to - 1 = 1)$
39	1 31 38	3syl	$⊢ φ \to (-1 \mod P = 1 \to - 1 = 1)$
40	30 39	sylbid	$⊢ φ \to (-1 \mod P = 1 \mod P \to - 1 = 1)$
41		oveq1	$⊢ {(- 1)}^{N} = 1 \to {(- 1)}^{N} \mod P = 1 \mod P$
42	41	eqeq2d	$⊢ {(- 1)}^{N} = 1 \to (-1 \mod P = {(- 1)}^{N} \mod P \leftrightarrow -1 \mod P = 1 \mod P)$
43		eqeq2	$⊢ {(- 1)}^{N} = 1 \to (- 1 = {(- 1)}^{N} \leftrightarrow - 1 = 1)$
44	42 43	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))$
45	40 44	imbitrrid	$⊢ {(- 1)}^{N} = 1 \to (φ \to (-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N}))$
46	22 45	jaoi	$⊢ ({(- 1)}^{N} = - 1 \lor {(- 1)}^{N} = 1) \to (φ \to (-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N}))$
47	19 46	sylbi	$⊢ {(- 1)}^{N} \in \{- 1, 1\} \to (φ \to (-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N}))$
48	17 47	mpcom	$⊢ φ \to (-1 \mod P = {(- 1)}^{N} \mod P \to - 1 = {(- 1)}^{N})$
49		oveq1	$⊢ 2 /_{L} P = - 1 \to (2 /_{L} P) \mod P = -1 \mod P$
50	49	eqeq1d	$⊢ 2 /_{L} P = - 1 \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \leftrightarrow -1 \mod P = {(- 1)}^{N} \mod P)$
51		eqeq1	$⊢ 2 /_{L} P = - 1 \to (2 /_{L} P = {(- 1)}^{N} \leftrightarrow - 1 = {(- 1)}^{N})$
52	50 51	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}))$
53	48 52	imbitrrid	$⊢ 2 /_{L} P = - 1 \to (φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}))$
54	1	gausslemma2dlem0a	$⊢ φ \to P \in ℕ$
55	54	nnrpd	$⊢ φ \to P \in ℝ^{+}$
56		0mod	$⊢ P \in ℝ^{+} \to 0 \mod P = 0$
57	55 56	syl	$⊢ φ \to 0 \mod P = 0$
58	57	eqeq1d	$⊢ φ \to (0 \mod P = {(- 1)}^{N} \mod P \leftrightarrow 0 = {(- 1)}^{N} \mod P)$
59		oveq1	$⊢ {(- 1)}^{N} = - 1 \to {(- 1)}^{N} \mod P = -1 \mod P$
60	59	eqeq2d	$⊢ {(- 1)}^{N} = - 1 \to (0 = {(- 1)}^{N} \mod P \leftrightarrow 0 = -1 \mod P)$
61	60	adantr	$⊢ ({(- 1)}^{N} = - 1 \land φ) \to (0 = {(- 1)}^{N} \mod P \leftrightarrow 0 = -1 \mod P)$
62		negmod0	$⊢ (1 \in ℝ \land P \in ℝ^{+}) \to (1 \mod P = 0 \leftrightarrow -1 \mod P = 0)$
63		eqcom	$⊢ -1 \mod P = 0 \leftrightarrow 0 = -1 \mod P$
64	62 63	bitrdi	$⊢ (1 \in ℝ \land P \in ℝ^{+}) \to (1 \mod P = 0 \leftrightarrow 0 = -1 \mod P)$
65	34 55 64	sylancr	$⊢ φ \to (1 \mod P = 0 \leftrightarrow 0 = -1 \mod P)$
66	29	eqeq1d	$⊢ φ \to (1 \mod P = 0 \leftrightarrow 1 = 0)$
67		ax-1ne0	$⊢ 1 \neq 0$
68		eqneqall	$⊢ 1 = 0 \to (1 \neq 0 \to 0 = {(- 1)}^{N})$
69	67 68	mpi	$⊢ 1 = 0 \to 0 = {(- 1)}^{N}$
70	66 69	biimtrdi	$⊢ φ \to (1 \mod P = 0 \to 0 = {(- 1)}^{N})$
71	65 70	sylbird	$⊢ φ \to (0 = -1 \mod P \to 0 = {(- 1)}^{N})$
72	71	adantl	$⊢ ({(- 1)}^{N} = - 1 \land φ) \to (0 = -1 \mod P \to 0 = {(- 1)}^{N})$
73	61 72	sylbid	$⊢ ({(- 1)}^{N} = - 1 \land φ) \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N})$
74	73	ex	$⊢ {(- 1)}^{N} = - 1 \to (φ \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N}))$
75	41	eqeq2d	$⊢ {(- 1)}^{N} = 1 \to (0 = {(- 1)}^{N} \mod P \leftrightarrow 0 = 1 \mod P)$
76	75	adantr	$⊢ ({(- 1)}^{N} = 1 \land φ) \to (0 = {(- 1)}^{N} \mod P \leftrightarrow 0 = 1 \mod P)$
77		eqcom	$⊢ 0 = 1 \mod P \leftrightarrow 1 \mod P = 0$
78	77 66	bitrid	$⊢ φ \to (0 = 1 \mod P \leftrightarrow 1 = 0)$
79	78 69	biimtrdi	$⊢ φ \to (0 = 1 \mod P \to 0 = {(- 1)}^{N})$
80	79	adantl	$⊢ ({(- 1)}^{N} = 1 \land φ) \to (0 = 1 \mod P \to 0 = {(- 1)}^{N})$
81	76 80	sylbid	$⊢ ({(- 1)}^{N} = 1 \land φ) \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N})$
82	81	ex	$⊢ {(- 1)}^{N} = 1 \to (φ \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N}))$
83	74 82	jaoi	$⊢ ({(- 1)}^{N} = - 1 \lor {(- 1)}^{N} = 1) \to (φ \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N}))$
84	19 83	sylbi	$⊢ {(- 1)}^{N} \in \{- 1, 1\} \to (φ \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N}))$
85	17 84	mpcom	$⊢ φ \to (0 = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N})$
86	58 85	sylbid	$⊢ φ \to (0 \mod P = {(- 1)}^{N} \mod P \to 0 = {(- 1)}^{N})$
87		oveq1	$⊢ 2 /_{L} P = 0 \to (2 /_{L} P) \mod P = 0 \mod P$
88	87	eqeq1d	$⊢ 2 /_{L} P = 0 \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \leftrightarrow 0 \mod P = {(- 1)}^{N} \mod P)$
89		eqeq1	$⊢ 2 /_{L} P = 0 \to (2 /_{L} P = {(- 1)}^{N} \leftrightarrow 0 = {(- 1)}^{N})$
90	88 89	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}))$
91	86 90	imbitrrid	$⊢ 2 /_{L} P = 0 \to (φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}))$
92	29	eqeq1d	$⊢ φ \to (1 \mod P = {(- 1)}^{N} \mod P \leftrightarrow 1 = {(- 1)}^{N} \mod P)$
93		eqcom	$⊢ 1 = -1 \mod P \leftrightarrow -1 \mod P = 1$
94		eqcom	$⊢ 1 = - 1 \leftrightarrow - 1 = 1$
95	39 93 94	3imtr4g	$⊢ φ \to (1 = -1 \mod P \to 1 = - 1)$
96	59	eqeq2d	$⊢ {(- 1)}^{N} = - 1 \to (1 = {(- 1)}^{N} \mod P \leftrightarrow 1 = -1 \mod P)$
97		eqeq2	$⊢ {(- 1)}^{N} = - 1 \to (1 = {(- 1)}^{N} \leftrightarrow 1 = - 1)$
98	96 97	imbi12d	$⊢ {(- 1)}^{N} = - 1 \to ((1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}) \leftrightarrow (1 = -1 \mod P \to 1 = - 1))$
99	95 98	imbitrrid	$⊢ {(- 1)}^{N} = - 1 \to (φ \to (1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}))$
100		eqcom	$⊢ {(- 1)}^{N} = 1 \leftrightarrow 1 = {(- 1)}^{N}$
101	100	biimpi	$⊢ {(- 1)}^{N} = 1 \to 1 = {(- 1)}^{N}$
102	101	2a1d	$⊢ {(- 1)}^{N} = 1 \to (φ \to (1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}))$
103	99 102	jaoi	$⊢ ({(- 1)}^{N} = - 1 \lor {(- 1)}^{N} = 1) \to (φ \to (1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}))$
104	19 103	sylbi	$⊢ {(- 1)}^{N} \in \{- 1, 1\} \to (φ \to (1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N}))$
105	17 104	mpcom	$⊢ φ \to (1 = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N})$
106	92 105	sylbid	$⊢ φ \to (1 \mod P = {(- 1)}^{N} \mod P \to 1 = {(- 1)}^{N})$
107		oveq1	$⊢ 2 /_{L} P = 1 \to (2 /_{L} P) \mod P = 1 \mod P$
108	107	eqeq1d	$⊢ 2 /_{L} P = 1 \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \leftrightarrow 1 \mod P = {(- 1)}^{N} \mod P)$
109		eqeq1	$⊢ 2 /_{L} P = 1 \to (2 /_{L} P = {(- 1)}^{N} \leftrightarrow 1 = {(- 1)}^{N})$
110	108 109	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}))$
111	106 110	imbitrrid	$⊢ 2 /_{L} P = 1 \to (φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N}))$
112	53 91 111	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}))$
113	13 112	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}))$
114	11 113	mpcom	$⊢ φ \to ((2 /_{L} P) \mod P = {(- 1)}^{N} \mod P \to 2 /_{L} P = {(- 1)}^{N})$

Metamath Proof Explorer

Theorem gausslemma2dlem0i

Proof