Functions and relations defined in $\mathsf{PA^-}$

This file provides functions and relations defined in $\mathsf{PA^-}

(Modified) Subtraction

theorem FFL.FirstOrder.Arithmetic.sub_existsUnique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (a b : V) : ∃! c : V, (a ≥ b → a = b + c) ∧ (a < b → c = 0)

noncomputable def FFL.FirstOrder.Arithmetic.sub {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (a b : V) : V

Equations

• FFL.FirstOrder.Arithmetic.sub a b = Classical.choose! ⋯

@[instance_reducible]

noncomputable def FFL.FirstOrder.Arithmetic.instSub_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : Sub V

Equations

• FFL.FirstOrder.Arithmetic.instSub_foundation = { sub := FFL.FirstOrder.Arithmetic.sub }

theorem FFL.FirstOrder.Arithmetic.sub_spec_of_ge {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} (h : a ≥ b) : a = b + (a - b)

theorem FFL.FirstOrder.Arithmetic.sub_spec_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} (h : a < b) : a - b = 0

theorem FFL.FirstOrder.Arithmetic.sub_eq_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b c : V} : c = a - b ↔ (a ≥ b → a = b + c) ∧ (a < b → c = 0)

@[simp]

theorem FFL.FirstOrder.Arithmetic.sub_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (a b : V) : a - b ≤ a

def FFL.FirstOrder.Arithmetic.subDef : 𝚺₀.Semisentence 3

Equations

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

instance FFL.FirstOrder.Arithmetic.sub_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : 𝚺₀-Function₂ fun (x1 x2 : V) => x1 - x2 via subDef

instance FFL.FirstOrder.Arithmetic.sub_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (ℌ : HierarchySymbol) : ℌ-Function₂ fun (x1 x2 : V) => x1 - x2

instance FFL.FirstOrder.Arithmetic.sub_polybounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : Bounded₂ fun (x1 x2 : V) => x1 - x2

@[simp]

theorem FFL.FirstOrder.Arithmetic.sub_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (a : V) : a - a = 0

theorem FFL.FirstOrder.Arithmetic.sub_spec_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} (h : a ≤ b) : a - b = 0

theorem FFL.FirstOrder.Arithmetic.sub_add_self_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} (h : b ≤ a) : a - b + b = a

theorem FFL.FirstOrder.Arithmetic.add_tsub_self_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} (h : b ≤ a) : b + (a - b) = a

@[simp]

theorem FFL.FirstOrder.Arithmetic.add_sub_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} : a + b - b = a

@[simp]

theorem FFL.FirstOrder.Arithmetic.add_sub_self' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} : b + a - b = a

@[simp]

theorem FFL.FirstOrder.Arithmetic.zero_sub {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (a : V) : 0 - a = 0

@[simp]

theorem FFL.FirstOrder.Arithmetic.sub_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (a : V) : a - 0 = a

theorem FFL.FirstOrder.Arithmetic.sub_remove_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b c : V} (e : a = b + c) : a - c = b

theorem FFL.FirstOrder.Arithmetic.sub_sub {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b c : V} : a - b - c = a - (b + c)

@[simp]

theorem FFL.FirstOrder.Arithmetic.pos_sub_iff_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} : 0 < a - b ↔ b < a

@[simp]

theorem FFL.FirstOrder.Arithmetic.sub_eq_zero_iff_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} : a - b = 0 ↔ a ≤ b

instance FFL.FirstOrder.Arithmetic.instOrderedSub_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : OrderedSub V

theorem FFL.FirstOrder.Arithmetic.pred_lt_self_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a : V} (h : 0 < a) : a - 1 < a

theorem FFL.FirstOrder.Arithmetic.tsub_lt_iff_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b c : V} (h : b ≤ a) : a - b < c ↔ a < c + b

theorem FFL.FirstOrder.Arithmetic.sub_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b c : V} (h : b ≤ a) : (a - b) * c = a * c - b * c

theorem FFL.FirstOrder.Arithmetic.mul_sub {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b c : V} (h : b ≤ a) : c * (a - b) = c * a - c * b

theorem FFL.FirstOrder.Arithmetic.add_sub_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {b c : V} (h : c ≤ b) (a : V) : a + b - c = a + (b - c)

theorem FFL.FirstOrder.Arithmetic.sub_succ_add_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {x y : V} (h : y < x) (z : V) : x - (y + 1) + (z + 1) = x - y + z

theorem FFL.FirstOrder.Arithmetic.le_sub_one_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} (h : a < b) : a ≤ b - 1

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.instAddCancelCommMonoid_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : AddCancelCommMonoid V

Equations

• FFL.FirstOrder.Arithmetic.instAddCancelCommMonoid_foundation = { toAddCommMonoid := FFL.FirstOrder.Arithmetic.instAddCommMonoid_foundation, toIsLeftCancelAdd := ⋯ }

Divisibility

theorem FFL.FirstOrder.Arithmetic.le_mul_self_of_pos_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} (hy : 0 < b) : a ≤ b * a

theorem FFL.FirstOrder.Arithmetic.le_mul_self_of_pos_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} (hy : 0 < b) : a ≤ a * b

theorem FFL.FirstOrder.Arithmetic.dvd_iff_bounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} : a ∣ b ↔ ∃ c ≤ b, b = a * c

def FFL.FirstOrder.Arithmetic.dvd : 𝚺₀.Semisentence 2

Equations

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

instance FFL.FirstOrder.Arithmetic.dvd_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : 𝚺₀-Relation fun (a b : V) => a ∣ b via dvd

instance FFL.FirstOrder.Arithmetic.dvd_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (ℌ : HierarchySymbol) : ℌ-Relation fun (x1 x2 : V) => x1 ∣ x2

def FFL.FirstOrder.Arithmetic.«first_order_formula_∣_» : Lean.ParserDescr

Equations

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

theorem FFL.FirstOrder.Arithmetic.le_of_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} (h : 0 < b) : a ∣ b → a ≤ b

theorem FFL.FirstOrder.Arithmetic.not_dvd_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} (pos : 0 < b) : b < a → ¬a ∣ b

theorem FFL.FirstOrder.Arithmetic.dvd_antisymm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a b : V} : a ∣ b → b ∣ a → a = b

theorem FFL.FirstOrder.Arithmetic.dvd_one_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a : V} : a ∣ 1 ↔ a = 1

theorem FFL.FirstOrder.Arithmetic.units_eq_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (u : Vˣ) : u = 1

@[simp]

theorem FFL.FirstOrder.Arithmetic.unit_iff_eq_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {a : V} : IsUnit a ↔ a = 1

Prime number

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.instCommMonoidWithZero_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : CommMonoidWithZero V

Equations

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

instance FFL.FirstOrder.Arithmetic.instIsCancelMulZero_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : IsCancelMulZero V

theorem FFL.FirstOrder.Arithmetic.eq_one_or_eq_of_dvd_of_prime {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] {p a : V} (pp : Prime p) (hxp : a ∣ p) : a = 1 ∨ a = p

def FFL.FirstOrder.Arithmetic.IsPrime {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (a : V) : Prop

Equations

• FFL.FirstOrder.Arithmetic.IsPrime a = (1 < a ∧ ∀ b ≤ a, b ∣ a → b = 1 ∨ b = a)

def FFL.FirstOrder.Arithmetic.isPrime : 𝚺₀.Semisentence 1

Equations

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

instance FFL.FirstOrder.Arithmetic.isPrime_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : 𝚺₀-Predicate fun (a : V) => IsPrime a via isPrime

Minimum

def FFL.FirstOrder.Arithmetic.min.dfn : 𝚺₀.Semisentence 3

Equations

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

instance FFL.FirstOrder.Arithmetic.min_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : 𝚺₀-Function₂ min via min.dfn

instance FFL.FirstOrder.Arithmetic.min_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (ℌ : HierarchySymbol) : ℌ-Function₂ min

instance FFL.FirstOrder.Arithmetic.min_polybounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : Bounded₂ min

Maximum

def FFL.FirstOrder.Arithmetic.max.dfn : 𝚺₀.Semisentence 3

Equations

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

instance FFL.FirstOrder.Arithmetic.max_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : 𝚺₀-Function₂ max via max.dfn

instance FFL.FirstOrder.Arithmetic.max_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (Γ : HierarchySymbol) : Γ-Function₂ max

instance FFL.FirstOrder.Arithmetic.max_polybounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] : Bounded₂ max