Theorem lbfzo0 13126

Description: An integer is strictly greater than zero iff it is a member of ℕ. (Contributed by Mario Carneiro, 29-Sep-2015.)

Assertion

Ref	Expression
lbfzo0	⊢ (0 ∈ (0..^𝐴) ↔ 𝐴 ∈ ℕ)

Proof of Theorem lbfzo0

Step	Hyp	Ref	Expression
1		0z 12031	. . 3 ⊢ 0 ∈ ℤ
2		3anass 1092	. . 3 ⊢ ((0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 < 𝐴) ↔ (0 ∈ ℤ ∧ (𝐴 ∈ ℤ ∧ 0 < 𝐴)))
3	1, 2	mpbiran 708	. 2 ⊢ ((0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 < 𝐴) ↔ (𝐴 ∈ ℤ ∧ 0 < 𝐴))
4		fzolb 13093	. 2 ⊢ (0 ∈ (0..^𝐴) ↔ (0 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 0 < 𝐴))
5		elnnz 12030	. 2 ⊢ (𝐴 ∈ ℕ ↔ (𝐴 ∈ ℤ ∧ 0 < 𝐴))
6	3, 4, 5	3bitr4i 306	1 ⊢ (0 ∈ (0..^𝐴) ↔ 𝐴 ∈ ℕ)

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   ∈ wcel 2111   class class class wbr 5032  (class class class)co 7150  0cc0 10575   < clt 10713  ℕcn 11674  ℤcz 12020  ..^cfzo 13082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-er 8299  df-en 8528  df-dom 8529  df-sdom 8530  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-nn 11675  df-n0 11935  df-z 12021  df-uz 12283  df-fz 12940  df-fzo 13083

This theorem is referenced by:  elfzo0  13127  fzo0n0  13138  fzo0end  13178  wrdsymb1  13952  ccatfv0  13984  ccat1st1st  14031  ccat2s1p1  14032  ccat2s1p1OLD  14034  lswccats1fst  14041  swrdfv0  14058  pfxn0  14095  pfxfv0  14101  pfxtrcfv0  14103  pfx1  14112  cats1un  14130  revs1  14174  repswfsts  14190  cshwidx0mod  14214  cshw1  14231  scshwfzeqfzo  14235  cats1fvn  14267  pfx2  14356  nnnn0modprm0  16198  cshwrepswhash1  16494  efgsval2  18926  efgs1b  18929  efgsp1  18930  efgsres  18931  efgredlemd  18937  efgredlem  18940  efgrelexlemb  18943  pgpfaclem1  19271  dchrisumlem3  26174  tgcgr4  26424  wlkonl1iedg  27554  usgr2pthlem  27651  pthdlem2lem  27655  lfgrn1cycl  27690  uspgrn2crct  27693  crctcshwlkn0lem6  27700  0enwwlksnge1  27749  wwlksm1edg  27766  wwlksnwwlksnon  27800  clwlkclwwlklem2  27884  clwlkclwwlkf1lem3  27890  clwwlkel  27930  clwwlkf1  27933  umgr2cwwk2dif  27948  clwwlknonwwlknonb  27990  upgr3v3e3cycl  28064  upgr4cycl4dv4e  28069  2clwwlk2clwwlk  28234  cycpmco2lem4  30922  cycpmco2lem5  30923  cycpmrn  30936  lmatcl  31287  fib0  31885  signsvtn0  32068  reprpmtf1o  32125  poimirlem3  35340  amgm2d  41277  amgm3d  41278  amgm4d  41279  iccpartigtl  44308  iccpartlt  44309  amgmw2d  45723