integerness of sum of sqrt

Stream: new members

[Ralf Stephan]

First, how to state "sqrt(a)+sqrt(b) is integer if both a and b are integer"? And is the proof in Mathlib?

I see this can be proved via properties of RR and NN / Galois structures, but is a formalization of the elementary proofs like in https://math.stackexchange.com/questions/457382/can-sqrtn-sqrtm-be-rational-if-neither-n-m-are-perfect-squares possible / in Mathlib?

In general I have a hard time finding a property in Mathlib that checks if anything is integer (of course a floating point val is never integer, but a real could be).

[Riccardo Brasca]

You can use docs#Set.range applied to the function (↑) : ℤ → ℝ

[Riccardo Brasca]

The point is that technically, a real number cannot be an integer, but it can be the coercion of an integer.

[Yaël Dillies]

I think Ralf means algebraic integer, here?

[Riccardo Brasca]

Oh, that's possible, in that case IsIntegral ℤ x says that x is an algebraic integer.

[Yaël Dillies]

Certainly, $\sqrt 2 + \sqrt 3$ is not an integer

[Riccardo Brasca]

I didn't mean this is always true, but we can state it! (Looking at the stackexchange question it seems this is what is wanted here, but maybe I misunderstood)

[Ralf Stephan]

Would this be the right statement to enable a formalization of, e.g. the 1st proof on the SO page?

import Mathlib
open Real
namespace Real

example (a m n : ℝ) (hab : sqrt m + sqrt n = a) (hm : IsIntegral ℤ a) :
    IsIntegral ℤ m ∧ IsIntegral ℤ n := by
  sorry

[Daniel Weber]

No, this statement is wrong (you don't have n m as integers, just general reals, and IsIntegral talks about being the root of a monic polynomial, not an integer).

import Mathlib
open Real
namespace Real

example (n m : ℕ) (a : ℚ) (hab : sqrt m + sqrt n = a) :
    IsSquare n ∧ IsSquare m := by
  sorry

seems good

[Ralf Stephan]

There could still be nonsquare m,n satisfying this. How would you know?

[Daniel Weber]

What do you mean? This would be a proof that any such numbers are necessarily square

[Daniel Weber]

It might be better to just use √n = (a^2 + n - m) / (2 * a) directly

[Daniel Weber]

You can start with

example (n m : ℕ) :
    √n = ((√m + √n)^2 + n - m) / (2 * (√m + √n)) := by
  by_cases hn : n = 0
  · simp_all
  by_cases hm : m = 0
  · field_simp [hm]
    ring_nf
    simp
  field_simp
  ring_nf
  simp only [Nat.cast_nonneg, sq_sqrt, add_add_sub_cancel]
  ring_nf

and the wanted result should be fairly simple from this

[Oliver D]

(deleted)

[Ralf Stephan]

Daniel Weber said:

You can start with

Thanks.

[Notification Bot]

Ralf Stephan has marked this topic as resolved.

[Notification Bot]

Ralf Stephan has marked this topic as unresolved.

[Ralf Stephan]

I could make it work. Is this of interest for mathlib?

import Mathlib
open Real

example (a m n : ℚ) (hm : 0 ≤ m) (hn : 0 ≤ n)
    (hab : a = sqrt m + sqrt n) :
    IsSquare m ∧ IsSquare n := by
  have h : √n = ((√m + √n)^2 + n - m) / (2 * (√m + √n)) := by
    by_cases hn : n = 0
    · simp_all
    by_cases hm : m = 0
    · field_simp [hm]
      ring_nf
      simp_all only [le_refl, Rat.cast_zero, sqrt_zero, zero_add,
        Rat.cast_nonneg, sq_sqrt]
    field_simp
    ring_nf
    simp_all only [Rat.cast_nonneg, sq_sqrt, add_add_sub_cancel]
    ring_nf
  rw [← hab] at h
  have hsqrule (x₁ x₂ : ℝ) (h: x₁ = x₂) : x₁ ^ 2 = x₂ ^ 2 :=
    congrFun (congrArg HPow.hPow h) 2
  have h₄ : n = ((a ^ 2 + n - m) / (2 * a)) ^ 2 := by
    apply hsqrule at h
    rw [sq_sqrt] at h
    norm_cast at h
    exact Rat.cast_nonneg.mpr hn
  have h₅ : IsSquare (((a ^ 2 + n - m) / (2 * a)) ^ 2) :=
      IsSquare_sq ((a ^ 2 + n - m) / (2 * a))
  rw [← h₄] at h₅
  constructor
  swap
  . exact h₅ /- This is the first statement: `IsSquare n`. -/
             /- Now solving for `m`. -/
  . have h₆ : a - sqrt n = sqrt m := sub_eq_iff_eq_add.mpr hab
    rw [h, sq] at h₆
    apply hsqrule at h₆
    rw [sq_sqrt (Rat.cast_nonneg.mpr hm)] at h₆
    norm_cast at h₆
    have h₈ : IsSquare ((a - (a * a + n - m) / (2 * a)) ^ 2) :=
      IsSquare_sq (a - (a * a + n - m) / (2 * a))
    rw [h₆] at h₈
    exact h₈