let n be Nat; :: thesis: ( Triangle n is triangular & Triangle n is square implies ( Triangle ((4 * n) * (n + 1)) is triangular & Triangle ((4 * n) * (n + 1)) is square ) )
assume ( Triangle n is triangular & Triangle n is square ) ; :: thesis: ( Triangle ((4 * n) * (n + 1)) is triangular & Triangle ((4 * n) * (n + 1)) is square )
then ( (n * (n + 1)) / 2 is triangular & (n * (n + 1)) / 2 is square ) by Th19;
then consider k being Nat such that
A1: (n * (n + 1)) / 2 = k ^2 by PYTHTRIP:def 3;
Triangle ((4 * n) * (n + 1)) = ((8 * (k ^2)) * ((8 * (k ^2)) + 1)) / 2 by Th19, A1
.= (4 * (k ^2)) * (((4 * n) * (n + 1)) + 1) by A1
.= ((2 * k) * ((2 * n) + 1)) ^2 ;
hence ( Triangle ((4 * n) * (n + 1)) is triangular & Triangle ((4 * n) * (n + 1)) is square ) ; :: thesis: verum