lgslem4 - Intuitionistic Logic Explorer

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

Theorem lgslem4 14882

Description: Lemma for lgsfcl2 14885. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 19-Mar-2022.)

**Hypothesis**
Ref	Expression
lgslem2.z	⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}

**Assertion**
Ref	Expression
lgslem4	⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)

Distinct variable group: 𝑥,𝐴 Allowed substitution hints: 𝑃(𝑥) 𝑍(𝑥)

**Proof of Theorem lgslem4**
Step	Hyp	Ref	Expression
1		eldifi 3272	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
2	1	adantl 277	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝑃 ∈ ℙ)
3		simpl 109	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝐴 ∈ ℤ)
4		oddprm 12294	. . . . . . . 8 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
5	4	adantl 277	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((𝑃 − 1) / 2) ∈ ℕ)
6		prmdvdsexp 12183	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈ ℕ) → (𝑃 ∥ (𝐴↑((𝑃 − 1) / 2)) ↔ 𝑃 ∥ 𝐴))
7	2, 3, 5, 6	syl3anc 1249	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 ∥ (𝐴↑((𝑃 − 1) / 2)) ↔ 𝑃 ∥ 𝐴))
8	7	biimpar 297	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑃 ∥ 𝐴) → 𝑃 ∥ (𝐴↑((𝑃 − 1) / 2)))
9		prmgt1 12167	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
10	1, 9	syl 14	. . . . . 6 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 1 < 𝑃)
11	10	ad2antlr 489	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑃 ∥ 𝐴) → 1 < 𝑃)
12		p1modz1 11836	. . . . 5 ⊢ ((𝑃 ∥ (𝐴↑((𝑃 − 1) / 2)) ∧ 1 < 𝑃) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 1)
13	8, 11, 12	syl2anc 411	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 1)
14	13	oveq1d 5912	. . 3 ⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (1 − 1))
15		1m1e0 9019	. . . 4 ⊢ (1 − 1) = 0
16		lgslem2.z	. . . . . 6 ⊢ 𝑍 = {𝑥 ∈ ℤ ∣ (abs‘𝑥) ≤ 1}
17	16	lgslem2 14880	. . . . 5 ⊢ (-1 ∈ 𝑍 ∧ 0 ∈ 𝑍 ∧ 1 ∈ 𝑍)
18	17	simp2i 1009	. . . 4 ⊢ 0 ∈ 𝑍
19	15, 18	eqeltri 2262	. . 3 ⊢ (1 − 1) ∈ 𝑍
20	14, 19	eqeltrdi 2280	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)
21		lgslem1 14879	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2})
22		elpri 3630	. . . 4 ⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2} → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2))
23		oveq1 5904	. . . . . 6 ⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (0 − 1))
24		df-neg 8162	. . . . . . 7 ⊢ -1 = (0 − 1)
25	17	simp1i 1008	. . . . . . 7 ⊢ -1 ∈ 𝑍
26	24, 25	eqeltrri 2263	. . . . . 6 ⊢ (0 − 1) ∈ 𝑍
27	23, 26	eqeltrdi 2280	. . . . 5 ⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)
28		oveq1 5904	. . . . . 6 ⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2 → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) = (2 − 1))
29		2m1e1 9068	. . . . . . 7 ⊢ (2 − 1) = 1
30	17	simp3i 1010	. . . . . . 7 ⊢ 1 ∈ 𝑍
31	29, 30	eqeltri 2262	. . . . . 6 ⊢ (2 − 1) ∈ 𝑍
32	28, 31	eqeltrdi 2280	. . . . 5 ⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2 → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)
33	27, 32	jaoi 717	. . . 4 ⊢ (((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)
34	21, 22, 33	3syl 17	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)
35	34	3expa 1205	. 2 ⊢ (((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)
36		prmnn 12145	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
37	1, 36	syl 14	. . . . 5 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℕ)
38	37	adantl 277	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → 𝑃 ∈ ℕ)
39		dvdsdc 11840	. . . 4 ⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ) → DECID 𝑃 ∥ 𝐴)
40	38, 3, 39	syl2anc 411	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → DECID 𝑃 ∥ 𝐴)
41		exmiddc 837	. . 3 ⊢ (DECID 𝑃 ∥ 𝐴 → (𝑃 ∥ 𝐴 ∨ ¬ 𝑃 ∥ 𝐴))
42	40, 41	syl 14	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → (𝑃 ∥ 𝐴 ∨ ¬ 𝑃 ∥ 𝐴))
43	20, 35, 42	mpjaodan 799	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) − 1) ∈ 𝑍)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 DECID wdc 835 ∧ w3a 980 = wceq 1364 ∈ wcel 2160 {crab 2472 ∖ cdif 3141 {csn 3607 {cpr 3608 class class class wbr 4018 ‘cfv 5235 (class class class)co 5897 0cc0 7842 1c1 7843 + caddc 7845 < clt 8023 ≤ cle 8024 − cmin 8159 -cneg 8160 / cdiv 8660 ℕcn 8950 2c2 9001 ℤcz 9284 mod cmo 10355 ↑cexp 10553 abscabs 11041 ∥ cdvds 11829 ℙcprime 12142

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4192 ax-pr 4227 ax-un 4451 ax-setind 4554 ax-iinf 4605 ax-cnex 7933 ax-resscn 7934 ax-1cn 7935 ax-1re 7936 ax-icn 7937 ax-addcl 7938 ax-addrcl 7939 ax-mulcl 7940 ax-mulrcl 7941 ax-addcom 7942 ax-mulcom 7943 ax-addass 7944 ax-mulass 7945 ax-distr 7946 ax-i2m1 7947 ax-0lt1 7948 ax-1rid 7949 ax-0id 7950 ax-rnegex 7951 ax-precex 7952 ax-cnre 7953 ax-pre-ltirr 7954 ax-pre-ltwlin 7955 ax-pre-lttrn 7956 ax-pre-apti 7957 ax-pre-ltadd 7958 ax-pre-mulgt0 7959 ax-pre-mulext 7960 ax-arch 7961 ax-caucvg 7962

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 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4311 df-po 4314 df-iso 4315 df-iord 4384 df-on 4386 df-ilim 4387 df-suc 4389 df-iom 4608 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-rn 4655 df-res 4656 df-ima 4657 df-iota 5196 df-fun 5237 df-fn 5238 df-f 5239 df-f1 5240 df-fo 5241 df-f1o 5242 df-fv 5243 df-isom 5244 df-riota 5852 df-ov 5900 df-oprab 5901 df-mpo 5902 df-1st 6166 df-2nd 6167 df-recs 6331 df-irdg 6396 df-frec 6417 df-1o 6442 df-2o 6443 df-oadd 6446 df-er 6560 df-en 6768 df-dom 6769 df-fin 6770 df-sup 7014 df-pnf 8025 df-mnf 8026 df-xr 8027 df-ltxr 8028 df-le 8029 df-sub 8161 df-neg 8162 df-reap 8563 df-ap 8570 df-div 8661 df-inn 8951 df-2 9009 df-3 9010 df-4 9011 df-n0 9208 df-z 9285 df-uz 9560 df-q 9652 df-rp 9686 df-fz 10041 df-fzo 10175 df-fl 10303 df-mod 10356 df-seqfrec 10479 df-exp 10554 df-ihash 10791 df-cj 10886 df-re 10887 df-im 10888 df-rsqrt 11042 df-abs 11043 df-clim 11322 df-proddc 11594 df-dvds 11830 df-gcd 11979 df-prm 12143 df-phi 12246

This theorem is referenced by: lgsfcl2 14885

W3C validator