Theorem fz0to5un2tp

Description: An integer range from 0 to 5 is the union of two triples. (Contributed by AV, 30-Jul-2025)

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

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		5nn0	|- 5 e. NN0
13	12	nn0zi	|- 5 e. ZZ
14		2re	|- 2 e. RR
15		5re	|- 5 e. RR
16		2lt5	|- 2 < 5
17	14 15 16	ltleii	|- 2 <_ 5
18		eluz2	|- ( 5 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 5 e. ZZ /\ 2 <_ 5 ) )
19	11 13 17 18	mpbir3an	|- 5 e. ( ZZ>= ` 2 )
20		fzsplit2	|- ( ( ( 2 + 1 ) e. ( ZZ>= ` 0 ) /\ 5 e. ( ZZ>= ` 2 ) ) -> ( 0 ... 5 ) = ( ( 0 ... 2 ) u. ( ( 2 + 1 ) ... 5 ) ) )
21	10 19 20	mp2an	|- ( 0 ... 5 ) = ( ( 0 ... 2 ) u. ( ( 2 + 1 ) ... 5 ) )
22		fz0tp	|- ( 0 ... 2 ) = { 0 , 1 , 2 }
23	1	oveq1i	|- ( ( 2 + 1 ) ... 5 ) = ( 3 ... 5 )
24		3p2e5	|- ( 3 + 2 ) = 5
25	24	eqcomi	|- 5 = ( 3 + 2 )
26	25	oveq2i	|- ( 3 ... 5 ) = ( 3 ... ( 3 + 2 ) )
27		fztp	|- ( 3 e. ZZ -> ( 3 ... ( 3 + 2 ) ) = { 3 , ( 3 + 1 ) , ( 3 + 2 ) } )
28	3 27	ax-mp	|- ( 3 ... ( 3 + 2 ) ) = { 3 , ( 3 + 1 ) , ( 3 + 2 ) }
29		eqid	|- 3 = 3
30		id	|- ( 3 = 3 -> 3 = 3 )
31		3p1e4	|- ( 3 + 1 ) = 4
32	31	a1i	|- ( 3 = 3 -> ( 3 + 1 ) = 4 )
33	24	a1i	|- ( 3 = 3 -> ( 3 + 2 ) = 5 )
34	30 32 33	tpeq123d	|- ( 3 = 3 -> { 3 , ( 3 + 1 ) , ( 3 + 2 ) } = { 3 , 4 , 5 } )
35	29 34	ax-mp	|- { 3 , ( 3 + 1 ) , ( 3 + 2 ) } = { 3 , 4 , 5 }
36	26 28 35	3eqtri	|- ( 3 ... 5 ) = { 3 , 4 , 5 }
37	23 36	eqtri	|- ( ( 2 + 1 ) ... 5 ) = { 3 , 4 , 5 }
38	22 37	uneq12i	|- ( ( 0 ... 2 ) u. ( ( 2 + 1 ) ... 5 ) ) = ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
39	21 38	eqtri	|- ( 0 ... 5 ) = ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )