let t, u be Integer; :: thesis: ( t is even & t,u are_coprime implies u is odd )

A1: (2 * 0) + 1 is odd ;

assume ( t is even & t,u are_coprime & not u is odd ) ; :: thesis: contradiction

hence contradiction by A1, Th9; :: thesis: verum

A1: (2 * 0) + 1 is odd ;

assume ( t is even & t,u are_coprime & not u is odd ) ; :: thesis: contradiction

hence contradiction by A1, Th9; :: thesis: verum