IMO 2024 P1
Google DeepMind IMO 2024
IMO 2024 P1IMO 2024 P2IMO 2024 P4IMO 2024 P6
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.
open scoped BigOperators
theorem imo_2024_p1 :
{(α : ℝ) | ∀ (n : ℕ), 0 < n → (n : ℤ) ∣ (∑ i in Finset.Icc 1 n, ⌊i * α⌋)}
= {α : ℝ | ∃ k : ℤ, Even k ∧ α = k} := by
⊢ {α | ∀ (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_2x:ℝ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_1x✝¹:ℝ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_2x:ℝ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_1x✝¹:ℝ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✝¹ = ↑SL:ℕ⊢ ⌊↑L * ↑S⌋ = ↑L * S norm_num[Int.floor_eq_iff]
All goals completed! 🐙 :⌊(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_1x✝¹:ℝ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_1x✝¹:ℝ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✝ - 1omega
All goals completed! 🐙]⟩ ↑↑(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_2x:ℝL:x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}l:ℤY:∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * lthis:∀ (n : ℕ), ⌊(↑n + 1) * x⌋ = ⌊x⌋ + 2 * ↑n * (l - ⌊x⌋)⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}
thisx:ℝ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_2x:ℝL:x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}l:ℤY:∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * lthis:∀ (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_2x:ℝL:x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}l:ℤY:∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * lthis:∀ (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
hx:ℝL:x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}l:ℤY:∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * lthis:∀ (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
hx:ℝL:x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}l:ℤY:∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * lthis:∀ (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.ax:ℝL:x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}l:ℤY:∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * lthis:∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1⊢ x ≤ (↑l - ↑⌊x⌋) * 2
h.ax:ℝL:x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}l:ℤY:∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * lthis:∀ (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
thisx:ℝL:x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}l:ℤY:∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * ln✝:ℕ⊢ ⌊(↑n✝ + 1) * x⌋ = ⌊x⌋ + 2 * ↑n✝ * (l - ⌊x⌋)
-- We argue by strong induction on `n`.
induction‹_› using@Nat.strongInductionOn
this.indx:ℝL:x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}l:ℤY:∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * ln✝:ℕ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.indx:ℝl:ℤY:∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * ln✝:ℕ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.indx:ℝl:ℤn✝:ℕY:⌊x⌋ + ⌊x + x⌋ = 2 * la✝:∀ 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.indx:ℝ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.introx:ℝl:ℤY:⌊x⌋ + ⌊x + x⌋ = 2 * lA:ℕ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.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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+d*x⌋=∑Q in .range A,(⌊x⌋+2*(Q * (l-.floor x)))
this.ind.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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⌋)))
thisx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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⌋)))
thisx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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
thisx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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) / 2this:↑A * (↑A - 1) % 2 = 0⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
·
thisx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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 cases@Int.emod_two_eq A with|_ B=>
this.inrx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B✝:∀ 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) / 2B:↑A % 2 = 1⊢ ↑A * (↑A - 1) % 2 = 0norm_num[B,Int.sub_emod,Int.mul_emod]
All goals completed! 🐙
norm_num at*
this.ind.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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) / 2this: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.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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) / 2this✝: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.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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) * cthis✝¹:∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2this✝: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.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this✝¹: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⌋)) + 1this✝:Truethis:True⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
zify[*]at*
this.ind.introx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this✝¹: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✝:Truethis:Trueh✝:(↑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.inlx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this✝¹: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✝:Truethis:Trueh✝¹:(↑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⌋)) + 1h✝:c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1S5:⋯ = ⋯⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
this.ind.intro.inrx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this✝¹: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✝:Truethis:Trueh✝¹:(↑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⌋)) + 1h✝:c ≥ ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1S5:⋯ = ⋯⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋))
·
this.ind.intro.inlx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this✝¹: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✝:Truethis:Trueh✝¹:(↑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⌋)) + 1h✝:c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1S5:⋯ = ⋯⊢ ↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋)) simp_all
this.ind.intro.inlx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this:2 ∣ ↑A * (↑A - 1)h✝¹:c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1B:∀ 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
All goals completed! 🐙
simp_all
this.ind.intro.inlx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this✝:2 ∣ ↑A * (↑A - 1)h✝¹:c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1B:∀ 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⌋)) + 1this:↑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.inlx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this✝:2 ∣ ↑A * (↑A - 1)h✝²:c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1B:∀ 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⌋)) + 1this:↑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.inrx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this✝:2 ∣ ↑A * (↑A - 1)h✝²:c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1B:∀ 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⌋)) + 1this:↑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.inlx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this✝:2 ∣ ↑A * (↑A - 1)h✝²:c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1B:∀ 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⌋)) + 1this:↑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⌋ + 1this✝:2 ∣ ↑A * (↑A - 1)h✝²:c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1B:∀ 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⌋)) + 1this:↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋h✝:↑c = ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋⊢ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * ↑A * (↑l - ↑⌊x⌋)) nlinarith
All goals completed! 🐙
/- 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⌋ + 1this✝:2 ∣ ↑A * (↑A - 1)h✝²:c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1B:∀ 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⌋)) + 1this:↑c ≤ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋h✝:↑c < ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋⊢ ↑A * (↑l - ↑⌊x⌋) + ↑⌊x⌋ ≥ ↑c + 1 norm_cast at*
All goals completed! 🐙 :(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.inrx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1this:2 ∣ ↑A * (↑A - 1)h✝¹:c ≥ ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1B:∀ 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⌋ + 1this:2 ∣ ↑A * (↑A - 1)h✝¹:c ≥ ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1B:∀ 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
All goals completed! 🐙:(c:ℝ)>=A*(l-⌊_⌋)+⌊_⌋+1),Int.floor_le x,Int.lt_floor_add_one x]
rw [←Nat.cast_sum, mul_sub, Finset.sum_range_id]
thisx:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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.succx:ℝl:ℤc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1n✝:ℕ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) / 2norm_num[mul_add]
All goals completed! 🐙
use Finset.sum_congr rfl<|by
x:ℝl:ℤA:ℕc:ℤY:2 * ↑l ≤ x + x + ↑⌊x⌋ ∧ x + x < 2 * ↑l - ↑⌊x⌋ + 1B:∀ 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]
All goals completed! 🐙
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
'imo_2024_p1' depends on axioms: [propext, Classical.choice, Quot.sound]
These are the standard built in axioms.