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

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		4z	⊢ 4 ∈ ℤ
13		2re	⊢ 2 ∈ ℝ
14		4re	⊢ 4 ∈ ℝ
15		2lt4	⊢ 2 < 4
16	13 14 15	ltleii	⊢ 2 ≤ 4
17		eluz2	⊢ ( 4 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 4 ∈ ℤ ∧ 2 ≤ 4 ) )
18	11 12 16 17	mpbir3an	⊢ 4 ∈ ( ℤ≥ ‘ 2 )
19		fzsplit2	⊢ ( ( ( 2 + 1 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 4 ∈ ( ℤ≥ ‘ 2 ) ) → ( 0 ... 4 ) = ( ( 0 ... 2 ) ∪ ( ( 2 + 1 ) ... 4 ) ) )
20	10 18 19	mp2an	⊢ ( 0 ... 4 ) = ( ( 0 ... 2 ) ∪ ( ( 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 ∈ ℤ → ( 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 ) ∪ ( ( 2 + 1 ) ... 4 ) ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )
32	20 31	eqtri	⊢ ( 0 ... 4 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )