Peano Arithmetic — Commutativity, Multiplication, Distributivity

graph TD A5["A5\nInduction"] DefAdd["DefAdd\nDefinition of +"] T5["T5\nAssociativity of +"] T6["T6\nLeft identity"] T7["T7\nSuccessor and add"] T8["T8\nCommutativity of +"] T9["T9\nCancellation for +"] DefMul["DefMul\nDefinition of ·"] T10["T10\nMul well-defined"] T11["T11\nZero times"] T12["T12\nZero from left"] T13["T13\nSuccessor and mul"] T14["T14\nCommutativity of ·"] T15["T15\nAssociativity of ·"] T16["T16\nDistributivity"] T17["T17\nDistributivity (right)"] A5 --> DefAdd DefAdd --> T5 A5 --> T5 DefAdd --> T6 A5 --> T6 DefAdd --> T7 T6 --> T7 A5 --> T7 DefAdd --> T8 T5 --> T8 T6 --> T8 T7 --> T8 A5 --> T8 DefAdd --> T9 T8 --> T9 A5 --> T9 DefAdd --> DefMul A5 --> DefMul DefMul --> T10 A5 --> T10 DefMul --> T11 DefMul --> T12 T6 --> T12 A5 --> T12 DefMul --> T13 T8 --> T13 A5 --> T13 DefMul --> T14 T12 --> T14 T13 --> T14 A5 --> T14 DefMul --> T15 T5 --> T15 T8 --> T15 A5 --> T15 DefMul --> T16 T5 --> T16 T8 --> T16 T15 --> T16 A5 --> T16 T16 --> T17 T8 --> T17 classDef axiom fill:#ff6b6b,color:#fff,stroke:#c0392b classDef definition fill:#b197fc,color:#fff,stroke:#9775fa classDef theorem fill:#51cf66,color:#fff,stroke:#40c057 class A5 axiom class DefAdd,DefMul definition class T5,T6,T7,T8,T9,T10,T11,T12,T13,T14,T15,T16,T17 theorem