Theorem elfzo0 13731

Description: Membership in a half-open integer range based at 0. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)

Assertion

Ref	Expression
elfzo0	⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵))

Proof of Theorem elfzo0

Step	Hyp	Ref	Expression
1		elfzouz 13694	. . . 4 ⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 ∈ (ℤ≥‘0))
2		elnn0uz 12923	. . . 4 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℤ≥‘0))
3	1, 2	sylibr 233	. . 3 ⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 ∈ ℕ0)
4		elfzolt3b 13702	. . . 4 ⊢ (𝐴 ∈ (0..^𝐵) → 0 ∈ (0..^𝐵))
5		lbfzo0 13730	. . . 4 ⊢ (0 ∈ (0..^𝐵) ↔ 𝐵 ∈ ℕ)
6	4, 5	sylib 217	. . 3 ⊢ (𝐴 ∈ (0..^𝐵) → 𝐵 ∈ ℕ)
7		elfzolt2 13699	. . 3 ⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 < 𝐵)
8	3, 6, 7	3jca 1125	. 2 ⊢ (𝐴 ∈ (0..^𝐵) → (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵))
9		simp1 1133	. . . 4 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℕ0)
10	9, 2	sylib 217	. . 3 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → 𝐴 ∈ (ℤ≥‘0))
11		nnz 12635	. . . 4 ⊢ (𝐵 ∈ ℕ → 𝐵 ∈ ℤ)
12	11	3ad2ant2 1131	. . 3 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℤ)
13		simp3 1135	. . 3 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵)
14		elfzo2 13693	. . 3 ⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ (ℤ≥‘0) ∧ 𝐵 ∈ ℤ ∧ 𝐴 < 𝐵))
15	10, 12, 13, 14	syl3anbrc 1340	. 2 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → 𝐴 ∈ (0..^𝐵))
16	8, 15	impbii 208	1 ⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵))

Syntax hints:   ↔ wb 205   ∧ w3a 1084   ∈ wcel 2100   class class class wbr 5154  ‘cfv 6556  (class class class)co 7427  0cc0 11159   < clt 11299  ℕcn 12268  ℕ₀cn0 12528  ℤcz 12614  ℤ_≥cuz 12878  ..^cfzo 13685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7748  ax-cnex 11215  ax-resscn 11216  ax-1cn 11217  ax-icn 11218  ax-addcl 11219  ax-addrcl 11220  ax-mulcl 11221  ax-mulrcl 11222  ax-mulcom 11223  ax-addass 11224  ax-mulass 11225  ax-distr 11226  ax-i2m1 11227  ax-1ne0 11228  ax-1rid 11229  ax-rnegex 11230  ax-rrecex 11231  ax-cnre 11232  ax-pre-lttri 11233  ax-pre-lttrn 11234  ax-pre-ltadd 11235  ax-pre-mulgt0 11236

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3788  df-csb 3904  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-pss 3978  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-iun 5006  df-br 5155  df-opab 5217  df-mpt 5238  df-tr 5272  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5639  df-we 5641  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6315  df-ord 6381  df-on 6382  df-lim 6383  df-suc 6384  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-riota 7383  df-ov 7430  df-oprab 7431  df-mpo 7432  df-om 7882  df-1st 8008  df-2nd 8009  df-frecs 8300  df-wrecs 8331  df-recs 8405  df-rdg 8444  df-er 8738  df-en 8979  df-dom 8980  df-sdom 8981  df-pnf 11301  df-mnf 11302  df-xr 11303  df-ltxr 11304  df-le 11305  df-sub 11497  df-neg 11498  df-nn 12269  df-n0 12529  df-z 12615  df-uz 12879  df-fz 13543  df-fzo 13686

This theorem is referenced by:  elfzo0z  13732  nn0p1elfzo  13733  elfzo0le  13734  fzonmapblen  13736  fzofzim  13737  fzo1fzo0n0  13741  ubmelfzo  13755  elfzodifsumelfzo  13756  elfzonlteqm1  13766  fzonn0p1  13767  fzonn0p1p1  13769  elfzo0l  13780  ubmelm1fzo  13787  elfznelfzo  13796  subfzo0  13813  fvf1tp  13814  zmodidfzoimp  13926  modfzo0difsn  13968  modsumfzodifsn  13969  addmodlteq  13971  tpf1ofv1  14519  tpf1ofv2  14520  tpfo  14522  ccatalpha  14614  ccat2s1fvw  14659  swrdswrd  14726  swrdccatin1  14746  pfxccatin12lem3  14753  repswswrd  14805  cshwidxmod  14824  cshwidxmodr  14825  cshwidx0  14827  cshwidxm1  14828  cshf1  14831  2cshw  14834  cshweqrep  14842  cshw1  14843  cshco  14858  swrds2  14962  pfx2  14969  2swrd2eqwrdeq  14975  wwlktovf  14978  addmodlteqALT  16340  smueqlem  16503  hashgcdlem  16803  prmgaplem3  17068  cshwshashlem2  17112  psgnunilem5  19504  psgnunilem2  19505  psgnunilem3  19506  psgnunilem4  19507  psdmul  22159  usgr2pthlem  29697  uspgrn2crct  29739  crctcshwlkn0lem4  29744  crctcshwlkn0lem5  29745  crctcshwlkn0  29752  wwlksnredwwlkn  29826  clwlkclwwlklem2fv2  29926  clwlkclwwlklem2a4  29927  clwlkclwwlklem2a  29928  clwwisshclwwslemlem  29943  clwwlkel  29976  wwlksext2clwwlk  29987  umgr2cwwkdifex  29995  clwwlknonex2lem2  30038  upgr3v3e3cycl  30110  upgr4cycl4dv4e  30115  eucrctshift  30173  eucrct2eupth  30175  cshwrnid  32828  fzo0pmtrlast  32985  wrdpmtrlast  32986  1arithidomlem1  33428  1arithidomlem2  33429  1arithidom  33430  fiblem  34263  fib1  34265  fibp1  34266  signstfveq0  34454  lpadleft  34560  poimirlem17  37378  poimirlem20  37381  subsubelfzo0  47005  iccpartigtl  47061  lswn0  47082  bgoldbtbndlem4  47446