let n be Nat; :: thesis: ( n = 1 implies 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n )
A2: 5 -' 1 = 5 - 1 by XREAL_0:def 2
.= 4 + 0 ;
assume A4: n = 1 ; :: thesis: 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n
((Fermat 1) -' 1) div 2 = (4 * 0) + 2 by A2, Th51;
then Fermat 1 divides (3 |^ (((Fermat n) -' 1) div 2)) + 1 by A4, Lm21;
then Fermat 1 divides (3 |^ (((Fermat n) -' 1) div 2)) - (- 1) ;
hence 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n by A4; :: thesis: verum