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 27747

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 27746	. 2 ⊢ (𝜑 → ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1)
7		eldifi 4070	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
8		prmnn 16890	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
9	8	nnred 12388	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
10		prmgt1 16914	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
11	9, 10	jca 521	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
12		1mod 14081	. . . . . 6 ⊢ ((𝑃 ∈ ℝ ∧ 1 < 𝑃) → (1 mod 𝑃) = 1)
13	1, 7, 11, 12	4syl 20	. . . . 5 ⊢ (𝜑 → (1 mod 𝑃) = 1)
14	13	eqcomd 2769	. . . 4 ⊢ (𝜑 → 1 = (1 mod 𝑃))
15	14	eqeq2d 2774	. . 3 ⊢ (𝜑 → (((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1 ↔ ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)))
16		neg1z 12770	. . . . . . . . . . 11 ⊢ -1 ∈ ℤ
17	1, 4, 2, 5	gausslemma2dlem0h 27736	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
18		zexpcl 14257	. . . . . . . . . . 11 ⊢ (( -1 ∈ ℤ ∧ 𝑁 ∈ ℕ₀) → ( -1↑𝑁) ∈ ℤ)
19	16, 17, 18	sylancr 599	. . . . . . . . . 10 ⊢ (𝜑 → ( -1↑𝑁) ∈ ℤ)
20		2nn 12454	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ
21	20	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℕ)
22	1, 2	gausslemma2dlem0b 27730	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 ∈ ℕ)
23	22	nnnn0d 12705	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 ∈ ℕ₀)
24	21, 23	nnexpcld 14428	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑𝐻) ∈ ℕ)
25	24	nnzd 12757	. . . . . . . . . 10 ⊢ (𝜑 → (2↑𝐻) ∈ ℤ)
26	19, 25	zmulcld 12847	. . . . . . . . 9 ⊢ (𝜑 → (( -1↑𝑁) · (2↑𝐻)) ∈ ℤ)
27	26	zred 12841	. . . . . . . 8 ⊢ (𝜑 → (( -1↑𝑁) · (2↑𝐻)) ∈ ℝ)
28		1red 11346	. . . . . . . 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 27729	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ ℕ)
32	31	nnrpd 13200	. . . . . . . 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 14105	. . . . . 6 ⊢ ((((( -1↑𝑁) · (2↑𝐻)) ∈ ℝ ∧ 1 ∈ ℝ) ∧ (( -1↑𝑁) ∈ ℤ ∧ 𝑃 ∈ ℝ⁺) ∧ ((( -1↑𝑁) · (2↑𝐻)) mod 𝑃) = (1 mod 𝑃)) → (((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) mod 𝑃) = ((1 · ( -1↑𝑁)) mod 𝑃))
37	30, 34, 35, 36	syl3anc 1399	. . . . 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 12842	. . . . . . . . 9 ⊢ (𝜑 → ( -1↑𝑁) ∈ ℂ)
40	24	nncnd 12389	. . . . . . . . 9 ⊢ (𝜑 → (2↑𝐻) ∈ ℂ)
41	39, 40, 39	mul32d 11557	. . . . . . . 8 ⊢ (𝜑 → ((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) = ((( -1↑𝑁) · ( -1↑𝑁)) · (2↑𝐻)))
42	17	nn0cnd 12707	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
43	42	2timesd 12627	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁))
44	43	eqcomd 2769	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 𝑁) = (2 · 𝑁))
45	44	oveq2d 7465	. . . . . . . . . 10 ⊢ (𝜑 → ( -1↑(𝑁 + 𝑁)) = ( -1↑(2 · 𝑁)))
46		neg1cn 12343	. . . . . . . . . . . 12 ⊢ -1 ∈ ℂ
47	46	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → -1 ∈ ℂ)
48	47, 17, 17	expaddd 14329	. . . . . . . . . 10 ⊢ (𝜑 → ( -1↑(𝑁 + 𝑁)) = (( -1↑𝑁) · ( -1↑𝑁)))
49	17	nn0zd 12756	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℤ)
50		m1expeven 14290	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → ( -1↑(2 · 𝑁)) = 1)
51	49, 50	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ( -1↑(2 · 𝑁)) = 1)
52	45, 48, 51	3eqtr3d 2806	. . . . . . . . 9 ⊢ (𝜑 → (( -1↑𝑁) · ( -1↑𝑁)) = 1)
53	52	oveq1d 7464	. . . . . . . 8 ⊢ (𝜑 → ((( -1↑𝑁) · ( -1↑𝑁)) · (2↑𝐻)) = (1 · (2↑𝐻)))
54	40	mullidd 11364	. . . . . . . 8 ⊢ (𝜑 → (1 · (2↑𝐻)) = (2↑𝐻))
55	41, 53, 54	3eqtrd 2802	. . . . . . 7 ⊢ (𝜑 → ((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) = (2↑𝐻))
56	55	oveq1d 7464	. . . . . 6 ⊢ (𝜑 → (((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) mod 𝑃) = ((2↑𝐻) mod 𝑃))
57	39	mullidd 11364	. . . . . . 7 ⊢ (𝜑 → (1 · ( -1↑𝑁)) = ( -1↑𝑁))
58	57	oveq1d 7464	. . . . . 6 ⊢ (𝜑 → ((1 · ( -1↑𝑁)) mod 𝑃) = (( -1↑𝑁) mod 𝑃))
59	56, 58	eqeq12d 2779	. . . . 5 ⊢ (𝜑 → ((((( -1↑𝑁) · (2↑𝐻)) · ( -1↑𝑁)) mod 𝑃) = ((1 · ( -1↑𝑁)) mod 𝑃) ↔ ((2↑𝐻) mod 𝑃) = (( -1↑𝑁) mod 𝑃)))
60	2	oveq2i 7460	. . . . . . . 8 ⊢ (2↑𝐻) = (2↑((𝑃 − 1) / 2))
61	60	oveq1i 7459	. . . . . . 7 ⊢ ((2↑𝐻) mod 𝑃) = ((2↑((𝑃 − 1) / 2)) mod 𝑃)
62	61	eqeq1i 2768	. . . . . 6 ⊢ (((2↑𝐻) mod 𝑃) = (( -1↑𝑁) mod 𝑃) ↔ ((2↑((𝑃 − 1) / 2)) mod 𝑃) = (( -1↑𝑁) mod 𝑃))
63		2z 12766	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
64		lgsvalmod 27689	. . . . . . . . . 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 2769	. . . . . . . 8 ⊢ (𝜑 → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = ((2 /_L 𝑃) mod 𝑃))
67	66	eqeq1d 2765	. . . . . . 7 ⊢ (𝜑 → (((2↑((𝑃 − 1) / 2)) mod 𝑃) = (( -1↑𝑁) mod 𝑃) ↔ ((2 /_L 𝑃) mod 𝑃) = (( -1↑𝑁) mod 𝑃)))
68	1, 4, 2, 5	gausslemma2dlem0i 27737	. . . . . . 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 1570 ∈ wcel 2147 ∖ cdif 4048 ifcif 4485 {csn 4588 class class class wbr 5106 ↦ cmpt 5190 ‘cfv 6564 (class class class)co 7449 ℂcc 11235 ℝcr 11236 1c1 11238 + caddc 11240 · cmul 11242 < clt 11380 − cmin 11578 -cneg 11579 / cdiv 12011 ℕcn 12373 2c2 12435 4c4 12437 ℕ₀cn0 12644 ℤcz 12731 ℝ⁺crp 13158 ...cfz 13677 ⌊cfl 13968 mod cmo 14047 ↑cexp 14242 ℙcprime 16887 /_L clgs 27667

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-inf2 9677 ax-cnex 11293 ax-resscn 11294 ax-1cn 11295 ax-icn 11296 ax-addcl 11297 ax-addrcl 11298 ax-mulcl 11299 ax-mulrcl 11300 ax-mulcom 11301 ax-addass 11302 ax-mulass 11303 ax-distr 11304 ax-i2m1 11305 ax-1ne0 11306 ax-1rid 11307 ax-rnegex 11308 ax-rrecex 11309 ax-cnre 11310 ax-pre-lttri 11311 ax-pre-lttrn 11312 ax-pre-ltadd 11313 ax-pre-mulgt0 11314 ax-pre-sup 11315

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-isom 6573 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-om 7910 df-1st 8033 df-2nd 8034 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-1o 8512 df-2o 8513 df-oadd 8516 df-er 8753 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-sup 9469 df-inf 9470 df-oi 9539 df-dju 10017 df-card 10055 df-pnf 11382 df-mnf 11383 df-xr 11384 df-ltxr 11385 df-le 11386 df-sub 11580 df-neg 11581 df-div 12012 df-nn 12374 df-2 12443 df-3 12444 df-4 12445 df-5 12446 df-6 12447 df-n0 12645 df-xnn0 12718 df-z 12732 df-uz 13004 df-q 13114 df-rp 13159 df-ioo 13518 df-fz 13678 df-fzo 13827 df-fl 13970 df-mod 14048 df-seq 14183 df-exp 14243 df-fac 14457 df-hash 14514 df-cj 15307 df-re 15308 df-im 15309 df-sqrt 15443 df-abs 15444 df-clim 15696 df-prod 16114 df-dvds 16464 df-gcd 16706 df-prm 16888 df-phi 16984 df-pc 17056 df-lgs 27668

This theorem is used by: 2lgs 27780

W3C validator