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, as formal differences a —— b of natural numbers a b:ℕ, up to equivalence. (This is a quotient of a scaffolding type Section_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 _root_.Int (or ℤ), 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)

structure Section_4_1.PreInt : Type

• minuend : ℕ
• subtrahend : ℕ

instance Section_4_1.PreInt.instSetoid : Setoid PreInt

Definition 4.1.1

Equations

• Section_4_1.PreInt.instSetoid = { r := fun (a b : Section_4_1.PreInt) => a.minuend + b.subtrahend = b.minuend + a.subtrahend, iseqv := Section_4_1.PreInt.instSetoid._proof_1 }

@[simp]

theorem Section_4_1.PreInt.eq (a b c d : ℕ) : { minuend := a, subtrahend := b } ≈ { minuend := c, subtrahend := d } ↔ a + d = c + b

@[reducible, inline]

abbrev Section_4_1.Int : Type

Equations

• Section_4_1.Int = Quotient Section_4_1.PreInt.instSetoid

@[reducible, inline]

abbrev Section_4_1.Int.formalDiff (a b : ℕ) : Int

Equations

• a —— b = ⟦{ minuend := a, subtrahend := b }⟧

def Section_4_1.«term_——_» : Lean.TrailingParserDescr

Equations

• Section_4_1.«term_——_» = Lean.ParserDescr.trailingNode `Section_4_1.«term_——_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " —— ") (Lean.ParserDescr.cat `term 101))

theorem Section_4_1.Int.eq (a b c d : ℕ) : a —— b = c —— d ↔ a + d = c + b

Definition 4.1.1 (Integers)

instance Section_4_1.Int.decidableEq : DecidableEq Int

Decidability of equality

Equations

• One or more equations did not get rendered due to their size.

theorem Section_4_1.Int.eq_diff (n : Int) : ∃ (a : ℕ) (b : ℕ), n = a —— b

Definition 4.1.1 (Integers)

instance Section_4_1.Int.instAdd : Add Int

Lemma 4.1.3 (Addition well-defined)

Equations

• One or more equations did not get rendered due to their size.

theorem Section_4_1.Int.add_eq (a b c d : ℕ) : a —— b + c —— d = (a + c) —— (b + d)

Definition 4.1.2 (Definition of addition)

theorem Section_4_1.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)

Lemma 4.1.3 (Multiplication well-defined)

theorem Section_4_1.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')

Lemma 4.1.3 (Multiplication well-defined)

theorem Section_4_1.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')

Lemma 4.1.3 (Multiplication well-defined)

instance Section_4_1.Int.instMul : Mul Int

Equations

• One or more equations did not get rendered due to their size.

theorem Section_4_1.Int.mul_eq (a b c d : ℕ) : a —— b * c —— d = (a * c + b * d) —— (a * d + b * c)

Definition 4.1.2 (Multiplication of integers)

instance Section_4_1.Int.instOfNat {n : ℕ} : OfNat Int n

Equations

• Section_4_1.Int.instOfNat = { ofNat := n —— 0 }

instance Section_4_1.Int.instNatCast : NatCast Int

Equations

• Section_4_1.Int.instNatCast = { natCast := fun (n : ℕ) => n —— 0 }

theorem Section_4_1.Int.ofNat_eq (n : ℕ) : OfNat.ofNat n = n —— 0

theorem Section_4_1.Int.natCast_eq (n : ℕ) : ↑n = n —— 0

@[simp]

theorem Section_4_1.Int.natCast_ofNat (n : ℕ) : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Section_4_1.Int.ofNat_inj (n m : ℕ) : OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m

@[simp]

theorem Section_4_1.Int.natCast_inj (n m : ℕ) : ↑n = ↑m ↔ n = m

theorem Section_4_1.Int.cast_eq_0_iff_eq_0 (n : ℕ) : ↑n = 0 ↔ n = 0

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

instance Section_4_1.Int.instNeg : Neg Int

Definition 4.1.4 (Negation of integers) / Exercise 4.1.2

Equations

• One or more equations did not get rendered due to their size.

theorem Section_4_1.Int.neg_eq (a b : ℕ) : -a —— b = b —— a

@[reducible, inline]

abbrev Section_4_1.Int.IsPos (x : Int) : Prop

Equations

• x.IsPos = ∃ n > 0, x = ↑n

@[reducible, inline]

abbrev Section_4_1.Int.IsNeg (x : Int) : Prop

Equations

• x.IsNeg = ∃ n > 0, x = -↑n

theorem Section_4_1.Int.trichotomous (x : Int) : x = 0 ∨ x.IsPos ∨ x.IsNeg

Lemma 4.1.5 (trichotomy of integers )

theorem Section_4_1.Int.not_pos_zero (x : Int) : x = 0 ∧ x.IsPos → False

Lemma 4.1.5 (trichotomy of integers)

theorem Section_4_1.Int.not_neg_zero (x : Int) : x = 0 ∧ x.IsNeg → False

Lemma 4.1.5 (trichotomy of integers)

theorem Section_4_1.Int.not_pos_neg (x : Int) : x.IsPos ∧ x.IsNeg → False

Lemma 4.1.5 (trichotomy of integers)

instance Section_4_1.Int.instAddGroup : AddGroup Int

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

Equations

• Section_4_1.Int.instAddGroup = AddGroup.ofLeftAxioms Section_4_1.Int.instAddGroup._proof_1 Section_4_1.Int.instAddGroup._proof_2 Section_4_1.Int.instAddGroup._proof_3

instance Section_4_1.Int.instAddCommGroup : AddCommGroup Int

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

Equations

• Section_4_1.Int.instAddCommGroup = { toAddGroup := Section_4_1.Int.instAddGroup, add_comm := Section_4_1.Int.instAddCommGroup._proof_1 }

instance Section_4_1.Int.instCommMonoid : CommMonoid Int

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

Equations

• One or more equations did not get rendered due to their size.

instance Section_4_1.Int.instCommRing : CommRing Int

Proposition 4.1.6 (laws of algebra) / Exercise 4.1.4

Equations

• One or more equations did not get rendered due to their size.

theorem Section_4_1.Int.sub_eq (a b : Int) : a - b = a + -b

Definition of subtraction

theorem Section_4_1.Int.sub_eq_formal_sub (a b : ℕ) : ↑a - ↑b = a —— b

theorem Section_4_1.Int.mul_eq_zero {a b : Int} (h : a * b = 0) : a = 0 ∨ b = 0

Proposition 4.1.8 (No zero divisors) / Exercise 4.1.5

theorem Section_4_1.Int.mul_right_cancel₀ (a b c : Int) (h : a * c = b * c) (hc : c ≠ 0) : a = b

Corollary 4.1.9 (Cancellation law) / Exercise 4.1.6

instance Section_4_1.Int.instLE : LE Int

Definition 4.1.10 (Ordering of the integers)

Equations

• Section_4_1.Int.instLE = { le := fun (n m : Section_4_1.Int) => ∃ (a : ℕ), m = n + ↑a }

instance Section_4_1.Int.instLT : LT Int

Definition 4.1.10 (Ordering of the integers)

Equations

• Section_4_1.Int.instLT = { lt := fun (n m : Section_4_1.Int) => n ≤ m ∧ n ≠ m }

theorem Section_4_1.Int.le_iff (a b : Int) : a ≤ b ↔ ∃ (t : ℕ), b = a + ↑t

theorem Section_4_1.Int.lt_iff (a b : Int) : a < b ↔ (∃ (t : ℕ), b = a + ↑t) ∧ a ≠ b

theorem Section_4_1.Int.lt_iff_exists_positive_difference (a b : Int) : a < b ↔ ∃ (n : ℕ), n ≠ 0 ∧ b = a + ↑n

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

theorem Section_4_1.Int.add_lt_add_right {a b : Int} (c : Int) (h : a < b) : a + c < b + c

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

theorem Section_4_1.Int.mul_lt_mul_of_pos_right {a b c : Int} (hab : a < b) (hc : 0 < c) : a * c < b * c

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

theorem Section_4_1.Int.neg_gt_neg {a b : Int} (h : b < a) : -a < -b

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

theorem Section_4_1.Int.neg_ge_neg {a b : Int} (h : b ≤ a) : -a ≤ -b

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

theorem Section_4_1.Int.lt_trans {a b c : Int} (hab : a < b) (hbc : b < c) : a < c

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

theorem Section_4_1.Int.trichotomous' (a b : Int) : a > b ∨ a < b ∨ a = b

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

theorem Section_4_1.Int.not_gt_and_lt (a b : Int) : ¬(a > b ∧ a < b)

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

theorem Section_4_1.Int.not_gt_and_eq (a b : Int) : ¬(a > b ∧ a = b)

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

theorem Section_4_1.Int.not_lt_and_eq (a b : Int) : ¬(a < b ∧ a = b)

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

instance Section_4_1.Int.decidableRel : DecidableRel fun (x1 x2 : Int) => x1 ≤ x2

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

Equations

• One or more equations did not get rendered due to their size.

theorem Section_4_1.Int.is_additive_identity_iff_eq_0 (b : Int) : (∀ (a : Int), a = a + b) ↔ b = 0

(Not from textbook) 0 is the only additive identity

instance Section_4_1.Int.instLinearOrder : LinearOrder Int

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

Equations

• One or more equations did not get rendered due to their size.

theorem Section_4_1.Int.neg_one_mul (a : Int) : -1 * a = -a

Exercise 4.1.3

theorem Section_4_1.Int.no_induction : ∃ (P : Int → Prop), (P 0 ∧ ∀ (n : Int), P n → P (n + 1)) ∧ ¬∀ (n : Int), P n

Exercise 4.1.8

theorem Section_4_1.Int.sq_nonneg_of_pos (n : Int) (h : 0 ≤ n) : 0 ≤ n * n

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

theorem Section_4_1.Int.sq_nonneg (n : Int) : 0 ≤ n * n

Exercise 4.1.9. The square of any integer is nonnegative.

theorem Section_4_1.Int.sq_nonneg' (n : Int) : ∃ (m : ℕ), n * n = ↑m

Exercise 4.1.9

@[reducible, inline]

abbrev Section_4_1.Int.equivInt : Int ≃ ℤ

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Section_4_1.Int.equivInt_ordered_ring : Int ≃+*o ℤ

Not in textbook: equivalence preserves order and ring operations

Equations

• One or more equations did not get rendered due to their size.