let
a
,
b
,
m
be
Nat
;
:: thesis:
(
(
(
a
,
b
)
In_Power
m
)
.
1
=
0
implies
m
<>
0
)
assume
A1
:
(
(
a
,
b
)
In_Power
m
)
.
1
=
0
;
:: thesis:
m
<>
0
a
|^
0
=
1
by
NEWTON:4
;
hence
m
<>
0
by
A1
,
NEWTON:28
;
:: thesis:
verum