Metamath Proof Explorer


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