ZFC Natural numbers

This file defines the natural numbers in ZF set theory. The definition is based on the construction of the Von Neumann ordinals, where each natural number is represented as the set of all smaller natural numbers.

The set of all natural numbers is defined as the smallest inductive set. Because of the axiom of separation, the definition relies on the existence of an infinite set, which is provided by the some_inf constant. It can be shown that the choice of some_inf does not affect the definition of the natural numbers and leads to isomorphic definitions.

The file also includes the definition of the ZFNat type for ZF natural numbers, and provides various properties and usual arithmetic operations on natural numbers.

Preliminary definitions

Natural numbers

noncomputable def ZFSet.Nat : ZFSet.{u_1}

The set of natural numbers Nat is defined as the smallest inductive set. This definition avoids the use of ω, even though ω may be thought of as ℕ.

Equations

• ZFSet.Nat = (ZFSet.sep ZFSet.inductive_set ZFSet.some_inf✝.powerset).sInter

@[reducible, inline]

abbrev ZFSet.ZFNat : Type (u_1 + 1)

The type of natural numbers ZFNat is defined as the subtype of Nat.

Equations

• ZFSet.ZFNat = ↥ZFSet.Nat

theorem ZFSet.ZFNat.zero_in_Nat : ∅ ∈ Nat

@[implicit_reducible]

instance ZFSet.ZFNat.nat_zero : Zero ZFNat

Equations

• ZFSet.ZFNat.nat_zero = { zero := ⟨∅, ZFSet.ZFNat.zero_in_Nat⟩ }

theorem ZFSet.ZFNat.nat_zero_eq : 0 = ⟨∅, zero_in_Nat⟩

@[implicit_reducible]

instance ZFSet.ZFNat.nat_lt : LT ZFNat

Equations

• ZFSet.ZFNat.nat_lt = { lt := fun (x y : ZFSet.ZFNat) => ↑x ∈ ↑y }

@[implicit_reducible]

instance ZFSet.ZFNat.nat_le : LE ZFNat

Equations

• ZFSet.ZFNat.nat_le = { le := fun (x y : ZFSet.ZFNat) => x < y ∨ x = y }

theorem ZFSet.ZFNat.not_lt_zero {n : ZFNat} : ¬n < 0

theorem ZFSet.ZFNat.zero_lt_ne_zero {n : ZFNat} : 0 < n → n ≠ 0

theorem ZFSet.ZFNat.zero_mem_inductive {a : ZFSet.{u_1}} (h : a.inductive_set) : ↑0 ∈ a

Any inductive set contains zero.

theorem ZFSet.ZFNat.insert_mem_inductive {a n : ZFSet.{u_1}} (h : a.inductive_set) (h' : n ∈ a) : insert n n ∈ a

Any inductive set containing an element also contains its successor.

theorem ZFSet.ZFNat.succ_mem_Nat' {n : ZFSet.{u_1}} (h : n ∈ Nat) : insert n n ∈ Nat

theorem ZFSet.ZFNat.Nat_subset_of_inductive {a : ZFSet.{u_1}} (h : a.inductive_set) : Nat ⊆ a

Nat is the least inductive set: it is contained in every inductive set, with no restriction to subsets of some_inf.

This is the unrestricted form of inductive_subset_some_inf_contains_Nat; the extra hypothesis a ⊆ some_inf is eliminated by intersecting a with some_inf first.

theorem ZFSet.ZFNat.Nat_eq_of_inductive {T : ZFSet.{u_1}} (hT : T.inductive_set) : Nat = (ZFSet.sep inductive_set T.powerset).sInter

The definition of Nat is independent of the witness granted by the axiom of infinity: intersecting the inductive subsets of any inductive set T yields the same set Nat.

In particular Nat = ⋂₀ ((powerset ω).sep inductive_set), so seeding the construction with some_inf rather than ω is a choice without observable consequence.

def ZFSet.ZFNat.succ (n : ZFNat) : ZFNat

The successor function succ is build from the insertion of a set into itself embedded into the ZFNat type.

Equations

• ZFSet.ZFNat.succ ⟨n_2, h⟩ = ⟨insert n_2 n_2, ⋯⟩

@[implicit_reducible]

instance ZFSet.ZFNat.nat_one : One ZFNat

Equations

• ZFSet.ZFNat.nat_one = { one := ZFSet.ZFNat.succ 0 }

theorem ZFSet.ZFNat.nat_one_eq : 1 = succ 0

theorem ZFSet.ZFNat.succ_ne_zero (n : ZFNat) : n.succ ≠ 0

theorem ZFSet.ZFNat.succ_inj_aux {m n a : ZFSet.{u_1}} (h : insert m m = insert n n) (h' : a ∈ m) : a ∈ n

theorem ZFSet.ZFNat.succ_inj_aux' {m n : ZFSet.{u_1}} (h : insert m m = insert n n) : m = n

theorem ZFSet.ZFNat.succ_inj {m n : ZFNat} (h : m.succ = n.succ) : m = n

theorem ZFSet.ZFNat.sep_of_ind_is_ind (P : ZFSet.{u_1} → Prop) {a : ZFSet.{u_1}} (h : a.inductive_set) (h₀ : P ∅) (ih : ∀ n ∈ a, P n → P (insert n n)) : (ZFSet.sep P a).inductive_set

Any inductive set a separated by an inductive predicate P is inductive.

Recursion on natural numbers

theorem ZFSet.ZFNat.succ_subrelation_mem' : Subrelation (fun (x y : ZFSet.{u_1}) => insert x x = y) fun (x y : ZFSet.{u_1}) => x ∈ y

theorem ZFSet.ZFNat.succ_wf' : WellFounded fun (x y : ZFSet.{u_1}) => insert x x = y

theorem ZFSet.ZFNat.mem_wf' : WellFounded fun (x1 x2 : ZFNat) => ↑x1 ∈ ↑x2

theorem ZFSet.ZFNat.succ_subrelation_mem : Subrelation (fun (x1 x2 : ZFNat) => x1.succ = x2) fun (x1 x2 : ZFNat) => ↑x1 ∈ ↑x2

The relation built over the successor function is a subrelation of the membership relation.

theorem ZFSet.ZFNat.succ_wf : WellFounded fun (x1 x2 : ZFNat) => x1.succ = x2

theorem ZFSet.ZFNat.ind {P : ZFSet.{u_1} → Prop} (n : ZFSet.{u_1}) (h : n ∈ Nat) (zero : P ∅) (succ : ∀ n ∈ Nat, P n → P (insert n n)) : P n

The induction principle for sets in Nat. This principle is meant to be used for definitional purposes only.

theorem ZFSet.ZFNat.induction {P : ZFNat → Prop} (n : ZFNat) (zero : P 0) (succ : ∀ (n : ZFNat), P n → P n.succ) : P n

The (weak) induction principle for natural numbers.

theorem ZFSet.ZFNat.cases {P : ZFNat → Prop} (n : ZFNat) (zero : P 0) (succ : ∀ (n : ZFNat), P n.succ) : P n

theorem ZFSet.ZFNat.every_nat_transitive {n : ZFSet.{u_1}} (h : n ∈ Nat) : n.transitive

theorem ZFSet.ZFNat.lt_succ {n : ZFNat} : n < n.succ

theorem ZFSet.ZFNat.le_succ {n : ZFNat} : n ≤ n.succ

theorem ZFSet.ZFNat.lt_trans {x y z : ZFNat} : x < y → y < z → x < z

theorem ZFSet.ZFNat.lt_irrefl {n : ZFNat} : ¬n < n

theorem ZFSet.ZFNat.lt_imp_ne {n m : ZFNat} : n < m → n ≠ m

theorem ZFSet.ZFNat.le_trans {x y z : ZFNat} : x ≤ y → y ≤ z → x ≤ z

theorem ZFSet.ZFNat.le_antisymm {x y : ZFNat} : x ≤ y → y ≤ x → x = y

theorem ZFSet.ZFNat.lt_le_iff {n m : ZFNat} : n ≤ m ↔ n < m.succ

theorem ZFSet.ZFNat.lt_mono {x y : ZFNat} : x < y → x.succ < y.succ

theorem ZFSet.ZFNat.succ_lt_mono {x y : ZFNat} : x.succ < y.succ → x < y

theorem ZFSet.ZFNat.le_mono {x y : ZFNat} : x ≤ y → x.succ ≤ y.succ

theorem ZFSet.ZFNat.succ_le_mono {x y : ZFNat} : x.succ ≤ y.succ → x ≤ y

theorem ZFSet.ZFNat.le_lt_iff {n m : ZFNat} : n.succ ≤ m ↔ n < m

theorem ZFSet.ZFNat.le_total {x y : ZFNat} : x ≤ y ∨ y ≤ x

theorem ZFSet.ZFNat.lt_iff_le_not_ge {x y : ZFNat} : x < y ↔ x ≤ y ∧ ¬y ≤ x

theorem ZFSet.ZFNat.strong_induction {P : ZFNat → Prop} (n : ZFNat) (ind : ∀ (n : ZFNat), (∀ m < n, P m) → P n) : P n

The (strong) induction principle for natural numbers.

theorem ZFSet.ZFNat.mem_Nat_of_mem_mem_Nat {n m : ZFSet.{u_1}} (hn : n ∈ Nat) : m ∈ n → m ∈ Nat

theorem ZFSet.ZFNat.not_zero_imp_succ {n : ZFNat} : n ≠ 0 → ∃ (m : ZFNat), n = m.succ

theorem ZFSet.ZFNat.sUnion_insert_nat {x : ZFSet.{u_1}} (h : x ∈ Nat) : (insert x x).sUnion = x

theorem ZFSet.ZFNat.pred_in_Nat' ⦃x : ZFSet.{u_1}⦄ (h : x ∈ Nat) : x.sUnion ∈ Nat

def ZFSet.ZFNat.pred (x : ZFNat) : ZFNat

The predecessor function on natural numbers, defined directly as the union of a set.

Equations

• x.pred = Subtype.map ZFSet.sUnion ZFSet.ZFNat.pred_in_Nat' x

theorem ZFSet.ZFNat.pred_eq (n : ZFNat) : n.pred = ⟨(↑n).sUnion, ⋯⟩

@[simp]

theorem ZFSet.ZFNat.pred_zero : pred 0 = 0

@[simp]

theorem ZFSet.ZFNat.pred_one : pred 1 = 0

@[simp]

theorem ZFSet.ZFNat.pred_succ {n : ZFNat} : n.succ.pred = n

@[simp]

theorem ZFSet.ZFNat.succ_pred {n : ZFNat} (h : n ≠ 0) : n.pred.succ = n

noncomputable def ZFSet.ZFNat.rec' {motive : ZFSet.{u_1} → Sort u} (n : ZFSet.{u_1}) (h : n ∈ Nat) (zero : motive ∅) (succ : (x : ZFSet.{u_1}) → x ∈ Nat → motive x → motive (insert x x)) : motive n

The recursion principle for sets in Nat. This principle is meant to be used for definitional purposes only.

Equations

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

theorem ZFSet.ZFNat.rec'_zero {motive : ZFSet.{u_1} → Sort u} (zero : motive ∅) (succ : (x : ZFSet.{u_1}) → x ∈ Nat → motive x → motive (insert x x)) : rec' ∅ zero_in_Nat zero succ = zero

Provides the base case of the recursion principle for sets in Nat.

theorem ZFSet.ZFNat.rec'_succ {motive : ZFSet.{u_1} → Sort u} (n : ZFSet.{u_1}) (n_Nat : n ∈ Nat) (zero : motive ∅) (succ : (x : ZFSet.{u_1}) → x ∈ Nat → motive x → motive (insert x x)) : rec' (insert n n) ⋯ zero succ = succ n n_Nat (rec' n n_Nat zero succ)

Provides the inductive step of the recursion principle for sets in Nat.

noncomputable def ZFSet.ZFNat.rec {motive : ZFNat → Sort u} (n : ZFNat) (zero : motive 0) (succ : (x : ZFNat) → motive x → motive x.succ) : motive n

The recursion principle for natural numbers. This recursor allows inductive definitions over natural numbers to be defined in a more natural way.

Equations

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

@[simp]

theorem ZFSet.ZFNat.induction_is_rec_into_Prop {motive : ZFNat → Prop} : ⋯ = ⋯

The induction principle of ZFNat is a universe-specialized version of the recursion principle.

theorem ZFSet.ZFNat.rec_zero {motive : ZFNat → Sort u} (zero : motive 0) (succ : (x : ZFNat) → motive x → motive x.succ) : rec 0 zero succ = zero

theorem ZFSet.ZFNat.rec_succ {motive : ZFNat → Sort u} (n : ZFNat) (zero : motive 0) (succ' : (x : ZFNat) → motive x → motive x.succ) : rec n.succ zero succ' = succ' n (rec n zero succ')

theorem ZFSet.ZFNat.rec_unique {motive : ZFNat → Sort u} (zero : motive 0) (succ' : (x : ZFNat) → motive x → motive x.succ) (f : (x : ZFNat) → motive x) (h₀ : f 0 = zero) (hs : ∀ (x : ZFNat), f x.succ = succ' x (f x)) (n : ZFNat) : f n = rec n zero succ'

Uniqueness half of the universal property of ZFNat: ZFNat.rec is the only family satisfying the two computation rules rec_zero and rec_succ.

Together with rec_zero/rec_succ this says that (ZFNat, 0, succ) is initial among sets equipped with a point and an endomorphism.

@[reducible, inline]

noncomputable abbrev ZFSet.ZFNat.pred' (m : ZFNat) : ZFNat

The predecessor function pred' on natural numbers, defined inductively. This definition is equivalent to pred, as proven by pred'_eq_pred.

Equations

• m.pred' = ZFSet.ZFNat.rec m 0 fun (x x_1 : ZFSet.ZFNat) => x

theorem ZFSet.ZFNat.pred'_eq_pred : pred = ZFNat.pred'

The definitions of pred and pred' are equivalent.

Arithmetic

theorem ZFSet.ZFNat.zero_lt_succ {n : ZFNat} : 0 < n.succ

theorem ZFSet.ZFNat.pos_of_ne_zero {n : ZFNat} : 0 ≠ n → 0 < n

@[implicit_reducible]

instance ZFSet.ZFNat.instPreorder : Preorder ZFNat

Equations

• ZFSet.ZFNat.instPreorder = { toLE := ZFSet.ZFNat.nat_le, toLT := ZFSet.ZFNat.nat_lt, le_refl := ZFSet.ZFNat.instPreorder._proof_1, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[implicit_reducible]

noncomputable instance ZFSet.ZFNat.instLinearOrder : LinearOrder ZFNat

Equations

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

instance ZFSet.ZFNat.instIsStrictTotalOrderLt : IsStrictTotalOrder ZFNat fun (x1 x2 : ZFNat) => x1 < x2

@[reducible, inline]

noncomputable abbrev ZFSet.ZFNat.add (n : ZFNat) (m : ZFNat) : ZFNat

The addition function on natural numbers, defined inductively.

Equations

• n.add m = ZFSet.ZFNat.rec n m fun (x : ZFSet.ZFNat) => ZFSet.ZFNat.succ

@[implicit_reducible]

noncomputable instance ZFSet.ZFNat.add_inst : Add ZFNat

Equations

• ZFSet.ZFNat.add_inst = { add := ZFSet.ZFNat.add }

theorem ZFSet.ZFNat.add_inst_eq {n m : ZFNat} : n + m = n.add m

theorem ZFSet.ZFNat.add_one_eq_succ {n : ZFNat} : n + 1 = n.succ

theorem ZFSet.ZFNat.add_one_eq_succ' {n : ZFNat} : 1 + n = n.succ

@[simp]

theorem ZFSet.ZFNat.add_zero {n : ZFNat} : n + 0 = n

@[simp]

theorem ZFSet.ZFNat.zero_add {n : ZFNat} : 0 + n = n

theorem ZFSet.ZFNat.add_succ {n m : ZFNat} : n.succ + m = (n + m).succ

theorem ZFSet.ZFNat.succ_add {n m : ZFNat} : (n + m).succ = n + m.succ

theorem ZFSet.ZFNat.add_comm (n m : ZFNat) : n + m = m + n

@[simp]

theorem ZFSet.ZFNat.add_assoc (n m k : ZFNat) : n + (m + k) = n + m + k

theorem ZFSet.ZFNat.add_left_comm (n m k : ZFNat) : n + (m + k) = m + (n + k)

theorem ZFSet.ZFNat.add_right_comm (n m k : ZFNat) : n + m + k = n + k + m

theorem ZFSet.ZFNat.add_left_cancel {n m k : ZFNat} : n + m = n + k ↔ m = k

theorem ZFSet.ZFNat.add_right_cancel {n m k : ZFNat} : n + m = k + m ↔ n = k

theorem ZFSet.ZFNat.eq_zero_of_add_eq_zero {n m : ZFNat} : n + m = 0 → n = 0 ∧ m = 0

theorem ZFSet.ZFNat.eq_zero_of_add_eq_zero_left {n m : ZFNat} (h : n + m = 0) : m = 0

@[simp]

theorem ZFSet.ZFNat.add_left_eq_self {a b : ZFNat} : a + b = b ↔ a = 0

@[simp]

theorem ZFSet.ZFNat.add_right_eq_self {a b : ZFNat} : a + b = a ↔ b = 0

@[simp]

theorem ZFSet.ZFNat.self_eq_add_right {a b : ZFNat} : a = a + b ↔ b = 0

@[simp]

theorem ZFSet.ZFNat.self_eq_add_left {a b : ZFNat} : a = b + a ↔ b = 0

theorem ZFSet.ZFNat.lt_of_succ_le {n m : ZFNat} (h : n.succ ≤ m) : n < m

theorem ZFSet.ZFNat.succ_le_of_lt {n m : ZFNat} (h : n < m) : n.succ ≤ m

theorem ZFSet.ZFNat.le.dest {n m : ZFNat} : n ≤ m → ∃ (k : ZFNat), n + k = m

theorem ZFSet.ZFNat.le_succ_of_le {n m : ZFNat} (h : n ≤ m) : n ≤ m.succ

@[simp]

theorem ZFSet.ZFNat.le_add_right (n k : ZFNat) : n ≤ n + k

@[simp]

theorem ZFSet.ZFNat.le_add_left (n m : ZFNat) : n ≤ m + n

theorem ZFSet.ZFNat.le.intro {n m k : ZFNat} (h : n + k = m) : n ≤ m

theorem ZFSet.ZFNat.zero_le {n : ZFNat} : 0 ≤ n

theorem ZFSet.ZFNat.le_of_add_le_add_left {a b c : ZFNat} (h : a + b ≤ a + c) : b ≤ c

theorem ZFSet.ZFNat.add_le_add_left {n m : ZFNat} (h : n ≤ m) (k : ZFNat) : k + n ≤ k + m

@[simp]

theorem ZFSet.ZFNat.add_le_add_iff_left {n m k : ZFNat} : n + m ≤ n + k ↔ m ≤ k

theorem ZFSet.ZFNat.lt_of_add_lt_add_right {n m k : ZFNat} : k + n < m + n → k < m

theorem ZFSet.ZFNat.add_lt_add_left {n m : ZFNat} (h : n < m) (k : ZFNat) : k + n < k + m

theorem ZFSet.ZFNat.add_lt_add_right {n m : ZFNat} (h : n < m) (k : ZFNat) : n + k < m + k

theorem ZFSet.ZFNat.lt_add_of_pos_right {n k : ZFNat} (h : 0 < k) : n < n + k

theorem ZFSet.ZFNat.lt_of_add_lt_add_left {n m k : ZFNat} : n + k < n + m → k < m

@[simp]

theorem ZFSet.ZFNat.add_lt_add_iff_left {k n m : ZFNat} : k + n < k + m ↔ n < m

@[simp]

theorem ZFSet.ZFNat.add_lt_add_iff_right {k n m : ZFNat} : n + k < m + k ↔ n < m

theorem ZFSet.ZFNat.add_le_add_right {n m : ZFNat} (h : n ≤ m) (k : ZFNat) : n + k ≤ m + k

theorem ZFSet.ZFNat.add_lt_add_of_le_of_lt {a b c d : ZFNat} (hle : a ≤ b) (hlt : c < d) : a + c < b + d

theorem ZFSet.ZFNat.add_lt_add_of_lt_of_le {a b c d : ZFNat} (hlt : a < b) (hle : c ≤ d) : a + c < b + d

theorem ZFSet.ZFNat.lt_add_of_pos_left {k n : ZFNat} : 0 < k → n < k + n

theorem ZFSet.ZFNat.pos_of_lt_add_right {n k : ZFNat} (h : n < n + k) : 0 < k

theorem ZFSet.ZFNat.pos_of_lt_add_left {n k : ZFNat} : n < k + n → 0 < k

@[simp]

theorem ZFSet.ZFNat.lt_add_right_iff_pos {n k : ZFNat} : n < n + k ↔ 0 < k

@[simp]

theorem ZFSet.ZFNat.lt_add_left_iff_pos {n k : ZFNat} : n < k + n ↔ 0 < k

theorem ZFSet.ZFNat.add_pos_left {m : ZFNat} (h : 0 < m) (n : ZFNat) : 0 < m + n

theorem ZFSet.ZFNat.add_pos_right {n : ZFNat} (m : ZFNat) (h : 0 < n) : 0 < m + n

theorem ZFSet.ZFNat.pred_le_pred {n m : ZFNat} : n ≤ m → n.pred ≤ m.pred

theorem ZFSet.ZFNat.le_of_succ_le_succ {n m : ZFNat} : n.succ ≤ m.succ → n ≤ m

theorem ZFSet.ZFNat.lt_of_succ_lt_succ {n m : ZFNat} : n.succ < m.succ → n < m

theorem ZFSet.ZFNat.add_self_ne_one {n : ZFNat} : n + n ≠ 1

@[reducible, inline]

noncomputable abbrev ZFSet.ZFNat.sub (n : ZFNat) (m : ZFNat) : ZFNat

Equations

• n.sub m = ZFSet.ZFNat.rec m n fun (x : ZFSet.ZFNat) => ZFSet.ZFNat.pred

@[implicit_reducible]

noncomputable instance ZFSet.ZFNat.sub_inst : Sub ZFNat

Equations

• ZFSet.ZFNat.sub_inst = { sub := ZFSet.ZFNat.sub }

theorem ZFSet.ZFNat.sub_inst_eq {n m : ZFNat} : n - m = n.sub m

@[simp]

theorem ZFSet.ZFNat.sub_zero {n : ZFNat} : n - 0 = n

theorem ZFSet.ZFNat.sub_one_eq_pred {n : ZFNat} : n - 1 = n.pred

theorem ZFSet.ZFNat.succ_mono {n m : ZFNat} : n < m ↔ n.succ < m.succ

theorem ZFSet.ZFNat.sub_succ (n m : ZFNat) : n - m.succ = (n - m).pred

@[simp]

theorem ZFSet.ZFNat.zero_sub {n : ZFNat} : 0 - n = 0

theorem ZFSet.ZFNat.succ_sub_succ (n m : ZFNat) : n.succ - m.succ = n - m

theorem ZFSet.ZFNat.succ_sub_self (n : ZFNat) : n.succ - n = 1

theorem ZFSet.ZFNat.sub_self {n : ZFNat} : n - n = 0

theorem ZFSet.ZFNat.sub_add_distrib {n m k : ZFNat} : n - (m + k) = n - m - k

theorem ZFSet.ZFNat.sub_ne_zero_of_lt {a b : ZFNat} : a < b → b - a ≠ 0

theorem ZFSet.ZFNat.le_of_succ_le {n m : ZFNat} : n.succ ≤ m → n ≤ m

theorem ZFSet.ZFNat.lt_of_succ_lt {n m : ZFNat} (h : n.succ < m) : n < m

theorem ZFSet.ZFNat.le_of_lt {n m : ZFNat} : n < m → n ≤ m

theorem ZFSet.ZFNat.add_sub_of_le {a b : ZFNat} (h : a ≤ b) : a + (b - a) = b

theorem ZFSet.ZFNat.sub_one_cancel {a b : ZFNat} : 0 < a → 0 < b → a - 1 = b - 1 → a = b

@[simp]

theorem ZFSet.ZFNat.sub_add_cancel {n m : ZFNat} (h : m ≤ n) : n - m + m = n

theorem ZFSet.ZFNat.add_sub_add_right (n k m : ZFNat) : n + k - (m + k) = n - m

theorem ZFSet.ZFNat.add_sub_add_left (k n m : ZFNat) : k + n - (k + m) = n - m

@[simp]

theorem ZFSet.ZFNat.add_sub_cancel (n m : ZFNat) : n + m - m = n

theorem ZFSet.ZFNat.add_sub_cancel_left (n m : ZFNat) : n + m - n = m

theorem ZFSet.ZFNat.add_sub_assoc {m k : ZFNat} (h : k ≤ m) (n : ZFNat) : n + m - k = n + (m - k)

theorem ZFSet.ZFNat.eq_add_of_sub_eq {a b c : ZFNat} (hle : b ≤ a) (h : a - b = c) : a = c + b

theorem ZFSet.ZFNat.sub_eq_of_eq_add {a b c : ZFNat} (h : a = c + b) : a - b = c

theorem ZFSet.ZFNat.add_eq_add_sub_eq_sub {a b c d : ZFNat} : a + b = c + d → a - c = d - b

theorem ZFSet.ZFNat.sub_factor {m k n : ZFNat} : k ≤ m → m ≤ n → n - m + k = n - (m - k)

theorem ZFSet.ZFNat.sub_add_comm {m n k : ZFNat} (h : m ≤ n) : n - m + k = n + k - m

theorem ZFSet.ZFNat.succ_le_succ {n m : ZFNat} : n ≤ m → n.succ ≤ m.succ

theorem ZFSet.ZFNat.succ_le_succ_iff {a b : ZFNat} : a.succ ≤ b.succ ↔ a ≤ b

theorem ZFSet.ZFNat.le_zero_imp_eq {n : ZFNat} : n ≤ 0 → n = 0

@[reducible, inline]

noncomputable abbrev ZFSet.ZFNat.mul (n : ZFNat) (m : ZFNat) : ZFNat

The multiplication function on natural numbers, defined inductively.

Equations

• n.mul m = ZFSet.ZFNat.rec n 0 fun (x : ZFSet.ZFNat) (x_1 : ZFSet.ZFNat) => x_1 + m

@[implicit_reducible]

noncomputable instance ZFSet.ZFNat.mul_inst : Mul ZFNat

Equations

• ZFSet.ZFNat.mul_inst = { mul := ZFSet.ZFNat.mul }

theorem ZFSet.ZFNat.mul_inst_eq {n m : ZFNat} : n * m = n.mul m

@[simp]

theorem ZFSet.ZFNat.mul_zero {n : ZFNat} : n * 0 = 0

@[simp]

theorem ZFSet.ZFNat.zero_mul {n : ZFNat} : 0 * n = 0

@[simp]

theorem ZFSet.ZFNat.mul_one {n : ZFNat} : n * 1 = n

@[simp]

theorem ZFSet.ZFNat.one_mul {n : ZFNat} : 1 * n = n

theorem ZFSet.ZFNat.mul_succ {n m : ZFNat} : (n + 1) * m = n * m + m

theorem ZFSet.ZFNat.succ_mul {n m : ZFNat} : n.succ * m = n * m + m

theorem ZFSet.ZFNat.left_distrib {n m k : ZFNat} : n * (m + k) = n * m + n * k

theorem ZFSet.ZFNat.mul_comm (n m : ZFNat) : n * m = m * n

theorem ZFSet.ZFNat.succ_mul' {n m : ZFNat} : m * n.succ = m * n + m

theorem ZFSet.ZFNat.right_distrib {n m k : ZFNat} : (n + m) * k = n * k + m * k

theorem ZFSet.ZFNat.mul_assoc (n m k : ZFNat) : n * m * k = n * (m * k)

theorem ZFSet.ZFNat.mul_left_comm (n m k : ZFNat) : n * (m * k) = m * (n * k)

theorem ZFSet.ZFNat.two_mul (n : ZFNat) : (1 + 1) * n = n + n

theorem ZFSet.ZFNat.mul_two (n : ZFNat) : n * (1 + 1) = n + n

theorem ZFSet.ZFNat.sub_lt_eq_zero {n m : ZFNat} (h : n ≤ m) : n - m = 0

theorem ZFSet.ZFNat.add_lt_trans {n m p q : ZFNat} : n < m → p < q → n + p < m + q

theorem ZFSet.ZFNat.pos_mul_pos {k n : ZFNat} (h : 0 < k) : 0 < k * n → 0 < n

theorem ZFSet.ZFNat.mul_lt_mono {n m k : ZFNat} (h : 0 < k) : n < m → k * n < k * m

theorem ZFSet.ZFNat.mul_le_mono {k m n : ZFNat} : n ≤ m → k * n ≤ k * m

theorem ZFSet.ZFNat.mul_lt_cancel {k m n : ZFNat} : k * n < k * m → n < m

theorem ZFSet.ZFNat.lt_mul_iff {n m k : ZFNat} : n < m ↔ (k + 1) * n < (k + 1) * m

theorem ZFSet.ZFNat.left_distrib_mul_sub_one {n m : ZFNat} : n * (m - 1) = n * m - n

theorem ZFSet.ZFNat.left_distrib_mul_sub_aux {n m k : ZFNat} (h : k < m) : n * (m - k) = n * m - n * k

theorem ZFSet.ZFNat.sub_eq_zero_imp_le {a b : ZFNat} : a - b = 0 ↔ a ≤ b

theorem ZFSet.ZFNat.sub_eq_zero_mul {n a b : ZFNat} : a - b = 0 → n * a - n * b = 0

theorem ZFSet.ZFNat.left_distrib_mul_sub {n m k : ZFNat} : n * (m - k) = n * m - n * k

theorem ZFSet.ZFNat.right_distrib_mul_sub {n m k : ZFNat} : (m - k) * n = m * n - k * n

theorem ZFSet.ZFNat.add_eq_zero_iff {n m : ZFNat} : n + m = 0 ↔ n = 0 ∧ m = 0

theorem ZFSet.ZFNat.mul_eq_zero_iff {n m : ZFNat} : n * m = 0 ↔ n = 0 ∨ m = 0

theorem ZFSet.ZFNat.eq_le_le_iff {n m : ZFNat} : n = m ↔ n ≤ m ∧ m ≤ n

theorem ZFSet.ZFNat.mul_left_cancel_iff {n m k : ZFNat} (k_pos : k ≠ 0) : k * m = k * n ↔ m = n

theorem ZFSet.ZFNat.mul_right_cancel_iff {n m k : ZFNat} (k_pos : k ≠ 0) : m * k = n * k ↔ m = n

@[reducible, inline]

noncomputable abbrev ZFSet.ZFNat.pow (n : ZFNat) (p : ZFNat) : ZFNat

The power function on natural numbers, defined inductively.

Equations

• n.pow p = ZFSet.ZFNat.rec p 1 fun (x : ZFSet.ZFNat) (x_1 : ZFSet.ZFNat) => x_1 * n

@[implicit_reducible]

noncomputable instance ZFSet.ZFNat.pow_inst : HomogeneousPow ZFNat

Equations

• ZFSet.ZFNat.pow_inst = { pow := ZFSet.ZFNat.pow }

theorem ZFSet.ZFNat.pow_inst_eq {n p : ZFNat} : n ^ p = n.pow p

theorem ZFSet.ZFNat.pow_zero {n : ZFNat} : n ^ 0 = 1

theorem ZFSet.ZFNat.pow_one {n : ZFNat} : n ^ 1 = n

theorem ZFSet.ZFNat.pow_succ {n p : ZFNat} : n ^ p.succ = n ^ p * n

theorem ZFSet.ZFNat.induction' {P : ZFNat → Prop} (n : ZFNat) (zero : P 0) (succ : ∀ (n : ZFNat), P n → P (n + 1)) : P n

Induction principle for ZFNat, using natural notations.

Declared as an induction eliminator.

@[reducible, inline]

abbrev ZFSet.ZFNat.nsmul : ℕ → ZFNat → ZFNat

Equations

• ZFSet.ZFNat.nsmul 0 x✝ = 0
• ZFSet.ZFNat.nsmul n.succ x✝ = x✝ + ZFSet.ZFNat.nsmul n x✝

@[implicit_reducible]

noncomputable instance ZFSet.ZFNat.instSemiring : Semiring ZFNat

Equations

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

@[implicit_reducible]

noncomputable instance ZFSet.ZFNat.instCommSemiring : CommSemiring ZFNat

Equations

• ZFSet.ZFNat.instCommSemiring = { toSemiring := ZFSet.ZFNat.instSemiring, mul_comm := ZFSet.ZFNat.mul_comm }

instance ZFSet.ZFNat.instAssociativeHAdd : Std.Associative fun (x1 x2 : ZFNat) => x1 + x2

instance ZFSet.ZFNat.instCommutativeHAdd : Std.Commutative fun (x1 x2 : ZFNat) => x1 + x2

instance ZFSet.ZFNat.instAssociativeHMul : Std.Associative fun (x1 x2 : ZFNat) => x1 * x2

instance ZFSet.ZFNat.instCommutativeHMul : Std.Commutative fun (x1 x2 : ZFNat) => x1 * x2

instance ZFSet.ZFNat.instIsLeftCancelAdd : IsLeftCancelAdd ZFNat

noncomputable def ZFSet.ZFNat.toNat (n : ZFNat) : ℕ

Equations

• n.toNat = ZFSet.ZFNat.rec n 0 fun (x : ZFSet.ZFNat) => Nat.succ

noncomputable def ZFSet.ZFNat.ofNat (n : ℕ) : ZFNat

Equations

• ZFSet.ZFNat.ofNat n = ZFSet.ZFNat.nsmul n 1

theorem ZFSet.ZFNat.toNat_is_id {n : ℕ} : (↑n).toNat = n

theorem ZFSet.Nat.is_transitive : Nat.transitive

theorem ZFSet.Nat.is_inductive : Nat.inductive_set

Nat is an inductive set.

theorem ZFSet.ZFNat.ofNat_inj {n m : ℕ} : ↑n = ↑m ↔ n = m

theorem ZFSet.ZFNat.toNat_eq (n : ZFNat) : ↑n.toNat = n

theorem ZFSet.ZFNat.toNat_iff {n m : ZFNat} : n = m ↔ n.toNat = m.toNat

noncomputable def ZFSet.ZFNat.equivZFNat_Nat : ZFNat ≃ ℕ

Equations

• ZFSet.ZFNat.equivZFNat_Nat = { toFun := ZFSet.ZFNat.toNat, invFun := ZFSet.ZFNat.ofNat, left_inv := ZFSet.ZFNat.equivZFNat_Nat._proof_1✝, right_inv := ZFSet.ZFNat.equivZFNat_Nat._proof_2✝ }

Transfer to ℕ

equivZFNat_Nat says that ZFNat and ℕ are the same type. Upgraded to a ring isomorphism and registered as a TransferEquiv, it lets the transfer tactic read a goal about ZFNat in ℕ:

example (n m : ZFNat) : n + m = m + n := by
  transfer ZFNat → ℕ =>
    rw [Nat.add_comm]

The block is proved in ℕ, and closing it closes the goal about ZFNat. The ring operations, the numerals and the casts travel through the generic map_… lemmas of the transfer_simps simp set; what those lemmas do not cover is stated here: succ, the truncated subtraction, the homogeneous power, and the two order relations.

theorem ZFSet.ZFNat.toNat_zero : toNat 0 = 0

theorem ZFSet.ZFNat.toNat_succ (a : ZFNat) : a.succ.toNat = a.toNat.succ

theorem ZFSet.ZFNat.toNat_one : toNat 1 = 1

theorem ZFSet.ZFNat.toNat_pred (a : ZFNat) : a.pred.toNat = a.toNat.pred

theorem ZFSet.ZFNat.toNat_add (a b : ZFNat) : (a + b).toNat = a.toNat + b.toNat

theorem ZFSet.ZFNat.toNat_mul (a b : ZFNat) : (a * b).toNat = a.toNat * b.toNat

theorem ZFSet.ZFNat.toNat_sub (a b : ZFNat) : (a - b).toNat = a.toNat - b.toNat

theorem ZFSet.ZFNat.toNat_pow (a b : ZFNat) : (a ^ b).toNat = a.toNat ^ b.toNat

theorem ZFSet.ZFNat.toNat_le (a b : ZFNat) : a ≤ b ↔ a.toNat ≤ b.toNat

theorem ZFSet.ZFNat.toNat_lt (a b : ZFNat) : a < b ↔ a.toNat < b.toNat

noncomputable def ZFSet.ZFNat.ringEquivNat : ZFNat ≃+* ℕ

equivZFNat_Nat as a ring isomorphism.

Equations

• ZFSet.ZFNat.ringEquivNat = { toEquiv := ZFSet.ZFNat.equivZFNat_Nat, map_mul' := ZFSet.ZFNat.toNat_mul, map_add' := ZFSet.ZFNat.toNat_add }

@[implicit_reducible]

noncomputable instance ZFSet.ZFNat.instTransferEquivNat : TransferEquiv ZFNat ℕ

Equivalence used by the transfer tactic to move goals between ZFNat and ℕ.

Equations

• ZFSet.ZFNat.instTransferEquivNat = { equiv := ZFSet.ZFNat.ringEquivNat.toEquiv }

theorem ZFSet.ZFNat.ringEquivNat_succ (a : ZFNat) : ringEquivNat a.succ = (ringEquivNat a).succ

theorem ZFSet.ZFNat.ringEquivNat_sub (a b : ZFNat) : ringEquivNat (a - b) = ringEquivNat a - ringEquivNat b

theorem ZFSet.ZFNat.ringEquivNat_pow (a b : ZFNat) : ringEquivNat (a ^ b) = ringEquivNat a ^ ringEquivNat b

theorem ZFSet.ZFNat.ringEquivNat_dvd (a b : ZFNat) : a ∣ b ↔ ringEquivNat a ∣ ringEquivNat b

theorem ZFSet.ZFNat.ringEquivNat_le (a b : ZFNat) : a ≤ b ↔ ringEquivNat a ≤ ringEquivNat b

theorem ZFSet.ZFNat.ringEquivNat_lt (a b : ZFNat) : a < b ↔ ringEquivNat a < ringEquivNat b