Metamath Proof Explorer


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