[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
[PROOFSTEP]
cases' lt_or_le x y with h' h'
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
[PROOFSTEP]
use x
[GOAL]
case property
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ x ∈ Ico x (x + dx) \ Ico y (y + dy)
[PROOFSTEP]
simp [*, not_le.2 h']
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
[PROOFSTEP]
use max x (x + dy)
[GOAL]
case property
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ max x (x + dy) ∈ Ico x (x + dx) \ Ico y (y + dy)
[PROOFSTEP]
simp [*, le_refl]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ioc (a * b ^ n) (a * b ^ (n + 1)))
[PROOFSTEP]
simp_rw [Function.onFun, Set.disjoint_iff]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise fun x y => Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
[PROOFSTEP]
intro m n hmn x hx
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ x ∈ ∅
[PROOFSTEP]
apply hmn
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ m = n
[PROOFSTEP]
have hb : 1 < b := by
  have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2
  rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b
[PROOFSTEP]
have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
⊢ 1 < b
[PROOFSTEP]
rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
⊢ m = n
[PROOFSTEP]
have i1 := hx.1.1.trans_le hx.2.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
⊢ m = n
[PROOFSTEP]
have i2 := hx.2.1.trans_le hx.1.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
⊢ m = n
[PROOFSTEP]
rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff hb, Int.lt_add_one_iff] at i1 i2 
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : m ≤ n
i2 : n ≤ m
⊢ m = n
[PROOFSTEP]
exact le_antisymm i1 i2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ico (a * b ^ n) (a * b ^ (n + 1)))
[PROOFSTEP]
simp_rw [Function.onFun, Set.disjoint_iff]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise fun x y => Ico (a * b ^ x) (a * b ^ (x + 1)) ∩ Ico (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
[PROOFSTEP]
intro m n hmn x hx
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ x ∈ ∅
[PROOFSTEP]
apply hmn
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ m = n
[PROOFSTEP]
have hb : 1 < b := by
  have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2
  rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b
[PROOFSTEP]
have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
⊢ 1 < b
[PROOFSTEP]
rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this 
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
⊢ m = n
[PROOFSTEP]
have i1 := hx.1.1.trans_lt hx.2.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
⊢ m = n
[PROOFSTEP]
have i2 := hx.2.1.trans_lt hx.1.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
⊢ m = n
[PROOFSTEP]
rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff hb, Int.lt_add_one_iff] at i1 i2 
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : m ≤ n
i2 : n ≤ m
⊢ m = n
[PROOFSTEP]
exact le_antisymm i1 i2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ioc (b ^ n) (b ^ (n + 1)))
[PROOFSTEP]
simpa only [one_mul] using pairwise_disjoint_Ioc_mul_zpow 1 b
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ico (b ^ n) (b ^ (n + 1)))
[PROOFSTEP]
simpa only [one_mul] using pairwise_disjoint_Ico_mul_zpow 1 b
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ioo (b ^ n) (b ^ (n + 1)))
[PROOFSTEP]
simpa only [one_mul] using pairwise_disjoint_Ioo_mul_zpow 1 b
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioc (a + ↑n) (a + ↑n + 1))
[PROOFSTEP]
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using pairwise_disjoint_Ioc_add_zsmul a (1 : α)
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ico (a + ↑n) (a + ↑n + 1))
[PROOFSTEP]
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using pairwise_disjoint_Ico_add_zsmul a (1 : α)
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioo (a + ↑n) (a + ↑n + 1))
[PROOFSTEP]
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using pairwise_disjoint_Ioo_add_zsmul a (1 : α)
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ico (↑n) (↑n + 1))
[PROOFSTEP]
simpa only [zero_add] using pairwise_disjoint_Ico_add_int_cast (0 : α)
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioo (↑n) (↑n + 1))
[PROOFSTEP]
simpa only [zero_add] using pairwise_disjoint_Ioo_add_int_cast (0 : α)
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioc (↑n) (↑n + 1))
[PROOFSTEP]
simpa only [zero_add] using pairwise_disjoint_Ioc_add_int_cast (0 : α)
