gausslemma2dlem7 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > gausslemma2dlem7		GIF version

Theorem gausslemma2dlem7 15319

Description: Lemma 7 for gausslemma2d 15320. (Contributed by AV, 13-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
gausslemma2dlem7	⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1)

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

**Proof of Theorem gausslemma2dlem7**
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	gausslemma2dlem6 15318	. 2 ⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃))
7	1, 2	gausslemma2dlem0b 15301	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℕ)
8	7	nnnn0d 9304	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ∈ ℕ₀)
9	8	faccld 10830	. . . . . . . . 9 ⊢ (𝜑 → (!‘𝐻) ∈ ℕ)
10	9	nncnd 9006	. . . . . . . 8 ⊢ (𝜑 → (!‘𝐻) ∈ ℂ)
11	10	mullidd 8046	. . . . . . 7 ⊢ (𝜑 → (1 · (!‘𝐻)) = (!‘𝐻))
12	11	eqcomd 2202	. . . . . 6 ⊢ (𝜑 → (!‘𝐻) = (1 · (!‘𝐻)))
13	12	oveq1d 5938	. . . . 5 ⊢ (𝜑 → ((!‘𝐻) mod 𝑃) = ((1 · (!‘𝐻)) mod 𝑃))
14	13	eqeq1d 2205	. . . 4 ⊢ (𝜑 → (((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃) ↔ ((1 · (!‘𝐻)) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃)))
15		1zzd 9355	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
16		neg1z 9360	. . . . . . 7 ⊢ -1 ∈ ℤ
17	1, 4, 2, 5	gausslemma2dlem0h 15307	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
18		zexpcl 10648	. . . . . . 7 ⊢ ((-1 ∈ ℤ ∧ 𝑁 ∈ ℕ₀) → (-1↑𝑁) ∈ ℤ)
19	16, 17, 18	sylancr 414	. . . . . 6 ⊢ (𝜑 → (-1↑𝑁) ∈ ℤ)
20		2z 9356	. . . . . . 7 ⊢ 2 ∈ ℤ
21		zexpcl 10648	. . . . . . 7 ⊢ ((2 ∈ ℤ ∧ 𝐻 ∈ ℕ₀) → (2↑𝐻) ∈ ℤ)
22	20, 8, 21	sylancr 414	. . . . . 6 ⊢ (𝜑 → (2↑𝐻) ∈ ℤ)
23	19, 22	zmulcld 9456	. . . . 5 ⊢ (𝜑 → ((-1↑𝑁) · (2↑𝐻)) ∈ ℤ)
24	9	nnzd 9449	. . . . 5 ⊢ (𝜑 → (!‘𝐻) ∈ ℤ)
25	1	gausslemma2dlem0a 15300	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ ℕ)
26	1, 2	gausslemma2dlem0c 15302	. . . . 5 ⊢ (𝜑 → ((!‘𝐻) gcd 𝑃) = 1)
27		cncongrcoprm 12284	. . . . 5 ⊢ (((1 ∈ ℤ ∧ ((-1↑𝑁) · (2↑𝐻)) ∈ ℤ ∧ (!‘𝐻) ∈ ℤ) ∧ (𝑃 ∈ ℕ ∧ ((!‘𝐻) gcd 𝑃) = 1)) → (((1 · (!‘𝐻)) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃) ↔ (1 mod 𝑃) = (((-1↑𝑁) · (2↑𝐻)) mod 𝑃)))
28	15, 23, 24, 25, 26, 27	syl32anc 1257	. . . 4 ⊢ (𝜑 → (((1 · (!‘𝐻)) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃) ↔ (1 mod 𝑃) = (((-1↑𝑁) · (2↑𝐻)) mod 𝑃)))
29	14, 28	bitrd 188	. . 3 ⊢ (𝜑 → (((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃) ↔ (1 mod 𝑃) = (((-1↑𝑁) · (2↑𝐻)) mod 𝑃)))
30		simpr 110	. . . . 5 ⊢ ((𝜑 ∧ (1 mod 𝑃) = (((-1↑𝑁) · (2↑𝐻)) mod 𝑃)) → (1 mod 𝑃) = (((-1↑𝑁) · (2↑𝐻)) mod 𝑃))
31		nnq 9709	. . . . . . . 8 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℚ)
32	25, 31	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℚ)
33	1	eldifad 3168	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ ℙ)
34		prmgt1 12310	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
35	33, 34	syl 14	. . . . . . 7 ⊢ (𝜑 → 1 < 𝑃)
36		q1mod 10450	. . . . . . 7 ⊢ ((𝑃 ∈ ℚ ∧ 1 < 𝑃) → (1 mod 𝑃) = 1)
37	32, 35, 36	syl2anc 411	. . . . . 6 ⊢ (𝜑 → (1 mod 𝑃) = 1)
38	37	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (1 mod 𝑃) = (((-1↑𝑁) · (2↑𝐻)) mod 𝑃)) → (1 mod 𝑃) = 1)
39	30, 38	eqtr3d 2231	. . . 4 ⊢ ((𝜑 ∧ (1 mod 𝑃) = (((-1↑𝑁) · (2↑𝐻)) mod 𝑃)) → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1)
40	39	ex 115	. . 3 ⊢ (𝜑 → ((1 mod 𝑃) = (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1))
41	29, 40	sylbid 150	. 2 ⊢ (𝜑 → (((!‘𝐻) mod 𝑃) = ((((-1↑𝑁) · (2↑𝐻)) · (!‘𝐻)) mod 𝑃) → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1))
42	6, 41	mpd 13	1 ⊢ (𝜑 → (((-1↑𝑁) · (2↑𝐻)) mod 𝑃) = 1)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1364 ∈ wcel 2167 ∖ cdif 3154 ifcif 3562 {csn 3623 class class class wbr 4034 ↦ cmpt 4095 ‘cfv 5259 (class class class)co 5923 1c1 7882 · cmul 7886 < clt 8063 − cmin 8199 -cneg 8200 / cdiv 8701 ℕcn 8992 2c2 9043 4c4 9045 ℕ₀cn0 9251 ℤcz 9328 ℚcq 9695 ...cfz 10085 ⌊cfl 10360 mod cmo 10416 ↑cexp 10632 !cfa 10819 gcd cgcd 12130 ℙcprime 12285

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7972 ax-resscn 7973 ax-1cn 7974 ax-1re 7975 ax-icn 7976 ax-addcl 7977 ax-addrcl 7978 ax-mulcl 7979 ax-mulrcl 7980 ax-addcom 7981 ax-mulcom 7982 ax-addass 7983 ax-mulass 7984 ax-distr 7985 ax-i2m1 7986 ax-0lt1 7987 ax-1rid 7988 ax-0id 7989 ax-rnegex 7990 ax-precex 7991 ax-cnre 7992 ax-pre-ltirr 7993 ax-pre-ltwlin 7994 ax-pre-lttrn 7995 ax-pre-apti 7996 ax-pre-ltadd 7997 ax-pre-mulgt0 7998 ax-pre-mulext 7999 ax-arch 8000 ax-caucvg 8001

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-xor 1387 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-tp 3631 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5878 df-ov 5926 df-oprab 5927 df-mpo 5928 df-1st 6199 df-2nd 6200 df-recs 6364 df-irdg 6429 df-frec 6450 df-1o 6475 df-2o 6476 df-oadd 6479 df-er 6593 df-en 6801 df-dom 6802 df-fin 6803 df-sup 7051 df-pnf 8065 df-mnf 8066 df-xr 8067 df-ltxr 8068 df-le 8069 df-sub 8201 df-neg 8202 df-reap 8604 df-ap 8611 df-div 8702 df-inn 8993 df-2 9051 df-3 9052 df-4 9053 df-5 9054 df-6 9055 df-n0 9252 df-z 9329 df-uz 9604 df-q 9696 df-rp 9731 df-ioo 9969 df-fz 10086 df-fzo 10220 df-fl 10362 df-mod 10417 df-seqfrec 10542 df-exp 10633 df-fac 10820 df-ihash 10870 df-cj 11009 df-re 11010 df-im 11011 df-rsqrt 11165 df-abs 11166 df-clim 11446 df-proddc 11718 df-dvds 11955 df-gcd 12131 df-prm 12286

This theorem is referenced by: gausslemma2d 15320

W3C validator