Theorem fzm1 10485

Description: Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)

Assertion

Ref	Expression
fzm1	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)))

Proof of Theorem fzm1

Step	Hyp	Ref	Expression
1		oveq1 6082	. . . . . . 7 ⊢ (𝑁 = 𝑀 → (𝑁...𝑁) = (𝑀...𝑁))
2	1	eleq2d 2308	. . . . . 6 ⊢ (𝑁 = 𝑀 → (𝐾 ∈ (𝑁...𝑁) ↔ 𝐾 ∈ (𝑀...𝑁)))
3		elfz1eq 10418	. . . . . 6 ⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁)
4	2, 3	biimtrrdi 164	. . . . 5 ⊢ (𝑁 = 𝑀 → (𝐾 ∈ (𝑀...𝑁) → 𝐾 = 𝑁))
5		olc 723	. . . . 5 ⊢ (𝐾 = 𝑁 → (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))
6	4, 5	syl6 33	. . . 4 ⊢ (𝑁 = 𝑀 → (𝐾 ∈ (𝑀...𝑁) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)))
7	6	adantl 277	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...𝑁) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)))
8		noel 3525	. . . . . 6 ⊢ ¬ 𝐾 ∈ ∅
9		eluzelz 9910	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
10	9	adantr 276	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 𝑁 ∈ ℤ)
11	10	zred 9747	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 𝑁 ∈ ℝ)
12	11	ltm1d 9252	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑁 − 1) < 𝑁)
13		breq2 4129	. . . . . . . . . 10 ⊢ (𝑁 = 𝑀 → ((𝑁 − 1) < 𝑁 ↔ (𝑁 − 1) < 𝑀))
14	13	adantl 277	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ((𝑁 − 1) < 𝑁 ↔ (𝑁 − 1) < 𝑀))
15	12, 14	mpbid 147	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑁 − 1) < 𝑀)
16		eluzel2 9905	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
17	16	adantr 276	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 𝑀 ∈ ℤ)
18		1zzd 9650	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 1 ∈ ℤ)
19	10, 18	zsubcld 9752	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑁 − 1) ∈ ℤ)
20		fzn 10425	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → ((𝑁 − 1) < 𝑀 ↔ (𝑀...(𝑁 − 1)) = ∅))
21	17, 19, 20	syl2anc 415	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ((𝑁 − 1) < 𝑀 ↔ (𝑀...(𝑁 − 1)) = ∅))
22	15, 21	mpbid 147	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑀...(𝑁 − 1)) = ∅)
23	22	eleq2d 2308	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ 𝐾 ∈ ∅))
24	8, 23	mtbiri 686	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ¬ 𝐾 ∈ (𝑀...(𝑁 − 1)))
25	24	pm2.21d 628	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...(𝑁 − 1)) → 𝐾 ∈ (𝑀...𝑁)))
26		eluzfz2 10415	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
27	26	ad2antrr 492	. . . . . 6 ⊢ (((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) ∧ 𝐾 = 𝑁) → 𝑁 ∈ (𝑀...𝑁))
28		eleq1 2301	. . . . . . 7 ⊢ (𝐾 = 𝑁 → (𝐾 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁)))
29	28	adantl 277	. . . . . 6 ⊢ (((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) ∧ 𝐾 = 𝑁) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁)))
30	27, 29	mpbird 167	. . . . 5 ⊢ (((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) ∧ 𝐾 = 𝑁) → 𝐾 ∈ (𝑀...𝑁))
31	30	ex 115	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 = 𝑁 → 𝐾 ∈ (𝑀...𝑁)))
32	25, 31	jaod 729	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ((𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁) → 𝐾 ∈ (𝑀...𝑁)))
33	7, 32	impbid 129	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)))
34		elfzp1 10457	. . . 4 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...((𝑁 − 1) + 1)) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = ((𝑁 − 1) + 1))))
35	34	adantl 277	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈ (ℤ≥‘𝑀)) → (𝐾 ∈ (𝑀...((𝑁 − 1) + 1)) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = ((𝑁 − 1) + 1))))
36	9	adantr 276	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈ (ℤ≥‘𝑀)) → 𝑁 ∈ ℤ)
37	36	zcnd 9748	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈ (ℤ≥‘𝑀)) → 𝑁 ∈ ℂ)
38		npcan1 8695	. . . . . 6 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
39	37, 38	syl 14	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈ (ℤ≥‘𝑀)) → ((𝑁 − 1) + 1) = 𝑁)
40	39	oveq2d 6091	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈ (ℤ≥‘𝑀)) → (𝑀...((𝑁 − 1) + 1)) = (𝑀...𝑁))
41	40	eleq2d 2308	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈ (ℤ≥‘𝑀)) → (𝐾 ∈ (𝑀...((𝑁 − 1) + 1)) ↔ 𝐾 ∈ (𝑀...𝑁)))
42	39	eqeq2d 2250	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈ (ℤ≥‘𝑀)) → (𝐾 = ((𝑁 − 1) + 1) ↔ 𝐾 = 𝑁))
43	42	orbi2d 802	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈ (ℤ≥‘𝑀)) → ((𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = ((𝑁 − 1) + 1)) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)))
44	35, 41, 43	3bitr3d 218	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈ (ℤ≥‘𝑀)) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)))
45		uzm1 9932	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈ (ℤ≥‘𝑀)))
46	33, 44, 45	mpjaodan 810	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 720   = wceq 1402   ∈ wcel 2209  ∅c0 3520   class class class wbr 4125  ‘cfv 5372  (class class class)co 6075  ℂcc 8167  1c1 8170   + caddc 8172   < clt 8350   − cmin 8487  ℤcz 9623  ℤ_≥cuz 9900  ...cfz 10390

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4244  ax-pow 4306  ax-pr 4341  ax-un 4573  ax-setind 4679  ax-cnex 8260  ax-resscn 8261  ax-1cn 8262  ax-1re 8263  ax-icn 8264  ax-addcl 8265  ax-addrcl 8266  ax-mulcl 8267  ax-addcom 8269  ax-addass 8271  ax-distr 8273  ax-i2m1 8274  ax-0lt1 8275  ax-0id 8277  ax-rnegex 8278  ax-cnre 8280  ax-pre-ltirr 8281  ax-pre-ltwlin 8282  ax-pre-lttrn 8283  ax-pre-apti 8284  ax-pre-ltadd 8285

This theorem depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-int 3966  df-br 4126  df-opab 4188  df-mpt 4189  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-res 4781  df-ima 4782  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-fv 5380  df-riota 6028  df-ov 6078  df-oprab 6079  df-mpo 6080  df-pnf 8352  df-mnf 8353  df-xr 8354  df-ltxr 8355  df-le 8356  df-sub 8489  df-neg 8490  df-inn 9284  df-n0 9543  df-z 9624  df-uz 9901  df-fz 10391

This theorem is referenced by:  bcpasc  11182  phibndlem  12972  lgsdir2lem2  16062