![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > prmuz2 | Structured version Visualization version Unicode version |
Description: A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
Ref | Expression |
---|---|
prmuz2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isprm4 14683 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 466 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-cnex 9621 ax-resscn 9622 ax-1cn 9623 ax-icn 9624 ax-addcl 9625 ax-addrcl 9626 ax-mulcl 9627 ax-mulrcl 9628 ax-mulcom 9629 ax-addass 9630 ax-mulass 9631 ax-distr 9632 ax-i2m1 9633 ax-1ne0 9634 ax-1rid 9635 ax-rnegex 9636 ax-rrecex 9637 ax-cnre 9638 ax-pre-lttri 9639 ax-pre-lttrn 9640 ax-pre-ltadd 9641 ax-pre-mulgt0 9642 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-br 4417 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6277 df-ov 6318 df-oprab 6319 df-mpt2 6320 df-om 6720 df-wrecs 7054 df-recs 7116 df-rdg 7154 df-1o 7208 df-2o 7209 df-oadd 7212 df-er 7389 df-en 7596 df-dom 7597 df-sdom 7598 df-fin 7599 df-pnf 9703 df-mnf 9704 df-xr 9705 df-ltxr 9706 df-le 9707 df-sub 9888 df-neg 9889 df-nn 10638 df-2 10696 df-n0 10899 df-z 10967 df-uz 11189 df-dvds 14355 df-prm 14672 |
This theorem is referenced by: prmgt1 14692 prmn2uzge3 14693 prmm2nn0 14694 sqnprm 14695 isprm5 14700 prmrp 14707 isprm6 14715 prmdvdsexpb 14717 prmdiv 14782 prmdiveq 14783 oddprm 14814 pcpremul 14842 pceulem 14844 pczpre 14846 pczcl 14847 pc1 14854 pczdvds 14861 pczndvds 14863 pczndvds2 14865 pcidlem 14870 pcmpt 14886 pcfaclem 14892 pcfac 14893 pockthlem 14898 pockthg 14899 prmunb 14907 prmreclem2 14910 prmgapprmorlemOLD 15066 prmgapprmolem 15081 odcau 17305 sylow3lem6 17333 gexexlem 17539 znfld 19180 wilthlem1 24042 wilthlem3 24044 wilth 24045 ppisval 24079 ppisval2 24080 chtge0 24088 isppw 24090 ppiprm 24127 chtprm 24129 chtwordi 24132 vma1 24142 fsumvma2 24191 chpval2 24195 chpchtsum 24196 chpub 24197 mersenne 24204 perfect1 24205 bposlem1 24261 lgslem1 24273 lgslem4 24276 lgsval2lem 24283 lgsdirprm 24306 lgsne0 24310 lgsqrlem2 24319 lgseisenlem1 24326 lgseisenlem3 24328 lgseisen 24330 lgsquadlem3 24333 m1lgs 24339 2sqblem 24354 chtppilimlem1 24360 rplogsumlem2 24372 rpvmasumlem 24374 dchrisum0flblem2 24396 padicabvcxp 24519 ostth3 24525 usghashecclwwlk 25612 clwlkfclwwlk 25621 isprm7 36704 gbogt5 38901 ztprmneprm 40401 |
Copyright terms: Public domain | W3C validator |