Theorem isprm3 12680

Description: The predicate "is a prime number". A prime number is an integer greater than or equal to 2 with no divisors strictly between 1 and itself. (Contributed by Paul Chapman, 26-Oct-2012.)

Assertion

Ref	Expression
isprm3	|- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( 2 ... ( P - 1 ) ) -. z || P ) )

Distinct variable group:   z, P

Proof of Theorem isprm3

Step	Hyp	Ref	Expression
1		isprm2 12679	. 2 |- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) )
2		dvdszrcl 12343	. . . . . . . . . . 11 |- ( z || P -> ( z e. ZZ /\ P e. ZZ ) )
3	2	simpld 112	. . . . . . . . . 10 |- ( z || P -> z e. ZZ )
4		1zzd 9496	. . . . . . . . . 10 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> 1 e. ZZ )
5		zdceq 9545	. . . . . . . . . 10 |- ( ( z e. ZZ /\ 1 e. ZZ ) -> DECID z = 1 )
6	3, 4, 5	syl2an2 596	. . . . . . . . 9 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> DECID z = 1 )
7	2	simprd 114	. . . . . . . . . . 11 |- ( z || P -> P e. ZZ )
8	7	adantl 277	. . . . . . . . . 10 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> P e. ZZ )
9		zdceq 9545	. . . . . . . . . 10 |- ( ( z e. ZZ /\ P e. ZZ ) -> DECID z = P )
10	3, 8, 9	syl2an2 596	. . . . . . . . 9 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> DECID z = P )
11		dcor 941	. . . . . . . . 9 |- (DECID z = 1 -> (DECID z = P -> DECID ( z = 1 \/ z = P ) ) )
12	6, 10, 11	sylc 62	. . . . . . . 8 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> DECID ( z = 1 \/ z = P ) )
13		imandc 894	. . . . . . . 8 |- (DECID ( z = 1 \/ z = P ) -> ( ( z e. NN -> ( z = 1 \/ z = P ) ) <-> -. ( z e. NN /\ -. ( z = 1 \/ z = P ) ) ) )
14	12, 13	syl 14	. . . . . . 7 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( ( z e. NN -> ( z = 1 \/ z = P ) ) <-> -. ( z e. NN /\ -. ( z = 1 \/ z = P ) ) ) )
15		eluz2nn 9790	. . . . . . . . . . . . . . . 16 |- ( P e. ( ZZ>= ` 2 ) -> P e. NN )
16		nnz 9488	. . . . . . . . . . . . . . . . . 18 |- ( z e. NN -> z e. ZZ )
17		dvdsle 12395	. . . . . . . . . . . . . . . . . 18 |- ( ( z e. ZZ /\ P e. NN ) -> ( z || P -> z <_ P ) )
18	16, 17	sylan 283	. . . . . . . . . . . . . . . . 17 |- ( ( z e. NN /\ P e. NN ) -> ( z || P -> z <_ P ) )
19		nnge1 9156	. . . . . . . . . . . . . . . . . 18 |- ( z e. NN -> 1 <_ z )
20	19	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( z e. NN /\ P e. NN ) -> 1 <_ z )
21	18, 20	jctild 316	. . . . . . . . . . . . . . . 16 |- ( ( z e. NN /\ P e. NN ) -> ( z || P -> ( 1 <_ z /\ z <_ P ) ) )
22	15, 21	sylan2 286	. . . . . . . . . . . . . . 15 |- ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) -> ( z || P -> ( 1 <_ z /\ z <_ P ) ) )
23		nnz 9488	. . . . . . . . . . . . . . . . . 18 |- ( P e. NN -> P e. ZZ )
24		zre 9473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z e. ZZ -> z e. RR )
25		1re 8168	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 e. RR
26		leltap 8795	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 1 e. RR /\ z e. RR /\ 1 <_ z ) -> ( 1 < z <-> z # 1 ) )
27	25, 26	mp3an1 1358	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( z e. RR /\ 1 <_ z ) -> ( 1 < z <-> z # 1 ) )
28	24, 27	sylan 283	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( z e. ZZ /\ 1 <_ z ) -> ( 1 < z <-> z # 1 ) )
29		1z 9495	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 e. ZZ
30		zapne 9544	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( z e. ZZ /\ 1 e. ZZ ) -> ( z # 1 <-> z =/= 1 ) )
31	29, 30	mpan2 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z e. ZZ -> ( z # 1 <-> z =/= 1 ) )
32	31	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( z e. ZZ /\ 1 <_ z ) -> ( z # 1 <-> z =/= 1 ) )
33	28, 32	bitrd 188	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z e. ZZ /\ 1 <_ z ) -> ( 1 < z <-> z =/= 1 ) )
34	33	3adant2 1040	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z e. ZZ /\ P e. ZZ /\ 1 <_ z ) -> ( 1 < z <-> z =/= 1 ) )
35	34	3expia 1229	. . . . . . . . . . . . . . . . . . 19 |- ( ( z e. ZZ /\ P e. ZZ ) -> ( 1 <_ z -> ( 1 < z <-> z =/= 1 ) ) )
36		zre 9473	. . . . . . . . . . . . . . . . . . . . . 22 |- ( P e. ZZ -> P e. RR )
37		leltap 8795	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( z e. RR /\ P e. RR /\ z <_ P ) -> ( z < P <-> P # z ) )
38	24, 37	syl3an1 1304	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( z e. ZZ /\ P e. RR /\ z <_ P ) -> ( z < P <-> P # z ) )
39	36, 38	syl3an2 1305	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z e. ZZ /\ P e. ZZ /\ z <_ P ) -> ( z < P <-> P # z ) )
40		zapne 9544	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( P e. ZZ /\ z e. ZZ ) -> ( P # z <-> P =/= z ) )
41	40	ancoms 268	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( z e. ZZ /\ P e. ZZ ) -> ( P # z <-> P =/= z ) )
42	41	3adant3 1041	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( z e. ZZ /\ P e. ZZ /\ z <_ P ) -> ( P # z <-> P =/= z ) )
43	39, 42	bitrd 188	. . . . . . . . . . . . . . . . . . . 20 |- ( ( z e. ZZ /\ P e. ZZ /\ z <_ P ) -> ( z < P <-> P =/= z ) )
44	43	3expia 1229	. . . . . . . . . . . . . . . . . . 19 |- ( ( z e. ZZ /\ P e. ZZ ) -> ( z <_ P -> ( z < P <-> P =/= z ) ) )
45	35, 44	anim12d 335	. . . . . . . . . . . . . . . . . 18 |- ( ( z e. ZZ /\ P e. ZZ ) -> ( ( 1 <_ z /\ z <_ P ) -> ( ( 1 < z <-> z =/= 1 ) /\ ( z < P <-> P =/= z ) ) ) )
46	23, 45	sylan2 286	. . . . . . . . . . . . . . . . 17 |- ( ( z e. ZZ /\ P e. NN ) -> ( ( 1 <_ z /\ z <_ P ) -> ( ( 1 < z <-> z =/= 1 ) /\ ( z < P <-> P =/= z ) ) ) )
47		pm4.38 607	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 1 < z <-> z =/= 1 ) /\ ( z < P <-> P =/= z ) ) -> ( ( 1 < z /\ z < P ) <-> ( z =/= 1 /\ P =/= z ) ) )
48		df-ne 2401	. . . . . . . . . . . . . . . . . . . 20 |- ( z =/= 1 <-> -. z = 1 )
49		nesym 2445	. . . . . . . . . . . . . . . . . . . 20 |- ( P =/= z <-> -. z = P )
50	48, 49	anbi12i 460	. . . . . . . . . . . . . . . . . . 19 |- ( ( z =/= 1 /\ P =/= z ) <-> ( -. z = 1 /\ -. z = P ) )
51		ioran 757	. . . . . . . . . . . . . . . . . . 19 |- ( -. ( z = 1 \/ z = P ) <-> ( -. z = 1 /\ -. z = P ) )
52	50, 51	bitr4i 187	. . . . . . . . . . . . . . . . . 18 |- ( ( z =/= 1 /\ P =/= z ) <-> -. ( z = 1 \/ z = P ) )
53	47, 52	bitrdi 196	. . . . . . . . . . . . . . . . 17 |- ( ( ( 1 < z <-> z =/= 1 ) /\ ( z < P <-> P =/= z ) ) -> ( ( 1 < z /\ z < P ) <-> -. ( z = 1 \/ z = P ) ) )
54	46, 53	syl6 33	. . . . . . . . . . . . . . . 16 |- ( ( z e. ZZ /\ P e. NN ) -> ( ( 1 <_ z /\ z <_ P ) -> ( ( 1 < z /\ z < P ) <-> -. ( z = 1 \/ z = P ) ) ) )
55	16, 15, 54	syl2an 289	. . . . . . . . . . . . . . 15 |- ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) -> ( ( 1 <_ z /\ z <_ P ) -> ( ( 1 < z /\ z < P ) <-> -. ( z = 1 \/ z = P ) ) ) )
56	22, 55	syld 45	. . . . . . . . . . . . . 14 |- ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) -> ( z || P -> ( ( 1 < z /\ z < P ) <-> -. ( z = 1 \/ z = P ) ) ) )
57	56	imp 124	. . . . . . . . . . . . 13 |- ( ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) /\ z || P ) -> ( ( 1 < z /\ z < P ) <-> -. ( z = 1 \/ z = P ) ) )
58		eluzelz 9755	. . . . . . . . . . . . . . 15 |- ( P e. ( ZZ>= ` 2 ) -> P e. ZZ )
59		zltp1le 9524	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 1 e. ZZ /\ z e. ZZ ) -> ( 1 < z <-> ( 1 + 1 ) <_ z ) )
60	29, 59	mpan 424	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ZZ -> ( 1 < z <-> ( 1 + 1 ) <_ z ) )
61		df-2 9192	. . . . . . . . . . . . . . . . . . . 20 |- 2 = ( 1 + 1 )
62	61	breq1i 4093	. . . . . . . . . . . . . . . . . . 19 |- ( 2 <_ z <-> ( 1 + 1 ) <_ z )
63	60, 62	bitr4di 198	. . . . . . . . . . . . . . . . . 18 |- ( z e. ZZ -> ( 1 < z <-> 2 <_ z ) )
64	63	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( z e. ZZ /\ P e. ZZ ) -> ( 1 < z <-> 2 <_ z ) )
65		zltlem1 9527	. . . . . . . . . . . . . . . . 17 |- ( ( z e. ZZ /\ P e. ZZ ) -> ( z < P <-> z <_ ( P - 1 ) ) )
66	64, 65	anbi12d 473	. . . . . . . . . . . . . . . 16 |- ( ( z e. ZZ /\ P e. ZZ ) -> ( ( 1 < z /\ z < P ) <-> ( 2 <_ z /\ z <_ ( P - 1 ) ) ) )
67		peano2zm 9507	. . . . . . . . . . . . . . . . 17 |- ( P e. ZZ -> ( P - 1 ) e. ZZ )
68		2z 9497	. . . . . . . . . . . . . . . . . 18 |- 2 e. ZZ
69		elfz 10239	. . . . . . . . . . . . . . . . . 18 |- ( ( z e. ZZ /\ 2 e. ZZ /\ ( P - 1 ) e. ZZ ) -> ( z e. ( 2 ... ( P - 1 ) ) <-> ( 2 <_ z /\ z <_ ( P - 1 ) ) ) )
70	68, 69	mp3an2 1359	. . . . . . . . . . . . . . . . 17 |- ( ( z e. ZZ /\ ( P - 1 ) e. ZZ ) -> ( z e. ( 2 ... ( P - 1 ) ) <-> ( 2 <_ z /\ z <_ ( P - 1 ) ) ) )
71	67, 70	sylan2 286	. . . . . . . . . . . . . . . 16 |- ( ( z e. ZZ /\ P e. ZZ ) -> ( z e. ( 2 ... ( P - 1 ) ) <-> ( 2 <_ z /\ z <_ ( P - 1 ) ) ) )
72	66, 71	bitr4d 191	. . . . . . . . . . . . . . 15 |- ( ( z e. ZZ /\ P e. ZZ ) -> ( ( 1 < z /\ z < P ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
73	16, 58, 72	syl2an 289	. . . . . . . . . . . . . 14 |- ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) -> ( ( 1 < z /\ z < P ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
74	73	adantr 276	. . . . . . . . . . . . 13 |- ( ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) /\ z || P ) -> ( ( 1 < z /\ z < P ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
75	57, 74	bitr3d 190	. . . . . . . . . . . 12 |- ( ( ( z e. NN /\ P e. ( ZZ>= ` 2 ) ) /\ z || P ) -> ( -. ( z = 1 \/ z = P ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
76	75	anasss 399	. . . . . . . . . . 11 |- ( ( z e. NN /\ ( P e. ( ZZ>= ` 2 ) /\ z || P ) ) -> ( -. ( z = 1 \/ z = P ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
77	76	expcom 116	. . . . . . . . . 10 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( z e. NN -> ( -. ( z = 1 \/ z = P ) <-> z e. ( 2 ... ( P - 1 ) ) ) ) )
78	77	pm5.32d 450	. . . . . . . . 9 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( ( z e. NN /\ -. ( z = 1 \/ z = P ) ) <-> ( z e. NN /\ z e. ( 2 ... ( P - 1 ) ) ) ) )
79		fzssuz 10290	. . . . . . . . . . . . 13 |- ( 2 ... ( P - 1 ) ) C_ ( ZZ>= ` 2 )
80		2eluzge1 9800	. . . . . . . . . . . . . 14 |- 2 e. ( ZZ>= ` 1 )
81		uzss 9767	. . . . . . . . . . . . . 14 |- ( 2 e. ( ZZ>= ` 1 ) -> ( ZZ>= ` 2 ) C_ ( ZZ>= ` 1 ) )
82	80, 81	ax-mp 5	. . . . . . . . . . . . 13 |- ( ZZ>= ` 2 ) C_ ( ZZ>= ` 1 )
83	79, 82	sstri 3234	. . . . . . . . . . . 12 |- ( 2 ... ( P - 1 ) ) C_ ( ZZ>= ` 1 )
84		nnuz 9782	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
85	83, 84	sseqtrri 3260	. . . . . . . . . . 11 |- ( 2 ... ( P - 1 ) ) C_ NN
86	85	sseli 3221	. . . . . . . . . 10 |- ( z e. ( 2 ... ( P - 1 ) ) -> z e. NN )
87	86	pm4.71ri 392	. . . . . . . . 9 |- ( z e. ( 2 ... ( P - 1 ) ) <-> ( z e. NN /\ z e. ( 2 ... ( P - 1 ) ) ) )
88	78, 87	bitr4di 198	. . . . . . . 8 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( ( z e. NN /\ -. ( z = 1 \/ z = P ) ) <-> z e. ( 2 ... ( P - 1 ) ) ) )
89	88	notbid 671	. . . . . . 7 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( -. ( z e. NN /\ -. ( z = 1 \/ z = P ) ) <-> -. z e. ( 2 ... ( P - 1 ) ) ) )
90	14, 89	bitrd 188	. . . . . 6 |- ( ( P e. ( ZZ>= ` 2 ) /\ z || P ) -> ( ( z e. NN -> ( z = 1 \/ z = P ) ) <-> -. z e. ( 2 ... ( P - 1 ) ) ) )
91	90	pm5.74da 443	. . . . 5 |- ( P e. ( ZZ>= ` 2 ) -> ( ( z || P -> ( z e. NN -> ( z = 1 \/ z = P ) ) ) <-> ( z || P -> -. z e. ( 2 ... ( P - 1 ) ) ) ) )
92		bi2.04 248	. . . . 5 |- ( ( z || P -> ( z e. NN -> ( z = 1 \/ z = P ) ) ) <-> ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) )
93		con2b 673	. . . . 5 |- ( ( z || P -> -. z e. ( 2 ... ( P - 1 ) ) ) <-> ( z e. ( 2 ... ( P - 1 ) ) -> -. z || P ) )
94	91, 92, 93	3bitr3g 222	. . . 4 |- ( P e. ( ZZ>= ` 2 ) -> ( ( z e. NN -> ( z || P -> ( z = 1 \/ z = P ) ) ) <-> ( z e. ( 2 ... ( P - 1 ) ) -> -. z || P ) ) )
95	94	ralbidv2 2532	. . 3 |- ( P e. ( ZZ>= ` 2 ) -> ( A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) <-> A. z e. ( 2 ... ( P - 1 ) ) -. z || P ) )
96	95	pm5.32i 454	. 2 |- ( ( P e. ( ZZ>= ` 2 ) /\ A. z e. NN ( z || P -> ( z = 1 \/ z = P ) ) ) <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( 2 ... ( P - 1 ) ) -. z || P ) )
97	1, 96	bitri 184	1 |- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( 2 ... ( P - 1 ) ) -. z || P ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 713  DECID wdc 839   /\ w3a 1002   = wceq 1395   e. wcel 2200   =/= wne 2400   A.wral 2508   C_ wss 3198   class class class wbr 4086   ` cfv 5324  (class class class)co 6013   RRcr 8021   1c1 8023   + caddc 8025   < clt 8204   <_ cle 8205   - cmin 8340   # cap 8751   NNcn 9133   2c2 9184   ZZcz 9469   ZZ>=cuz 9745   ...cfz 10233   || cdvds 12338   Primecprime 12669

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4202  ax-sep 4205  ax-nul 4213  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-iinf 4684  ax-cnex 8113  ax-resscn 8114  ax-1cn 8115  ax-1re 8116  ax-icn 8117  ax-addcl 8118  ax-addrcl 8119  ax-mulcl 8120  ax-mulrcl 8121  ax-addcom 8122  ax-mulcom 8123  ax-addass 8124  ax-mulass 8125  ax-distr 8126  ax-i2m1 8127  ax-0lt1 8128  ax-1rid 8129  ax-0id 8130  ax-rnegex 8131  ax-precex 8132  ax-cnre 8133  ax-pre-ltirr 8134  ax-pre-ltwlin 8135  ax-pre-lttrn 8136  ax-pre-apti 8137  ax-pre-ltadd 8138  ax-pre-mulgt0 8139  ax-pre-mulext 8140  ax-arch 8141  ax-caucvg 8142

This theorem depends on definitions:  df-bi 117  df-stab 836  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2802  df-sbc 3030  df-csb 3126  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-nul 3493  df-if 3604  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-iun 3970  df-br 4087  df-opab 4149  df-mpt 4150  df-tr 4186  df-id 4388  df-po 4391  df-iso 4392  df-iord 4461  df-on 4463  df-ilim 4464  df-suc 4466  df-iom 4687  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-res 4735  df-ima 4736  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-f1 5329  df-fo 5330  df-f1o 5331  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-1st 6298  df-2nd 6299  df-recs 6466  df-frec 6552  df-1o 6577  df-2o 6578  df-er 6697  df-en 6905  df-pnf 8206  df-mnf 8207  df-xr 8208  df-ltxr 8209  df-le 8210  df-sub 8342  df-neg 8343  df-reap 8745  df-ap 8752  df-div 8843  df-inn 9134  df-2 9192  df-3 9193  df-4 9194  df-n0 9393  df-z 9470  df-uz 9746  df-q 9844  df-rp 9879  df-fz 10234  df-seqfrec 10700  df-exp 10791  df-cj 11393  df-re 11394  df-im 11395  df-rsqrt 11549  df-abs 11550  df-dvds 12339  df-prm 12670

This theorem is referenced by:  prmind2  12682  2prm  12689  3prm  12690  prmdc  12692  isprm5  12704  mersenne  15711