let n, m be Nat; :: thesis: ( m mod 2 = 0 implies (n |^ (m div 2)) ^2 = n |^ m )
assume A1: m mod 2 = 0 ; :: thesis: (n |^ (m div 2)) ^2 = n |^ m
(n |^ (m div 2)) ^2 = n |^ ((m div 2) + (m div 2)) by NEWTON:8
.= n |^ ((m + m) div 2) by A1, NAT_D:19
.= n |^ ((2 * m) div 2)
.= n |^ m by NAT_D:18 ;
hence (n |^ (m div 2)) ^2 = n |^ m ; :: thesis: verum