HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem prime 8218
Description: Two ways to express " is a prime number (or 1)." See also isprm 10017.
Assertion
Ref Expression
prime
Distinct variable group:   ,

Proof of Theorem prime
StepHypRef Expression
1 bi2.04 349 . . . 4
2 impexp 426 . . . 4
3 neor 2116 . . . . 5
43imbi2i 301 . . . 4
51, 2, 43bitr4ri 267 . . 3
6 nngt1ne1 7945 . . . . . . 7
76adantl 445 . . . . . 6
87anbi1d 679 . . . . 5
9 nnz 8171 . . . . . . . . 9
10 nnre 7928 . . . . . . . . . . . . 13
11 gtndiv 8216 . . . . . . . . . . . . . 14
12113expia 1114 . . . . . . . . . . . . 13
1310, 12sylan 450 . . . . . . . . . . . 12
1413con2d 105 . . . . . . . . . . 11
15 nnre 7928 . . . . . . . . . . . 12
16 lenlt 7351 . . . . . . . . . . . 12
1710, 15, 16syl2an 456 . . . . . . . . . . 11
1814, 17sylibrd 223 . . . . . . . . . 10
1918ancoms 432 . . . . . . . . 9
209, 19syl5 28 . . . . . . . 8
2120pm4.71rd 609 . . . . . . 7
2221anbi2d 678 . . . . . 6
23 3anass 903 . . . . . 6
2422, 23syl6bbr 252 . . . . 5
258, 24bitr3d 244 . . . 4
2625imbi1d 306 . . 3
275, 26syl5bb 246 . 2
2827ralbidva 2141 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wb 174   wo 356   wa 357   w3a 899   wceq 1414   wcel 1416   wne 2035  wral 2127   class class class wbr 3385  (class class class)co 5004  cr 7213  c1 7215   cle 7322   clt 7326   cdiv 7440  cn 7441  cz 7443
This theorem is referenced by:  infpnlem1 10162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-rep 3471  ax-sep 3481  ax-nul 3490  ax-pow 3526  ax-pr 3550  ax-un 3825  ax-resscn 7268  ax-1cn 7269  ax-icn 7270  ax-addcl 7271  ax-addrcl 7272  ax-mulcl 7273  ax-mulrcl 7274  ax-mulcom 7275  ax-addass 7276  ax-mulass 7277  ax-distr 7278  ax-i2m1 7279  ax-1ne0 7280  ax-1rid 7281  ax-rnegex 7282  ax-rrecex 7283  ax-cnre 7284  ax-pre-lttri 7285  ax-pre-lttrn 7286  ax-pre-ltadd 7287  ax-pre-mulgt0 7288
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1309  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-nel 2038  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2328  df-sbc 2495  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-pss 2649  df-nul 2907  df-if 3014  df-pw 3074  df-sn 3091  df-pr 3092  df-tp 3093  df-op 3094  df-uni 3236  df-iun 3309  df-br 3386  df-opab 3440  df-tr 3455  df-eprel 3636  df-id 3639  df-po 3644  df-so 3658  df-fr 3678  df-we 3694  df-ord 3710  df-on 3711  df-lim 3712  df-suc 3713  df-om 3990  df-xp 4037  df-rel 4038  df-cnv 4039  df-co 4040  df-dm 4041  df-rn 4042  df-res 4043  df-ima 4044  df-fun 4045  df-fn 4046  df-f 4047  df-f1 4048  df-fo 4049  df-f1o 4050  df-fv 4051  df-ov 5006  df-oprab 5007  df-mpt 5167  df-mpt2 5168  df-iota 5409  df-rdg 5500  df-er 5675  df-en 5832  df-dom 5833  df-sdom 5834  df-riota 5989  df-pnf 7327  df-mnf 7328  df-xr 7329  df-ltxr 7330  df-le 7331  df-sub 7457  df-neg 7459  df-div 7684  df-n 7923  df-n0 8107  df-z 8152
Copyright terms: Public domain