Theorem fzopth 13534

Description: A finite set of sequential integers has the ordered pair property (compare opth 5475) under certain conditions. (Contributed by NM, 31-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
fzopth	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾)))

Proof of Theorem fzopth

Step	Hyp	Ref	Expression
1		eluzfz1 13504	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))
2	1	adantr 482	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝑀 ∈ (𝑀...𝑁))
3		simpr 486	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → (𝑀...𝑁) = (𝐽...𝐾))
4	2, 3	eleqtrd 2836	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝑀 ∈ (𝐽...𝐾))
5		elfzuz 13493	. . . . . . 7 ⊢ (𝑀 ∈ (𝐽...𝐾) → 𝑀 ∈ (ℤ≥‘𝐽))
6		uzss 12841	. . . . . . 7 ⊢ (𝑀 ∈ (ℤ≥‘𝐽) → (ℤ≥‘𝑀) ⊆ (ℤ≥‘𝐽))
7	4, 5, 6	3syl 18	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → (ℤ≥‘𝑀) ⊆ (ℤ≥‘𝐽))
8		elfzuz2 13502	. . . . . . . . 9 ⊢ (𝑀 ∈ (𝐽...𝐾) → 𝐾 ∈ (ℤ≥‘𝐽))
9		eluzfz1 13504	. . . . . . . . 9 ⊢ (𝐾 ∈ (ℤ≥‘𝐽) → 𝐽 ∈ (𝐽...𝐾))
10	4, 8, 9	3syl 18	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝐽 ∈ (𝐽...𝐾))
11	10, 3	eleqtrrd 2837	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝐽 ∈ (𝑀...𝑁))
12		elfzuz 13493	. . . . . . 7 ⊢ (𝐽 ∈ (𝑀...𝑁) → 𝐽 ∈ (ℤ≥‘𝑀))
13		uzss 12841	. . . . . . 7 ⊢ (𝐽 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝐽) ⊆ (ℤ≥‘𝑀))
14	11, 12, 13	3syl 18	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → (ℤ≥‘𝐽) ⊆ (ℤ≥‘𝑀))
15	7, 14	eqssd 3998	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → (ℤ≥‘𝑀) = (ℤ≥‘𝐽))
16		eluzel2 12823	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
17	16	adantr 482	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝑀 ∈ ℤ)
18		uz11 12843	. . . . . 6 ⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝐽) ↔ 𝑀 = 𝐽))
19	17, 18	syl 17	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → ((ℤ≥‘𝑀) = (ℤ≥‘𝐽) ↔ 𝑀 = 𝐽))
20	15, 19	mpbid 231	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝑀 = 𝐽)
21		eluzfz2 13505	. . . . . . . . 9 ⊢ (𝐾 ∈ (ℤ≥‘𝐽) → 𝐾 ∈ (𝐽...𝐾))
22	4, 8, 21	3syl 18	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝐾 ∈ (𝐽...𝐾))
23	22, 3	eleqtrrd 2837	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝐾 ∈ (𝑀...𝑁))
24		elfzuz3 13494	. . . . . . 7 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
25		uzss 12841	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝐾))
26	23, 24, 25	3syl 18	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝐾))
27		eluzfz2 13505	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
28	27	adantr 482	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝑁 ∈ (𝑀...𝑁))
29	28, 3	eleqtrd 2836	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝑁 ∈ (𝐽...𝐾))
30		elfzuz3 13494	. . . . . . 7 ⊢ (𝑁 ∈ (𝐽...𝐾) → 𝐾 ∈ (ℤ≥‘𝑁))
31		uzss 12841	. . . . . . 7 ⊢ (𝐾 ∈ (ℤ≥‘𝑁) → (ℤ≥‘𝐾) ⊆ (ℤ≥‘𝑁))
32	29, 30, 31	3syl 18	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → (ℤ≥‘𝐾) ⊆ (ℤ≥‘𝑁))
33	26, 32	eqssd 3998	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → (ℤ≥‘𝑁) = (ℤ≥‘𝐾))
34		eluzelz 12828	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
35	34	adantr 482	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝑁 ∈ ℤ)
36		uz11 12843	. . . . . 6 ⊢ (𝑁 ∈ ℤ → ((ℤ≥‘𝑁) = (ℤ≥‘𝐾) ↔ 𝑁 = 𝐾))
37	35, 36	syl 17	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → ((ℤ≥‘𝑁) = (ℤ≥‘𝐾) ↔ 𝑁 = 𝐾))
38	33, 37	mpbid 231	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → 𝑁 = 𝐾)
39	20, 38	jca 513	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (𝑀...𝑁) = (𝐽...𝐾)) → (𝑀 = 𝐽 ∧ 𝑁 = 𝐾))
40	39	ex 414	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) → (𝑀 = 𝐽 ∧ 𝑁 = 𝐾)))
41		oveq12 7413	. 2 ⊢ ((𝑀 = 𝐽 ∧ 𝑁 = 𝐾) → (𝑀...𝑁) = (𝐽...𝐾))
42	40, 41	impbid1 224	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) = (𝐽...𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   ⊆ wss 3947  ‘cfv 6540  (class class class)co 7404  ℤcz 12554  ℤ_≥cuz 12818  ...cfz 13480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-cnex 11162  ax-resscn 11163  ax-pre-lttri 11180  ax-pre-lttrn 11181

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7970  df-2nd 7971  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-neg 11443  df-z 12555  df-uz 12819  df-fz 13481

This theorem is referenced by:  fz0to4untppr  13600  2ffzeq  13618  gsumval2a  18600  eedimeq  28136  sdclem2  36548