Metamath Proof Explorer

Theorem fz0to4untppr

Description: An integer range from 0 to 4 is the union of a triple and a pair. (Contributed by Alexander van der Vekens, 13-Aug-2017)

Ref Expression
Assertion fz0to4untppr 
|- ( 0 ... 4 ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )

Proof

Step Hyp Ref Expression
1 df-3 
 |-  3 = ( 2 + 1 )
2 2cn 
 |-  2 e. CC
3 2 addid2i 
 |-  ( 0 + 2 ) = 2
4 3 eqcomi 
 |-  2 = ( 0 + 2 )
5 4 oveq1i 
 |-  ( 2 + 1 ) = ( ( 0 + 2 ) + 1 )
6 1 5 eqtri 
 |-  3 = ( ( 0 + 2 ) + 1 )
7 3z 
 |-  3 e. ZZ
8 0re 
 |-  0 e. RR
9 3re 
 |-  3 e. RR
10 3pos 
 |-  0 < 3
11 8 9 10 ltleii 
 |-  0 <_ 3
12 0z 
 |-  0 e. ZZ
13 12 eluz1i 
 |-  ( 3 e. ( ZZ>= ` 0 ) <-> ( 3 e. ZZ /\ 0 <_ 3 ) )
14 7 11 13 mpbir2an 
 |-  3 e. ( ZZ>= ` 0 )
15 6 14 eqeltrri 
 |-  ( ( 0 + 2 ) + 1 ) e. ( ZZ>= ` 0 )
16 4z 
 |-  4 e. ZZ
17 2re 
 |-  2 e. RR
18 4re 
 |-  4 e. RR
19 2lt4 
 |-  2 < 4
20 17 18 19 ltleii 
 |-  2 <_ 4
21 2z 
 |-  2 e. ZZ
22 21 eluz1i 
 |-  ( 4 e. ( ZZ>= ` 2 ) <-> ( 4 e. ZZ /\ 2 <_ 4 ) )
23 16 20 22 mpbir2an 
 |-  4 e. ( ZZ>= ` 2 )
24 4 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 0 + 2 ) )
25 23 24 eleqtri 
 |-  4 e. ( ZZ>= ` ( 0 + 2 ) )
26 fzsplit2 
 |-  ( ( ( ( 0 + 2 ) + 1 ) e. ( ZZ>= ` 0 ) /\ 4 e. ( ZZ>= ` ( 0 + 2 ) ) ) -> ( 0 ... 4 ) = ( ( 0 ... ( 0 + 2 ) ) u. ( ( ( 0 + 2 ) + 1 ) ... 4 ) ) )
27 15 25 26 mp2an 
 |-  ( 0 ... 4 ) = ( ( 0 ... ( 0 + 2 ) ) u. ( ( ( 0 + 2 ) + 1 ) ... 4 ) )
28 fztp 
 |-  ( 0 e. ZZ -> ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) } )
29 12 28 ax-mp 
 |-  ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) }
30 ax-1cn 
 |-  1 e. CC
31 eqidd 
 |-  ( 1 e. CC -> 0 = 0 )
32 addid2 
 |-  ( 1 e. CC -> ( 0 + 1 ) = 1 )
33 3 a1i 
 |-  ( 1 e. CC -> ( 0 + 2 ) = 2 )
34 31 32 33 tpeq123d 
 |-  ( 1 e. CC -> { 0 , ( 0 + 1 ) , ( 0 + 2 ) } = { 0 , 1 , 2 } )
35 30 34 ax-mp 
 |-  { 0 , ( 0 + 1 ) , ( 0 + 2 ) } = { 0 , 1 , 2 }
36 29 35 eqtri 
 |-  ( 0 ... ( 0 + 2 ) ) = { 0 , 1 , 2 }
37 3 a1i 
 |-  ( 3 e. ZZ -> ( 0 + 2 ) = 2 )
38 37 oveq1d 
 |-  ( 3 e. ZZ -> ( ( 0 + 2 ) + 1 ) = ( 2 + 1 ) )
39 38 1 eqtr4di 
 |-  ( 3 e. ZZ -> ( ( 0 + 2 ) + 1 ) = 3 )
40 39 oveq1d 
 |-  ( 3 e. ZZ -> ( ( ( 0 + 2 ) + 1 ) ... 4 ) = ( 3 ... 4 ) )
41 eqid 
 |-  3 = 3
42 df-4 
 |-  4 = ( 3 + 1 )
43 41 42 pm3.2i 
 |-  ( 3 = 3 /\ 4 = ( 3 + 1 ) )
44 43 a1i 
 |-  ( 3 e. ZZ -> ( 3 = 3 /\ 4 = ( 3 + 1 ) ) )
45 3lt4 
 |-  3 < 4
46 9 18 45 ltleii 
 |-  3 <_ 4
47 7 eluz1i 
 |-  ( 4 e. ( ZZ>= ` 3 ) <-> ( 4 e. ZZ /\ 3 <_ 4 ) )
48 16 46 47 mpbir2an 
 |-  4 e. ( ZZ>= ` 3 )
49 fzopth 
 |-  ( 4 e. ( ZZ>= ` 3 ) -> ( ( 3 ... 4 ) = ( 3 ... ( 3 + 1 ) ) <-> ( 3 = 3 /\ 4 = ( 3 + 1 ) ) ) )
50 48 49 ax-mp 
 |-  ( ( 3 ... 4 ) = ( 3 ... ( 3 + 1 ) ) <-> ( 3 = 3 /\ 4 = ( 3 + 1 ) ) )
51 44 50 sylibr 
 |-  ( 3 e. ZZ -> ( 3 ... 4 ) = ( 3 ... ( 3 + 1 ) ) )
52 fzpr 
 |-  ( 3 e. ZZ -> ( 3 ... ( 3 + 1 ) ) = { 3 , ( 3 + 1 ) } )
53 51 52 eqtrd 
 |-  ( 3 e. ZZ -> ( 3 ... 4 ) = { 3 , ( 3 + 1 ) } )
54 42 eqcomi 
 |-  ( 3 + 1 ) = 4
55 54 preq2i 
 |-  { 3 , ( 3 + 1 ) } = { 3 , 4 }
56 53 55 eqtrdi 
 |-  ( 3 e. ZZ -> ( 3 ... 4 ) = { 3 , 4 } )
57 40 56 eqtrd 
 |-  ( 3 e. ZZ -> ( ( ( 0 + 2 ) + 1 ) ... 4 ) = { 3 , 4 } )
58 7 57 ax-mp 
 |-  ( ( ( 0 + 2 ) + 1 ) ... 4 ) = { 3 , 4 }
59 36 58 uneq12i 
 |-  ( ( 0 ... ( 0 + 2 ) ) u. ( ( ( 0 + 2 ) + 1 ) ... 4 ) ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )
60 27 59 eqtri 
 |-  ( 0 ... 4 ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )