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)

	Ref	Expression
Assertion	fz0to4untppr	⊢ ( 0 ... 4 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )

Proof

Step	Hyp	Ref	Expression
1		df-3	⊢ 3 = ( 2 + 1 )
2		2cn	⊢ 2 ∈ ℂ
3	2	addid2i	⊢ ( 0 + 2 ) = 2
4	3	eqcomi	⊢ 2 = ( 0 + 2 )
5	4	oveq1i	⊢ ( 2 + 1 ) = ( ( 0 + 2 ) + 1 )
6	1 5	eqtri	⊢ 3 = ( ( 0 + 2 ) + 1 )
7		3z	⊢ 3 ∈ ℤ
8		0re	⊢ 0 ∈ ℝ
9		3re	⊢ 3 ∈ ℝ
10		3pos	⊢ 0 < 3
11	8 9 10	ltleii	⊢ 0 ≤ 3
12		0z	⊢ 0 ∈ ℤ
13	12	eluz1i	⊢ ( 3 ∈ ( ℤ≥ ‘ 0 ) ↔ ( 3 ∈ ℤ ∧ 0 ≤ 3 ) )
14	7 11 13	mpbir2an	⊢ 3 ∈ ( ℤ≥ ‘ 0 )
15	6 14	eqeltrri	⊢ ( ( 0 + 2 ) + 1 ) ∈ ( ℤ≥ ‘ 0 )
16		4z	⊢ 4 ∈ ℤ
17		2re	⊢ 2 ∈ ℝ
18		4re	⊢ 4 ∈ ℝ
19		2lt4	⊢ 2 < 4
20	17 18 19	ltleii	⊢ 2 ≤ 4
21		2z	⊢ 2 ∈ ℤ
22	21	eluz1i	⊢ ( 4 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 4 ∈ ℤ ∧ 2 ≤ 4 ) )
23	16 20 22	mpbir2an	⊢ 4 ∈ ( ℤ≥ ‘ 2 )
24	4	fveq2i	⊢ ( ℤ≥ ‘ 2 ) = ( ℤ≥ ‘ ( 0 + 2 ) )
25	23 24	eleqtri	⊢ 4 ∈ ( ℤ≥ ‘ ( 0 + 2 ) )
26		fzsplit2	⊢ ( ( ( ( 0 + 2 ) + 1 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 4 ∈ ( ℤ≥ ‘ ( 0 + 2 ) ) ) → ( 0 ... 4 ) = ( ( 0 ... ( 0 + 2 ) ) ∪ ( ( ( 0 + 2 ) + 1 ) ... 4 ) ) )
27	15 25 26	mp2an	⊢ ( 0 ... 4 ) = ( ( 0 ... ( 0 + 2 ) ) ∪ ( ( ( 0 + 2 ) + 1 ) ... 4 ) )
28		fztp	⊢ ( 0 ∈ ℤ → ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) } )
29	12 28	ax-mp	⊢ ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) }
30		ax-1cn	⊢ 1 ∈ ℂ
31		eqidd	⊢ ( 1 ∈ ℂ → 0 = 0 )
32		addid2	⊢ ( 1 ∈ ℂ → ( 0 + 1 ) = 1 )
33	3	a1i	⊢ ( 1 ∈ ℂ → ( 0 + 2 ) = 2 )
34	31 32 33	tpeq123d	⊢ ( 1 ∈ ℂ → { 0 , ( 0 + 1 ) , ( 0 + 2 ) } = { 0 , 1 , 2 } )
35	30 34	ax-mp	⊢ { 0 , ( 0 + 1 ) , ( 0 + 2 ) } = { 0 , 1 , 2 }
36	29 35	eqtri	⊢ ( 0 ... ( 0 + 2 ) ) = { 0 , 1 , 2 }
37	3	a1i	⊢ ( 3 ∈ ℤ → ( 0 + 2 ) = 2 )
38	37	oveq1d	⊢ ( 3 ∈ ℤ → ( ( 0 + 2 ) + 1 ) = ( 2 + 1 ) )
39	38 1	eqtr4di	⊢ ( 3 ∈ ℤ → ( ( 0 + 2 ) + 1 ) = 3 )
40	39	oveq1d	⊢ ( 3 ∈ ℤ → ( ( ( 0 + 2 ) + 1 ) ... 4 ) = ( 3 ... 4 ) )
41		eqid	⊢ 3 = 3
42		df-4	⊢ 4 = ( 3 + 1 )
43	41 42	pm3.2i	⊢ ( 3 = 3 ∧ 4 = ( 3 + 1 ) )
44	43	a1i	⊢ ( 3 ∈ ℤ → ( 3 = 3 ∧ 4 = ( 3 + 1 ) ) )
45		3lt4	⊢ 3 < 4
46	9 18 45	ltleii	⊢ 3 ≤ 4
47	7	eluz1i	⊢ ( 4 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 4 ∈ ℤ ∧ 3 ≤ 4 ) )
48	16 46 47	mpbir2an	⊢ 4 ∈ ( ℤ≥ ‘ 3 )
49		fzopth	⊢ ( 4 ∈ ( ℤ≥ ‘ 3 ) → ( ( 3 ... 4 ) = ( 3 ... ( 3 + 1 ) ) ↔ ( 3 = 3 ∧ 4 = ( 3 + 1 ) ) ) )
50	48 49	ax-mp	⊢ ( ( 3 ... 4 ) = ( 3 ... ( 3 + 1 ) ) ↔ ( 3 = 3 ∧ 4 = ( 3 + 1 ) ) )
51	44 50	sylibr	⊢ ( 3 ∈ ℤ → ( 3 ... 4 ) = ( 3 ... ( 3 + 1 ) ) )
52		fzpr	⊢ ( 3 ∈ ℤ → ( 3 ... ( 3 + 1 ) ) = { 3 , ( 3 + 1 ) } )
53	51 52	eqtrd	⊢ ( 3 ∈ ℤ → ( 3 ... 4 ) = { 3 , ( 3 + 1 ) } )
54	42	eqcomi	⊢ ( 3 + 1 ) = 4
55	54	preq2i	⊢ { 3 , ( 3 + 1 ) } = { 3 , 4 }
56	53 55	eqtrdi	⊢ ( 3 ∈ ℤ → ( 3 ... 4 ) = { 3 , 4 } )
57	40 56	eqtrd	⊢ ( 3 ∈ ℤ → ( ( ( 0 + 2 ) + 1 ) ... 4 ) = { 3 , 4 } )
58	7 57	ax-mp	⊢ ( ( ( 0 + 2 ) + 1 ) ... 4 ) = { 3 , 4 }
59	36 58	uneq12i	⊢ ( ( 0 ... ( 0 + 2 ) ) ∪ ( ( ( 0 + 2 ) + 1 ) ... 4 ) ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )
60	27 59	eqtri	⊢ ( 0 ... 4 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )