IMO 2024 P1

Determine all real numbers \alpha such that, for every positive integer n, the integer \lfloor \alpha\rfloor + \lfloor2\alpha\rfloor + \cdots + \lfloor n\alpha\rfloor is a multiple of n. (Note that \lfloor z\rfloor denotes the greatest integer less than or equal to z. For example, \lfloor-\pi\rfloor = -4 and \lfloor2\rfloor = \lfloor2.9\rfloor = 2.)

Solution: \alpha is an even integer.

⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, Even k ∧ α = ↑k}

rw [(Set.Subset.antisymm_iff ), (Set.subset_def), ]

⊢ (∀ x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}, x ∈ {α | ∃ k, Even k ∧ α = ↑k}) ∧ {α | ∃ k, Even k ∧ α = ↑k} ⊆ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

/- We introduce a variable that will be used in the second part of the proof (the hard direction), namely the integer l such that 2l = ⌊α⌋ + ⌊2α⌋ (this comes from the given divisibility condition with n = 2). -/ existsλx L=>(L 2 two_pos).rec λl Y=>?_

refine_1⊢ {α | ∃ k, Even k ∧ α = ↑k} ⊆ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

refine_2

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}

useλy . x=>y.rec λS p=>?_

refine_1

x✝¹

:

ℝ

y

:

x✝¹ ∈ {α | ∃ k, Even k ∧ α = ↑k}

x✝

:

ℕ

x

:

0 < x✝

S

:

ℤ

p

:

Even S ∧ x✝¹ = ↑S

⊢ ↑x✝ ∣ ∑ i ∈ Finset.Icc 1 x✝, ⌊↑i * x✝¹⌋

refine_2

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}

·

refine_1

x✝¹

:

ℝ

y

:

x✝¹ ∈ {α | ∃ k, Even k ∧ α = ↑k}

x✝

:

ℕ

x

:

0 < x✝

S

:

ℤ

p

:

Even S ∧ x✝¹ = ↑S

⊢ ↑x✝ ∣ ∑ i ∈ Finset.Icc 1 x✝, ⌊↑i * x✝¹⌋

/- We start by showing that every α of the form 2k works. In this case, the sum simplifies to kn(n+1)), which is clearly divisible by n. -/ simp_all[λL:ℕ=>(by

x✝¹

:

ℝ

y

:

x✝¹ ∈ {α | ∃ k, Even k ∧ α = ↑k}

x✝

:

ℕ

x

:

0 < x✝

S

:

ℤ

p

:

Even S ∧ x✝¹ = ↑S

L

:

ℕ

⊢ ⌊↑L * ↑S⌋ = ↑L * S

norm_num[Int.floor_eq_iff] :⌊(L:ℝ)S⌋=L S )] rw[p.2,Int.dvd_iff_emod_eq_zero,Nat.lt_iff_add_one_le,<-Finset.sum_mul,←Nat.cast_sum, S.even_iff, ←Nat.Ico_succ_right,@ .((( Finset.sum_Ico_eq_sum_range))),Finset.sum_add_distrib ]at*

refine_1

x✝¹

:

ℝ

x✝

:

ℕ

x

:

0 + 1 ≤ x✝

S

:

ℤ

p

:

S % 2 = 0 ∧ ↑S = ↑S

⊢ ↑(∑ x ∈ Finset.range (x✝.succ - 1), 1 + ∑ x ∈ Finset.range (x✝.succ - 1), x) * S % ↑x✝ = 0

simp_all[Finset.sum_range_id]

refine_1

x✝¹

:

ℝ

x✝

:

ℕ

S

:

ℤ

x

:

1 ≤ x✝

p

:

2 ∣ S

⊢ ↑x✝ ∣ (↑x✝ + ↑x✝ * (↑x✝ - 1) / 2) * S

exact dvd_trans ⟨2+((_:ℕ)-1),by

x✝¹

:

ℝ

x✝

:

ℕ

S

:

ℤ

x

:

1 ≤ x✝

p

:

2 ∣ S

⊢ (↑x✝ + ↑x✝ * (↑x✝ - 1) / 2) * 2 = ↑x✝ * (2 + (↑x✝ - 1))

linarith[((‹ℕ›:Int)*(‹Nat›-1)).ediv_mul_cancel$ Int.prime_two.dvd_mul.2<|by

x✝¹

:

ℝ

x✝

:

ℕ

S

:

ℤ

x

:

1 ≤ x✝

p

:

2 ∣ S

⊢ 2 ∣ ↑x✝ ∨ 2 ∣ ↑x✝ - 1

·

x✝¹

:

ℝ

x✝

:

ℕ

S

:

ℤ

x

:

1 ≤ x✝

p

:

2 ∣ S

⊢ 2 ∣ ↑x✝ ∨ 2 ∣ ↑x✝ - 1

omega]⟩ ↑↑(mul_dvd_mul_left @_ (p)) /- Now let's prove the converse, i.e. that every α in the LHS is an even integer. We claim for all such α and n ∈ ℕ, we have ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋). -/ suffices: ∀ (n : ℕ),⌊(n+1)*x⌋ =⌊ x⌋+2 * ↑ (n : ℕ) * (l-(⌊(x)⌋))

refine_2

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

this

:

∀ (n : ℕ), ⌊(↑n + 1) * x⌋ = ⌊x⌋ + 2 * ↑n * (l - ⌊x⌋)

⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}

this

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

⊢ ∀ (n : ℕ), ⌊(↑n + 1) * x⌋ = ⌊x⌋ + 2 * ↑n * (l - ⌊x⌋)

·

refine_2

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

this

:

∀ (n : ℕ), ⌊(↑n + 1) * x⌋ = ⌊x⌋ + 2 * ↑n * (l - ⌊x⌋)

⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}

/- Let's assume for now that the claim is true, and see how this is enough to finish our proof. -/ zify[mul_comm,Int.floor_eq_iff] at this

refine_2

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

this

:

∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1

⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}

-- We'll show that α = 2(l-⌊α⌋), which is obviously even. use(l-⌊x⌋)*2

h

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

this

:

∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1

⊢ Even ((l - ⌊x⌋) * 2) ∧ x = ↑((l - ⌊x⌋) * 2)

norm_num

h

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

this

:

∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1

⊢ x = (↑l - ↑⌊x⌋) * 2

-- To do so, it suffices to show α ≤ 2(l-⌊α⌋) and α ≥ 2(l-⌊α⌋). apply@le_antisymm

h.a

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

this

:

∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1

⊢ x ≤ (↑l - ↑⌊x⌋) * 2

h.a

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

this

:

∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1

⊢ (↑l - ↑⌊x⌋) * 2 ≤ x

/- To prove the first inequality, notice that if α > 2(l-⌊α⌋) then there exists an integer N > 0 such that N ≥ 1/(α - 2(l -⌊α⌋)). By our assumed claim (with n = N), we have ⌊α⌋ + 2(l-⌊α⌋)N + 1 > (N+1)α, i.e. ⌊α⌋ + (2(l-⌊α⌋) - α)N + 1 > α, and this implies ⌊α⌋ > α; contradiction. -/ use not_lt.1 (by

⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, Even k ∧ α = ↑k}

cases exists_nat_ge (1/(x-)) with| N =>nlinarith[ one_div_mul_cancel $ sub_ne_zero.2 ·.ne',9,Int.floor_le x, this N]) /- Similarly, if α < 2(l-⌊α⌋) then we can find a positive natural N such that N ≥ 1/(2(l-⌊α⌋) - α). By our claim (with n = N), we have (N+1)α ≥ ⌊α⌋ + 2(l-⌊α⌋)N, i.e. α ≥ ⌊α⌋ + (2(l-⌊α⌋) - α)N, and this implies a ≥ ⌊α⌋ + 1; contradiction. -/ use not_lt.1 (by

⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, Even k ∧ α = ↑k}

cases exists_nat_ge (1/:ℝ)with| A=>nlinarith[Int.lt_floor_add_one x,one_div_mul_cancel$ sub_ne_zero.2 ·.ne',this A]) /- Now all that's left to do is to prove our claim ⌊(n + 1)α⌋ = ⌊α⌋ + 2n(l - ⌊α⌋). -/ intro

this

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

n✝

:

ℕ

⊢ ⌊(↑n✝ + 1) * x⌋ = ⌊x⌋ + 2 * ↑n✝ * (l - ⌊x⌋)

-- We argue by strong induction on n. induction‹_› [email protected]

this.ind

x

:

ℝ

L

:

x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

n✝

:

ℕ

a✝

:

∀ m < n✝, ⌊(↑m + 1) * x⌋ = ⌊x⌋ + 2 * ↑m * (l - ⌊x⌋)

⊢ ⌊(↑n✝ + 1) * x⌋ = ⌊x⌋ + 2 * ↑n✝ * (l - ⌊x⌋)

-- By our hypothesis on α, we know that (n+1) | ∑_{i=1}^(n+1) ⌊iα⌋ specialize L$ ‹_›+1

this.ind

x

:

ℝ

l

:

ℤ

Y

:

∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l

n✝

:

ℕ

a✝

:

∀ m < n✝, ⌊(↑m + 1) * x⌋ = ⌊x⌋ + 2 * ↑m * (l - ⌊x⌋)

L

:

0 < n✝ + 1 → ↑(n✝ + 1) ∣ ∑ i ∈ Finset.Icc 1 (n✝ + 1), ⌊↑i * x⌋

⊢ ⌊(↑n✝ + 1) * x⌋ = ⌊x⌋ + 2 * ↑n✝ * (l - ⌊x⌋)

simp_all[add_comm,mul_assoc,Int.floor_eq_iff,<-Nat.Ico_succ_right, add_mul,(Finset.range_succ), Finset.sum_Ico_eq_sum_range]

this.ind

x

:

ℝ

l

:

ℤ

n✝

:

ℕ

Y

:

⌊x⌋ + ⌊x + x⌋ = 2 * l

a✝

:

∀ m < n✝, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

L

:

↑n✝ + 1 ∣ ⌊x + ↑n✝ * x⌋ + ∑ x_1 ∈ Finset.range n✝, ⌊x + ↑x_1 * x⌋

⊢ ↑⌊x⌋ + 2 * (↑n✝ * (↑l - ↑⌊x⌋)) ≤ x + ↑n✝ * x ∧ x + ↑n✝ * x < 1 + (↑⌊x⌋ + 2 * (↑n✝ * (↑l - ↑⌊x⌋)))

revert‹ℕ›

this.ind

x

:

ℝ

l

:

ℤ

Y

:

⌊x⌋ + ⌊x + x⌋ = 2 * l

⊢ ∀ (n : ℕ), (∀ m < n, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))) → ↑n + 1 ∣ ⌊x + ↑n * x⌋ + ∑ x_1 ∈ Finset.range n, ⌊x + ↑x_1 * x⌋ → ↑⌊x⌋ + 2 * (↑n * (↑l - ↑⌊x⌋)) ≤ x + ↑n * x ∧ x + ↑n * x < 1 + (↑⌊x⌋ + 2 * (↑n * (↑l - ↑⌊x⌋)))

/- Thus, there exists c such that (n+1)*c = ∑_{i=1}^{n+1} ⌊iα⌋ = ⌊nα+α⌋ + ∑_{i=1}^n ⌊iα⌋. -/ rintro A B@c

this.ind.intro

x

:

ℝ

l

:

ℤ

Y

:

⌊x⌋ + ⌊x + x⌋ = 2 * l

A

:

ℕ

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

c

:

ℤ

h✝

:

⌊x + ↑A * x⌋ + ∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c

⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))

simp_all[ Finset.mem_range.mp _,←eq_sub_iff_add_eq',Int.floor_eq_iff]

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))

/- By the inductive hypothesis, ∑_{i=0}^{n-1}, ⌊α+iα⌋ = ∑_{i=0}^{n-1}, ⌊α⌋+2*i*(l-⌊α⌋). -/ suffices:∑d in .range A,⌊x+dx⌋=∑Q in .range A,(⌊x⌋+2(Q * (l-.floor x)))

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))

this

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

⊢ ∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

·

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))

suffices:∑d in ( .range A),(((d)):ℤ) =A * ( A-1)/2

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this✝

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

this

:

∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2

⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))

this

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

⊢ ∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2

·

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this✝

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

this

:

∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2

⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))

have:(A : ℤ) * (A-1)%2=0

this

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this✝

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

this

:

∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2

⊢ ↑A * (↑A - 1) % 2 = 0

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this✝¹

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

this✝

:

∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2

this

:

↑A * (↑A - 1) % 2 = 0

⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))

·

this

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this✝

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

this

:

∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2

⊢ ↑A * (↑A - 1) % 2 = 0

[email protected]_two_eq A with|_ B=>

this.inr

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B✝

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this✝

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

this

:

∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2

B

:

↑A % 2 = 1

⊢ ↑A * (↑A - 1) % 2 = 0

norm_num[B,Int.sub_emod,Int.mul_emod] norm_num at*

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this✝¹

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

this✝

:

∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2

this

:

2 ∣ ↑A * (↑A - 1)

⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))

norm_num[ Finset.sum_add_distrib,<-Finset.sum_mul, ←Finset.mul_sum _ _] at*

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this✝¹

:

∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2

this✝

:

2 ∣ ↑A * (↑A - 1)

this

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ↑A * ⌊x⌋ + 2 * ((∑ i ∈ Finset.range A, ↑i) * (l - ⌊x⌋))

⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))

rw[eq_sub_iff_add_eq]at*

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ + ⌊x + ↑A * x⌋ = (↑A + 1) * c

this✝¹

:

∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2

this✝

:

2 ∣ ↑A * (↑A - 1)

this

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ↑A * ⌊x⌋ + 2 * ((∑ i ∈ Finset.range A, ↑i) * (l - ⌊x⌋))

⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))

/- Combined with ∑_{i=0}^{n-1},⌊iα+α⌋ = (n+1)c - ⌊nα+α⌋, we have ⌊nα+α⌋ = (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋), so ⌊nα+α⌋ ≥ (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋) and ⌊nα+α⌋ < (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋) + 1. Also, since 2*l = ⌊α⌋ + ⌊2α⌋, we have 2α+⌊α⌋-1 < 2*l ≤ 2α+⌊α⌋.-/ zify[←mul_assoc, this,←eq_sub_iff_add_eq',‹_ =(@ ) /@›,Int.floor_eq_iff] at *

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝¹

:

2 ∣ ↑A * (↑A - 1)

B

:

∀ (m : ℕ), ↑m < ↑A → ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

h✝

:

(↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * ↑(↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * ↑(↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

this✝

:

True

this

:

True

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

zify[]at

this.ind.intro

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝¹

:

2 ∣ ↑A * (↑A - 1)

B

:

∀ (m : ℕ), ↑m < ↑A → ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

this✝

:

True

this

:

True

h✝

:

(↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

-- We will now show that c = n*(l-⌊α⌋) + ⌊α⌋. cases unused variable `S5` note: this linter can be disabled with `set_option linter.unusedVariables false` S5:lt_or_ge c (A * (l-.floor ↑x)+⌊x⌋ + 1)

this.ind.intro.inl

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝¹

:

2 ∣ ↑A * (↑A - 1)

B

:

∀ (m : ℕ), ↑m < ↑A → ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

this✝

:

True

this

:

True

h✝¹

:

(↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

h✝

:

c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

S5

:

⋯ = ⋯

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

this.ind.intro.inr

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝¹

:

2 ∣ ↑A * (↑A - 1)

B

:

∀ (m : ℕ), ↑m < ↑A → ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

this✝

:

True

this

:

True

h✝¹

:

(↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

h✝

:

c ≥ ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

S5

:

⋯ = ⋯

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

·

this.ind.intro.inl

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝¹

:

2 ∣ ↑A * (↑A - 1)

B

:

∀ (m : ℕ), ↑m < ↑A → ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

this✝

:

True

this

:

True

h✝¹

:

(↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

h✝

:

c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

S5

:

⋯ = ⋯

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

simp_all

this.ind.intro.inl

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this

:

2 ∣ ↑A * (↑A - 1)

h✝¹

:

c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

h✝

:

(↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

have:(c+1:ℝ)<=A*(l-⌊x⌋)+⌊x⌋+1:=by

⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, Even k ∧ α = ↑k}

norm_cast simp_all

this.ind.intro.inl

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝

:

2 ∣ ↑A * (↑A - 1)

h✝¹

:

c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

h✝

:

(↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

this

:

↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

cases this.eq_or_lt

this.ind.intro.inl.inl

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝

:

2 ∣ ↑A * (↑A - 1)

h✝²

:

c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

h✝¹

:

(↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

this

:

↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

h✝

:

↑c = ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

this.ind.intro.inl.inr

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝

:

2 ∣ ↑A * (↑A - 1)

h✝²

:

c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

h✝¹

:

(↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

this

:

↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

h✝

:

↑c < ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

·

this.ind.intro.inl.inl

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝

:

2 ∣ ↑A * (↑A - 1)

h✝²

:

c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

h✝¹

:

(↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

this

:

↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

h✝

:

↑c = ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

/- For if c = n*(l-⌊α⌋) + ⌊α⌋, then $$⌊(n+1)α⌋ = (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋) = (n+1)(n(l - ⌊α⌋) + ⌊α⌋) - n⌊α⌋ - n(n-1)(l-⌊α⌋) = 2n(l-⌊α⌋) + ⌊α⌋ as desired. -/ repeat use by

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝

:

2 ∣ ↑A * (↑A - 1)

h✝²

:

c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

h✝¹

:

(↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

this

:

↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

h✝

:

↑c = ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

⊢ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

nlinarith /- Now, we show c = n*(l-⌊α⌋) + ⌊α⌋ via contradiction split into two cases. First suppose c ≤ n(l - ⌊α⌋) + ⌊α⌋ - 1. $$(n+1)α < (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋) + 1 ≤ (n+1)(n(l-⌊α⌋) + ⌊α⌋ - 1) - n⌊α⌋ - n(n-1)(l-⌊α⌋) + 1 = 2n(l-⌊α⌋) + ⌊α⌋ - n = 2ln - 2n⌊α⌋ + ⌊α⌋ - n ≤ (2α+⌊α⌋)n - 2n⌊α⌋ + ⌊α⌋ - n = nα + n(α-⌊α⌋-1) + ⌊α⌋ n + α. contradiction. -/ nlinarith[(by

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this✝

:

2 ∣ ↑A * (↑A - 1)

h✝²

:

c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

h✝¹

:

(↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

this

:

↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

h✝

:

↑c < ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋

⊢ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋ ≥ ↑c + 1

norm_cast at* :(A*(l -⌊x⌋):ℝ)+⌊(x)⌋ >=(c)+01),9,Int.add_emod ↑5,Int.floor_le (@x : ℝ),Int.lt_floor_add_one (x:)] /- Next, suppose c ≥ n(l - ⌊α⌋) + ⌊α⌋ + 1. $$(n+1)α ≥ (n+1)c - n⌊α⌋ - n(n-1)(l-⌊α⌋) ≥ (n+1)(n(l-⌊α⌋) + ⌊α⌋ + 1) - n⌊α⌋ - n(n-1)(l-⌊α⌋) = 2n(l-⌊α⌋) + ⌊α⌋ + n + 1 = 2ln - 2n⌊α⌋ + ⌊α⌋ + n + 1 > (2α+⌊α⌋-1)n - 2n⌊α⌋ + ⌊α⌋ + n + 1 = nα + n(α-⌊α⌋) + ⌊α⌋ + 1 > n + α contradiction. -/ simp_all

this.ind.intro.inr

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this

:

2 ∣ ↑A * (↑A - 1)

h✝¹

:

c ≥ ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

h✝

:

(↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))

nlinarith[(by

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

this

:

2 ∣ ↑A * (↑A - 1)

h✝¹

:

c ≥ ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * ↑m * (↑l - ↑⌊x⌋))

h✝

:

(↑A + 1) * ↑c ≤ x + ↑A * x + (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) ∧ x + ↑A * x < (↑A + 1) * ↑c - (↑A * ↑⌊x⌋ + 2 * (↑A * (↑A - 1) / 2) * (↑l - ↑⌊x⌋)) + 1

⊢ ↑c ≥ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋ + 1

norm_cast:(c:ℝ)>=A*(l-⌊⌋)+⌊⌋+1),Int.floor_le x,Int.lt_floor_add_one x] rw [←Nat.cast_sum, mul_sub, Finset.sum_range_id]

this

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

this

:

∑ d ∈ Finset.range A, ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range A, (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

⊢ ↑(A * (A - 1) / 2) = (↑A * ↑A - ↑A * 1) / 2

cases A with|_=>

this.succ

x

:

ℝ

l

:

ℤ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

n✝

:

ℕ

B

:

∀ m < n✝ + 1, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range (n✝ + 1), ⌊x + ↑x_1 * x⌋ = (↑(n✝ + 1) + 1) * c - ⌊x + ↑(n✝ + 1) * x⌋

this

:

∑ d ∈ Finset.range (n✝ + 1), ⌊x + ↑d * x⌋ = ∑ Q ∈ Finset.range (n✝ + 1), (⌊x⌋ + 2 * (↑Q * (l - ⌊x⌋)))

⊢ ↑((n✝ + 1) * (n✝ + 1 - 1) / 2) = (↑(n✝ + 1) * ↑(n✝ + 1) - ↑(n✝ + 1) * 1) / 2

norm_num[mul_add] use Finset.sum_congr rfl<|by

x

:

ℝ

l

:

ℤ

A

:

ℕ

c

:

ℤ

Y

:

2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1

B

:

∀ m < A, ↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)) ≤ x + ↑m * x ∧ x + ↑m * x < 1 + (↑⌊x⌋ + 2 * (↑m * (↑l - ↑⌊x⌋)))

h✝

:

∑ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = (↑A + 1) * c - ⌊x + ↑A * x⌋

⊢ ∀ x_1 ∈ Finset.range A, ⌊x + ↑x_1 * x⌋ = ⌊x⌋ + 2 * (↑x_1 * (l - ⌊x⌋))

simp_all[add_comm,Int.floor_eq_iff]```

The following command shows which axioms the proof relies upon:

`'imo_2024_p1' depends on axioms: [propext, Classical.choice, Quot.sound]`#print axioms imo_2024_p1

These are the standard built in axioms.