let m be Nat; :: thesis: ( (2 |^ m) - 1 divides (2 |^ ((2 * m) + 1)) - 2 & (2 |^ m) + 1 divides (2 |^ ((2 * m) + 1)) - 2 )
(2 |^ ((2 * m) + 1)) - 2 = (2 * (2 |^ (2 * m))) - 2 by NEWTON:6
.= ((2 |^ (2 * m)) - (1 |^ m)) * 2
.= (((2 |^ m) |^ 2) - ((1 |^ m) |^ 2)) * 2 by NEWTON:9
.= (((2 |^ m) - (1 |^ m)) * ((2 |^ m) + (1 |^ m))) * 2 by NEWTON01:1
.= ((2 |^ m) - 1) * (((2 |^ m) + 1) * 2) ;
hence ( (2 |^ m) - 1 divides (2 |^ ((2 * m) + 1)) - 2 & (2 |^ m) + 1 divides (2 |^ ((2 * m) + 1)) - 2 ) by INT_1:def 3, INT_2:2; :: thesis: verum