:: Pythagorean triples :: by Freek Wiedijk :: :: Received August 26, 2001 :: Copyright (c) 2001-2012 Association of Mizar Users begin definition let m, n be Nat; redefine pred m,n are_relative_prime means :Def1: :: PYTHTRIP:def 1 for k being Nat st k divides m & k divides n holds k = 1; compatibility ( m,n are_relative_prime iff for k being Nat st k divides m & k divides n holds k = 1 ) proofend; end; :: deftheorem Def1 defines are_relative_prime PYTHTRIP:def_1_:_ for m, n being Nat holds ( m,n are_relative_prime iff for k being Nat st k divides m & k divides n holds k = 1 ); definition let m, n be Nat; redefine pred m,n are_relative_prime means :Def2: :: PYTHTRIP:def 2 for p being prime Nat holds ( not p divides m or not p divides n ); compatibility ( m,n are_relative_prime iff for p being prime Nat holds ( not p divides m or not p divides n ) ) proofend; end; :: deftheorem Def2 defines are_relative_prime PYTHTRIP:def_2_:_ for m, n being Nat holds ( m,n are_relative_prime iff for p being prime Nat holds ( not p divides m or not p divides n ) ); begin definition let n be number ; attrn is square means :Def3: :: PYTHTRIP:def 3 ex m being Nat st n = m ^2 ; end; :: deftheorem Def3 defines square PYTHTRIP:def_3_:_ for n being number holds ( n is square iff ex m being Nat st n = m ^2 ); registration cluster square -> natural for set ; coherence for b1 being number st b1 is square holds b1 is natural proofend; end; registration let n be Nat; clustern ^2 -> square ; coherence n ^2 is square by Def3; end; registration cluster epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even square for Element of NAT ; existence ex b1 being Element of NAT st ( b1 is even & b1 is square ) proofend; end; registration cluster epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer odd square for Element of NAT ; existence ex b1 being Element of NAT st ( b1 is odd & b1 is square ) proofend; end; registration clusterV24() V25() ext-real integer even square for set ; existence ex b1 being Integer st ( b1 is even & b1 is square ) proofend; end; registration clusterV24() V25() ext-real integer odd square for set ; existence ex b1 being Integer st ( b1 is odd & b1 is square ) proofend; end; registration let m, n be square number ; clusterm * n -> square ; coherence m * n is square proofend; end; theorem Th1: :: PYTHTRIP:1 for m, n being Element of NAT st m * n is square & m,n are_relative_prime holds ( m is square & n is square ) proofend; registration let i be Integer; clusteri ^2 -> integer ; coherence i ^2 is integer ; end; registration let i be even Integer; clusteri ^2 -> even ; coherence i ^2 is even ; end; registration let i be odd Integer; clusteri ^2 -> odd ; coherence not i ^2 is even ; end; theorem :: PYTHTRIP:2 for i being Integer holds ( i is even iff i ^2 is even ) ; theorem Th3: :: PYTHTRIP:3 for i being Integer st i is even holds (i ^2) mod 4 = 0 proofend; theorem Th4: :: PYTHTRIP:4 for i being Integer st i is odd holds (i ^2) mod 4 = 1 proofend; registration let m, n be odd square Integer; clusterm + n -> non square ; coherence not m + n is square proofend; end; theorem Th5: :: PYTHTRIP:5 for m, n being Element of NAT st m ^2 = n ^2 holds m = n proofend; theorem Th6: :: PYTHTRIP:6 for m, n being Element of NAT holds ( m divides n iff m ^2 divides n ^2 ) proofend; begin theorem Th7: :: PYTHTRIP:7 for m, n, k being Element of NAT holds ( ( m divides n or k = 0 ) iff k * m divides k * n ) proofend; theorem Th8: :: PYTHTRIP:8 for k, m, n being Element of NAT holds (k * m) gcd (k * n) = k * (m gcd n) proofend; begin theorem Th9: :: PYTHTRIP:9 for X being set st ( for m being Element of NAT ex n being Element of NAT st ( n >= m & n in X ) ) holds X is infinite proofend; begin theorem Th10: :: PYTHTRIP:10 for a, b being Element of NAT holds ( not a,b are_relative_prime or a is odd or b is odd ) proofend; theorem Th11: :: PYTHTRIP:11 for a, b, c being Element of NAT st (a ^2) + (b ^2) = c ^2 & a,b are_relative_prime & a is odd holds ex m, n being Element of NAT st ( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) proofend; theorem :: PYTHTRIP:12 for a, n, m, b, c being Element of NAT st a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) holds (a ^2) + (b ^2) = c ^2 ; definition mode Pythagorean_triple -> Subset of NAT means :Def4: :: PYTHTRIP:def 4 ex a, b, c being Element of NAT st ( (a ^2) + (b ^2) = c ^2 & it = {a,b,c} ); existence ex b1 being Subset of NAT ex a, b, c being Element of NAT st ( (a ^2) + (b ^2) = c ^2 & b1 = {a,b,c} ) proofend; end; :: deftheorem Def4 defines Pythagorean_triple PYTHTRIP:def_4_:_ for b1 being Subset of NAT holds ( b1 is Pythagorean_triple iff ex a, b, c being Element of NAT st ( (a ^2) + (b ^2) = c ^2 & b1 = {a,b,c} ) ); registration cluster -> finite for Pythagorean_triple ; coherence for b1 being Pythagorean_triple holds b1 is finite proofend; end; definition redefine mode Pythagorean_triple means :Def5: :: PYTHTRIP:def 5 ex k, m, n being Element of NAT st ( m <= n & it = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ); compatibility for b1 being Subset of NAT holds ( b1 is Pythagorean_triple iff ex k, m, n being Element of NAT st ( m <= n & b1 = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) ) proofend; end; :: deftheorem Def5 defines Pythagorean_triple PYTHTRIP:def_5_:_ for b1 being Subset of NAT holds ( b1 is Pythagorean_triple iff ex k, m, n being Element of NAT st ( m <= n & b1 = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) ); definition let X be Pythagorean_triple ; attrX is degenerate means :Def6: :: PYTHTRIP:def 6 0 in X; end; :: deftheorem Def6 defines degenerate PYTHTRIP:def_6_:_ for X being Pythagorean_triple holds ( X is degenerate iff 0 in X ); theorem :: PYTHTRIP:13 for n being Element of NAT st n > 2 holds ex X being Pythagorean_triple st ( not X is degenerate & n in X ) proofend; definition let X be Pythagorean_triple ; attrX is simplified means :Def7: :: PYTHTRIP:def 7 for k being Element of NAT st ( for n being Element of NAT st n in X holds k divides n ) holds k = 1; end; :: deftheorem Def7 defines simplified PYTHTRIP:def_7_:_ for X being Pythagorean_triple holds ( X is simplified iff for k being Element of NAT st ( for n being Element of NAT st n in X holds k divides n ) holds k = 1 ); definition let X be Pythagorean_triple ; redefine attr X is simplified means :Def8: :: PYTHTRIP:def 8 ex m, n being Element of NAT st ( m in X & n in X & m,n are_relative_prime ); compatibility ( X is simplified iff ex m, n being Element of NAT st ( m in X & n in X & m,n are_relative_prime ) ) proofend; end; :: deftheorem Def8 defines simplified PYTHTRIP:def_8_:_ for X being Pythagorean_triple holds ( X is simplified iff ex m, n being Element of NAT st ( m in X & n in X & m,n are_relative_prime ) ); theorem Th14: :: PYTHTRIP:14 for n being Element of NAT st n > 0 holds ex X being Pythagorean_triple st ( not X is degenerate & X is simplified & 4 * n in X ) proofend; registration cluster finite non degenerate simplified for Pythagorean_triple ; existence ex b1 being Pythagorean_triple st ( not b1 is degenerate & b1 is simplified ) proofend; end; theorem :: PYTHTRIP:15 {3,4,5} is non degenerate simplified Pythagorean_triple proofend; theorem :: PYTHTRIP:16 { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is infinite proofend;