let n be Nat; :: thesis: ( n = 1 implies 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n )
A1: 2 -' 1 = 2 - 1 by XREAL_0:def 2
.= 1 + 0 ;
A2: 5 -' 1 = 5 - 1 by XREAL_0:def 2
.= 4 + 0 ;
A3: 2 to_power 2 = 2 |^ (1 + 1)
.= (2 |^ 1) * 2 by NEWTON:6
.= 2 * 2 ;
assume A4: n = 1 ; :: thesis: 3 |^ (((Fermat n) -' 1) div 2), - 1 are_congruent_mod Fermat n
4 div 2 = 2 by A1, A3, Lm22, NAT_2:16;
then ((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