Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 2 | ∀a: (a+0)=a | |||||||||
| (2) | Spezialisierung (1) a ← b | (b+0)=b | |||||||||
| (3) | Theorem 1 | ∀a: a=a | |||||||||
| (4) | Spezialisierung (3) a ← (a·b) | (a·b)=(a·b) | |||||||||
| (5) | Axiom 4 | ∀a: (a·0)=0 | |||||||||
| (6) | Spezialisierung (5) a ← a | (a·0)=0 | |||||||||
| (7) | Spezialisierung (1) a ← (a·b) | ((a·b)+0)=(a·b) | |||||||||
| (8) | Theorem 10 | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a+b)=(c+d)> | |||||||||
| (9) | Spezialisierung (8) a ← c | ∀b: ∀c: ∀d: <<c=c∧b=d> ⇒ (c+b)=(c+d)> | |||||||||
| (10) | Spezialisierung (9) b ← (a·0) | ∀c: ∀d: <<c=c∧(a·0)=d> ⇒ (c+(a·0))=(c+d)> | |||||||||
| (11) | Spezialisierung (10) c ← (a·b) | ∀d: <<(a·b)=(a·b)∧(a·0)=d> ⇒ ((a·b)+(a·0))=((a·b)+d)> | |||||||||
| (12) | Spezialisierung (11) d ← 0 | <<(a·b)=(a·b)∧(a·0)=0> ⇒ ((a·b)+(a·0))=((a·b)+0)> | |||||||||
| (13) | Konjunktion (4), (6) | <(a·b)=(a·b)∧(a·0)=0> | |||||||||
| (14) | Modus ponens (12), (13) | ((a·b)+(a·0))=((a·b)+0) | |||||||||
| (15) | Transitivität (14), (7) | ((a·b)+(a·0))=(a·b) | |||||||||
| (16) | Symmetrie (15) | (a·b)=((a·b)+(a·0)) | |||||||||
| (17) | Theorem 18 | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a·b)=(c·d)> | |||||||||
| (18) | Spezialisierung (17) a ← c | ∀b: ∀c: ∀d: <<c=c∧b=d> ⇒ (c·b)=(c·d)> | |||||||||
| (19) | Spezialisierung (18) b ← e | ∀c: ∀d: <<c=c∧e=d> ⇒ (c·e)=(c·d)> | |||||||||
| (20) | Spezialisierung (19) c ← c | ∀d: <<c=c∧e=d> ⇒ (c·e)=(c·d)> | |||||||||
| (21) | Spezialisierung (20) d ← d | <<c=c∧e=d> ⇒ (c·e)=(c·d)> | |||||||||
| (22) | Spezialisierung (3) a ← c | c=c | |||||||||
| (23) | Hypothese | e=d | |||||||||
| (24) | Übernahme (21) | <<c=c∧e=d> ⇒ (c·e)=(c·d)> | |||||||||
| (25) | Übernahme (22) | c=c | |||||||||
| (26) | Konjunktion (25), (23) | <c=c∧e=d> | |||||||||
| (27) | Modus ponens (24), (26) | (c·e)=(c·d) | |||||||||
| (28) | Konklusion (23), (27) | <e=d ⇒ (c·e)=(c·d)> | |||||||||
| (29) | Verallgemeinerung (28) nach d | ∀d: <e=d ⇒ (c·e)=(c·d)> | |||||||||
| (30) | Verallgemeinerung (29) nach e | ∀e: ∀d: <e=d ⇒ (c·e)=(c·d)> | |||||||||
| (31) | Verallgemeinerung (30) nach c | ∀c: ∀e: ∀d: <e=d ⇒ (c·e)=(c·d)> | |||||||||
| (32) | Spezialisierung (31) c ← a | ∀e: ∀d: <e=d ⇒ (a·e)=(a·d)> | |||||||||
| (33) | Spezialisierung (32) e ← (b+0) | ∀d: <(b+0)=d ⇒ (a·(b+0))=(a·d)> | |||||||||
| (34) | Spezialisierung (33) d ← b | <(b+0)=b ⇒ (a·(b+0))=(a·b)> | |||||||||
| (35) | Modus ponens (34), (2) | (a·(b+0))=(a·b) | |||||||||
| (36) | Transitivität (35), (16) | (a·(b+0))=((a·b)+(a·0)) | |||||||||
| (37) | Spezialisierung (32) e ← (b+Sc) | ∀d: <(b+Sc)=d ⇒ (a·(b+Sc))=(a·d)> | |||||||||
| (38) | Spezialisierung (37) d ← S(b+c) | <(b+Sc)=S(b+c) ⇒ (a·(b+Sc))=(a·S(b+c))> | |||||||||
| (39) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (40) | Spezialisierung (39) a ← a | ∀b: (a+Sb)=S(a+b) | |||||||||
| (41) | Spezialisierung (40) b ← c | (a+Sc)=S(a+c) | |||||||||
| (42) | Verallgemeinerung (41) nach a | ∀a: (a+Sc)=S(a+c) | |||||||||
| (43) | Spezialisierung (42) a ← b | (b+Sc)=S(b+c) | |||||||||
| (44) | Modus ponens (38), (43) | (a·(b+Sc))=(a·S(b+c)) | |||||||||
| (45) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (46) | Spezialisierung (45) a ← a | ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (47) | Spezialisierung (46) b ← (b+c) | (a·S(b+c))=((a·(b+c))+a) | |||||||||
| (48) | Transitivität (44), (47) | (a·(b+Sc))=((a·(b+c))+a) | |||||||||
| (49) | Theorem 12 | ∀a: ∀b: ∀c: (a+(b+c))=((a+b)+c) | |||||||||
| (50) | Spezialisierung (49) a ← (c·d) | ∀b: ∀c: ((c·d)+(b+c))=(((c·d)+b)+c) | |||||||||
| (51) | Spezialisierung (50) b ← (c·e) | ∀c: ((c·d)+((c·e)+c))=(((c·d)+(c·e))+c) | |||||||||
| (52) | Spezialisierung (51) c ← a | ((a·d)+((a·e)+a))=(((a·d)+(a·e))+a) | |||||||||
| (53) | Verallgemeinerung (52) nach d | ∀d: ((a·d)+((a·e)+a))=(((a·d)+(a·e))+a) | |||||||||
| (54) | Spezialisierung (53) d ← b | ((a·b)+((a·e)+a))=(((a·b)+(a·e))+a) | |||||||||
| (55) | Verallgemeinerung (54) nach e | ∀e: ((a·b)+((a·e)+a))=(((a·b)+(a·e))+a) | |||||||||
| (56) | Spezialisierung (55) e ← c | ((a·b)+((a·c)+a))=(((a·b)+(a·c))+a) | |||||||||
| (57) | Spezialisierung (9) b ← e | ∀c: ∀d: <<c=c∧e=d> ⇒ (c+e)=(c+d)> | |||||||||
| (58) | Spezialisierung (57) c ← (a·b) | ∀d: <<(a·b)=(a·b)∧e=d> ⇒ ((a·b)+e)=((a·b)+d)> | |||||||||
| (59) | Spezialisierung (58) d ← ((a·c)+a) | <<(a·b)=(a·b)∧e=((a·c)+a)> ⇒ ((a·b)+e)=((a·b)+((a·c)+a))> | |||||||||
| (60) | Verallgemeinerung (59) nach e | ∀e: <<(a·b)=(a·b)∧e=((a·c)+a)> ⇒ ((a·b)+e)=((a·b)+((a·c)+a))> | |||||||||
| (61) | Spezialisierung (60) e ← (a·Sc) | <<(a·b)=(a·b)∧(a·Sc)=((a·c)+a)> ⇒ ((a·b)+(a·Sc))=((a·b)+((a·c)+a))> | |||||||||
| (62) | Spezialisierung (46) b ← c | (a·Sc)=((a·c)+a) | |||||||||
| (63) | Konjunktion (4), (62) | <(a·b)=(a·b)∧(a·Sc)=((a·c)+a)> | |||||||||
| (64) | Modus ponens (61), (63) | ((a·b)+(a·Sc))=((a·b)+((a·c)+a)) | |||||||||
| (65) | Transitivität (64), (56) | ((a·b)+(a·Sc))=(((a·b)+(a·c))+a) | |||||||||
| (66) | Symmetrie (65) | (((a·b)+(a·c))+a)=((a·b)+(a·Sc)) | |||||||||
| (67) | Theorem 9 | ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (68) | Spezialisierung (67) a ← d | ∀b: ∀c: <d=b ⇒ (d+c)=(b+c)> | |||||||||
| (69) | Spezialisierung (68) b ← e | ∀c: <d=e ⇒ (d+c)=(e+c)> | |||||||||
| (70) | Spezialisierung (69) c ← a | <d=e ⇒ (d+a)=(e+a)> | |||||||||
| (71) | Verallgemeinerung (70) nach d | ∀d: <d=e ⇒ (d+a)=(e+a)> | |||||||||
| (72) | Spezialisierung (71) d ← (a·(b+c)) | <(a·(b+c))=e ⇒ ((a·(b+c))+a)=(e+a)> | |||||||||
| (73) | Verallgemeinerung (72) nach e | ∀e: <(a·(b+c))=e ⇒ ((a·(b+c))+a)=(e+a)> | |||||||||
| (74) | Spezialisierung (73) e ← ((a·b)+(a·c)) | <(a·(b+c))=((a·b)+(a·c)) ⇒ ((a·(b+c))+a)=(((a·b)+(a·c))+a)> | |||||||||
| (75) | Hypothese | (a·(b+c))=((a·b)+(a·c)) | |||||||||
| (76) | Übernahme (48) | (a·(b+Sc))=((a·(b+c))+a) | |||||||||
| (77) | Übernahme (66) | (((a·b)+(a·c))+a)=((a·b)+(a·Sc)) | |||||||||
| (78) | Übernahme (74) | <(a·(b+c))=((a·b)+(a·c)) ⇒ ((a·(b+c))+a)=(((a·b)+(a·c))+a)> | |||||||||
| (79) | Modus ponens (78), (75) | ((a·(b+c))+a)=(((a·b)+(a·c))+a) | |||||||||
| (80) | Transitivität (76), (79) | (a·(b+Sc))=(((a·b)+(a·c))+a) | |||||||||
| (81) | Transitivität (80), (77) | (a·(b+Sc))=((a·b)+(a·Sc)) | |||||||||
| (82) | Konklusion (75), (81) | <(a·(b+c))=((a·b)+(a·c)) ⇒ (a·(b+Sc))=((a·b)+(a·Sc))> | |||||||||
| (83) | Verallgemeinerung (82) nach c | ∀c: <(a·(b+c))=((a·b)+(a·c)) ⇒ (a·(b+Sc))=((a·b)+(a·Sc))> | |||||||||
| (84) | Induktion (36), (83) | ∀c: (a·(b+c))=((a·b)+(a·c)) | |||||||||
| (85) | Verallgemeinerung (84) nach b | ∀b: ∀c: (a·(b+c))=((a·b)+(a·c)) | |||||||||
| (86) | Verallgemeinerung (85) nach a | ∀a: ∀b: ∀c: (a·(b+c))=((a·b)+(a·c)) | |||||||||
Interpretation:
Multiplikation ist rechtsdistributiv über die Addition