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 } )

Metamath Proof Explorer

Theorem fz0to5un2tp

Proof