Theorem 2pos 12474

Description: The number 2 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
2pos	⊢ 0 < 2

Proof of Theorem 2pos

Step	Hyp	Ref	Expression
1		2nn 12443	. 2 ⊢ 2 ∈ ℕ
2	1	nngt0i 12404	1 ⊢ 0 < 2

This proof depends on syntax axioms:   class class class wbr 5106  0cc0 11227   < clt 11370  2c2 12424

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-nn 12363  df-2 12432

This theorem is used by:  halfgt0  12588  halflt1  12590  halfpos2  12602  halfnneg2  12604  nominpos  12610  avglt1  12611  avglt2  12612  nn0n0n1ge2b  12702  3halfnz  12805  2rp  13152  hashgt23el  14596  s3fv0  15071  sqreulem  15556  cos2bnd  16385  sin02gt0  16389  sincos2sgn  16391  sin4lt0  16392  epos  16404  sqrt2re  16447  nnoddm1d2  16585  2mulprm  16897  prmgaplem7  17264  slotsdifdsndx  17594  odrngstr  17603  imasvalstr  17651  psgnunilem2  19739  cnfldstr  21710  bl2in  24749  iihalf1  25282  iihalf2  25284  pcoass  25375  tcphcphlem1  25586  trirn  25751  minveclem2  25777  minveclem4  25783  ovolunlem1a  25847  vitalilem4  25962  mbfi1fseqlem5  26070  pilem2  26809  pilem3  26810  pipos  26817  sinhalfpilem  26822  sincosq1lem  26856  tangtx  26864  sinq12gt0  26866  tan4thpi  26873  sincos6thpi  26874  cosordlem  26888  tanord1  26895  efif1olem2  26901  efif1olem4  26903  cxpcn3lem  27105  ang180lem1  27167  ang180lem2  27168  atantan  27281  atanbndlem  27283  atans2  27289  leibpi  27300  log2tlbnd  27303  basellem1  27438  basellem2  27439  basellem3  27440  ppiltx  27534  ppiub  27561  chtublem  27568  chtub  27569  chpval2  27575  bcmono  27634  bpos1lem  27639  bposlem1  27641  bposlem2  27642  bposlem3  27643  bposlem4  27644  bposlem5  27645  bposlem6  27646  bposlem7  27647  gausslemma2dlem0c  27715  gausslemma2dlem1a  27722  gausslemma2dlem2  27724  gausslemma2dlem3  27725  lgseisenlem1  27732  lgseisenlem2  27733  lgseisenlem3  27734  lgsquadlem1  27737  lgsquadlem2  27738  2lgslem1a1  27746  2lgslem1a2  27747  2lgslem1c  27750  chebbnd1lem1  27826  chebbnd1lem2  27827  chebbnd1lem3  27828  chebbnd1  27829  chtppilimlem1  27830  chtppilimlem2  27831  chtppilim  27832  chebbnd2  27834  chto1lb  27835  chpchtlim  27836  chpo1ub  27837  dchrisum0fno1  27868  mulog2sumlem2  27892  selberglem2  27903  selberg2lem  27907  chpdifbndlem1  27910  logdivbnd  27913  pntrsumo1  27922  pntpbnd1a  27942  pntlemh  27956  pntlemr  27959  pntlemk  27963  pntlemo  27964  pnt2  27970  umgrislfupgrlem  29730  lfgrnloop  29733  lfuhgr1v0e  29865  wwlksnextwrd  30516  wwlksnextfun  30517  wwlksnextinj  30518  clwlkclwwlklem2a2  30614  konigsberg  30888  ex-fl  31078  minvecolem2  31507  minvecolem4  31512  bcsiALT  31811  opsqrlem6  32777  cdj3lem1  33066  wrdt2ind  33586  cyc2fv2  33753  rtelextdg2lem  34428  2sqr3minply  34482  sqsscirc1  34610  omssubadd  35002  signslema  35261  hgt750lem  35350  subfacval3  36121  nn0prpwlem  37288  knoppndvlem18  37573  knoppndvlem19  37574  knoppndvlem21  37576  cnndvlem1  37581  iccioo01  38442  sin2h  38725  cos2h  38726  tan2h  38727  itg2addnclem  38781  3lexlogpow5ineq2  43297  3lexlogpow5ineq4  43298  3lexlogpow5ineq3  43299  3lexlogpow2ineq1  43300  3lexlogpow2ineq2  43301  3lexlogpow5ineq5  43302  aks4d1lem1  43304  aks4d1p1p3  43311  aks4d1p1p2  43312  aks4d1p1p4  43313  aks4d1p1p6  43315  aks4d1p1p7  43316  aks4d1p1p5  43317  aks4d1p1  43318  aks4d1p2  43319  aks4d1p3  43320  aks4d1p5  43322  aks4d1p6  43323  aks4d1p7d1  43324  aks4d1p7  43325  aks4d1p8  43329  aks4d1p9  43330  posbezout  43342  aks6d1c3  43365  2ap1caineq  43387  aks6d1c6lem4  43415  aks6d1c7lem1  43422  aks6d1c7lem2  43423  oexpreposd  43572  asin1half  43601  pellfundex  44086  jm2.22  44195  jm2.23  44196  imo72b2lem0  45357  sumnnodd  46847  sinaover2ne0  47083  stoweidlem14  47229  stoweidlem49  47264  stoweidlem52  47267  wallispilem4  47283  wallispi2lem2  47287  stirlinglem6  47294  stirlinglem15  47303  stirlingr  47305  dirkerval2  47309  dirkertrigeqlem3  47315  dirkercncflem4  47321  fourierdlem24  47346  fourierdlem79  47400  fourierdlem103  47424  fourierdlem104  47425  fourierdlem112  47433  fourierswlem  47445  fouriersw  47446  goldrapos  48135  goldratmolem4  48140  goldratval  48141  2ltceilhalf  48607  2tceilhalfelfzo1  48611  lighneallem4a  48898  nprmdvdsfacm1lem4  48913  nnoALTV  48998  nn0oALTV  48999  nn0e  49000  nneven  49001  evengpoap3  49102  gpg3kgrtriexlem1  49386  nn0eo  49845  flnn0div2ge  49850  fldivexpfllog2  49882  fllog2  49885  blennngt2o2  49909  dignn0flhalf  49935  sepfsepc  50247