确定所有实数 \alpha，使得对于每个正整数 n，整数 \lfloor \alpha\rfloor + \lfloor2\alpha\rfloor + \cdots + \lfloor n\alpha\rfloor 是 n 的倍数。（注意 \lfloor z\rfloor 表示小于或等于 z 的最大整数。例如，\lfloor-\pi\rfloor = -4 和 \lfloor2\rfloor = \lfloor2.9\rfloor = 2。）
解决方案：eta 是一个偶数。
⊢ {α | ∀ (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 * α⌋}
/- 我们引入一个变量，将在证明的第二部分（难方向）中使用，即整数 l，满足 2l = ⌊α⌋ + ⌊2α⌋（这来自于给定的可整除条件，其中 n = 2）。 -/ 存在λ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 * α⌋}
精炼_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=>?_
精炼_1
x✝¹
：
实数集
y
:
x✝¹ ∈ {α | ∃ k, Even k ∧ α = ↑k}
x✝
:
ℕ
x
:
0 < x✝
S
:
ℤ
段落
：
即使 S ∧ x✝¹ = ↑S
⊢ ↑x✝ ∣ ∑ i ∈ Finset.Icc 1 x✝, ⌊↑i * x✝¹⌋
精炼_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}
·
精炼_1
x✝¹
：
ℝ
y
：
x✝¹ ∈ {α | ∃ k, 偶数 k ∧ α = ↑k}
x✝
：
ℕ
x
：
0 < x✝
S
：
ℤ
p
：
即使 S ∧ x✝¹ = ↑S
⊢ ↑x✝ ∣ ∑ i ∈ Finset.Icc 1 x✝, ⌊↑i * x✝¹⌋
/- 我们首先证明每个形式为 2k 的 α 都有效。在这种情况下，和简化为 kn(n+1)，显然可以被 n 整除。-/ simp_all[λL:ℕ=>(by'
x✝¹
：
ℝ
y
：
x✝¹ ∈ {α | ∃ k, 偶数 k ∧ α = ↑k}
x✝
：
ℕ
x
：
0 < x✝
S
：
ℤ
p
：
即使 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*
精炼_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]
精炼_1
x✝¹
：
ℝ
x✝
：
ℕ
S
：
ℤ
x
：
1 ≤ x✝
p
：
2 ∣ S
⊢ ↑x✝ ∣ (↑x✝ + ↑x✝ * (↑x✝ - 1) / 2) * S
确切 dvd_trans ⟨2+((_:ℕ)-1),by
x✝¹
：
实数集
x✝
:
ℕ
S
：
ℤ
x
：
1 ≤ x✝
段落
：
2 ∣ S
⊢ (↑x✝ + ↑x✝ * (↑x✝ - 1) / 2) * 2 = ↑x✝ * (2 + (↑x✝ - 1))
linarith[((\langle ℕ\rangle:Int)*(\langle Nat\rangle-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)) /- 现在让我们证明反命题，即 LHS 中的每个 α 都是一个偶数。我们声称对于所有这样的 α 和 n ∈ ℕ，我们有 ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋)。-/ 足够：∀ (n : ℕ),⌊(n+1)*x⌋ =⌊ x⌋+2 * ↑ (n : ℕ) * (l-(⌊(x)⌋))
精炼_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
这个
：
∀ (n : ℕ), ⌊(↑n + 1) * x⌋ = ⌊x⌋ + 2 * ↑n * (l - ⌊x⌋)
⊢ x ∈ {α | ∃ k, 偶数 k ∧ α = ↑k}
这个
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⌋)
·
精炼_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
这个
：
∀ (n : ℕ), ⌊(↑n + 1) * x⌋ = ⌊x⌋ + 2 * ↑n * (l - ⌊x⌋)
⊢ x ∈ {α | ∃ k, 偶数 k ∧ α = ↑k}
/- 让我们暂时假设这个声明是真的，看看这如何足以完成我们的证明。 -/ zify[mul_comm,Int.floor_eq_iff] 在这里
精炼_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
这个
：
∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1
⊢ x ∈ {α | ∃ k, 偶数 k ∧ α = ↑k}
-- 我们将展示 α = 2(l-⌊α⌋)，这显然是偶数。 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
这个
：
∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1
⊢ 即使 ((l - ⌊x⌋) * 2) ∧ x = ↑((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
这个
：
∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1
⊢ x = (↑l - ↑⌊x⌋) * 2
-- 要做到这一点，只需证明 α ≤ 2(l-⌊α⌋) 和 α ≥ 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
这个
：
∀ (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
这个
：
∀ (n : ℕ), ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) ≤ x * (↑n + 1) ∧ x * (↑n + 1) < ↑⌊x⌋ + (↑l - ↑⌊x⌋) * (↑n * 2) + 1
⊢ (↑l - ↑⌊x⌋) * 2 ≤ x
/- 为了证明第一个不等式，注意到如果 α > 2(l-⌊α⌋)，那么存在一个整数 N > 0，使得 N ≥ 1/(α - 2(l -⌊α⌋))。根据我们假设的主张（取 n = N），我们有 ⌊α⌋ + 2(l-⌊α⌋)N + 1 > (N+1)α，即 ⌊α⌋ + (2(l-⌊α⌋) - α)N + 1 > α，这意味着 ⌊α⌋ > α；矛盾。 -/ use not_lt.1 (by
⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, 偶数 k ∧ α = ↑k}
存在_nat_ge (1/(x-)) 的情况| N =>nlinarith[ one_div_mul_cancel $ sub_ne_zero.2 ·.ne',9,Int.floor_le x, this N]) /- 类似地，如果 α < 2(l-⌊α⌋)，那么我们可以找到一个正自然数 N，使得 N ≥ 1/(2(l-⌊α⌋) - α)。根据我们的主张（取 n = N），我们有 (N+1)α ≥ ⌊α⌋ + 2(l-⌊α⌋)N，即 α ≥ ⌊α⌋ + (2(l-⌊α⌋) - α)N，这意味着 a ≥ ⌊α⌋ + 1；矛盾。 -/ 使用 not_lt.1 (by
⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, 偶数 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]) /- 现在剩下的就是证明我们的主张 ⌊(n + 1)α⌋ = ⌊α⌋ + 2n(l - ⌊α⌋)。-/ intro
这个
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⌋)
-- 我们通过对 n 的强归纳法进行论证。 induction‹_› 使用@Nat.strongInductionOn
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⌋)
-- 根据我们对 α 的假设，我们知道 (n+1) | ∑_{i=1}^(n+1) ⌊iα⌋ 专门化 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[加法交换律, 乘法结合律, 整数下取整等价, <-自然数区间右侧后继, 加法乘法, (有限集范围后继), 有限集求和区间等于求和范围]
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⌋)))
/- 因此，存在 c 使得 (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⌋)))
/- 根据归纳假设， ∑_{i=0}^{n-1}, ⌊α+iα⌋ = ∑_{i=0}^{n-1}, ⌊α⌋+2*i*(l-⌊α⌋). -/ 足够：∑d 在 .范围 A,⌊x+dx⌋=∑Q 在 .范围 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⌋
这个
：
∑ 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⌋)))
这个
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⌋
这个
：
∑ 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⌋)))
足够:∑d 在 ( .范围 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⌋
这个✝
：
∑ 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
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
这个
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⌋)))
⊢ ∑ 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⌋
这个✝
：
∑ 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
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
have:(A : ℤ) * (A-1)%2=0
这个
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⌋)))
这个
：
∑ 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⌋
这个✝¹
：
∑ 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
这个
：
↑A * (↑A - 1) % 2 = 0
⊢ ↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)) ≤ x + ↑A * x ∧ x + ↑A * x < 1 + (↑⌊x⌋ + 2 * (↑A * (↑l - ↑⌊x⌋)))
·
这个
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⌋)))
这个
：
∑ 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⌋
这个✝
：
∑ 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
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⌋
这个✝¹
：
∑ 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
这个
：
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⌋
这个✝¹
：
∑ d ∈ Finset.range A, ↑d = ↑A * (↑A - 1) / 2
这个✝
：
2 ∣ ↑A * (↑A - 1)
这个
：
∑ 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[等价于加法等于]at*
this.ind.intro