let n be non zero Nat; :: thesis: ( n is even & n is perfect implies n is triangular )
assume ( n is even & n is perfect ) ; :: thesis: n is triangular
then consider p being Nat such that
A1: ( (2 |^ p) -' 1 is prime & n = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) ) by NAT_5:39;
set p1 = Mersenne p;
A2: p <> 0
proof
assume p = 0 ; :: thesis: contradiction
then (2 |^ p) -' 1 = 1 -' 1 by NEWTON:4
.= 0 by XREAL_1:232 ;
hence contradiction by A1; :: thesis: verum
end;
A3: n = (2 |^ (p -' 1)) * (Mersenne p) by A1, XREAL_0:def 2;
A4: p -' 1 = p - 1 by XREAL_1:233, A2, NAT_1:14;
(2 to_power p) / (2 to_power 1) = ((Mersenne p) + 1) / 2 ;
then A5: 2 to_power (p -' 1) = ((Mersenne p) + 1) / 2 by A4, POWER:29;
((Mersenne p) * ((Mersenne p) + 1)) / 2 = Triangle (Mersenne p) by Th19;
hence n is triangular by A3, A5; :: thesis: verum