gausslemma2d - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > gausslemma2d		Structured version Visualization version GIF version

Theorem gausslemma2d 27707

Description: Gauss' Lemma (see also theorem 9.6 in [ApostolNT] p. 182) for integer 2: Let p be an odd prime. Let S = {2, 4, 6, ..., p - 1}. Let n denote the number of elements of S whose least positive residue modulo p is greater than p/2. Then ( 2 | p ) = (-1)^n. (Contributed by AV, 14-Jul-2021.)

**Hypotheses**
Ref	Expression
gausslemma2d.p	⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
gausslemma2d.h	⊢ 𝐻 = ((𝑃 − 1) / 2)
gausslemma2d.r	⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
gausslemma2d.m	⊢ 𝑀 = (⌊‘(𝑃 / 4))
gausslemma2d.n	⊢ 𝑁 = (𝐻 − 𝑀)

**Assertion**
Ref	Expression
gausslemma2d	⊢ (𝜑 → (2 /_L 𝑃) = ( -1↑𝑁))

Distinct variable groups: 𝑥,𝐻 𝑥,𝑃 𝜑,𝑥 𝑥,𝑀 Allowed substitution hints: 𝑅(𝑥) 𝑁(𝑥)

**Proof of Theorem gausslemma2d**
Step	Hyp	Ref	Expression
1		gausslemma2d.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
2		gausslemma2d.h	. . 3 ⊢ 𝐻 = ((𝑃 − 1) / 2)
3		gausslemma2d.r	. . 3 ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
4		gausslemma2d.m	. . 3 ⊢ 𝑀 = (⌊‘(𝑃 / 4))
5		gausslemma2d.n	. . 3 ⊢ 𝑁 = (𝐻 − 𝑀)
6	1, 2, 3, 4, 5	gausslemma2dlem7 27706	. 2 ⊢ (𝜑 → ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1)
7		eldifi 4067	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
8		prmnn 16855	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	8	nnred 12354	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
10		prmgt1 16879	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
11	9, 10	jca 521	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
12		1mod 14047	. . . . . 6 ⊢ ((𝑃 ∈ ℝ ∧ 1 < 𝑃) → (1 mod 𝑃) = 1)
13	1, 7, 11, 12	4syl 20	. . . . 5 ⊢ (𝜑 → (1 mod 𝑃) = 1)
14	13	eqcomd 2766	. . . 4 ⊢ (𝜑 → 1 = (1 mod 𝑃))
15	14	eqeq2d 2771	. . 3 ⊢ (𝜑 → (((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1 ↔ ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)))
16		neg1z 12736	. . . . . . . . . . 11 ⊢ -1 ∈ ℤ
17	1, 4, 2, 5	gausslemma2dlem0h 27696	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
18		zexpcl 14223	. . . . . . . . . . 11 ⊢ (( -1 ∈ ℤ ∧ 𝑁 ∈ ℕ₀) → ( -1↑𝑁) ∈ ℤ)
19	16, 17, 18	sylancr 599	. . . . . . . . . 10 ⊢ (𝜑 → ( -1↑𝑁) ∈ ℤ)
20		2nn 12420	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ
21	20	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℕ)
22	1, 2	gausslemma2dlem0b 27690	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ∈ ℕ)
23	22	nnnn0d 12671	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 ∈ ℕ₀)
24	21, 23	nnexpcld 14393	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑𝐻) ∈ ℕ)
25	24	nnzd 12723	. . . . . . . . . 10 ⊢ (𝜑 → (2↑𝐻) ∈ ℤ)
26	19, 25	zmulcld 12813	. . . . . . . . 9 ⊢ (𝜑 → (( -1↑𝑁) · (2↑𝐻)) ∈ ℤ)
27	26	zred 12807	. . . . . . . 8 ⊢ (𝜑 → (( -1↑𝑁) · (2↑𝐻)) ∈ ℝ)
28		1red 11313	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
29	27, 28	jca 521	. . . . . . 7 ⊢ (𝜑 → ((( -1↑𝑁) · (2↑𝐻)) ∈ ℝ ∧ 1 ∈ ℝ))
30	29	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → ((( -1↑𝑁) · (2↑𝐻)) ∈ ℝ ∧ 1 ∈ ℝ))
31	1	gausslemma2dlem0a 27689	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ℕ)
32	31	nnrpd 13166	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℝ⁺)
33	19, 32	jca 521	. . . . . . 7 ⊢ (𝜑 → (( -1↑𝑁) ∈ ℤ ∧ 𝑃 ∈ ℝ⁺))
34	33	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → (( -1↑𝑁) ∈ ℤ ∧ 𝑃 ∈ ℝ⁺))
35		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃))
36		modmul1 14071	. . . . . 6 ⊢ ((((( -1↑𝑁) · (2↑𝐻)) ∈ ℝ ∧ 1 ∈ ℝ) ∧ (( -1↑𝑁) ∈ ℤ ∧ 𝑃 ∈ ℝ⁺) ∧ ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → (((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) mod 𝑃) = ((1 · ( -1↑𝑁)) mod 𝑃))
37	30, 34, 35, 36	syl3anc 1398	. . . . 5 ⊢ ((𝜑 ∧ ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → (((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) mod 𝑃) = ((1 · ( -1↑𝑁)) mod 𝑃))
38	37	ex 418	. . . 4 ⊢ (𝜑 → (((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃) → (((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) mod 𝑃) = ((1 · ( -1↑𝑁)) mod 𝑃)))
39	19	zcnd 12808	. . . . . . . . 9 ⊢ (𝜑 → ( -1↑𝑁) ∈ ℂ)
40	24	nncnd 12355	. . . . . . . . 9 ⊢ (𝜑 → (2↑𝐻) ∈ ℂ)
41	39, 40, 39	mul32d 11524	. . . . . . . 8 ⊢ (𝜑 → ((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) = ((( -1↑𝑁) · ( -1↑𝑁)) · (2↑𝐻)))
42	17	nn0cnd 12673	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
43	42	2timesd 12593	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁))
44	43	eqcomd 2766	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 𝑁) = (2 · 𝑁))
45	44	oveq2d 7437	. . . . . . . . . 10 ⊢ (𝜑 → ( -1↑(𝑁 + 𝑁)) = ( -1↑(2 · 𝑁)))
46		neg1cn 12309	. . . . . . . . . . . 12 ⊢ -1 ∈ ℂ
47	46	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → -1 ∈ ℂ)
48	47, 17, 17	expaddd 14295	. . . . . . . . . 10 ⊢ (𝜑 → ( -1↑(𝑁 + 𝑁)) = (( -1↑𝑁) · ( -1↑𝑁)))
49	17	nn0zd 12722	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
50		m1expeven 14256	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → ( -1↑(2 · 𝑁)) = 1)
51	49, 50	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ( -1↑(2 · 𝑁)) = 1)
52	45, 48, 51	3eqtr3d 2803	. . . . . . . . 9 ⊢ (𝜑 → (( -1↑𝑁) · ( -1↑𝑁)) = 1)
53	52	oveq1d 7436	. . . . . . . 8 ⊢ (𝜑 → ((( -1↑𝑁) · ( -1↑𝑁)) · (2↑𝐻)) = (1 · (2↑𝐻)))
54	40	mullidd 11331	. . . . . . . 8 ⊢ (𝜑 → (1 · (2↑𝐻)) = (2↑𝐻))
55	41, 53, 54	3eqtrd 2799	. . . . . . 7 ⊢ (𝜑 → ((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) = (2↑𝐻))
56	55	oveq1d 7436	. . . . . 6 ⊢ (𝜑 → (((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) mod 𝑃) = ((2↑𝐻) mod 𝑃))
57	39	mullidd 11331	. . . . . . 7 ⊢ (𝜑 → (1 · ( -1↑𝑁)) = ( -1↑𝑁))
58	57	oveq1d 7436	. . . . . 6 ⊢ (𝜑 → ((1 · ( -1↑𝑁)) mod 𝑃) = (( -1↑𝑁) mod 𝑃))
59	56, 58	eqeq12d 2776	. . . . 5 ⊢ (𝜑 → ((((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) mod 𝑃) = ((1 · ( -1↑𝑁)) mod 𝑃) ↔ ((2↑𝐻) mod 𝑃) = (( -1↑𝑁) mod 𝑃)))
60	2	oveq2i 7432	. . . . . . . 8 ⊢ (2↑𝐻) = (2↑((𝑃 − 1) / 2))
61	60	oveq1i 7431	. . . . . . 7 ⊢ ((2↑𝐻) mod 𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃)
62	61	eqeq1i 2765	. . . . . 6 ⊢ (((2↑𝐻) mod 𝑃) = (( -1↑𝑁) mod 𝑃) ↔ ((2↑((𝑃 − 1) / 2)) mod 𝑃) = (( -1↑𝑁) mod 𝑃))
63		2z 12732	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
64		lgsvalmod 27649	. . . . . . . . . 10 ⊢ ((2 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((2 /_L 𝑃) mod 𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃))
65	63, 1, 64	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → ((2 /_L 𝑃) mod 𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃))
66	65	eqcomd 2766	. . . . . . . 8 ⊢ (𝜑 → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((2 /_L 𝑃) mod 𝑃))
67	66	eqeq1d 2762	. . . . . . 7 ⊢ (𝜑 → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = (( -1↑𝑁) mod 𝑃) ↔ ((2 /_L 𝑃) mod 𝑃) = (( -1↑𝑁) mod 𝑃)))
68	1, 4, 2, 5	gausslemma2dlem0i 27697	. . . . . . 7 ⊢ (𝜑 → (((2 /_L 𝑃) mod 𝑃) = (( -1↑𝑁) mod 𝑃) → (2 /_L 𝑃) = ( -1↑𝑁)))
69	67, 68	sylbid 243	. . . . . 6 ⊢ (𝜑 → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = (( -1↑𝑁) mod 𝑃) → (2 /_L 𝑃) = ( -1↑𝑁)))
70	62, 69	biimtrid 245	. . . . 5 ⊢ (𝜑 → (((2↑𝐻) mod 𝑃) = (( -1↑𝑁) mod 𝑃) → (2 /_L 𝑃) = ( -1↑𝑁)))
71	59, 70	sylbid 243	. . . 4 ⊢ (𝜑 → ((((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) mod 𝑃) = ((1 · ( -1↑𝑁)) mod 𝑃) → (2 /_L 𝑃) = ( -1↑𝑁)))
72	38, 71	syld 48	. . 3 ⊢ (𝜑 → (((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃) → (2 /_L 𝑃) = ( -1↑𝑁)))
73	15, 72	sylbid 243	. 2 ⊢ (𝜑 → (((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1 → (2 /_L 𝑃) = ( -1↑𝑁)))
74	6, 73	mpd 16	1 ⊢ (𝜑 → (2 /_L 𝑃) = ( -1↑𝑁))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∖ cdif 4045 ifcif 4481 {csn 4584 class class class wbr 5102 ↦ cmpt 5185 ‘cfv 6539 (class class class)co 7421 ℂcc 11202 ℝcr 11203 1c1 11205 + caddc 11207 · cmul 11209 < clt 11347 − cmin 11545 -cneg 11546 / cdiv 11977 ℕcn 12339 2c2 12401 4c4 12403 ℕ₀cn0 12610 ℤcz 12697 ℝ⁺crp 13124 ...cfz 13643 ⌊cfl 13934 mod cmo 14013 ↑cexp 14208 ℙcprime 16852 /_L clgs 27627

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-inf2 9646 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-2o 8481 df-oadd 8484 df-er 8721 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-sup 9438 df-inf 9439 df-oi 9508 df-dju 9986 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-3 12410 df-4 12411 df-5 12412 df-6 12413 df-n0 12611 df-xnn0 12684 df-z 12698 df-uz 12970 df-q 13080 df-rp 13125 df-ioo 13484 df-fz 13644 df-fzo 13793 df-fl 13936 df-mod 14014 df-seq 14149 df-exp 14209 df-fac 14422 df-hash 14479 df-cj 15272 df-re 15273 df-im 15274 df-sqrt 15408 df-abs 15409 df-clim 15661 df-prod 16079 df-dvds 16429 df-gcd 16671 df-prm 16853 df-phi 16949 df-pc 17021 df-lgs 27628

This theorem is used by: 2lgs 27740

W3C validator