let
a
be
Nat
;
:: thesis:
154
divides
(
a
^
61
)

a
( 6
+
1 is
odd
& 6
+
1 is
prime
& 10
+
1 is
odd
& 10
+
1 is
prime
)
by
NAT_4:26
,
NAT_4:27
;
then
(
2
*
(
6
+
1
)
)
*
(
10
+
1
)
divides
(
a
^
(
(
6
*
10
)
+
1
)
)

a
by
Th78
;
hence
154
divides
(
a
^
61
)

a
;
:: thesis:
verum