Integer triples with square symmetric functions

DefinitionInteger triples with square elementary symmetric functions#✓fully proved

Integers \(a\), \(b\) and \(c\) have square elementary symmetric functions when \(a + b + c\), \(ab + bc + ca\) and \(abc\) are each the square of an integer.

def HasSquareElementarySymmetricFunctions (a b c : ℤ) : Prop :=
  IsSquare (a + b + c) ∧
    IsSquare (a * b + b * c + c * a) ∧
    IsSquare (a * b * c)

Used by 11

Used byChoudhry's family (3.32) of square triples with square symmetric functions · Choudhry's family (3.33) of square triples with square symmetric functions · Choudhry's family (3.34) of sums of two nonzero squares · Pairwise products preserve square symmetric functions · Choudhry's family (3.3) of integer triples with square symmetric functions · Choudhry's family (3.4) of integer triples with square symmetric functions · Choudhry's family (3.5) of integer triples with square symmetric functions · Choudhry's family (3.6) of integer triples with square symmetric functions · Choudhry's family (3.30) of square triples with square symmetric functions · Choudhry's family (3.31) of square triples with square symmetric functions · Rational solutions are sums of two squares and rescale to integer solutions

DefinitionRationals with square elementary symmetric functions#✓fully proved

Rational numbers \(a\), \(b\), \(c\) have square elementary symmetric functions when each of \(a + b + c\), \(ab + bc + ca\) and \(abc\) is the square of a rational number.

def HasSquareElementarySymmetricFunctionsℚ (a b c : ℚ) : Prop :=
  IsSquare (a + b + c) ∧
    IsSquare (a * b + b * c + c * a) ∧
    IsSquare (a * b * c)

Used by 1

Used byRational solutions are sums of two squares and rescale to integer solutions

DefinitionSums of two rational squares#✓fully proved

A rational number \(q\) is a sum of two squares when \(q = x^2 + y^2\) for some rational numbers \(x\) and \(y\).

def IsSumTwoSquaresℚ (q : ℚ) : Prop :=
  ∃ x y : ℚ, q = x ^ 2 + y ^ 2

Used by 2

Used byRational solutions are sums of two squares and rescale to integer solutions · Quotients of sums of two rational squares

DefinitionSums of two integer squares#✓fully proved

An integer \(z\) is a sum of two squares when \(z = x^2 + y^2\) for some integers \(x\) and \(y\).

def IsSumTwoSquaresℤ (z : ℤ) : Prop :=
  ∃ x y : ℤ, z = x ^ 2 + y ^ 2

Used by 1

Used byRational solutions are sums of two squares and rescale to integer solutions

DefinitionSums of two nonzero integer squares#✓fully proved

An integer \(z\) is a sum of two nonzero squares when \(z = x^2 + y^2\) for some nonzero integers \(x\) and \(y\).

def IsSumTwoNonzeroSquaresℤ (z : ℤ) : Prop :=
  ∃ x y : ℤ, x ≠ 0 ∧ y ≠ 0 ∧ z = x ^ 2 + y ^ 2

Used by 1

Used byChoudhry's family (3.34) of sums of two nonzero squares

TheoremQuotients of sums of two rational squares#●ready to prove

If \(\alpha\) and \(\beta\) are nonzero rational numbers that are each a sum of two squares of rational numbers, then \(\alpha / \beta\) is also a sum of two squares of rational numbers.

theorem_wanted sum_two_squares_div_sum_two_squaresℚ
    {α β : ℚ} (hα : α ≠ 0) (hβ : β ≠ 0)
    (hα₂ : IsSumTwoSquaresℚ α) (hβ₂ : IsSumTwoSquaresℚ β) :
    IsSumTwoSquaresℚ (α / β)

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Lemma 1.

Uses 1

Statement usesSums of two rational squares

TheoremPairwise products preserve square symmetric functions#●ready to prove

If \(a\), \(b\), \(c\) are integers such that each of \(a + b + c\), \(ab + bc + ca\) and \(abc\) is the square of an integer, then the same holds for the triple \(ab\), \(bc\), \(ca\).

theorem_wanted hasSquareElementarySymmetricFunctions_pairwise_products
    {a b c : ℤ}
    (h : HasSquareElementarySymmetricFunctions a b c) :
    HasSquareElementarySymmetricFunctions (a * b) (b * c) (c * a)

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Lemma 2.

Uses 1

Statement usesInteger triples with square elementary symmetric functions

TheoremRational solutions are sums of two squares and rescale to integer solutions#●ready to prove

Let \(a\), \(b\), \(c\) be rational numbers such that \(a + b + c\), \(ab + bc + ca\) and \(abc\) are squares of rational numbers. Then each of \(a\), \(b\) and \(c\) is a sum of two squares of rational numbers. Moreover, there is a nonzero rational number \(k\) such that \(A = ka\), \(B = kb\) and \(C = kc\) are integers, \(A + B + C\), \(AB + BC + CA\) and \(ABC\) are squares of integers, and each of \(A\), \(B\) and \(C\) is a sum of two squares of integers.

MathlibExt.NumberTheory.ThreeIntegersSymmetricSquaresWanted.isSumTwoSquaresℚ_of_hasSquareElementarySymmetricFunctionsℚ_and_scaling · 15 lines

theorem_wanted isSumTwoSquaresℚ_of_hasSquareElementarySymmetricFunctionsℚ_and_scaling
    {a b c : ℚ}
    (h : HasSquareElementarySymmetricFunctionsℚ a b c) :
    IsSumTwoSquaresℚ a ∧
      IsSumTwoSquaresℚ b ∧
      IsSumTwoSquaresℚ c ∧
      ∃ (k : ℚ) (A B C : ℤ),
        k ≠ 0 ∧
          (A : ℚ) = k * a ∧
          (B : ℚ) = k * b ∧
          (C : ℚ) = k * c ∧
          HasSquareElementarySymmetricFunctions A B C ∧
          IsSumTwoSquaresℤ A ∧
          IsSumTwoSquaresℤ B ∧
          IsSumTwoSquaresℤ C

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Lemma 3.

Uses 4

Statement usesInteger triples with square elementary symmetric functions · Rationals with square elementary symmetric functions · Sums of two rational squares · Sums of two integer squares

TheoremChoudhry's family (3.3) of integer triples with square symmetric functions#●ready to prove

For all integers \(s\) and \(t\), put \(a = t^2 (s^2 - t^2)^2 (s^2 + t^2)\), \(b = s^2 (s^2 - t^2)^2 (s^2 + t^2)\) and \(c = 4 s^4 t^4\). Then each of \(a + b + c\), \(ab + bc + ca\) and \(abc\) is the square of an integer.

theorem_wanted hasSquareElementarySymmetricFunctions_family33
    (s t : ℤ) :
    HasSquareElementarySymmetricFunctions
      (t ^ 2 * (s ^ 2 - t ^ 2) ^ 2 * (s ^ 2 + t ^ 2))
      (s ^ 2 * (s ^ 2 - t ^ 2) ^ 2 * (s ^ 2 + t ^ 2))
      (4 * s ^ 4 * t ^ 4)

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Theorem 1, family (3.3).

Uses 1

Statement usesInteger triples with square elementary symmetric functions

TheoremChoudhry's family (3.4) of integer triples with square symmetric functions#●ready to prove

For all integers \(s\) and \(t\), put \(a = 4 s^4 t^2 (s^2 + t^2)\), \(b = 4 s^2 t^4 (s^2 + t^2)\) and \(c = (s^4 - t^4)^2\). Then each of \(a + b + c\), \(ab + bc + ca\) and \(abc\) is the square of an integer.

theorem_wanted hasSquareElementarySymmetricFunctions_family34
    (s t : ℤ) :
    HasSquareElementarySymmetricFunctions
      (4 * s ^ 4 * t ^ 2 * (s ^ 2 + t ^ 2))
      (4 * s ^ 2 * t ^ 4 * (s ^ 2 + t ^ 2))
      ((s ^ 4 - t ^ 4) ^ 2)

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Theorem 1, family (3.4).

Uses 1

Statement usesInteger triples with square elementary symmetric functions

TheoremChoudhry's family (3.5) of integer triples with square symmetric functions#●ready to prove

For all integers \(s\) and \(t\), let \(f = s^6 - s^4 t^2 - 5 s^2 t^4 + t^6\) and \(g = 3 s^6 + s^4 t^2 + s^2 t^4 - t^6\), and put \(a = 4 s^4 t^2 (s^2 + t^2) f^2\), \(b = (s^4 - t^4)^2 f^2\) and \(c = 4 s^2 t^4 (s^2 + t^2) g^2\). Then each of \(a + b + c\), \(ab + bc + ca\) and \(abc\) is the square of an integer.

theorem_wanted hasSquareElementarySymmetricFunctions_family35
    (s t : ℤ) :
    HasSquareElementarySymmetricFunctions
      (4 * s ^ 4 * t ^ 2 * (s ^ 2 + t ^ 2) *
        (firstShiftedSextic s t) ^ 2)
      ((s ^ 4 - t ^ 4) ^ 2 * (firstShiftedSextic s t) ^ 2)
      (4 * s ^ 2 * t ^ 4 * (s ^ 2 + t ^ 2) *
        (secondShiftedSextic s t) ^ 2)

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Theorem 1, family (3.5).

Uses 1

Statement usesInteger triples with square elementary symmetric functions

TheoremChoudhry's family (3.6) of integer triples with square symmetric functions#●ready to prove

For all integers \(s\) and \(t\), let \(f = s^6 - s^4 t^2 - 5 s^2 t^4 + t^6\) and \(g = 3 s^6 + s^4 t^2 + s^2 t^4 - t^6\), and put \(a = t^2 (s^2 - t^2)^2 (s^2 + t^2) g^2\), \(b = 4 s^4 t^4 g^2\) and \(c = s^2 (s^2 - t^2)^2 (s^2 + t^2) f^2\). Then each of \(a + b + c\), \(ab + bc + ca\) and \(abc\) is the square of an integer.

theorem_wanted hasSquareElementarySymmetricFunctions_family36
    (s t : ℤ) :
    HasSquareElementarySymmetricFunctions
      (t ^ 2 * (s ^ 2 - t ^ 2) ^ 2 * (s ^ 2 + t ^ 2) *
        (secondShiftedSextic s t) ^ 2)
      (4 * s ^ 4 * t ^ 4 * (secondShiftedSextic s t) ^ 2)
      (s ^ 2 * (s ^ 2 - t ^ 2) ^ 2 * (s ^ 2 + t ^ 2) *
        (firstShiftedSextic s t) ^ 2)

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Theorem 1, family (3.6).

Uses 1

Statement usesInteger triples with square elementary symmetric functions

TheoremChoudhry's family (3.30) of square triples with square symmetric functions#●ready to prove

For all integers \(m\) and \(n\), let \(Q = m^4 - 6 m^2 n^2 + n^4\) and put \(a = (m^4 - n^4)^2 Q^2\), \(b = 4 m^2 n^2 (m^2 + n^2)^2 Q^2\) and \(c = 64 m^4 n^4 (m^2 - n^2)^4\). Then each of \(a\), \(b\), \(c\), \(a + b + c\), \(ab + bc + ca\) and \(abc\) is the square of an integer.

theorem_wanted hasSquareElementarySymmetricFunctions_family330_and_entries_square
    (m n : ℤ) :
    let a := (m ^ 4 - n ^ 4) ^ 2 * (shiftedQuartic m n) ^ 2
    let b := 4 * m ^ 2 * n ^ 2 * (m ^ 2 + n ^ 2) ^ 2
      * (shiftedQuartic m n) ^ 2
    let c := 64 * m ^ 4 * n ^ 4 * (m ^ 2 - n ^ 2) ^ 4
    HasSquareElementarySymmetricFunctions a b c ∧
      IsSquare a ∧ IsSquare b ∧ IsSquare c

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Theorem 2, family (3.30).

Uses 1

Statement usesInteger triples with square elementary symmetric functions

TheoremChoudhry's family (3.31) of square triples with square symmetric functions#●ready to prove

For all integers \(m\) and \(n\), let \(a = 64 m^4 n^4 (m^2 - n^2)^2\), \(b = 16 m^2 n^2 (m^2 - n^2)^4\) and \(c = (m^2 + n^2)^2 (m^4 - 6 m^2 n^2 + n^4)^2\). Then \(a + b + c\), \(ab + bc + ca\) and \(abc\) are squares of integers, and \(a\), \(b\) and \(c\) are themselves squares of integers.

theorem_wanted hasSquareElementarySymmetricFunctions_family331_and_entries_square
    (m n : ℤ) :
    let a := 64 * m ^ 4 * n ^ 4 * (m ^ 2 - n ^ 2) ^ 2
    let b := 16 * m ^ 2 * n ^ 2 * (m ^ 2 - n ^ 2) ^ 4
    let c := (m ^ 2 + n ^ 2) ^ 2 * (shiftedQuartic m n) ^ 2
    HasSquareElementarySymmetricFunctions a b c ∧
      IsSquare a ∧ IsSquare b ∧ IsSquare c

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Theorem 2, family (3.31).

Uses 1

Statement usesInteger triples with square elementary symmetric functions

TheoremChoudhry's family (3.32) of square triples with square symmetric functions#●ready to prove

For all integers \(m\) and \(n\), let \(Q = m^4 - 6 m^2 n^2 + n^4\), \(P = m^{12} - 26 m^{10} n^2 + 79 m^8 n^4 - 44 m^6 n^6 + 79 m^4 n^8 - 26 m^2 n^{10} + n^{12}\) and \(R = m^{12} - 10 m^{10} n^2 + 15 m^8 n^4 - 204 m^6 n^6 + 15 m^4 n^8 - 10 m^2 n^{10} + n^{12}\), and put \(a = 64 m^4 n^4 (m^2 - n^2)^2 P^2\), \(b = (m^2 + n^2)^2 Q^2 P^2\) and \(c = 16 m^2 n^2 (m^2 - n^2)^4 R^2\). Then each of \(a\), \(b\), \(c\), \(a + b + c\), \(ab + bc + ca\) and \(abc\) is the square of an integer.

theorem_wanted hasSquareElementarySymmetricFunctions_family332_and_entries_square
    (m n : ℤ) :
    let a := 64 * m ^ 4 * n ^ 4 * (m ^ 2 - n ^ 2) ^ 2
      * (firstDegreeTwelve m n) ^ 2
    let b := (m ^ 2 + n ^ 2) ^ 2 * (shiftedQuartic m n) ^ 2
      * (firstDegreeTwelve m n) ^ 2
    let c := 16 * m ^ 2 * n ^ 2 * (m ^ 2 - n ^ 2) ^ 4
      * (secondDegreeTwelve m n) ^ 2
    HasSquareElementarySymmetricFunctions a b c ∧
      IsSquare a ∧ IsSquare b ∧ IsSquare c

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Theorem 2, family (3.32).

Uses 1

Statement usesInteger triples with square elementary symmetric functions

TheoremChoudhry's family (3.33) of square triples with square symmetric functions#●ready to prove

For all integers \(m\) and \(n\), let \(Q = m^4 - 6 m^2 n^2 + n^4\), \(P = m^{12} - 26 m^{10} n^2 + 79 m^8 n^4 - 44 m^6 n^6 + 79 m^4 n^8 - 26 m^2 n^{10} + n^{12}\) and \(R = m^{12} - 10 m^{10} n^2 + 15 m^8 n^4 - 204 m^6 n^6 + 15 m^4 n^8 - 10 m^2 n^{10} + n^{12}\), and put \(a = (m^4 - n^4)^2 Q^2 R^2\), \(b = 64 m^4 n^4 (m^2 - n^2)^4 R^2\) and \(c = 4 m^2 n^2 (m^2 + n^2)^2 Q^2 P^2\). Then each of \(a\), \(b\), \(c\), \(a + b + c\), \(ab + bc + ca\) and \(abc\) is the square of an integer.

theorem_wanted hasSquareElementarySymmetricFunctions_family333_and_entries_square
    (m n : ℤ) :
    let a := (m ^ 4 - n ^ 4) ^ 2 * (shiftedQuartic m n) ^ 2
      * (secondDegreeTwelve m n) ^ 2
    let b := 64 * m ^ 4 * n ^ 4 * (m ^ 2 - n ^ 2) ^ 4
      * (secondDegreeTwelve m n) ^ 2
    let c := 4 * m ^ 2 * n ^ 2 * (m ^ 2 + n ^ 2) ^ 2
      * (shiftedQuartic m n) ^ 2 * (firstDegreeTwelve m n) ^ 2
    HasSquareElementarySymmetricFunctions a b c ∧
      IsSquare a ∧ IsSquare b ∧ IsSquare c

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Theorem 2, family (3.33).

Uses 1

Statement usesInteger triples with square elementary symmetric functions

TheoremChoudhry's family (3.34) of sums of two nonzero squares#●ready to prove

For all nonzero integers \(r\) and \(s\), let \(E = r^8 + 2 r^6 s^2 - 12 r^4 s^4 - 6 r^2 s^6 - s^8\), \(T = r^{12} + 6 r^{10} s^2 + 87 r^8 s^4 + 108 r^6 s^6 + 55 r^4 s^8 + 14 r^2 s^{10} + s^{12}\) and \(S = 5 r^6 + 3 r^4 s^2 + 3 r^2 s^4 + s^6\), and put \(a = r^2 (r^2 + s^2) E^2 T\), \(b = s^2 (r^2 + s^2) S^2 E^2\) and \(c = 4 r^4 s^4 S^2 T\). Then each of \(a + b + c\), \(ab + bc + ca\) and \(abc\) is the square of an integer, and each of \(a\), \(b\), \(c\) is a sum \(x^2 + y^2\) of the squares of two nonzero integers \(x\) and \(y\).

The hypothesis that \(r\) and \(s\) are nonzero is the nondegenerate range used in the proof.

theorem_wanted hasSquareElementarySymmetricFunctions_family334_and_entries_sum_two_nonzero_squares
    (r s : ℤ) (hr : r ≠ 0) (hs : s ≠ 0) :
    let a := r ^ 2 * (r ^ 2 + s ^ 2) * (degreeEightFactor r s) ^ 2
      * degreeTwelveFactor r s
    let b := s ^ 2 * (r ^ 2 + s ^ 2) * (degreeSixFactor r s) ^ 2
      * (degreeEightFactor r s) ^ 2
    let c := 4 * r ^ 4 * s ^ 4 * (degreeSixFactor r s) ^ 2
      * degreeTwelveFactor r s
    HasSquareElementarySymmetricFunctions a b c ∧
      IsSumTwoNonzeroSquaresℤ a ∧
      IsSumTwoNonzeroSquaresℤ b ∧
      IsSumTwoNonzeroSquaresℤ c

Sources

• Ajai Choudhry, "Three Integers Whose Sum, Product, and the Sum of the Products of the Integers, Taken Two at a Time, Are Perfect Squares", Theorem 3, family (3.34).

Uses 2

Statement usesInteger triples with square elementary symmetric functions · Sums of two nonzero integer squares

5 fully proved12 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.