:: Pythagorean triples
:: by Freek Wiedijk
::
:: Received August 26, 2001
:: Copyright (c) 2001 Association of Mizar Users
:: deftheorem Def1 defines are_relative_prime PYTHTRIP:def 1 :
:: deftheorem Def2 defines are_relative_prime PYTHTRIP:def 2 :
:: deftheorem Def3 defines square PYTHTRIP:def 3 :
theorem Th1: :: PYTHTRIP:1
theorem :: PYTHTRIP:2
theorem Th3: :: PYTHTRIP:3
theorem Th4: :: PYTHTRIP:4
theorem Th5: :: PYTHTRIP:5
theorem Th6: :: PYTHTRIP:6
theorem Th7: :: PYTHTRIP:7
theorem Th8: :: PYTHTRIP:8
theorem Th9: :: PYTHTRIP:9
theorem Th10: :: PYTHTRIP:10
theorem Th11: :: PYTHTRIP:11
theorem :: PYTHTRIP:12
:: deftheorem Def4 defines Pythagorean_triple PYTHTRIP:def 4 :
:: deftheorem Def5 defines Pythagorean_triple PYTHTRIP:def 5 :
:: deftheorem Def6 defines degenerate PYTHTRIP:def 6 :
theorem :: PYTHTRIP:13
:: deftheorem Def7 defines simplified PYTHTRIP:def 7 :
:: deftheorem Def8 defines simplified PYTHTRIP:def 8 :
theorem Th14: :: PYTHTRIP:14
theorem :: PYTHTRIP:15
theorem :: PYTHTRIP:16