Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 1 | ∀a: a=a | |||||||||
| (2) | Spezialisierung (1) a ← 0 | 0=0 | |||||||||
| (3) | Hypothese | <¬a=0∧¬0=0> | |||||||||
| (4) | Abtrennung II (3) | ¬0=0 | |||||||||
| (5) | Konklusion (3), (4) | <<¬a=0∧¬0=0> ⇒ ¬0=0> | |||||||||
| (6) | Kontraposition (5) | <¬¬0=0 ⇒ ¬<¬a=0∧¬0=0>> | |||||||||
| (7) | Doppelte Negation (2) | ¬¬0=0 | |||||||||
| (8) | Modus ponens (6), (7) | ¬<¬a=0∧¬0=0> | |||||||||
| (9) | Hypothese | (a·0)=0 | |||||||||
| (10) | Übernahme (8) | ¬<¬a=0∧¬0=0> | |||||||||
| (11) | Konklusion (9), (10) | <(a·0)=0 ⇒ ¬<¬a=0∧¬0=0>> | |||||||||
| (12) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (13) | Spezialisierung (12) a ← a | ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (14) | Spezialisierung (13) b ← b | (a·Sb)=((a·b)+a) | |||||||||
| (15) | Symmetrie (14) | ((a·b)+a)=(a·Sb) | |||||||||
| (16) | Theorem 4 | ∀a: ∀b: <(a+b)=0 ⇒ <a=0∧b=0>> | |||||||||
| (17) | Spezialisierung (16) a ← (b·c) | ∀b: <((b·c)+b)=0 ⇒ <(b·c)=0∧b=0>> | |||||||||
| (18) | Spezialisierung (17) b ← a | <((a·c)+a)=0 ⇒ <(a·c)=0∧a=0>> | |||||||||
| (19) | Verallgemeinerung (18) nach c | ∀c: <((a·c)+a)=0 ⇒ <(a·c)=0∧a=0>> | |||||||||
| (20) | Spezialisierung (19) c ← b | <((a·b)+a)=0 ⇒ <(a·b)=0∧a=0>> | |||||||||
| (21) | Hypothese | <(a·b)=0 ⇒ ¬<¬a=0∧¬b=0>> | |||||||||
| (22) | Hypothese | (a·Sb)=0 | |||||||||
| (23) | Übernahme (15) | ((a·b)+a)=(a·Sb) | |||||||||
| (24) | Transitivität (23), (22) | ((a·b)+a)=0 | |||||||||
| (25) | Übernahme (20) | <((a·b)+a)=0 ⇒ <(a·b)=0∧a=0>> | |||||||||
| (26) | Modus ponens (25), (24) | <(a·b)=0∧a=0> | |||||||||
| (27) | Abtrennung II (26) | a=0 | |||||||||
| (28) | Hypothese | <¬a=0∧¬Sb=0> | |||||||||
| (29) | Abtrennung I (28) | ¬a=0 | |||||||||
| (30) | Konklusion (28), (29) | <<¬a=0∧¬Sb=0> ⇒ ¬a=0> | |||||||||
| (31) | Kontraposition (30) | <¬¬a=0 ⇒ ¬<¬a=0∧¬Sb=0>> | |||||||||
| (32) | Doppelte Negation (27) | ¬¬a=0 | |||||||||
| (33) | Modus ponens (31), (32) | ¬<¬a=0∧¬Sb=0> | |||||||||
| (34) | Konklusion (22), (33) | <(a·Sb)=0 ⇒ ¬<¬a=0∧¬Sb=0>> | |||||||||
| (35) | Konklusion (21), (34) | <<(a·b)=0 ⇒ ¬<¬a=0∧¬b=0>> ⇒ <(a·Sb)=0 ⇒ ¬<¬a=0∧¬Sb=0>>> | |||||||||
| (36) | Verallgemeinerung (35) nach b | ∀b: <<(a·b)=0 ⇒ ¬<¬a=0∧¬b=0>> ⇒ <(a·Sb)=0 ⇒ ¬<¬a=0∧¬Sb=0>>> | |||||||||
| (37) | Induktion (11), (36) | ∀b: <(a·b)=0 ⇒ ¬<¬a=0∧¬b=0>> | |||||||||
| (38) | Verallgemeinerung (37) nach a | ∀a: ∀b: <(a·b)=0 ⇒ ¬<¬a=0∧¬b=0>> | |||||||||
Interpretation:
Ein Produkt ist nur dann 0, wenn ein Faktor 0 ist