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) (Proof shortened by AV, 7-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		2p1e3	|- ( 2 + 1 ) = 3
2		0z	|- 0 e. ZZ
3		3z	|- 3 e. ZZ
4		0re	|- 0 e. RR
5		3re	|- 3 e. RR
6		3pos	|- 0 < 3
7	4 5 6	ltleii	|- 0 <_ 3
8		eluz2	|- ( 3 e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ 3 e. ZZ /\ 0 <_ 3 ) )
9	2 3 7 8	mpbir3an	|- 3 e. ( ZZ>= ` 0 )
10	1 9	eqeltri	|- ( 2 + 1 ) e. ( ZZ>= ` 0 )
11		2z	|- 2 e. ZZ
12		4z	|- 4 e. ZZ
13		2re	|- 2 e. RR
14		4re	|- 4 e. RR
15		2lt4	|- 2 < 4
16	13 14 15	ltleii	|- 2 <_ 4
17		eluz2	|- ( 4 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 4 e. ZZ /\ 2 <_ 4 ) )
18	11 12 16 17	mpbir3an	|- 4 e. ( ZZ>= ` 2 )
19		fzsplit2	|- ( ( ( 2 + 1 ) e. ( ZZ>= ` 0 ) /\ 4 e. ( ZZ>= ` 2 ) ) -> ( 0 ... 4 ) = ( ( 0 ... 2 ) u. ( ( 2 + 1 ) ... 4 ) ) )
20	10 18 19	mp2an	|- ( 0 ... 4 ) = ( ( 0 ... 2 ) u. ( ( 2 + 1 ) ... 4 ) )
21		fz0tp	|- ( 0 ... 2 ) = { 0 , 1 , 2 }
22	1	oveq1i	|- ( ( 2 + 1 ) ... 4 ) = ( 3 ... 4 )
23		df-4	|- 4 = ( 3 + 1 )
24	23	oveq2i	|- ( 3 ... 4 ) = ( 3 ... ( 3 + 1 ) )
25		fzpr	|- ( 3 e. ZZ -> ( 3 ... ( 3 + 1 ) ) = { 3 , ( 3 + 1 ) } )
26	3 25	ax-mp	|- ( 3 ... ( 3 + 1 ) ) = { 3 , ( 3 + 1 ) }
27		3p1e4	|- ( 3 + 1 ) = 4
28	27	preq2i	|- { 3 , ( 3 + 1 ) } = { 3 , 4 }
29	24 26 28	3eqtri	|- ( 3 ... 4 ) = { 3 , 4 }
30	22 29	eqtri	|- ( ( 2 + 1 ) ... 4 ) = { 3 , 4 }
31	21 30	uneq12i	|- ( ( 0 ... 2 ) u. ( ( 2 + 1 ) ... 4 ) ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )
32	20 31	eqtri	|- ( 0 ... 4 ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )