[GOAL]
⊢ LinearOrderedAddCommGroup ℤ
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑(natAbs n) = ↑|n|
[PROOFSTEP]
rw [← coe_natAbs, Int.cast_ofNat]
[GOAL]
a : ℤ
⊢ natAbs |a| = natAbs a
[PROOFSTEP]
rw [abs_eq_natAbs]
[GOAL]
a : ℤ
⊢ natAbs ↑(natAbs a) = natAbs a
[PROOFSTEP]
rfl
[GOAL]
a : ℤ
⊢ sign a * |a| = a
[PROOFSTEP]
rw [abs_eq_natAbs, sign_mul_natAbs a]
[GOAL]
n : ℕ
⊢ ↑n ≠ 0 ↔ n ≠ 0
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {m n : ℤ}, sign m = sign n → sign (m + n) = sign n
[PROOFSTEP]
have : (1 : ℤ) ≠ -1 := by decide
[GOAL]
⊢ 1 ≠ -1
[PROOFSTEP]
decide
[GOAL]
this : 1 ≠ -1
⊢ ∀ {m n : ℤ}, sign m = sign n → sign (m + n) = sign n
[PROOFSTEP]
rintro ((_ | m) | m) ((_ | n) | n)
[GOAL]
case ofNat.zero.ofNat.zero
this : 1 ≠ -1
⊢ sign (ofNat zero) = sign (ofNat zero) → sign (ofNat zero + ofNat zero) = sign (ofNat zero)
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.zero.ofNat.succ
this : 1 ≠ -1
n : ℕ
⊢ sign (ofNat zero) = sign (ofNat (Nat.succ n)) → sign (ofNat zero + ofNat (Nat.succ n)) = sign (ofNat (Nat.succ n))
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.zero.negSucc
this : 1 ≠ -1
n : ℕ
⊢ sign (ofNat zero) = sign -[n+1] → sign (ofNat zero + -[n+1]) = sign -[n+1]
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.succ.ofNat.zero
this : 1 ≠ -1
m : ℕ
⊢ sign (ofNat (Nat.succ m)) = sign (ofNat zero) → sign (ofNat (Nat.succ m) + ofNat zero) = sign (ofNat zero)
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ sign (ofNat (Nat.succ m)) = sign (ofNat (Nat.succ n)) →
    sign (ofNat (Nat.succ m) + ofNat (Nat.succ n)) = sign (ofNat (Nat.succ n))
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.succ.negSucc
this : 1 ≠ -1
m n : ℕ
⊢ sign (ofNat (Nat.succ m)) = sign -[n+1] → sign (ofNat (Nat.succ m) + -[n+1]) = sign -[n+1]
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case negSucc.ofNat.zero
this : 1 ≠ -1
m : ℕ
⊢ sign -[m+1] = sign (ofNat zero) → sign (-[m+1] + ofNat zero) = sign (ofNat zero)
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case negSucc.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ sign -[m+1] = sign (ofNat (Nat.succ n)) → sign (-[m+1] + ofNat (Nat.succ n)) = sign (ofNat (Nat.succ n))
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case negSucc.negSucc
this : 1 ≠ -1
m n : ℕ
⊢ sign -[m+1] = sign -[n+1] → sign (-[m+1] + -[n+1]) = sign -[n+1]
[PROOFSTEP]
simp [this, this.symm]
[GOAL]
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ sign (↑m + 1 + (↑n + 1)) = 1
[PROOFSTEP]
rw [Int.sign_eq_one_iff_pos]
[GOAL]
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ 0 < ↑m + 1 + (↑n + 1)
[PROOFSTEP]
apply Int.add_pos
[GOAL]
case ofNat.succ.ofNat.succ.ha
this : 1 ≠ -1
m n : ℕ
⊢ 0 < ↑m + 1
[PROOFSTEP]
exact zero_lt_one.trans_le (le_add_of_nonneg_left <| coe_nat_nonneg _)
[GOAL]
case ofNat.succ.ofNat.succ.hb
this : 1 ≠ -1
m n : ℕ
⊢ 0 < ↑n + 1
[PROOFSTEP]
exact zero_lt_one.trans_le (le_add_of_nonneg_left <| coe_nat_nonneg _)
[GOAL]
a : ℤ
a0 : |a| < 1
⊢ a = 0
[PROOFSTEP]
let ⟨hn, hp⟩ := abs_lt.mp a0
[GOAL]
a : ℤ
a0 : |a| < 1
hn : -1 < a
hp : a < 1
⊢ a = 0
[PROOFSTEP]
rw [← zero_add 1, lt_add_one_iff] at hp 
[GOAL]
a : ℤ
a0 : |a| < 1
hn : -1 < a
hp✝ : a < 1
hp : a ≤ 0
⊢ a = 0
[PROOFSTEP]
exact hp.antisymm hn
[GOAL]
a : ℤ
⊢ |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1
[PROOFSTEP]
rw [le_iff_lt_or_eq, abs_lt_one_iff, abs_eq (zero_le_one' ℤ)]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ C b = C (b + ↑0)
[PROOFSTEP]
erw [add_zero]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ C (b + ↑n + 1) = C (b + ↑(n + 1))
[PROOFSTEP]
rw [add_assoc]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ C (b + (↑n + 1)) = C (b + ↑(n + 1))
[PROOFSTEP]
rfl
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ C (b + -[n + 1+1])
[PROOFSTEP]
refine _root_.cast (by rw [add_sub_assoc]; rfl) (Hp _ (Int.le_of_lt ?_) (neg n))
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ C (b + -[n+1] - 1) = C (b + -[n + 1+1])
[PROOFSTEP]
rw [add_sub_assoc]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ C (b + (-[n+1] - 1)) = C (b + -[n + 1+1])
[PROOFSTEP]
rfl
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ b + -[n+1] < b
[PROOFSTEP]
conv => rhs; apply (add_zero b).symm
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
| b + -[n+1] < b
[PROOFSTEP]
rhs; apply (add_zero b).symm
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
| b + -[n+1] < b
[PROOFSTEP]
rhs; apply (add_zero b).symm
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
| b + -[n+1] < b
[PROOFSTEP]
rhs
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
| b
[PROOFSTEP]
apply (add_zero b).symm
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ b + -[n+1] < b + 0
[PROOFSTEP]
rw [Int.add_lt_add_iff_left]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
⊢ -[n+1] < 0
[PROOFSTEP]
apply negSucc_lt_zero
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ C z
[PROOFSTEP]
rw [← sub_add_cancel (G := ℤ) z b, add_comm]
[GOAL]
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
⊢ C (b + (z - b))
[PROOFSTEP]
exact
  match z - b with
  | .ofNat n => pos n
  | .negSucc n => neg n
[GOAL]
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ m ≤ n → P n
[PROOFSTEP]
refine Int.inductionOn' n m ?_ ?_ ?_
[GOAL]
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ m ≤ m → P m
[PROOFSTEP]
intro
[GOAL]
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
a✝ : m ≤ m
⊢ P m
[PROOFSTEP]
exact h0
[GOAL]
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ ∀ (k : ℤ), m ≤ k → (m ≤ k → P k) → m ≤ k + 1 → P (k + 1)
[PROOFSTEP]
intro k hle hi _
[GOAL]
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : m ≤ k
hi : m ≤ k → P k
a✝ : m ≤ k + 1
⊢ P (k + 1)
[PROOFSTEP]
exact h1 k hle (hi hle)
[GOAL]
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n : ℤ
⊢ ∀ (k : ℤ), k ≤ m → (m ≤ k → P k) → m ≤ k - 1 → P (k - 1)
[PROOFSTEP]
intro k hle _ hle'
[GOAL]
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : k ≤ m
a✝ : m ≤ k → P k
hle' : m ≤ k - 1
⊢ P (k - 1)
[PROOFSTEP]
exfalso
[GOAL]
case refine_3.h
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), m ≤ n → P n → P (n + 1)
n k : ℤ
hle : k ≤ m
a✝ : m ≤ k → P k
hle' : m ≤ k - 1
⊢ False
[PROOFSTEP]
exact lt_irrefl k (le_sub_one_iff.mp (hle.trans hle'))
[GOAL]
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n : ℤ
⊢ n ≤ m → P n
[PROOFSTEP]
refine Int.inductionOn' n m ?_ ?_ ?_
[GOAL]
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n : ℤ
⊢ m ≤ m → P m
[PROOFSTEP]
intro
[GOAL]
case refine_1
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n : ℤ
a✝ : m ≤ m
⊢ P m
[PROOFSTEP]
exact h0
[GOAL]
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n : ℤ
⊢ ∀ (k : ℤ), m ≤ k → (k ≤ m → P k) → k + 1 ≤ m → P (k + 1)
[PROOFSTEP]
intro k hle _ hle'
[GOAL]
case refine_2
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n k : ℤ
hle : m ≤ k
a✝ : k ≤ m → P k
hle' : k + 1 ≤ m
⊢ P (k + 1)
[PROOFSTEP]
exfalso
[GOAL]
case refine_2.h
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n k : ℤ
hle : m ≤ k
a✝ : k ≤ m → P k
hle' : k + 1 ≤ m
⊢ False
[PROOFSTEP]
exact lt_irrefl k (add_one_le_iff.mp (hle'.trans hle))
[GOAL]
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n : ℤ
⊢ ∀ (k : ℤ), k ≤ m → (k ≤ m → P k) → k - 1 ≤ m → P (k - 1)
[PROOFSTEP]
intro k hle hi _
[GOAL]
case refine_3
P : ℤ → Prop
m : ℤ
h0 : P m
h1 : ∀ (n : ℤ), n ≤ m → P n → P (n - 1)
n k : ℤ
hle : k ≤ m
hi : k ≤ m → P k
a✝ : k - 1 ≤ m
⊢ P (k - 1)
[PROOFSTEP]
exact h1 k hle (hi hle)
[GOAL]
a✝ b✝ : ℤ
n✝ : ℕ
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑(natAbs -[n+1])
⊢ -(a / -[n+1]) = -0
[PROOFSTEP]
rw [← Int.ediv_neg]
[GOAL]
a✝ b✝ : ℤ
n✝ : ℕ
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑(natAbs -[n+1])
⊢ a / - -[n+1] = -0
[PROOFSTEP]
exact ediv_eq_zero_of_lt H1 H2
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
H : b ≠ 0
⊢ a % b < |b|
[PROOFSTEP]
rw [← emod_abs]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
H : b ≠ 0
⊢ a % |b| < |b|
[PROOFSTEP]
exact emod_lt_of_pos _ (abs_pos.2 H)
[GOAL]
a b : ℤ
n✝ : ℕ
m n k i : ℤ
H : m % n = k % n
⊢ (m + i) % n = (k + i) % n
[PROOFSTEP]
rw [← emod_add_emod, ← emod_add_emod k, H]
[GOAL]
a b : ℤ
n : ℕ
i : ℤ
⊢ -i % 2 = i % 2
[PROOFSTEP]
apply Int.emod_eq_emod_iff_emod_sub_eq_zero.mpr
[GOAL]
a b : ℤ
n : ℕ
i : ℤ
⊢ (-i - i) % 2 = 0
[PROOFSTEP]
convert Int.mul_emod_right 2 (-i) using 2
[GOAL]
case h.e'_2.h.e'_5
a b : ℤ
n : ℕ
i : ℤ
⊢ -i - i = 2 * -i
[PROOFSTEP]
rw [two_mul, sub_eq_add_neg]
[GOAL]
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|
[PROOFSTEP]
rw [abs_eq_natAbs, abs_eq_natAbs]
[GOAL]
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ ↑(natAbs (a / ↑n)) ≤ ↑(natAbs a)
[PROOFSTEP]
exact
  ofNat_le_ofNat_of_le
    (match a, n with
    | (m : ℕ), n => Nat.div_le_self _ _
    | -[m+1], 0 => Nat.zero_le _
    | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))
[GOAL]
a✝ b✝ : ℤ
n✝ : ℕ
this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / -↑n| ≤ |a|
[PROOFSTEP]
rw [Int.ediv_neg, abs_neg]
[GOAL]
a✝ b✝ : ℤ
n✝ : ℕ
this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|
[PROOFSTEP]
apply this
[GOAL]
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ 0 ≤ 2
[PROOFSTEP]
decide
[GOAL]
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ |2| ≠ 0
[PROOFSTEP]
decide
[GOAL]
a b : ℤ
n✝ : ℕ
n : ℤ
h : n % 2 < 2
⊢ 2 ≠ 0
[PROOFSTEP]
decide
[GOAL]
a b : ℤ
n✝ : ℕ
n : ℤ
h : n % 2 < 2
h₁✝ : 0 ≤ n % 2
k : ℕ
h₁ : ↑(k + 2) < 2
x✝ : 0 ≤ ↑(k + 2)
⊢ 2 ≤ ↑(k + 2)
[PROOFSTEP]
rw [Nat.cast_add]
[GOAL]
a b : ℤ
n✝ : ℕ
n : ℤ
h : n % 2 < 2
h₁✝ : 0 ≤ n % 2
k : ℕ
h₁ : ↑(k + 2) < 2
x✝ : 0 ≤ ↑(k + 2)
⊢ 2 ≤ ↑k + ↑2
[PROOFSTEP]
exact (le_add_iff_nonneg_left 2).2 (NonNeg.mk k)
[GOAL]
a✝ b : ℤ
n✝ : ℕ
n : ℤ
h : n % 2 < 2
h₁✝ : 0 ≤ n % 2
a : ℕ
x✝ : -[a+1] < 2
h₁ : 0 ≤ -[a+1]
⊢ -[a+1] = 0 ∨ -[a+1] = 1
[PROOFSTEP]
cases h₁
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
az : a = 0
⊢ a * b / a ∣ a * b * c / a
[PROOFSTEP]
simp [az]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
az : ¬a = 0
⊢ a * b / a ∣ a * b * c / a
[PROOFSTEP]
rw [Int.mul_ediv_cancel_left _ az, mul_assoc, Int.mul_ediv_cancel_left _ az]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
az : ¬a = 0
⊢ b ∣ b * c
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
a b : ℤ
n : ℕ
z : ℤ
hz : z ≠ 0
⊢ |sign z| = 1
[PROOFSTEP]
rw [abs_eq_natAbs, natAbs_sign_of_nonzero hz, Int.ofNat_one]
[GOAL]
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m
[PROOFSTEP]
constructor
[GOAL]
case mp
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ (∃ k, n * k < m ∧ m < n * (k + 1)) → ¬n ∣ m
[PROOFSTEP]
rintro ⟨k, h1k, h2k⟩ ⟨l, rfl⟩
[GOAL]
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : n * k < n * l
h2k : n * l < n * (k + 1)
⊢ False
[PROOFSTEP]
rw [mul_lt_mul_left hn] at h1k h2k 
[GOAL]
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : l < k + 1
⊢ False
[PROOFSTEP]
rw [lt_add_one_iff, ← not_lt] at h2k 
[GOAL]
case mp.intro.intro.intro
a b : ℤ
n✝ : ℕ
n : ℤ
hn : 0 < n
k l : ℤ
h1k : k < l
h2k : ¬k < l
⊢ False
[PROOFSTEP]
exact h2k h1k
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
⊢ ¬n ∣ m → ∃ k, n * k < m ∧ m < n * (k + 1)
[PROOFSTEP]
intro h
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : ¬n ∣ m
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
[PROOFSTEP]
rw [dvd_iff_emod_eq_zero, ← Ne.def] at h 
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
[PROOFSTEP]
have := (emod_nonneg m hn.ne.symm).lt_of_ne h.symm
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ ∃ k, n * k < m ∧ m < n * (k + 1)
[PROOFSTEP]
simp (config := { singlePass := true }) only [← emod_add_ediv m n]
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ ∃ k, n * k < m % n + n * (m / n) ∧ m % n + n * (m / n) < n * (k + 1)
[PROOFSTEP]
refine' ⟨m / n, lt_add_of_pos_left _ this, _⟩
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ m % n + n * (m / n) < n * (m / n + 1)
[PROOFSTEP]
rw [add_comm _ (1 : ℤ), left_distrib, mul_one]
[GOAL]
case mpr
a b : ℤ
n✝ : ℕ
m n : ℤ
hn : 0 < n
h : m % n ≠ 0
this : 0 < m % n
⊢ m % n + n * (m / n) < n + n * (m / n)
[PROOFSTEP]
exact add_lt_add_right (emod_lt_of_pos _ hn) _
[GOAL]
a✝ b : ℤ
n : ℕ
a : ℤ
az : a = 0
⊢ sign a = a / |a|
[PROOFSTEP]
simp [az]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
H : b ≠ 0
⊢ 0 ≤ a - a / b * b
[PROOFSTEP]
rw [mul_comm, ← emod_def]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
H : b ≠ 0
⊢ 0 ≤ a % b
[PROOFSTEP]
apply emod_nonneg _ H
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
H1 : 0 ≤ b
H2 : b ∣ a
H3 : a / b ≤ c
⊢ a ≤ c * b
[PROOFSTEP]
rw [← Int.ediv_mul_cancel H2]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
H1 : 0 ≤ b
H2 : b ∣ a
H3 : a / b ≤ c
⊢ a / b * b ≤ c * b
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right H3 H1
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
H1 : 0 < a
H2 : 0 ≤ b
H3 : b ∣ a
⊢ 0 * b < a
[PROOFSTEP]
rwa [zero_mul]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c d : ℤ
H2 : d ∣ c
H3 : b ≠ 0
H4 : d ≠ 0
H5 : a * d = b * c
⊢ a = b * (c / d)
[PROOFSTEP]
rw [← Int.mul_ediv_assoc _ H2]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b c d : ℤ
H2 : d ∣ c
H3 : b ≠ 0
H4 : d ≠ 0
H5 : a * d = b * c
⊢ a = b * c / d
[PROOFSTEP]
exact (Int.ediv_eq_of_eq_mul_left H4 H5.symm).symm
[GOAL]
a b : ℤ
n : ℕ
s t : ℤ
hst : s ∣ t
⊢ t / s ∣ t
[PROOFSTEP]
rcases eq_or_ne s 0 with (rfl | hs)
[GOAL]
case inl
a b : ℤ
n : ℕ
t : ℤ
hst : 0 ∣ t
⊢ t / 0 ∣ t
[PROOFSTEP]
simpa using hst
[GOAL]
case inr
a b : ℤ
n : ℕ
s t : ℤ
hst : s ∣ t
hs : s ≠ 0
⊢ t / s ∣ t
[PROOFSTEP]
rcases hst with ⟨c, hc⟩
[GOAL]
case inr.intro
a b : ℤ
n : ℕ
s t : ℤ
hs : s ≠ 0
c : ℤ
hc : t = s * c
⊢ t / s ∣ t
[PROOFSTEP]
simp [hc, Int.mul_ediv_cancel_left _ hs]
[GOAL]
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ toNat a ≤ n ↔ a ≤ ↑n
[PROOFSTEP]
rw [ofNat_le.symm, toNat_eq_max, max_le_iff]
[GOAL]
a✝ b : ℤ
n✝ : ℕ
a : ℤ
n : ℕ
⊢ a ≤ ↑n ∧ 0 ≤ ↑n ↔ a ≤ ↑n
[PROOFSTEP]
exact and_iff_left (ofNat_zero_le _)
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
h : a ≤ b
⊢ toNat a ≤ toNat b
[PROOFSTEP]
rw [toNat_le]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
h : a ≤ b
⊢ a ≤ ↑(toNat b)
[PROOFSTEP]
exact le_trans h (self_le_toNat b)
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
hb : 0 < b
h : toNat a < toNat b
⊢ a < b
[PROOFSTEP]
cases a
[GOAL]
case ofNat
a b✝ : ℤ
n : ℕ
b : ℤ
hb : 0 < b
a✝ : ℕ
h : toNat (ofNat a✝) < toNat b
⊢ ofNat a✝ < b
case negSucc a b✝ : ℤ n : ℕ b : ℤ hb : 0 < b a✝ : ℕ h : toNat -[a✝+1] < toNat b ⊢ -[a✝+1] < b
[PROOFSTEP]
exact lt_toNat.1 h
[GOAL]
case negSucc
a b✝ : ℤ
n : ℕ
b : ℤ
hb : 0 < b
a✝ : ℕ
h : toNat -[a✝+1] < toNat b
⊢ -[a✝+1] < b
[PROOFSTEP]
exact lt_trans (neg_of_sign_eq_neg_one rfl) hb
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
hb : 0 < b
h : a < b
⊢ toNat a < toNat b
[PROOFSTEP]
rw [lt_toNat]
[GOAL]
a✝ b✝ : ℤ
n : ℕ
a b : ℤ
hb : 0 < b
h : a < b
⊢ ↑(toNat a) < b
[PROOFSTEP]
cases a
[GOAL]
case ofNat
a b✝ : ℤ
n : ℕ
b : ℤ
hb : 0 < b
a✝ : ℕ
h : ofNat a✝ < b
⊢ ↑(toNat (ofNat a✝)) < b
case negSucc a b✝ : ℤ n : ℕ b : ℤ hb : 0 < b a✝ : ℕ h : -[a✝+1] < b ⊢ ↑(toNat -[a✝+1]) < b
[PROOFSTEP]
exact h
[GOAL]
case negSucc
a b✝ : ℤ
n : ℕ
b : ℤ
hb : 0 < b
a✝ : ℕ
h : -[a✝+1] < b
⊢ ↑(toNat -[a✝+1]) < b
[PROOFSTEP]
exact hb
[GOAL]
a b : ℤ
n : ℕ
i : ℤ
h : 0 < i
⊢ ↑(toNat i - 1) = i - 1
[PROOFSTEP]
simp [h, le_of_lt h, push_cast]
