reconsider
e
= 1 as
natural
odd
number
by
Lm5
;
take
e
;
:: according to
NAT_6:def 5
:: thesis:
ex
n
being
natural
positive
number
st
( 2
|^
n
>
e
& 3
=
(
e
*
(
2
|^
n
)
)
+
1 )
take
1 ;
:: thesis:
( 2
|^
1
>
e
& 3
=
(
e
*
(
2
|^
1
)
)
+
1 )
thus
( 2
|^
1
>
e
& 3
=
(
e
*
(
2
|^
1
)
)
+
1 ) ;
:: thesis:
verum