isprm5lem - Intuitionistic Logic Explorer

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

Theorem isprm5lem 12154

Description: Lemma for isprm5 12155. The interesting direction (showing that one only needs to check prime divisors up to the square root of

). (Contributed by Jim Kingdon, 20-Oct-2024.)

**Hypotheses**
Ref	Expression
isprm5lem.p
isprm5lem.z
isprm5lem.x

**Assertion**
Ref	Expression
isprm5lem

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem isprm5lem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isprm5lem.x	. . 3
2		elfzuz 10034	. . 3
3		exprmfct 12151	. . 3
4	1, 2, 3	3syl 17	. 2
5		simpr 110	. . . . 5 $/\$ $/\$ $/\$
6		oveq1 5895	. . . . . . . 8
7	6	breq1d 4025	. . . . . . 7
8		breq1 4018	. . . . . . . 8
9	8	notbid 668	. . . . . . 7
10	7, 9	imbi12d 234	. . . . . 6
11		isprm5lem.z	. . . . . . 7
12	11	ad2antrr 488	. . . . . 6 $/\$ $/\$ $/\$
13		simplrl 535	. . . . . 6 $/\$ $/\$ $/\$
14	10, 12, 13	rspcdva 2858	. . . . 5 $/\$ $/\$ $/\$
15	5, 14	mpd 13	. . . 4 $/\$ $/\$ $/\$
16		prmz 12124	. . . . . . 7
17	16	ad2antrl 490	. . . . . 6 $/\$ $/\$
18	17	ad2antrr 488	. . . . 5 $/\$ $/\$ $/\$ $/\$
19		elfzelz 10038	. . . . . . . 8
20	1, 19	syl 14	. . . . . . 7
21	20	ad2antrr 488	. . . . . 6 $/\$ $/\$ $/\$
22	21	adantlr 477	. . . . 5 $/\$ $/\$ $/\$ $/\$
23		isprm5lem.p	. . . . . . . 8
24		eluzelz 9550	. . . . . . . 8
25	23, 24	syl 14	. . . . . . 7
26	25	ad2antrr 488	. . . . . 6 $/\$ $/\$ $/\$
27	26	adantlr 477	. . . . 5 $/\$ $/\$ $/\$ $/\$
28		simplrr 536	. . . . . 6 $/\$ $/\$ $/\$
29	28	adantlr 477	. . . . 5 $/\$ $/\$ $/\$ $/\$
30		simpr 110	. . . . 5 $/\$ $/\$ $/\$ $/\$
31	18, 22, 27, 29, 30	dvdstrd 11850	. . . 4 $/\$ $/\$ $/\$ $/\$
32	15, 31	mtand 666	. . 3 $/\$ $/\$ $/\$
33	17	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
34	21	adantlr 477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
35	25	adantr 276	. . . . . . . . . 10 $/\$ $/\$
36	35	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
37	28	adantlr 477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
38		simpr 110	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
39	33, 34, 36, 37, 38	dvdstrd 11850	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
40	17	adantr 276	. . . . . . . . . 10 $/\$ $/\$ $/\$
41		prmnn 12123	. . . . . . . . . . . . 13
42	41	nnne0d 8977	. . . . . . . . . . . 12
43	42	ad2antrl 490	. . . . . . . . . . 11 $/\$ $/\$
44	43	adantr 276	. . . . . . . . . 10 $/\$ $/\$ $/\$
45	25	ad2antrr 488	. . . . . . . . . 10 $/\$ $/\$ $/\$
46		dvdsval2 11810	. . . . . . . . . 10 $/\$ $/\$
47	40, 44, 45, 46	syl3anc 1248	. . . . . . . . 9 $/\$ $/\$ $/\$
48	47	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
49	39, 48	mpbid 147	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
50	40	zred 9388	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
51	50	recnd 7999	. . . . . . . . . . 11 $/\$ $/\$ $/\$
52	51	mulid2d 7989	. . . . . . . . . 10 $/\$ $/\$ $/\$
53		2nn 9093	. . . . . . . . . . . . . . 15
54		fzssnn 10081	. . . . . . . . . . . . . . 15
55	53, 54	ax-mp 5	. . . . . . . . . . . . . 14
56	55, 1	sselid 3165	. . . . . . . . . . . . 13
57	56	ad2antrr 488	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
58	57	nnred 8945	. . . . . . . . . . 11 $/\$ $/\$ $/\$
59	25	zred 9388	. . . . . . . . . . . 12
60	59	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$ $/\$
61		simplrr 536	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
62		dvdsle 11863	. . . . . . . . . . . . 13 $/\$
63	40, 57, 62	syl2anc 411	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
64	61, 63	mpd 13	. . . . . . . . . . 11 $/\$ $/\$ $/\$
65		elfzle2 10041	. . . . . . . . . . . . . 14
66	1, 65	syl 14	. . . . . . . . . . . . 13
67		zltlem1 9323	. . . . . . . . . . . . . 14 $/\$
68	20, 25, 67	syl2anc 411	. . . . . . . . . . . . 13
69	66, 68	mpbird 167	. . . . . . . . . . . 12
70	69	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$ $/\$
71	50, 58, 60, 64, 70	lelttrd 8095	. . . . . . . . . 10 $/\$ $/\$ $/\$
72	52, 71	eqbrtrd 4037	. . . . . . . . 9 $/\$ $/\$ $/\$
73		1red 7985	. . . . . . . . . 10 $/\$ $/\$ $/\$
74	41	nnrpd 9707	. . . . . . . . . . . 12
75	74	ad2antrl 490	. . . . . . . . . . 11 $/\$ $/\$
76	75	adantr 276	. . . . . . . . . 10 $/\$ $/\$ $/\$
77	73, 60, 76	ltmuldivd 9757	. . . . . . . . 9 $/\$ $/\$ $/\$
78	72, 77	mpbid 147	. . . . . . . 8 $/\$ $/\$ $/\$
79	78	adantr 276	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
80		eluz2b1 9614	. . . . . . 7 $/\$
81	49, 79, 80	sylanbrc 417	. . . . . 6 $/\$ $/\$ $/\$ $/\$
82		exprmfct 12151	. . . . . 6
83	81, 82	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
84		prmz 12124	. . . . . . . 8
85	84	ad2antrl 490	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86	49	adantr 276	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	45	ad2antrr 488	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88		simprr 531	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89	39	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90	44	ad2antrr 488	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91		divconjdvds 11868	. . . . . . . 8 $/\$
92	89, 90, 91	syl2anc 411	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	85, 86, 87, 88, 92	dvdstrd 11850	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	85	zred 9388	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	94	resqcld 10693	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	60	ad2antrr 488	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	81	adantr 276	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98		eluz2nn 9579	. . . . . . . . . . . 12
99	97, 98	syl 14	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	99	nnred 8945	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	resqcld 10693	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		dvdsle 11863	. . . . . . . . . . . 12 $/\$
103	85, 99, 102	syl2anc 411	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	88, 103	mpd 13	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105		prmnn 12123	. . . . . . . . . . . . . 14
106	105	nnnn0d 9242	. . . . . . . . . . . . 13
107	106	nn0ge0d 9245	. . . . . . . . . . . 12
108	107	ad2antrl 490	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109		0red 7971	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110		1red 7985	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111		0le1 8451	. . . . . . . . . . . . 13
112	111	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113	99	nnge1d 8975	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	109, 110, 100, 112, 113	letrd 8094	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	94, 100, 108, 114	le2sqd 10699	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116	104, 115	mpbid 147	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
117	60	recnd 7999	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	41	ad2antrl 490	. . . . . . . . . . . . . 14 $/\$ $/\$
119	118	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120	119	nnap0d 8978	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ #
121	117, 51, 120	sqdivapd 10680	. . . . . . . . . . 11 $/\$ $/\$ $/\$
122	117	sqvald 10664	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
123	50	resqcld 10693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
124		eluz2nn 9579	. . . . . . . . . . . . . . . . 17
125	23, 124	syl 14	. . . . . . . . . . . . . . . 16
126	125	nnrpd 9707	. . . . . . . . . . . . . . 15
127	126	ad2antrr 488	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
128		simpr 110	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
129	60, 123, 127, 128	ltmul2dd 9766	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
130	122, 129	eqbrtrd 4037	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	60	resqcld 10693	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
132	119	nnsqcld 10688	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
133	132	nnrpd 9707	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
134	131, 60, 133	ltdivmul2d 9762	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
135	130, 134	mpbird 167	. . . . . . . . . . 11 $/\$ $/\$ $/\$
136	121, 135	eqbrtrd 4037	. . . . . . . . . 10 $/\$ $/\$ $/\$
137	136	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
138	95, 101, 96, 116, 137	lelttrd 8095	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
139	95, 96, 138	ltled 8089	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140		oveq1 5895	. . . . . . . . . 10
141	140	breq1d 4025	. . . . . . . . 9
142		breq1 4018	. . . . . . . . . 10
143	142	notbid 668	. . . . . . . . 9
144	141, 143	imbi12d 234	. . . . . . . 8
145	11	ad4antr 494	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146		simprl 529	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	144, 145, 146	rspcdva 2858	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
148	139, 147	mpd 13	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149	93, 148	pm2.21fal 1383	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
150	83, 149	rexlimddv 2609	. . . 4 $/\$ $/\$ $/\$ $/\$
151	150	inegd 1382	. . 3 $/\$ $/\$ $/\$
152		zsqcl 10604	. . . . 5
153	17, 152	syl 14	. . . 4 $/\$ $/\$
154		zlelttric 9311	. . . 4 $/\$ $\/$
155	153, 35, 154	syl2anc 411	. . 3 $/\$ $/\$ $\/$
156	32, 151, 155	mpjaodan 799	. 2 $/\$ $/\$
157	4, 156	rexlimddv 2609	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709

wfal 1368

wcel 2158

wne 2357

wral 2465

wrex 2466

wss 3141 class class class wbr 4015

cfv 5228 (class class class)co 5888

cr 7823

cc0 7824

c1 7825

cmul 7829

clt 8005

cle 8006

cmin 8141

cdiv 8642

cn 8932

c2 8983

cz 9266

cuz 9541

crp 9666

cfz 10021

cexp 10532

cdvds 11807

cprime 12120

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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-coll 4130 ax-sep 4133 ax-nul 4141 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-setind 4548 ax-iinf 4599 ax-cnex 7915 ax-resscn 7916 ax-1cn 7917 ax-1re 7918 ax-icn 7919 ax-addcl 7920 ax-addrcl 7921 ax-mulcl 7922 ax-mulrcl 7923 ax-addcom 7924 ax-mulcom 7925 ax-addass 7926 ax-mulass 7927 ax-distr 7928 ax-i2m1 7929 ax-0lt1 7930 ax-1rid 7931 ax-0id 7932 ax-rnegex 7933 ax-precex 7934 ax-cnre 7935 ax-pre-ltirr 7936 ax-pre-ltwlin 7937 ax-pre-lttrn 7938 ax-pre-apti 7939 ax-pre-ltadd 7940 ax-pre-mulgt0 7941 ax-pre-mulext 7942 ax-arch 7943 ax-caucvg 7944

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ne 2358 df-nel 2453 df-ral 2470 df-rex 2471 df-reu 2472 df-rmo 2473 df-rab 2474 df-v 2751 df-sbc 2975 df-csb 3070 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-nul 3435 df-if 3547 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-int 3857 df-iun 3900 df-br 4016 df-opab 4077 df-mpt 4078 df-tr 4114 df-id 4305 df-po 4308 df-iso 4309 df-iord 4378 df-on 4380 df-ilim 4381 df-suc 4383 df-iom 4602 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-rn 4649 df-res 4650 df-ima 4651 df-iota 5190 df-fun 5230 df-fn 5231 df-f 5232 df-f1 5233 df-fo 5234 df-f1o 5235 df-fv 5236 df-riota 5844 df-ov 5891 df-oprab 5892 df-mpo 5893 df-1st 6154 df-2nd 6155 df-recs 6319 df-frec 6405 df-1o 6430 df-2o 6431 df-er 6548 df-en 6754 df-pnf 8007 df-mnf 8008 df-xr 8009 df-ltxr 8010 df-le 8011 df-sub 8143 df-neg 8144 df-reap 8545 df-ap 8552 df-div 8643 df-inn 8933 df-2 8991 df-3 8992 df-4 8993 df-n0 9190 df-z 9267 df-uz 9542 df-q 9633 df-rp 9667 df-fz 10022 df-fzo 10156 df-fl 10283 df-mod 10336 df-seqfrec 10459 df-exp 10533 df-cj 10864 df-re 10865 df-im 10866 df-rsqrt 11020 df-abs 11021 df-dvds 11808 df-prm 12121

This theorem is referenced by: isprm5 12155

W3C validator