Metamath Proof Explorer


Theorem naddass

Description: Natural ordinal addition is associative. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Assertion naddass A On B On C On A + B + C = A + B + C

Proof

Step Hyp Ref Expression
1 oveq1 a = x a + b = x + b
2 1 oveq1d a = x a + b + c = x + b + c
3 oveq1 a = x a + b + c = x + b + c
4 2 3 eqeq12d a = x a + b + c = a + b + c x + b + c = x + b + c
5 oveq2 b = y x + b = x + y
6 5 oveq1d b = y x + b + c = x + y + c
7 oveq1 b = y b + c = y + c
8 7 oveq2d b = y x + b + c = x + y + c
9 6 8 eqeq12d b = y x + b + c = x + b + c x + y + c = x + y + c
10 oveq2 c = z x + y + c = x + y + z
11 oveq2 c = z y + c = y + z
12 11 oveq2d c = z x + y + c = x + y + z
13 10 12 eqeq12d c = z x + y + c = x + y + c x + y + z = x + y + z
14 oveq1 a = x a + y = x + y
15 14 oveq1d a = x a + y + z = x + y + z
16 oveq1 a = x a + y + z = x + y + z
17 15 16 eqeq12d a = x a + y + z = a + y + z x + y + z = x + y + z
18 oveq2 b = y a + b = a + y
19 18 oveq1d b = y a + b + z = a + y + z
20 oveq1 b = y b + z = y + z
21 20 oveq2d b = y a + b + z = a + y + z
22 19 21 eqeq12d b = y a + b + z = a + b + z a + y + z = a + y + z
23 5 oveq1d b = y x + b + z = x + y + z
24 20 oveq2d b = y x + b + z = x + y + z
25 23 24 eqeq12d b = y x + b + z = x + b + z x + y + z = x + y + z
26 oveq2 c = z a + y + c = a + y + z
27 11 oveq2d c = z a + y + c = a + y + z
28 26 27 eqeq12d c = z a + y + c = a + y + c a + y + z = a + y + z
29 oveq1 a = A a + b = A + b
30 29 oveq1d a = A a + b + c = A + b + c
31 oveq1 a = A a + b + c = A + b + c
32 30 31 eqeq12d a = A a + b + c = a + b + c A + b + c = A + b + c
33 oveq2 b = B A + b = A + B
34 33 oveq1d b = B A + b + c = A + B + c
35 oveq1 b = B b + c = B + c
36 35 oveq2d b = B A + b + c = A + B + c
37 34 36 eqeq12d b = B A + b + c = A + b + c A + B + c = A + B + c
38 oveq2 c = C A + B + c = A + B + C
39 oveq2 c = C B + c = B + C
40 39 oveq2d c = C A + B + c = A + B + C
41 38 40 eqeq12d c = C A + B + c = A + B + c A + B + C = A + B + C
42 simpr21 a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z x a x + b + c = x + b + c
43 eleq1 x + b + c = x + b + c x + b + c w x + b + c w
44 43 ralimi x a x + b + c = x + b + c x a x + b + c w x + b + c w
45 ralbi x a x + b + c w x + b + c w x a x + b + c w x a x + b + c w
46 42 44 45 3syl a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z x a x + b + c w x a x + b + c w
47 simpr23 a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z y b a + y + c = a + y + c
48 eleq1 a + y + c = a + y + c a + y + c w a + y + c w
49 48 ralimi y b a + y + c = a + y + c y b a + y + c w a + y + c w
50 ralbi y b a + y + c w a + y + c w y b a + y + c w y b a + y + c w
51 47 49 50 3syl a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z y b a + y + c w y b a + y + c w
52 simpr3 a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z z c a + b + z = a + b + z
53 eleq1 a + b + z = a + b + z a + b + z w a + b + z w
54 53 ralimi z c a + b + z = a + b + z z c a + b + z w a + b + z w
55 ralbi z c a + b + z w a + b + z w z c a + b + z w z c a + b + z w
56 52 54 55 3syl a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z z c a + b + z w z c a + b + z w
57 46 51 56 3anbi123d a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z x a x + b + c w y b a + y + c w z c a + b + z w x a x + b + c w y b a + y + c w z c a + b + z w
58 57 rabbidv a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z w On | x a x + b + c w y b a + y + c w z c a + b + z w = w On | x a x + b + c w y b a + y + c w z c a + b + z w
59 58 inteqd a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z w On | x a x + b + c w y b a + y + c w z c a + b + z w = w On | x a x + b + c w y b a + y + c w z c a + b + z w
60 naddasslem1 a On b On c On a + b + c = w On | x a x + b + c w y b a + y + c w z c a + b + z w
61 60 adantr a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z a + b + c = w On | x a x + b + c w y b a + y + c w z c a + b + z w
62 naddasslem2 a On b On c On a + b + c = w On | x a x + b + c w y b a + y + c w z c a + b + z w
63 62 adantr a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z a + b + c = w On | x a x + b + c w y b a + y + c w z c a + b + z w
64 59 61 63 3eqtr4d a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z a + b + c = a + b + c
65 64 ex a On b On c On x a y b z c x + y + z = x + y + z x a y b x + y + c = x + y + c x a z c x + b + z = x + b + z x a x + b + c = x + b + c y b z c a + y + z = a + y + z y b a + y + c = a + y + c z c a + b + z = a + b + z a + b + c = a + b + c
66 4 9 13 17 22 25 28 32 37 41 65 on3ind A On B On C On A + B + C = A + B + C