Theorem fzo0to2pr 13112

Description: A half-open integer range from 0 to 2 is an unordered pair. (Contributed by Alexander van der Vekens, 4-Dec-2017.)

Assertion

Ref	Expression
fzo0to2pr	⊢ (0..^2) = {0, 1}

Proof of Theorem fzo0to2pr

Step	Hyp	Ref	Expression
1		2z 12001	. . 3 ⊢ 2 ∈ ℤ
2		fzoval 13029	. . 3 ⊢ (2 ∈ ℤ → (0..^2) = (0...(2 − 1)))
3	1, 2	ax-mp 5	. 2 ⊢ (0..^2) = (0...(2 − 1))
4		2m1e1 11750	. . . 4 ⊢ (2 − 1) = 1
5		0p1e1 11746	. . . 4 ⊢ (0 + 1) = 1
6	4, 5	eqtr4i 2847	. . 3 ⊢ (2 − 1) = (0 + 1)
7	6	oveq2i 7153	. 2 ⊢ (0...(2 − 1)) = (0...(0 + 1))
8		0z 11979	. . 3 ⊢ 0 ∈ ℤ
9		fzpr 12952	. . . 4 ⊢ (0 ∈ ℤ → (0...(0 + 1)) = {0, (0 + 1)})
10	5	preq2i 4659	. . . 4 ⊢ {0, (0 + 1)} = {0, 1}
11	9, 10	syl6eq 2872	. . 3 ⊢ (0 ∈ ℤ → (0...(0 + 1)) = {0, 1})
12	8, 11	ax-mp 5	. 2 ⊢ (0...(0 + 1)) = {0, 1}
13	3, 7, 12	3eqtri 2848	1 ⊢ (0..^2) = {0, 1}

Syntax hints:   = wceq 1537   ∈ wcel 2114  {cpr 4555  (class class class)co 7142  0cc0 10523  1c1 10524   + caddc 10526   − cmin 10856  2c2 11679  ℤcz 11968  ...cfz 12882  ..^cfzo 13023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-cnex 10579  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599  ax-pre-mulgt0 10600

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-pss 3942  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-tp 4558  df-op 4560  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5446  df-eprel 5451  df-po 5460  df-so 5461  df-fr 5500  df-we 5502  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-pred 6134  df-ord 6180  df-on 6181  df-lim 6182  df-suc 6183  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7567  df-1st 7675  df-2nd 7676  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666  df-le 10667  df-sub 10858  df-neg 10859  df-nn 11625  df-2 11687  df-n0 11885  df-z 11969  df-uz 12231  df-fz 12883  df-fzo 13024

This theorem is referenced by:  fzo0to42pr  13114  s2dm  14237  wrdlen2i  14289  wrd2pr2op  14290  pfx2  14294  wwlktovf1  14306  bitsinv1lem  15773  upgr2wlk  27436  usgr2wlkneq  27523  usgr2trlncl  27527  usgr2pthlem  27530  usgr2pth  27531  uspgrn2crct  27572  2wlkdlem2  27690  umgrwwlks2on  27721  s2rn  30606  cyc3fv1  30786  cyc3fv2  30787  lmat22lem  31092  eulerpartlemd  31631  prodfzo03  31881  elmod2  43620