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 } ∪ { 3 , 4 , 5 } )

Proof

Step	Hyp	Ref	Expression
1		2p1e3	⊢ ( 2 + 1 ) = 3
2		0z	⊢ 0 ∈ ℤ
3		3z	⊢ 3 ∈ ℤ
4		0re	⊢ 0 ∈ ℝ
5		3re	⊢ 3 ∈ ℝ
6		3pos	⊢ 0 < 3
7	4 5 6	ltleii	⊢ 0 ≤ 3
8		eluz2	⊢ ( 3 ∈ ( ℤ≥ ‘ 0 ) ↔ ( 0 ∈ ℤ ∧ 3 ∈ ℤ ∧ 0 ≤ 3 ) )
9	2 3 7 8	mpbir3an	⊢ 3 ∈ ( ℤ≥ ‘ 0 )
10	1 9	eqeltri	⊢ ( 2 + 1 ) ∈ ( ℤ≥ ‘ 0 )
11		2z	⊢ 2 ∈ ℤ
12		5nn0	⊢ 5 ∈ ℕ0
13	12	nn0zi	⊢ 5 ∈ ℤ
14		2re	⊢ 2 ∈ ℝ
15		5re	⊢ 5 ∈ ℝ
16		2lt5	⊢ 2 < 5
17	14 15 16	ltleii	⊢ 2 ≤ 5
18		eluz2	⊢ ( 5 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 5 ∈ ℤ ∧ 2 ≤ 5 ) )
19	11 13 17 18	mpbir3an	⊢ 5 ∈ ( ℤ≥ ‘ 2 )
20		fzsplit2	⊢ ( ( ( 2 + 1 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 5 ∈ ( ℤ≥ ‘ 2 ) ) → ( 0 ... 5 ) = ( ( 0 ... 2 ) ∪ ( ( 2 + 1 ) ... 5 ) ) )
21	10 19 20	mp2an	⊢ ( 0 ... 5 ) = ( ( 0 ... 2 ) ∪ ( ( 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 ∈ ℤ → ( 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 ) ∪ ( ( 2 + 1 ) ... 5 ) ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
39	21 38	eqtri	⊢ ( 0 ... 5 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )