Theorem elfzoelz 10382

Description: Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)

Assertion

Ref	Expression
elfzoelz	⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Proof of Theorem elfzoelz

Step	Hyp	Ref	Expression
1		elfzoel1 10380	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 10381	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 10379	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 6127	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 411	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 3663	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 19	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3228	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2202  𝒫 cpw 3652  (class class class)co 6018  ℤcz 9479  ..^cfzo 10377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-csb 3128  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-iun 3972  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-1st 6303  df-2nd 6304  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-n0 9403  df-z 9480  df-fz 10244  df-fzo 10378

This theorem is referenced by:  elfzo2  10385  elfzole1  10391  elfzolt2  10392  elfzolt3  10393  elfzolt2b  10394  elfzouz2  10397  fzonnsub  10406  fzospliti  10413  fzodisj  10415  fzodisjsn  10419  fzonmapblen  10427  fzoaddel  10433  elincfzoext  10439  fzosubel  10440  modaddmodup  10650  modaddmodlo  10651  modfzo0difsn  10658  modsumfzodifsn  10659  addmodlteq  10661  iseqf1olemqk  10770  seq3f1olemp  10778  seqfeq4g  10794  ccatcl  11174  ccatlen  11176  ccatval2  11179  ccatval3  11180  ccatvalfn  11182  ccatlid  11187  ccatass  11189  ccatrn  11190  ccatalpha  11194  swrdlen  11237  swrdfv  11238  swrdfv0  11239  swrdfv2  11248  swrdwrdsymbg  11249  swrdspsleq  11252  swrds1  11253  ccatswrd  11255  pfxfv  11269  ccatpfx  11286  swrdswrd  11290  pfxccatin12lem2a  11312  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12  11318  fzomaxdiflem  11677  fzomaxdif  11678  fzo0dvdseq  12423  fzocongeq  12424  addmodlteqALT  12425  crth  12801  phimullem  12802  eulerthlem1  12804  eulerthlemfi  12805  eulerthlemrprm  12806  hashgcdlem  12815  hashgcdeq  12817  phisum  12818  reumodprminv  12831  modprm0  12832  nnnn0modprm0  12833  modprmn0modprm0  12834  4sqlemafi  12973  nninfdclemlt  13077  gsumfzfsumlemm  14607  znf1o  14671  wlk1walkdom  16216  clwwlkccatlem  16257  trlsegvdeglem6  16322  trilpolemeq1  16670