Theorem elfzo 13692

Description: Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)

Assertion

Ref	Expression
elfzo	⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁)))

Proof of Theorem elfzo

Step	Hyp	Ref	Expression
1		peano2zm 12661	. . 3 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
2		elfz 13548	. . 3 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑁 − 1))))
3	1, 2	syl3an3 1162	. 2 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑁 − 1))))
4		fzoval 13691	. . . 4 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
5	4	eleq2d 2815	. . 3 ⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (𝑀..^𝑁) ↔ 𝐾 ∈ (𝑀...(𝑁 − 1))))
6	5	3ad2ant3 1132	. 2 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ 𝐾 ∈ (𝑀...(𝑁 − 1))))
7		zltlem1 12671	. . . 4 ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 ↔ 𝐾 ≤ (𝑁 − 1)))
8	7	3adant2 1128	. . 3 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 ↔ 𝐾 ≤ (𝑁 − 1)))
9	8	anbi2d 628	. 2 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑁 − 1))))
10	3, 6, 9	3bitr4d 310	1 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   ∈ wcel 2100   class class class wbr 5154  (class class class)co 7427  1c1 11160   < clt 11299   ≤ cle 11300   − cmin 11495  ℤcz 12614  ...cfz 13542  ..^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:  elfzo2  13693  nelfzo  13695  elfzole1  13698  elfzolt2  13699  fzospliti  13722  fzo1fzo0n0  13741  fzoaddel  13743  elincfzoext  13748  fzind2  13809  ccatsymb  14603  fzomaxdiflem  15360  submateqlem2  33699  breprexplemc  34554  bccbc  44131  fourierdlem11  45850  fourierdlem12  45851  fourierdlem15  45854  fourierdlem79  45917  natglobalincr  46607  iccpartiltu  47105  nnpw2blenfzo  48091