Beweis von Theorem 16

Es gelten die allgemeinen Vorbemerkungen.

(1) Axiom 4 ∀a: (a·0)=0
(2) Theorem 13 ∀a: (0·a)=0
(3) Spezialisierung (1) ab (b·0)=0
(4) Spezialisierung (2) ab (0·b)=0
(5) Symmetrie (3) 0=(b·0)
(6) Transitivität (4), (5) (0·b)=(b·0)
(7) Theorem 15 ∀a: ∀b: (Sa·b)=((a·b)+b)
(8) Spezialisierung (7) aa ∀b: (Sa·b)=((a·b)+b)
(9) Spezialisierung (8) bb (Sa·b)=((a·b)+b)
(10) Axiom 5 ∀a: ∀b: (a·Sb)=((a·b)+a)
(11) Spezialisierung (10) ac ∀b: (c·Sb)=((c·b)+c)
(12) Spezialisierung (11) ba (c·Sa)=((c·a)+c)
(13) Verallgemeinerung (12) nach c ∀c: (c·Sa)=((c·a)+c)
(14) Spezialisierung (13) cb (b·Sa)=((b·a)+b)
(15) Symmetrie (14) ((b·a)+b)=(b·Sa)
(16) Theorem 9 ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)>
(17) Spezialisierung (16) a(a·c) ∀b: ∀c: <(a·c)=b ⇒ ((a·c)+c)=(b+c)>
(18) Spezialisierung (17) b(c·a) ∀c: <(a·c)=(c·a) ⇒ ((a·c)+c)=((c·a)+c)>
(19) Spezialisierung (18) cb <(a·b)=(b·a) ⇒ ((a·b)+b)=((b·a)+b)>
(20) Hypothese  (a·b)=(b·a)
(21) Übernahme (19)  <(a·b)=(b·a) ⇒ ((a·b)+b)=((b·a)+b)>
(22) Modus ponens (21), (20)  ((a·b)+b)=((b·a)+b)
(23) Übernahme (9)  (Sa·b)=((a·b)+b)
(24) Übernahme (15)  ((b·a)+b)=(b·Sa)
(25) Transitivität (23), (22)  (Sa·b)=((b·a)+b)
(26) Transitivität (25), (24)  (Sa·b)=(b·Sa)
(27) Konklusion (20), (26) <(a·b)=(b·a) ⇒ (Sa·b)=(b·Sa)>
(28) Verallgemeinerung (27) nach a ∀a: <(a·b)=(b·a) ⇒ (Sa·b)=(b·Sa)>
(29) Induktion (6), (28) ∀a: (a·b)=(b·a)
(30) Spezialisierung (29) aa (a·b)=(b·a)
(31) Verallgemeinerung (30) nach b ∀b: (a·b)=(b·a)
(32) Verallgemeinerung (31) nach a ∀a: ∀b: (a·b)=(b·a)

Interpretation:

Multiplikation ist kommutativ

Übersicht