This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzo0to42pr

Description: A half-open integer range from 0 to 4 is a union of two unordered pairs. (Contributed by Alexander van der Vekens, 17-Nov-2017)

Ref Expression
Assertion fzo0to42pr ( 0 ..^ 4 ) = ( { 0 , 1 } ∪ { 2 , 3 } )

Proof

Step Hyp Ref Expression
1 2nn0 ⊢ 2 ∈ ℕ0
2 4nn0 ⊢ 4 ∈ ℕ0
3 2re ⊢ 2 ∈ ℝ
4 4re ⊢ 4 ∈ ℝ
5 2lt4 ⊢ 2 < 4
6 3 4 5 ltleii ⊢ 2 ≤ 4
7 elfz2nn0 ⊢ ( 2 ∈ ( 0 ... 4 ) ↔ ( 2 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 2 ≤ 4 ) )
8 1 2 6 7 mpbir3an ⊢ 2 ∈ ( 0 ... 4 )
9 fzosplit ⊢ ( 2 ∈ ( 0 ... 4 ) → ( 0 ..^ 4 ) = ( ( 0 ..^ 2 ) ∪ ( 2 ..^ 4 ) ) )
10 8 9 ax-mp ⊢ ( 0 ..^ 4 ) = ( ( 0 ..^ 2 ) ∪ ( 2 ..^ 4 ) )
11 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
12 4z ⊢ 4 ∈ ℤ
13 fzoval ⊢ ( 4 ∈ ℤ → ( 2 ..^ 4 ) = ( 2 ... ( 4 − 1 ) ) )
14 12 13 ax-mp ⊢ ( 2 ..^ 4 ) = ( 2 ... ( 4 − 1 ) )
15 4m1e3 ⊢ ( 4 − 1 ) = 3
16 df-3 ⊢ 3 = ( 2 + 1 )
17 15 16 eqtri ⊢ ( 4 − 1 ) = ( 2 + 1 )
18 17 oveq2i ⊢ ( 2 ... ( 4 − 1 ) ) = ( 2 ... ( 2 + 1 ) )
19 2z ⊢ 2 ∈ ℤ
20 fzpr ⊢ ( 2 ∈ ℤ → ( 2 ... ( 2 + 1 ) ) = { 2 , ( 2 + 1 ) } )
21 19 20 ax-mp ⊢ ( 2 ... ( 2 + 1 ) ) = { 2 , ( 2 + 1 ) }
22 18 21 eqtri ⊢ ( 2 ... ( 4 − 1 ) ) = { 2 , ( 2 + 1 ) }
23 2p1e3 ⊢ ( 2 + 1 ) = 3
24 23 preq2i ⊢ { 2 , ( 2 + 1 ) } = { 2 , 3 }
25 14 22 24 3eqtri ⊢ ( 2 ..^ 4 ) = { 2 , 3 }
26 11 25 uneq12i ⊢ ( ( 0 ..^ 2 ) ∪ ( 2 ..^ 4 ) ) = ( { 0 , 1 } ∪ { 2 , 3 } )
27 10 26 eqtri ⊢ ( 0 ..^ 4 ) = ( { 0 , 1 } ∪ { 2 , 3 } )