The integers

Analysis I, Section 4.1: The integers

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Definition of the "Section 4.1" integers, Section_4_1.Int : TypeSection_4_1.Int, as formal differences Unknown identifier `a`sorry —— sorry : Section_4_1.Inta —— Unknown identifier `b`b of natural numbers , up to equivalence. (This is a quotient of a scaffolding type Section_4_1.PreInt : TypeSection_4_1.PreInt, which consists of formal differences without any equivalence imposed.)
ring operations and order these integers, as well as an embedding of ℕ.
Equivalence with the Mathlib integers Int : Type_root_.Int (or ℤ : Typeℤ), which we will use going forward.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

namespace Section_4_1

structure PreInt where
  minuend : ℕ
  subtrahend : ℕ

Definition 4.1.1

instance declaration uses 'sorry'PreInt.instSetoid : Setoid PreInt where
  r a b := a.minuend + b.subtrahend = b.minuend + a.subtrahend
  iseqv := {
    refl := by⊢ ∀ (x : PreInt), x.minuend + x.subtrahend = x.minuend + x.subtrahend sorryAll goals completed! 🐙
    symm := by⊢ ∀ {x y : PreInt},
  x.minuend + y.subtrahend = y.minuend + x.subtrahend → y.minuend + x.subtrahend = x.minuend + y.subtrahend sorryAll goals completed! 🐙
    trans := by⊢ ∀ {x y z : PreInt},
  x.minuend + y.subtrahend = y.minuend + x.subtrahend →
    y.minuend + z.subtrahend = z.minuend + y.subtrahend → x.minuend + z.subtrahend = z.minuend + x.subtrahend
      -- This proof is written to follow the structure of the original text.
      intro ⟨ a,b ⟩ ⟨ c,d ⟩ ⟨ e,f ⟩ h1 h2a:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:{ minuend := a, subtrahend := b }.minuend + { minuend := c, subtrahend := d }.subtrahend =
  { minuend := c, subtrahend := d }.minuend + { minuend := a, subtrahend := b }.subtrahendh2:{ minuend := c, subtrahend := d }.minuend + { minuend := e, subtrahend := f }.subtrahend =
  { minuend := e, subtrahend := f }.minuend + { minuend := c, subtrahend := d }.subtrahend⊢ { minuend := a, subtrahend := b }.minuend + { minuend := e, subtrahend := f }.subtrahend =
  { minuend := e, subtrahend := f }.minuend + { minuend := a, subtrahend := b }.subtrahend; simp_alla:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + d⊢ a + f = e + b
      have h3 := congrArg₂ (·+ ·) h1 h2a:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:?_mvar.1854 := congrArg₂ (fun x1 x2 => x1 + x2) _fvar.1847 _fvar.1848⊢ a + f = e + b; simp at h3a:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:_fvar.591 + _fvar.678 + (_fvar.677 + _fvar.754) = _fvar.677 + _fvar.592 + (_fvar.753 + _fvar.678) := congrArg₂ (fun x1 x2 => x1 + x2) _fvar.1847 _fvar.1848⊢ a + f = e + b
      have : (a + f) + (c + d) = (e + b) + (c + d) := calc
        (a + f) + (c + d) = a + d + (c + f) := bya:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:_fvar.591 + _fvar.678 + (_fvar.677 + _fvar.754) = _fvar.677 + _fvar.592 + (_fvar.753 + _fvar.678) := congrArg₂ (fun x1 x2 => x1 + x2) _fvar.1847 _fvar.1848⊢ a + f + (c + d) = a + d + (c + f) abelAll goals completed! 🐙
        _ = c + b + (e + d) := h3
        _ = (e + b) + (c + d) := bya:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:_fvar.591 + _fvar.678 + (_fvar.677 + _fvar.754) = _fvar.677 + _fvar.592 + (_fvar.753 + _fvar.678) := congrArg₂ (fun x1 x2 => x1 + x2) _fvar.1847 _fvar.1848⊢ c + b + (e + d) = e + b + (c + d) abelAll goals completed! 🐙
      exact Nat.add_right_cancel thisAll goals completed! 🐙
    }

@[simp]
theorem PreInt.eq (a b c d:ℕ) : (⟨ a,b ⟩: PreInt) ≈ ⟨ c,d ⟩ ↔ a + d = c + b := bya:ℕb:ℕc:ℕd:ℕ⊢ { minuend := a, subtrahend := b } ≈ { minuend := c, subtrahend := d } ↔ a + d = c + b rflAll goals completed! 🐙

abbrev Int := Quotient PreInt.instSetoidabbrev Int.formalDiff (a b:ℕ) : Int := Quotient.mk PreInt.instSetoid ⟨ a,b ⟩infix:100 " —— " => Int.formalDiff

Definition 4.1.1 (Integers)

theorem Int.eq (a b c d:ℕ): a —— b = c —— d ↔ a + d = c + b :=
  ⟨ Quotient.exact, bya:ℕb:ℕc:ℕd:ℕ⊢ a + d = c + b → a —— b = c —— d intro ha:ℕb:ℕc:ℕd:ℕh:a + d = c + b⊢ a —— b = c —— d; exact Quotient.sound hAll goals completed! 🐙 ⟩

Decidability of equality

instance Int.decidableEq : DecidableEq Int := by⊢ DecidableEq Int
  intro a ba:Intb:Int⊢ Decidable (a = b)
  have : ∀ (n:PreInt) (m: PreInt),
      Decidable (Quotient.mk PreInt.instSetoid n = Quotient.mk PreInt.instSetoid m) := by⊢ DecidableEq Int
    intro ⟨ a,b ⟩ ⟨ c,d ⟩a✝:Intb✝:Inta:ℕb:ℕc:ℕd:ℕ⊢ Decidable (⟦{ minuend := a, subtrahend := b }⟧ = ⟦{ minuend := c, subtrahend := d }⟧)
    rw [eq]a✝:Intb✝:Inta:ℕb:ℕc:ℕd:ℕ⊢ Decidable (a + d = c + b)
    exact decEq _ _All goals completed! 🐙
  exact Quotient.recOnSubsingleton₂ a b thisAll goals completed! 🐙

Definition 4.1.1 (Integers)

theorem Int.eq_diff (n:Int) : ∃ a b, n = a —— b := byn:Int⊢ ∃ a b, n = a —— b apply n.ind _n:Int⊢ ∀ (a : PreInt), ∃ a_1 b, ⟦a⟧ = a_1 —— b; intro ⟨ a, b ⟩n:Inta:ℕb:ℕ⊢ ∃ a_1 b_1, ⟦{ minuend := a, subtrahend := b }⟧ = a_1 —— b_1; use a, bAll goals completed! 🐙

Lemma 4.1.3 (Addition well-defined)

instance Int.instAdd : Add Int where
  add := Quotient.lift₂ (fun ⟨ a, b ⟩ ⟨ c, d ⟩ ↦ (a+c) —— (b+d) ) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreInt),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
          a₂ b₂
    intro ⟨ a, b ⟩ ⟨ c, d ⟩ ⟨ a', b' ⟩ ⟨ c', d' ⟩ h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:{ minuend := a, subtrahend := b } ≈ { minuend := a', subtrahend := b' }h2:{ minuend := c, subtrahend := d } ≈ { minuend := c', subtrahend := d' }⊢ (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
    { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } =
  (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
    { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' }
    simp [Setoid.r] at *a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a + c + (b' + d') = a' + c' + (b + d)
    calc
      _ = (a+b') + (c+d') := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a + c + (b' + d') = a + b' + (c + d') abelAll goals completed! 🐙
      _ = (a'+b) + (c'+d) := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a + b' + (c + d') = a' + b + (c' + d) rw [h1,h2]All goals completed! 🐙
      _ = _ := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a' + b + (c' + d) = a' + c' + (b + d) abelAll goals completed! 🐙)

Definition 4.1.2 (Definition of addition)

theorem Int.add_eq (a b c d:ℕ) : a —— b + c —— d = (a+c)——(b+d) := Quotient.lift₂_mk _ _ _ _

Lemma 4.1.3 (Multiplication well-defined)

theorem Int.mul_congr_left (a b a' b' c d : ℕ) (h: a —— b = a' —— b') :
    (a*c+b*d) —— (a*d+b*c) = (a'*c+b'*d) —— (a'*d+b'*c) := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a —— b = a' —— b'⊢ (a * c + b * d) —— (a * d + b * c) = (a' * c + b' * d) —— (a' * d + b' * c)
  simp only [eq] at *a:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ a * c + b * d + (a' * d + b' * c) = a' * c + b' * d + (a * d + b * c)
  calc
    _ = c*(a+b') + d*(a'+b) := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ a * c + b * d + (a' * d + b' * c) = c * (a + b') + d * (a' + b) ringAll goals completed! 🐙
    _ = c*(a'+b) + d*(a+b') := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ c * (a + b') + d * (a' + b) = c * (a' + b) + d * (a + b') rw [h]All goals completed! 🐙
    _ = _ := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ c * (a' + b) + d * (a + b') = a' * c + b' * d + (a * d + b * c) ringAll goals completed! 🐙

Lemma 4.1.3 (Multiplication well-defined)

theorem Int.mul_congr_right (a b c d c' d' : ℕ) (h: c —— d = c' —— d') :
    (a*c+b*d) —— (a*d+b*c) = (a*c'+b*d') —— (a*d'+b*c') := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c —— d = c' —— d'⊢ (a * c + b * d) —— (a * d + b * c) = (a * c' + b * d') —— (a * d' + b * c')
  simp only [eq] at *a:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * c + b * d + (a * d' + b * c') = a * c' + b * d' + (a * d + b * c)
  calc
    _ = a*(c+d') + b*(c'+d) := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * c + b * d + (a * d' + b * c') = a * (c + d') + b * (c' + d) ringAll goals completed! 🐙
    _ = a*(c'+d) + b*(c+d') := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * (c + d') + b * (c' + d) = a * (c' + d) + b * (c + d') rw [h]All goals completed! 🐙
    _ = _ := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * (c' + d) + b * (c + d') = a * c' + b * d' + (a * d + b * c) ringAll goals completed! 🐙

Lemma 4.1.3 (Multiplication well-defined)

theorem Int.mul_congr {a b c d a' b' c' d' : ℕ} (h1: a —— b = a' —— b') (h2: c —— d = c' —— d') :
  (a*c+b*d) —— (a*d+b*c) = (a'*c'+b'*d') —— (a'*d'+b'*c') := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a —— b = a' —— b'h2:c —— d = c' —— d'⊢ (a * c + b * d) —— (a * d + b * c) = (a' * c' + b' * d') —— (a' * d' + b' * c')
  rw [mul_congr_left a b a' b' c d h1, mul_congr_right a' b' c d c' d' h2]All goals completed! 🐙

instance Int.instMul : Mul Int where
  mul := Quotient.lift₂ (fun ⟨ a, b ⟩ ⟨ c, d ⟩ ↦ (a * c + b * d) —— (a * d + b * c)) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreInt),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
          a₂ b₂
    intro ⟨ a, b ⟩ ⟨ c, d ⟩ ⟨ a', b' ⟩ ⟨ c', d' ⟩ h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:{ minuend := a, subtrahend := b } ≈ { minuend := a', subtrahend := b' }h2:{ minuend := c, subtrahend := d } ≈ { minuend := c', subtrahend := d' }⊢ (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } =
  (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' }; simp at h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } =
  (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' }
    convert mul_congr _ _convert_9a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a —— b = a' —— b'convert_10a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ c —— d = c' —— d' <;>convert_9a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a —— b = a' —— b'convert_10a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ c —— d = c' —— d' simpaAll goals completed! 🐙
    )

Definition 4.1.2 (Multiplication of integers)

theorem Int.mul_eq (a b c d:ℕ) : a —— b * c —— d = (a*c+b*d) —— (a*d+b*c) := Quotient.lift₂_mk _ _ _ _

instance Int.instOfNat {n:ℕ} : OfNat Int n where
  ofNat := n —— 0

instance Int.instNatCast : NatCast Int where
  natCast n := n —— 0

theorem Int.ofNat_eq (n:ℕ) : ofNat(n) = n —— 0 := rfltheorem Int.natCast_eq (n:ℕ) : (n:Int) = n —— 0 := rfl

@[simp]
theorem Int.natCast_ofNat (n:ℕ) : ((ofNat(n):ℕ): Int) = ofNat(n) := byn:ℕ⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n rflAll goals completed! 🐙

@[simp]
theorem Int.ofNat_inj (n m:ℕ) : (ofNat(n) : Int) = (ofNat(m) : Int) ↔ ofNat(n) = ofNat(m) := byn:ℕm:ℕ⊢ OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m
  simp only [ofNat_eq, eq, add_zero]n:ℕm:ℕ⊢ n = m ↔ OfNat.ofNat n = OfNat.ofNat m; rflAll goals completed! 🐙

@[simp]
theorem Int.natCast_inj (n m:ℕ) : (n : Int) = (m : Int) ↔ n = m := byn:ℕm:ℕ⊢ ↑n = ↑m ↔ n = m
  simp only [natCast_eq, eq, add_zero]All goals completed! 🐙

example : 3 = 3 —— 0 := rflexample : 3 = 4 —— 1 := by⊢ 3 = 4 —— 1 rw [Int.ofNat_eq, Int.eq]All goals completed! 🐙

(Not from textbook) 0 is the only natural whose cast is 0

lemma declaration uses 'sorry'Int.cast_eq_0_iff_eq_0 (n : ℕ) : (n : Int) = 0 ↔ n = 0 := byn:ℕ⊢ ↑n = 0 ↔ n = 0 sorryAll goals completed! 🐙

Definition 4.1.4 (Negation of integers) / Exercise 4.1.2

instance declaration uses 'sorry'Int.instNeg : Neg Int where
  neg := Quotient.lift (fun ⟨ a, b ⟩ ↦ b —— a) (by⊢ ∀ (a b : PreInt),
  a ≈ b →
    (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => b —— a)
        a =
      (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => b —— a)
        b sorryAll goals completed! 🐙)

theorem Int.neg_eq (a b:ℕ) : -(a —— b) = b —— a := rflexample : -(3 —— 5) = 5 —— 3 := rflabbrev Int.IsPos (x:Int) : Prop := ∃ (n:ℕ), n > 0 ∧ x = nabbrev Int.IsNeg (x:Int) : Prop := ∃ (n:ℕ), n > 0 ∧ x = -n

Lemma 4.1.5 (trichotomy of integers )

theorem Int.trichotomous (x:Int) : x = 0 ∨ x.IsPos ∨ x.IsNeg := byx:Int⊢ x = 0 ∨ x.IsPos ∨ x.IsNeg
  -- This proof is slightly modified from that in the original text.
  obtain ⟨ a, b, rfl ⟩ := eq_diff xintro.introa:ℕb:ℕ⊢ a —— b = 0 ∨ (a —— b).IsPos ∨ (a —— b).IsNeg
  obtain h_lt | rfl | h_gt := _root_.trichotomous (r := LT.lt) a bintro.intro.inla:ℕb:ℕh_lt:a < b⊢ a —— b = 0 ∨ (a —— b).IsPos ∨ (a —— b).IsNegintro.intro.inr.inla:ℕ⊢ a —— a = 0 ∨ (a —— a).IsPos ∨ (a —— a).IsNegintro.intro.inr.inra:ℕb:ℕh_gt:b < a⊢ a —— b = 0 ∨ (a —— b).IsPos ∨ (a —— b).IsNeg
  .intro.intro.inla:ℕb:ℕh_lt:a < b⊢ a —— b = 0 ∨ (a —— b).IsPos ∨ (a —— b).IsNeg obtain ⟨ c, rfl ⟩ := Nat.exists_eq_add_of_lt h_ltintro.intro.inl.introa:ℕc:ℕh_lt:a < a + c + 1⊢ a —— (a + c + 1) = 0 ∨ (a —— (a + c + 1)).IsPos ∨ (a —— (a + c + 1)).IsNeg
    rightintro.intro.inl.intro.ha:ℕc:ℕh_lt:a < a + c + 1⊢ (a —— (a + c + 1)).IsPos ∨ (a —— (a + c + 1)).IsNeg; rightintro.intro.inl.intro.h.ha:ℕc:ℕh_lt:a < a + c + 1⊢ (a —— (a + c + 1)).IsNeg; refine ⟨ c+1, bya:ℕc:ℕh_lt:a < a + c + 1⊢ c + 1 > 0 linarithAll goals completed! 🐙, ?_ ⟩
    simp_rw [natCast_eq, neg_eq, eq]intro.intro.inl.intro.h.ha:ℕc:ℕh_lt:a < a + c + 1⊢ a + (c + 1) = 0 + (a + c + 1); abelAll goals completed! 🐙
  .intro.intro.inr.inla:ℕ⊢ a —— a = 0 ∨ (a —— a).IsPos ∨ (a —— a).IsNeg leftintro.intro.inr.inl.ha:ℕ⊢ a —— a = 0; simp_rw [ofNat_eq, eq, add_zero, zero_add]All goals completed! 🐙
  obtain ⟨ c, rfl ⟩ := Nat.exists_eq_add_of_lt h_gtintro.intro.inr.inr.introb:ℕc:ℕh_gt:b < b + c + 1⊢ (b + c + 1) —— b = 0 ∨ ((b + c + 1) —— b).IsPos ∨ ((b + c + 1) —— b).IsNeg
  rightintro.intro.inr.inr.intro.hb:ℕc:ℕh_gt:b < b + c + 1⊢ ((b + c + 1) —— b).IsPos ∨ ((b + c + 1) —— b).IsNeg; leftintro.intro.inr.inr.intro.h.hb:ℕc:ℕh_gt:b < b + c + 1⊢ ((b + c + 1) —— b).IsPos; refine ⟨ c+1, byb:ℕc:ℕh_gt:b < b + c + 1⊢ c + 1 > 0 linarithAll goals completed! 🐙, ?_ ⟩
  simp_rw [natCast_eq, eq]intro.intro.inr.inr.intro.h.hb:ℕc:ℕh_gt:b < b + c + 1⊢ b + c + 1 + 0 = c + 1 + b; abelAll goals completed! 🐙

Lemma 4.1.5 (trichotomy of integers)

theorem Int.not_pos_zero (x:Int) : x = 0 ∧ x.IsPos → False := byx:Int⊢ x = 0 ∧ x.IsPos → False
  rintro ⟨ rfl, ⟨ n, _, _ ⟩ ⟩intro.intro.intron:ℕleft✝:n > 0right✝:0 = ↑n⊢ False; simp_all [←natCast_ofNat]All goals completed! 🐙

Lemma 4.1.5 (trichotomy of integers)

theorem Int.not_neg_zero (x:Int) : x = 0 ∧ x.IsNeg → False := byx:Int⊢ x = 0 ∧ x.IsNeg → False
  rintro ⟨ rfl, ⟨ n, _, hn ⟩ ⟩intro.intro.intron:ℕleft✝:n > 0hn:0 = -↑n⊢ False; simp_rw [←natCast_ofNat, natCast_eq, neg_eq, eq] at hnintro.intro.intron:ℕleft✝:n > 0hn:0 + n = 0 + 0⊢ False
  linarithAll goals completed! 🐙

Lemma 4.1.5 (trichotomy of integers)

theorem Int.not_pos_neg (x:Int) : x.IsPos ∧ x.IsNeg → False := byx:Int⊢ x.IsPos ∧ x.IsNeg → False
  rintro ⟨ ⟨ n, _, rfl ⟩, ⟨ m, _, hm ⟩ ⟩intro.intro.intro.intro.intron:ℕleft✝¹:n > 0m:ℕleft✝:m > 0hm:↑n = -↑m⊢ False; simp_rw [natCast_eq, neg_eq, eq] at hmintro.intro.intro.intro.intron:ℕleft✝¹:n > 0m:ℕleft✝:m > 0hm:n + m = 0 + 0⊢ False
  linarithAll goals completed! 🐙

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instAddGroup : AddGroup Int :=
  AddGroup.ofLeftAxioms (by⊢ ∀ (a b c : Int), a + b + c = a + (b + c) sorryAll goals completed! 🐙) (by⊢ ∀ (a : Int), 0 + a = a sorryAll goals completed! 🐙) (by⊢ ∀ (a : Int), -a + a = 0 sorryAll goals completed! 🐙)

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

instance declaration uses 'sorry'Int.instAddCommGroup : AddCommGroup Int where
  add_comm := by⊢ ∀ (a b : Int), a + b = b + a sorryAll goals completed! 🐙

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instCommMonoid : CommMonoid Int where
  mul_comm := by⊢ ∀ (a b : Int), a * b = b * a sorryAll goals completed! 🐙
  mul_assoc := by⊢ ∀ (a b c : Int), a * b * c = a * (b * c)
    -- This proof is written to follow the structure of the original text.
    intro x y zx:Inty:Intz:Int⊢ x * y * z = x * (y * z)
    obtain ⟨ a, b, rfl ⟩ := eq_diff xintro.introy:Intz:Inta:ℕb:ℕ⊢ a —— b * y * z = a —— b * (y * z)
    obtain ⟨ c, d, rfl ⟩ := eq_diff yintro.intro.intro.introz:Inta:ℕb:ℕc:ℕd:ℕ⊢ a —— b * c —— d * z = a —— b * (c —— d * z)
    obtain ⟨ e, f, rfl ⟩ := eq_diff zintro.intro.intro.intro.intro.introa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ a —— b * c —— d * e —— f = a —— b * (c —— d * e —— f)
    simp_rw [mul_eq]intro.intro.intro.intro.intro.introa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ ((a * c + b * d) * e + (a * d + b * c) * f) —— ((a * c + b * d) * f + (a * d + b * c) * e) =
  (a * (c * e + d * f) + b * (c * f + d * e)) —— (a * (c * f + d * e) + b * (c * e + d * f)); congr 1intro.intro.intro.intro.intro.intro.e_aa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * e + (a * d + b * c) * f = a * (c * e + d * f) + b * (c * f + d * e)intro.intro.intro.intro.intro.intro.e_ba:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * f + (a * d + b * c) * e = a * (c * f + d * e) + b * (c * e + d * f) <;>intro.intro.intro.intro.intro.intro.e_aa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * e + (a * d + b * c) * f = a * (c * e + d * f) + b * (c * f + d * e)intro.intro.intro.intro.intro.intro.e_ba:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * f + (a * d + b * c) * e = a * (c * f + d * e) + b * (c * e + d * f) ringAll goals completed! 🐙
  one_mul := by⊢ ∀ (a : Int), 1 * a = a sorryAll goals completed! 🐙
  mul_one := by⊢ ∀ (a : Int), a * 1 = a sorryAll goals completed! 🐙

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instCommRing : CommRing Int where
  left_distrib := by⊢ ∀ (a b c : Int), a * (b + c) = a * b + a * c sorryAll goals completed! 🐙
  right_distrib := by⊢ ∀ (a b c : Int), (a + b) * c = a * c + b * c sorryAll goals completed! 🐙
  zero_mul := by⊢ ∀ (a : Int), 0 * a = 0 sorryAll goals completed! 🐙
  mul_zero := by⊢ ∀ (a : Int), a * 0 = 0 sorryAll goals completed! 🐙

Definition of subtraction

theorem Int.sub_eq (a b:Int) : a - b = a + (-b) := bya:Intb:Int⊢ a - b = a + -b rflAll goals completed! 🐙

theorem declaration uses 'sorry'Int.sub_eq_formal_sub (a b:ℕ) : (a:Int) - (b:Int) = a —— b := bya:ℕb:ℕ⊢ ↑a - ↑b = a —— b sorryAll goals completed! 🐙

Proposition 4.1.8 (No zero divisors) / Exercise 4.1.5

theorem declaration uses 'sorry'Int.mul_eq_zero {a b:Int} (h: a * b = 0) : a = 0 ∨ b = 0 := bya:Intb:Inth:a * b = 0⊢ a = 0 ∨ b = 0 sorryAll goals completed! 🐙

Corollary 4.1.9 (Cancellation law) / Exercise 4.1.6

theorem declaration uses 'sorry'Int.mul_right_cancel₀ (a b c:Int) (h: a*c = b*c) (hc: c ≠ 0) : a = b := bya:Intb:Intc:Inth:a * c = b * chc:c ≠ 0⊢ a = b sorryAll goals completed! 🐙

Definition 4.1.10 (Ordering of the integers)

instance Int.instLE : LE Int where
  le n m := ∃ a:ℕ, m = n + a

Definition 4.1.10 (Ordering of the integers)

instance Int.instLT : LT Int where
  lt n m := n ≤ m ∧ n ≠ m

theorem Int.le_iff (a b:Int) : a ≤ b ↔ ∃ t:ℕ, b = a + t := bya:Intb:Int⊢ a ≤ b ↔ ∃ t, b = a + ↑t rflAll goals completed! 🐙

theorem Int.lt_iff (a b:Int): a < b ↔ (∃ t:ℕ, b = a + t) ∧ a ≠ b := bya:Intb:Int⊢ a < b ↔ (∃ t, b = a + ↑t) ∧ a ≠ b rflAll goals completed! 🐙

Lemma 4.1.11(a) (Properties of order) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.lt_iff_exists_positive_difference (a b:Int) : a < b ↔ ∃ n:ℕ, n ≠ 0 ∧ b = a + n := bya:Intb:Int⊢ a < b ↔ ∃ n, n ≠ 0 ∧ b = a + ↑n sorryAll goals completed! 🐙

Lemma 4.1.11(b) (Addition preserves order) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.add_lt_add_right {a b:Int} (c:Int) (h: a < b) : a+c < b+c := bya:Intb:Intc:Inth:a < b⊢ a + c < b + c sorryAll goals completed! 🐙

Lemma 4.1.11(c) (Positive multiplication preserves order) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.mul_lt_mul_of_pos_right {a b c:Int} (hab : a < b) (hc: 0 < c) : a*c < b*c := bya:Intb:Intc:Inthab:a < bhc:0 < c⊢ a * c < b * c sorryAll goals completed! 🐙

Lemma 4.1.11(d) (Negation reverses order) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.neg_gt_neg {a b:Int} (h: b < a) : -a < -b := bya:Intb:Inth:b < a⊢ -a < -b sorryAll goals completed! 🐙

Lemma 4.1.11(d) (Negation reverses order) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.neg_ge_neg {a b:Int} (h: b ≤ a) : -a ≤ -b := bya:Intb:Inth:b ≤ a⊢ -a ≤ -b sorryAll goals completed! 🐙

Lemma 4.1.11(e) (Order is transitive) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.lt_trans {a b c:Int} (hab: a < b) (hbc: b < c) : a < c := bya:Intb:Intc:Inthab:a < bhbc:b < c⊢ a < c sorryAll goals completed! 🐙

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.trichotomous' (a b:Int) : a > b ∨ a < b ∨ a = b := bya:Intb:Int⊢ a > b ∨ a < b ∨ a = b sorryAll goals completed! 🐙

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.not_gt_and_lt (a b:Int) : ¬ (a > b ∧ a < b):= bya:Intb:Int⊢ ¬(a > b ∧ a < b) sorryAll goals completed! 🐙

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.not_gt_and_eq (a b:Int) : ¬ (a > b ∧ a = b):= bya:Intb:Int⊢ ¬(a > b ∧ a = b) sorryAll goals completed! 🐙

Lemma 4.1.11(f) (Order trichotomy) / Exercise 4.1.7

theorem declaration uses 'sorry'Int.not_lt_and_eq (a b:Int) : ¬ (a < b ∧ a = b):= bya:Intb:Int⊢ ¬(a < b ∧ a = b) sorryAll goals completed! 🐙

(Not from textbook) Establish the decidability of this order.

instance declaration uses 'sorry'declaration uses 'sorry'Int.decidableRel : DecidableRel (·≤ ·: Int → Int → Prop) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2
  intro n mn:Intm:Int⊢ Decidable ((fun x1 x2 => x1 ≤ x2) n m)
  have : ∀ (n:PreInt) (m: PreInt),
      Decidable (Quotient.mk PreInt.instSetoid n ≤ Quotient.mk PreInt.instSetoid m) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2
    intro ⟨ a,b ⟩ ⟨ c,d ⟩n:Intm:Inta:ℕb:ℕc:ℕd:ℕ⊢ Decidable (⟦{ minuend := a, subtrahend := b }⟧ ≤ ⟦{ minuend := c, subtrahend := d }⟧)
    change Decidable (a —— b ≤ c —— d)n:Intm:Inta:ℕb:ℕc:ℕd:ℕ⊢ Decidable (a —— b ≤ c —— d)
    cases (a + d).decLe (b + c) with
      | isTrue h =>isTruen:Intm:Inta:ℕb:ℕc:ℕd:ℕh:a + d ≤ b + c⊢ Decidable (a —— b ≤ c —— d)
        apply isTrueisTrue.hn:Intm:Inta:ℕb:ℕc:ℕd:ℕh:a + d ≤ b + c⊢ a —— b ≤ c —— d
        sorryAll goals completed! 🐙
      | isFalse h =>isFalsen:Intm:Inta:ℕb:ℕc:ℕd:ℕh:¬a + d ≤ b + c⊢ Decidable (a —— b ≤ c —— d)
        apply isFalseisFalse.hn:Intm:Inta:ℕb:ℕc:ℕd:ℕh:¬a + d ≤ b + c⊢ ¬a —— b ≤ c —— d
        sorryAll goals completed! 🐙
  exact Quotient.recOnSubsingleton₂ n m thisAll goals completed! 🐙

(Not from textbook) 0 is the only additive identity

lemma declaration uses 'sorry'Int.is_additive_identity_iff_eq_0 (b : Int) : (∀ a, a = a + b) ↔ b = 0 := byb:Int⊢ (∀ (a : Int), a = a + b) ↔ b = 0 sorryAll goals completed! 🐙

(Not from textbook) Int has the structure of a linear ordering.

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instLinearOrder : LinearOrder Int where
  le_refl := sorry
  le_trans := sorry
  lt_iff_le_not_ge := sorry
  le_antisymm := sorry
  le_total := sorry
  toDecidableLE := decidableRel

Exercise 4.1.3

theorem declaration uses 'sorry'Int.neg_one_mul (a:Int) : -1 * a = -a := bya:Int⊢ -1 * a = -a sorryAll goals completed! 🐙

Exercise 4.1.8

theorem declaration uses 'sorry'Int.no_induction : ∃ P: Int → Prop, (P 0 ∧ ∀ n, P n → P (n+1)) ∧ ¬ ∀ n, P n := by⊢ ∃ P, (P 0 ∧ ∀ (n : Int), P n → P (n + 1)) ∧ ¬∀ (n : Int), P n sorryAll goals completed! 🐙

A nonnegative number squared is nonnegative. This is a special case of 4.1.9 that's useful for proving the general case. -

lemma declaration uses 'sorry'Int.sq_nonneg_of_pos (n:Int) (h: 0 ≤ n) : 0 ≤ n*n := byn:Inth:0 ≤ n⊢ 0 ≤ n * n sorryAll goals completed! 🐙

Exercise 4.1.9. The square of any integer is nonnegative.

theorem declaration uses 'sorry'Int.sq_nonneg (n:Int) : 0 ≤ n*n := byn:Int⊢ 0 ≤ n * n sorryAll goals completed! 🐙

Exercise 4.1.9

theorem declaration uses 'sorry'Int.sq_nonneg' (n:Int) : ∃ (m:Nat), n*n = m := byn:Int⊢ ∃ m, n * n = ↑m sorryAll goals completed! 🐙

Not in textbook: create an equivalence between Int and ℤ. This requires some familiarity with the API for Mathlib's version of the integers.

abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.equivInt : Int ≃ ℤ where
  toFun := Quotient.lift (fun ⟨ a, b ⟩ ↦ a - b) (by⊢ ∀ (a b : PreInt),
  a ≈ b →
    (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => ↑a - ↑b)
        a =
      (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => ↑a - ↑b)
        b
    sorryAll goals completed! 🐙)
  invFun := sorry
  left_inv n := sorry
  right_inv n := sorry

Not in textbook: equivalence preserves order and ring operations

abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.equivInt_ordered_ring : Int ≃+*o ℤ where
  toEquiv := equivInt
  map_add' := by⊢ ∀ (x y : Int), equivInt.toFun (x + y) = equivInt.toFun x + equivInt.toFun y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : Int), equivInt.toFun (x * y) = equivInt.toFun x * equivInt.toFun y sorryAll goals completed! 🐙
  map_le_map_iff' := by⊢ ∀ {a b : Int}, equivInt.toFun a ≤ equivInt.toFun b ↔ a ≤ b sorryAll goals completed! 🐙

end Section_4_1