Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 17 | ∀a: ∀b: ∀c: <a=b ⇒ (a·c)=(b·c)> | |||||||||
| (2) | Spezialisierung (1) a ← (Sa·Sd) | ∀b: ∀c: <(Sa·Sd)=b ⇒ ((Sa·Sd)·c)=(b·c)> | |||||||||
| (3) | Spezialisierung (2) b ← b | ∀c: <(Sa·Sd)=b ⇒ ((Sa·Sd)·c)=(b·c)> | |||||||||
| (4) | Spezialisierung (3) c ← Se | <(Sa·Sd)=b ⇒ ((Sa·Sd)·Se)=(b·Se)> | |||||||||
| (5) | Theorem 21 | ∀a: ∀b: ∀c: (a·(b·c))=((a·b)·c) | |||||||||
| (6) | Spezialisierung (5) a ← Sa | ∀b: ∀c: (Sa·(b·c))=((Sa·b)·c) | |||||||||
| (7) | Spezialisierung (6) b ← Sd | ∀c: (Sa·(Sd·c))=((Sa·Sd)·c) | |||||||||
| (8) | Spezialisierung (7) c ← Se | (Sa·(Sd·Se))=((Sa·Sd)·Se) | |||||||||
| (9) | Theorem 30 | ∀a: ∀b: <(Sa·b)=Sa ⇒ b=S0> | |||||||||
| (10) | Spezialisierung (9) a ← a | ∀b: <(Sa·b)=Sa ⇒ b=S0> | |||||||||
| (11) | Spezialisierung (10) b ← (Sd·Se) | <(Sa·(Sd·Se))=Sa ⇒ (Sd·Se)=S0> | |||||||||
| (12) | Theorem 31 | ∀a: ∀b: <(a·b)=S0 ⇒ <a=S0∧b=S0>> | |||||||||
| (13) | Spezialisierung (12) a ← Sd | ∀b: <(Sd·b)=S0 ⇒ <Sd=S0∧b=S0>> | |||||||||
| (14) | Spezialisierung (13) b ← Se | <(Sd·Se)=S0 ⇒ <Sd=S0∧Se=S0>> | |||||||||
| (15) | Theorem 26 | ∀a: ∀b: <b=S0 ⇒ (a·b)=a> | |||||||||
| (16) | Spezialisierung (15) a ← Sa | ∀b: <b=S0 ⇒ (Sa·b)=Sa> | |||||||||
| (17) | Spezialisierung (16) b ← Sd | <Sd=S0 ⇒ (Sa·Sd)=Sa> | |||||||||
| (18) | Hypothese | <(Sa·Sd)=b∧(b·Se)=Sa> | |||||||||
| (19) | Abtrennung I (18) | (Sa·Sd)=b | |||||||||
| (20) | Abtrennung II (18) | (b·Se)=Sa | |||||||||
| (21) | Übernahme (4) | <(Sa·Sd)=b ⇒ ((Sa·Sd)·Se)=(b·Se)> | |||||||||
| (22) | Modus ponens (21), (19) | ((Sa·Sd)·Se)=(b·Se) | |||||||||
| (23) | Transitivität (22), (20) | ((Sa·Sd)·Se)=Sa | |||||||||
| (24) | Übernahme (8) | (Sa·(Sd·Se))=((Sa·Sd)·Se) | |||||||||
| (25) | Transitivität (24), (23) | (Sa·(Sd·Se))=Sa | |||||||||
| (26) | Übernahme (11) | <(Sa·(Sd·Se))=Sa ⇒ (Sd·Se)=S0> | |||||||||
| (27) | Modus ponens (26), (25) | (Sd·Se)=S0 | |||||||||
| (28) | Übernahme (14) | <(Sd·Se)=S0 ⇒ <Sd=S0∧Se=S0>> | |||||||||
| (29) | Modus ponens (28), (27) | <Sd=S0∧Se=S0> | |||||||||
| (30) | Abtrennung I (29) | Sd=S0 | |||||||||
| (31) | Übernahme (17) | <Sd=S0 ⇒ (Sa·Sd)=Sa> | |||||||||
| (32) | Modus ponens (31), (30) | (Sa·Sd)=Sa | |||||||||
| (33) | Symmetrie (32) | Sa=(Sa·Sd) | |||||||||
| (34) | Transitivität (33), (19) | Sa=b | |||||||||
| (35) | Konklusion (18), (34) | <<(Sa·Sd)=b∧(b·Se)=Sa> ⇒ Sa=b> | |||||||||
| (36) | Hypothese | <<(a·Sd)=b∧(b·Se)=a> ⇒ a=b> | |||||||||
| (37) | Übernahme (35) | <<(Sa·Sd)=b∧(b·Se)=Sa> ⇒ Sa=b> | |||||||||
| (38) | Konklusion (36), (37) | <<<(a·Sd)=b∧(b·Se)=a> ⇒ a=b> ⇒ <<(Sa·Sd)=b∧(b·Se)=Sa> ⇒ Sa=b>> | |||||||||
| (39) | Verallgemeinerung (38) nach a | ∀a: <<<(a·Sd)=b∧(b·Se)=a> ⇒ a=b> ⇒ <<(Sa·Sd)=b∧(b·Se)=Sa> ⇒ Sa=b>> | |||||||||
| (40) | Theorem 13 | ∀a: (0·a)=0 | |||||||||
| (41) | Spezialisierung (40) a ← Sd | (0·Sd)=0 | |||||||||
| (42) | Hypothese | <(0·Sd)=b∧(b·Se)=0> | |||||||||
| (43) | Abtrennung I (42) | (0·Sd)=b | |||||||||
| (44) | Übernahme (41) | (0·Sd)=0 | |||||||||
| (45) | Symmetrie (44) | 0=(0·Sd) | |||||||||
| (46) | Transitivität (45), (43) | 0=b | |||||||||
| (47) | Konklusion (42), (46) | <<(0·Sd)=b∧(b·Se)=0> ⇒ 0=b> | |||||||||
| (48) | Induktion (47), (39) | ∀a: <<(a·Sd)=b∧(b·Se)=a> ⇒ a=b> | |||||||||
| (49) | Spezialisierung (48) a ← a | <<(a·Sd)=b∧(b·Se)=a> ⇒ a=b> | |||||||||
| (50) | Kontraposition (49) | <¬a=b ⇒ ¬<(a·Sd)=b∧(b·Se)=a>> | |||||||||
| (51) | Hypothese | ¬a=b | |||||||||
| (52) | Übernahme (50) | <¬a=b ⇒ ¬<(a·Sd)=b∧(b·Se)=a>> | |||||||||
| (53) | Modus ponens (52), (51) | ¬<(a·Sd)=b∧(b·Se)=a> | |||||||||
| (54) | Hypothese | (a·Sd)=b | |||||||||
| (55) | Hypothese | (b·Se)=a | |||||||||
| (56) | Übernahme (54) | (a·Sd)=b | |||||||||
| (57) | Konjunktion (56), (55) | <(a·Sd)=b∧(b·Se)=a> | |||||||||
| (58) | Konklusion (55), (57) | <(b·Se)=a ⇒ <(a·Sd)=b∧(b·Se)=a>> | |||||||||
| (59) | Kontraposition (58) | <¬<(a·Sd)=b∧(b·Se)=a> ⇒ ¬(b·Se)=a> | |||||||||
| (60) | Übernahme (53) | ¬<(a·Sd)=b∧(b·Se)=a> | |||||||||
| (61) | Modus ponens (59), (60) | ¬(b·Se)=a | |||||||||
| (62) | Verallgemeinerung (61) nach e | ∀e: ¬(b·Se)=a | |||||||||
| (63) | Spezialisierung (62) e ← c | ¬(b·Sc)=a | |||||||||
| (64) | Verallgemeinerung (63) nach c | ∀c: ¬(b·Sc)=a | |||||||||
| (65) | Konklusion (54), (64) | <(a·Sd)=b ⇒ ∀c: ¬(b·Sc)=a> | |||||||||
| (66) | Kontraposition (65) | <¬∀c: ¬(b·Sc)=a ⇒ ¬(a·Sd)=b> | |||||||||
| (67) | Hypothese | ¬∀c: ¬(b·Sc)=a | |||||||||
| (68) | Übernahme (66) | <¬∀c: ¬(b·Sc)=a ⇒ ¬(a·Sd)=b> | |||||||||
| (69) | Modus ponens (68), (67) | ¬(a·Sd)=b | |||||||||
| (70) | Verallgemeinerung (69) nach d | ∀d: ¬(a·Sd)=b | |||||||||
| (71) | Spezialisierung (70) d ← c | ¬(a·Sc)=b | |||||||||
| (72) | Verallgemeinerung (71) nach c | ∀c: ¬(a·Sc)=b | |||||||||
| (73) | Konklusion (67), (72) | <¬∀c: ¬(b·Sc)=a ⇒ ∀c: ¬(a·Sc)=b> | |||||||||
| (74) | Hypothese | <¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> | |||||||||
| (75) | Abtrennung I (74) | ¬∀c: ¬(b·Sc)=a | |||||||||
| (76) | Hypothese | <¬∀c: ¬(b·Sc)=a ⇒ ∀c: ¬(a·Sc)=b> | |||||||||
| (77) | Übernahme (75) | ¬∀c: ¬(b·Sc)=a | |||||||||
| (78) | Modus ponens (76), (77) | ∀c: ¬(a·Sc)=b | |||||||||
| (79) | Konklusion (76), (78) | <<¬∀c: ¬(b·Sc)=a ⇒ ∀c: ¬(a·Sc)=b> ⇒ ∀c: ¬(a·Sc)=b> | |||||||||
| (80) | Kontraposition (79) | <¬∀c: ¬(a·Sc)=b ⇒ ¬<¬∀c: ¬(b·Sc)=a ⇒ ∀c: ¬(a·Sc)=b>> | |||||||||
| (81) | Abtrennung II (74) | ¬∀c: ¬(a·Sc)=b | |||||||||
| (82) | Modus ponens (80), (81) | ¬<¬∀c: ¬(b·Sc)=a ⇒ ∀c: ¬(a·Sc)=b> | |||||||||
| (83) | Konklusion (74), (82) | <<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> ⇒ ¬<¬∀c: ¬(b·Sc)=a ⇒ ∀c: ¬(a·Sc)=b>> | |||||||||
| (84) | Kontraposition (83) | <¬¬<¬∀c: ¬(b·Sc)=a ⇒ ∀c: ¬(a·Sc)=b> ⇒ ¬<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b>> | |||||||||
| (85) | Doppelte Negation (73) | ¬¬<¬∀c: ¬(b·Sc)=a ⇒ ∀c: ¬(a·Sc)=b> | |||||||||
| (86) | Modus ponens (84), (85) | ¬<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> | |||||||||
| (87) | Konklusion (51), (86) | <¬a=b ⇒ ¬<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b>> | |||||||||
| (88) | Kontraposition (87) | <¬¬<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> ⇒ ¬¬a=b> | |||||||||
| (89) | Hypothese | <¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> | |||||||||
| (90) | Doppelte Negation (89) | ¬¬<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> | |||||||||
| (91) | Übernahme (88) | <¬¬<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> ⇒ ¬¬a=b> | |||||||||
| (92) | Modus ponens (91), (90) | ¬¬a=b | |||||||||
| (93) | Doppelte Negation (92) | a=b | |||||||||
| (94) | Konklusion (89), (93) | <<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> ⇒ a=b> | |||||||||
| (95) | Verallgemeinerung (94) nach b | ∀b: <<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> ⇒ a=b> | |||||||||
| (96) | Verallgemeinerung (95) nach a | ∀a: ∀b: <<¬∀c: ¬(b·Sc)=a∧¬∀c: ¬(a·Sc)=b> ⇒ a=b> | |||||||||
Interpretation:
'teilt' ist eine Ordnungsrelation