structure Section_4_1.PreInt : Type

• minuend : ℕ
• subtrahend : ℕ

@[implicit_reducible]

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 := ⋯ }

@[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, equality)

@[implicit_reducible]

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, existence of a representation)

@[implicit_reducible]

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, left argument)

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, right argument)

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, both arguments)

@[implicit_reducible]

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)

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Section_4_1.Int.instNeg : Neg Int

Definition 4.1.4 (Negation of integers) / Exercise 4.1.2

Equations

• Section_4_1.Int.instNeg = { neg := Quotient.lift (fun (x : Section_4_1.PreInt) => match x with | { minuend := a, subtrahend := b } => b —— a) ⋯ }

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 (zero is not positive).

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

Lemma 4.1.5 (zero is not negative).

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

Lemma 4.1.5 (positive and negative are disjoint).

@[implicit_reducible]

instance Section_4_1.Int.instAddGroup : AddGroup Int

Proposition 4.1.6 (laws of algebra, additive group) / Exercise 4.1.4

Equations

• Section_4_1.Int.instAddGroup = AddGroup.ofLeftAxioms ⋯ ⋯ ⋯

@[implicit_reducible]

instance Section_4_1.Int.instAddCommGroup : AddCommGroup Int

Proposition 4.1.6 (laws of algebra, additive commutative group) / Exercise 4.1.4

Equations

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

@[implicit_reducible]

instance Section_4_1.Int.instCommMonoid : CommMonoid Int

Proposition 4.1.6 (laws of algebra, commutative monoid) / Exercise 4.1.4

Equations

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

@[implicit_reducible]

instance Section_4_1.Int.instCommRing : CommRing Int

Proposition 4.1.6 (laws of algebra, commutative ring) / 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 (integers).

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

@[implicit_reducible]

instance Section_4_1.Int.instLE : LE Int

Definition 4.1.10 (Ordering of the integers, non-strict)

Equations

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

@[implicit_reducible]

instance Section_4_1.Int.instLT : LT Int

Definition 4.1.10 (Ordering of the integers, strict)

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, strict) / 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, non-strict) / 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, 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, greater vs less) / 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, greater vs equal) / 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, less vs equal) / Exercise 4.1.7

@[implicit_reducible]

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

@[implicit_reducible]

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

• Section_4_1.Int.equivInt_ordered_ring = { toEquiv := Section_4_1.Int.equivInt, map_mul' := ⋯, map_add' := ⋯, map_le_map_iff' := ⋯ }