let n be Nat; :: thesis: ( n = 1 implies 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n )
assume A1: n = 1 ; :: thesis: 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n
A2: 5 -' 1 = 5 - 1 by XREAL_0:def 2
.= 4 + 0 ;
A3: 2 to_power 1 = 2 |^ 1
.= 2 by NEWTON:10 ;
A4: 2 -' 1 = 2 - 1 by XREAL_0:def 2
.= 1 + 0 ;
2 to_power 2 = 2 |^ (1 + 1)
.= (2 |^ 1) * 2 by NEWTON:11
.= 2 * 2 by NEWTON:10 ;
then 4 div 2 = 2 to_power (2 -' 1) by A3, NAT_2:18
.= 2 |^ 1 by A4
.= 2 by NEWTON:10 ;
then ((Fermat 1) -' 1) div 2 = (4 * 0 ) + 2 by A2, Th56;
then Fermat 1 divides (3 |^ (((Fermat n) -' 1) div 2)) + 1 by A1, Lm25;
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 A1, INT_2:19; :: thesis: verum