Theorem elfzoel2 13715

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

Assertion

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

Proof of Theorem elfzoel2

Step	Hyp	Ref	Expression
1		ne0i 4364	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ≠ ∅)
2		fzof 13713	. . . . . 6 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
3	2	fdmi 6758	. . . . 5 ⊢ dom ..^ = (ℤ × ℤ)
4	3	ndmov 7634	. . . 4 ⊢ (¬ (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) = ∅)
5	4	necon1ai 2974	. . 3 ⊢ ((𝐵..^𝐶) ≠ ∅ → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
6	1, 5	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ))
7	6	simprd 495	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ≠ wne 2946  ∅c0 4352  𝒫 cpw 4622   × cxp 5698  (class class class)co 7448  ℤcz 12639  ..^cfzo 13711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-neg 11523  df-z 12640  df-uz 12904  df-fz 13568  df-fzo 13712

This theorem is referenced by:  elfzoelz  13716  elfzo2  13719  elfzole1  13724  elfzolt2  13725  elfzolt3  13726  elfzolt2b  13727  elfzolt3b  13728  elfzop1le2  13729  fzonel  13730  elfzouz2  13731  fzonnsub  13741  fzoss1  13743  fzospliti  13748  fzodisj  13750  fzoaddel  13769  fzo0addelr  13771  elfzoext  13773  elincfzoext  13774  fzosubel  13775  fzoend  13807  ssfzo12  13809  fzoopth  13812  fzofzp1  13814  elfzo1elm1fzo0  13818  fzonfzoufzol  13820  elfznelfzob  13823  peano2fzor  13824  fzostep1  13833  modsumfzodifsn  13995  addmodlteq  13997  cshwidxm1  14855  cshimadifsn0  14879  fzomaxdiflem  15391  fzo0dvdseq  16371  fzocongeq  16372  addmodlteqALT  16373  efgsp1  19779  efgsres  19780  crctcshwlkn0lem2  29844  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  crctcshwlkn0lem6  29848  crctcshwlkn0  29854  crctcsh  29857  eucrctshift  30275  eucrct2eupth  30277  fzssfzo  34516  signsvfn  34559  elfzolem1  45236  dvnmul  45864  iblspltprt  45894  stoweidlem3  45924  fourierdlem12  46040  fourierdlem50  46077  fourierdlem64  46091  fourierdlem79  46106  natglobalincr  46796  iccpartiltu  47296  iccpartgt  47301  bgoldbtbndlem2  47680