2lgslem1a - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 2lgslem1a		Unicode version

Theorem 2lgslem1a 15948

Description: Lemma 1 for 2lgslem1 15951. (Contributed by AV, 18-Jun-2021.)

**Assertion**
Ref	Expression
2lgslem1a	$/\$ $/\$

Distinct variable group:

Proof of Theorem 2lgslem1a Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmnn 12800	. . . . . . . . . 10
2	1	nnnn0d 9549	. . . . . . . . 9
3	2	ad2antrr 488	. . . . . . . 8 $/\$ $/\$
4		4nn 9397	. . . . . . . 8
5	3, 4	jctir 313	. . . . . . 7 $/\$ $/\$ $/\$
6		fldivnn0 10651	. . . . . . 7 $/\$
7		nn0p1nn 9531	. . . . . . 7
8	5, 6, 7	3syl 17	. . . . . 6 $/\$ $/\$
9		elnnuz 9887	. . . . . 6
10	8, 9	sylib 122	. . . . 5 $/\$ $/\$
11		fzss1 10393	. . . . 5
12		rexss 3304	. . . . 5 $/\$
13	10, 11, 12	3syl 17	. . . 4 $/\$ $/\$ $/\$
14		ancom 266	. . . . . 6 $/\$ $/\$
15	2, 4	jctir 313	. . . . . . . . . . . . . . . . 17 $/\$
16	15, 6	syl 14	. . . . . . . . . . . . . . . 16
17	16	nn0zd 9694	. . . . . . . . . . . . . . 15
18	17	ad2antrr 488	. . . . . . . . . . . . . 14 $/\$ $/\$
19		elfzelz 10355	. . . . . . . . . . . . . 14
20		zltp1le 9628	. . . . . . . . . . . . . 14 $/\$
21	18, 19, 20	syl2an 289	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
22	21	bicomd 141	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
23	22	anbi1d 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
24	19	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
25	17	peano2zd 9699	. . . . . . . . . . . . . 14
26	25	adantr 276	. . . . . . . . . . . . 13 $/\$
27	26	ad2antrr 488	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
28		prmz 12801	. . . . . . . . . . . . . . 15
29		oddm1d2 12571	. . . . . . . . . . . . . . 15
30	28, 29	syl 14	. . . . . . . . . . . . . 14
31	30	biimpa 296	. . . . . . . . . . . . 13 $/\$
32	31	ad2antrr 488	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
33		elfz 10344	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
34	24, 27, 32, 33	syl3anc 1274	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
35		elfzle2 10358	. . . . . . . . . . . . 13
36	35	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
37	36	biantrud 304	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
38	23, 34, 37	3bitr4d 220	. . . . . . . . . 10 $/\$ $/\$ $/\$
39	28	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$
40		2lgslem1a2 15947	. . . . . . . . . . 11 $/\$
41	39, 19, 40	syl2an 289	. . . . . . . . . 10 $/\$ $/\$ $/\$
42	38, 41	bitrd 188	. . . . . . . . 9 $/\$ $/\$ $/\$
43		2lgslem1a1 15946	. . . . . . . . . . . . 13 $/\$
44	1, 43	sylan 283	. . . . . . . . . . . 12 $/\$
45	44	adantr 276	. . . . . . . . . . 11 $/\$ $/\$
46		oveq1 6056	. . . . . . . . . . . . 13
47	46	oveq1d 6064	. . . . . . . . . . . . 13
48	46, 47	eqeq12d 2247	. . . . . . . . . . . 12
49	48	rspccva 2919	. . . . . . . . . . 11 $/\$
50	45, 49	sylan 283	. . . . . . . . . 10 $/\$ $/\$ $/\$
51	50	breq2d 4120	. . . . . . . . 9 $/\$ $/\$ $/\$
52	42, 51	bitrd 188	. . . . . . . 8 $/\$ $/\$ $/\$
53		oveq1 6056	. . . . . . . . . 10
54	53	eqcomd 2238	. . . . . . . . 9
55	54	breq2d 4120	. . . . . . . 8
56	52, 55	sylan9bb 462	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
57	56	pm5.32da 452	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
58	14, 57	bitrid 192	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
59	58	rexbidva 2539	. . . 4 $/\$ $/\$ $/\$ $/\$
60	13, 59	bitrd 188	. . 3 $/\$ $/\$ $/\$
61	60	bicomd 141	. 2 $/\$ $/\$ $/\$
62	61	rabbidva 2800	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105

wceq 1398

wcel 2203

wral 2520

wrex 2521

crab 2524

wss 3210 class class class wbr 4108

cfv 5351 (class class class)co 6049

c1 8124

caddc 8126

cmul 8128

clt 8304

cle 8305

cmin 8440

cdiv 8942

cn 9233

c2 9284

c4 9286

cn0 9492

cz 9573

cuz 9849

cfz 10338

cfl 10624

cmo 10680

cdvds 12466

cprime 12797

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-sep 4227 ax-pow 4286 ax-pr 4321 ax-un 4553 ax-setind 4658 ax-cnex 8214 ax-resscn 8215 ax-1cn 8216 ax-1re 8217 ax-icn 8218 ax-addcl 8219 ax-addrcl 8220 ax-mulcl 8221 ax-mulrcl 8222 ax-addcom 8223 ax-mulcom 8224 ax-addass 8225 ax-mulass 8226 ax-distr 8227 ax-i2m1 8228 ax-0lt1 8229 ax-1rid 8230 ax-0id 8231 ax-rnegex 8232 ax-precex 8233 ax-cnre 8234 ax-pre-ltirr 8235 ax-pre-ltwlin 8236 ax-pre-lttrn 8237 ax-pre-apti 8238 ax-pre-ltadd 8239 ax-pre-mulgt0 8240 ax-pre-mulext 8241 ax-arch 8242

This theorem depends on definitions: df-bi 117 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-xor 1421 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rmo 2528 df-rab 2529 df-v 2814 df-sbc 3042 df-csb 3138 df-dif 3212 df-un 3214 df-in 3216 df-ss 3223 df-pw 3670 df-sn 3694 df-pr 3695 df-op 3697 df-uni 3914 df-int 3949 df-iun 3992 df-br 4109 df-opab 4171 df-mpt 4172 df-id 4413 df-po 4416 df-iso 4417 df-xp 4754 df-rel 4755 df-cnv 4756 df-co 4757 df-dm 4758 df-rn 4759 df-res 4760 df-ima 4761 df-iota 5311 df-fun 5353 df-fn 5354 df-f 5355 df-fv 5359 df-riota 6002 df-ov 6052 df-oprab 6053 df-mpo 6054 df-1st 6333 df-2nd 6334 df-pnf 8306 df-mnf 8307 df-xr 8308 df-ltxr 8309 df-le 8310 df-sub 8442 df-neg 8443 df-reap 8845 df-ap 8852 df-div 8943 df-inn 9234 df-2 9292 df-3 9293 df-4 9294 df-n0 9493 df-z 9574 df-uz 9850 df-q 9948 df-rp 9983 df-fz 10339 df-fl 10626 df-mod 10681 df-dvds 12467 df-prm 12798

This theorem is referenced by: 2lgslem1 15951

W3C validator