mul0 Show Code edit
## Multiply by 0
##
## This rederives one of the Peano axioms from a different set of axioms. But those
## axioms are valid for any number, not just natural numbers.
##
thm (mul0 () () (= (* A (0)) (0))
A mulid eqcomi
(= A (* A (1)))
## <d>
(1) addidr eqcomi
(= (1) (+ (0) (1)))
EqReplaceEq1Mul1
(= A (* A (+ (0) (1))))
## </d>
## <d 'Distributive Property '>
## <d 'Distributive Property '>
A (0) (1) distr
(= (* A (+ (0) (1))) (+ (* A (0)) (* A (1))))
EqReplaceEq1
(= A (+ (* A (0)) (* A (1))))
## </d 'Distributive Property '>
## <d 'Evaluate'>
A mulid
(= (* A (1)) A)
EqReplaceEq1Add1
(= A (+ (* A (0)) A))
## </d 'Evaluate'>
## </d>
## <d 'Subtract A from both sides'>
## <d>
A addidr eqcomi
(= A (+ (0) A))
EqReplaceEq0
(= (+ (0) A) (+ (* A (0)) A))
## </d>
(0) A (* A (0)) addcan
(<-> (= (+ (0) A) (+ (* A (0)) A)) (= (0) (* A (0))))
mpbi
(= (0) (* A (0)))
## </d>
eqcomi
(= (* A (0)) (0))
)
edit