Documentation

Arithmetization.ISigmaZero.Exponential.Pow2

def LO.Arith.Pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) :

Equations

LO.Arith.Pow2 a = (0 < a ∧ ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r)

Instances For

LO.Arith.pow2_definable

def LO.FirstOrder.Arith.pow2Def :

𝚺₀.Semisentence 1

Equations

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

theorem LO.Arith.pow2_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] :

𝚺₀ -Predicate LO.Arith.Pow2 via LO.FirstOrder.Arith.pow2Def

instance LO.Arith.pow2_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] :

𝚺₀ -Predicate LO.Arith.Pow2

Equations

⋯ = ⋯

theorem LO.Arith.Pow2.pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} (h : LO.Arith.Pow2 a) :

0 < a

theorem LO.Arith.Pow2.dvd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} (h : LO.Arith.Pow2 a) {r : V} (hr : r ≤ a) :

1 < r → r ∣ a → 2 ∣ r

@[simp]

theorem LO.Arith.pow2_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] :

LO.Arith.Pow2 1

@[simp]

theorem LO.Arith.not_pow2_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] :

¬LO.Arith.Pow2 0

theorem LO.Arith.Pow2.two_dvd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} (h : LO.Arith.Pow2 a) (lt : 1 < a) :

2 ∣ a

theorem LO.Arith.Pow2.two_dvd' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} (h : LO.Arith.Pow2 a) (lt : a ≠ 1) :

2 ∣ a

theorem LO.Arith.Pow2.of_dvd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} {b : V} (h : b ∣ a) :

LO.Arith.Pow2 a → LO.Arith.Pow2 b

theorem LO.Arith.pow2_mul_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} :

LO.Arith.Pow2 (2 * a) ↔ LO.Arith.Pow2 a

theorem LO.Arith.pow2_mul_four {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} :

LO.Arith.Pow2 (4 * a) ↔ LO.Arith.Pow2 a

theorem LO.Arith.Pow2.elim {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {p : V} :

LO.Arith.Pow2 p ↔ p = 1 ∨ ∃ (q : V), p = 2 * q ∧ LO.Arith.Pow2 q

@[simp]

theorem LO.Arith.pow2_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] :

LO.Arith.Pow2 2

theorem LO.Arith.Pow2.div_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {p : V} (h : LO.Arith.Pow2 p) (ne : p ≠ 1) :

LO.Arith.Pow2 (p / 2)

theorem LO.Arith.Pow2.two_mul_div_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {p : V} (h : LO.Arith.Pow2 p) (ne : p ≠ 1) :

2 * (p / 2) = p

theorem LO.Arith.Pow2.div_two_mul_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {p : V} (h : LO.Arith.Pow2 p) (ne : p ≠ 1) :

p / 2 * 2 = p

theorem LO.Arith.Pow2.elim' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {p : V} :

LO.Arith.Pow2 p ↔ p = 1 ∨ 1 < p ∧ ∃ (q : V), p = 2 * q ∧ LO.Arith.Pow2 q

def LO.Arith.LenBit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] (i : V) (a : V) :

$LenBit (2^{i}, a) ⟺ i th-bit of a is 1$ .

Equations

LO.Arith.LenBit i a = ¬2 ∣ a / i

Instances For

LO.Arith.lenbit_definable

def LO.FirstOrder.Arith.lenbitDef :

𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.lenbit_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] :

𝚺₀ -Relation LO.Arith.LenBit via LO.FirstOrder.Arith.lenbitDef

@[simp]

theorem LO.Arith.lenbit_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 2 → V) :

V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.lenbitDef) ↔ LO.Arith.LenBit (v 0) (v 1)

instance LO.Arith.lenbit_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] :

𝚺₀ -Relation LO.Arith.LenBit

Equations

⋯ = ⋯

theorem LO.Arith.LenBit.le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {i : V} {a : V} (h : LO.Arith.LenBit i a) :

i ≤ a

theorem LO.Arith.not_lenbit_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {i : V} {a : V} (h : a < i) :

¬LO.Arith.LenBit i a

@[simp]

theorem LO.Arith.LenBit.zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) :

¬LO.Arith.LenBit 0 a

@[simp]

theorem LO.Arith.LenBit.on_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) :

¬LO.Arith.LenBit a 0

theorem LO.Arith.LenBit.one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) :

LO.Arith.LenBit 1 a ↔ ¬2 ∣ a

theorem LO.Arith.LenBit.iff_rem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {i : V} {a : V} :

LO.Arith.LenBit i a ↔ a / i % 2 = 1

theorem LO.Arith.not_lenbit_iff_rem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {i : V} {a : V} :

¬LO.Arith.LenBit i a ↔ a / i % 2 = 0

@[simp]

theorem LO.Arith.LenBit.self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} (pos : 0 < a) :

LO.Arith.LenBit a a

theorem LO.Arith.LenBit.mod {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {i : V} {a : V} {k : V} (h : 2 * i ∣ k) :

LO.Arith.LenBit i (a % k) ↔ LO.Arith.LenBit i a

@[simp]

theorem LO.Arith.LenBit.mod_two_mul_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} {i : V} :

LO.Arith.LenBit i (a % (2 * i)) ↔ LO.Arith.LenBit i a

theorem LO.Arith.LenBit.add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {i : V} {a : V} {b : V} (h : 2 * i ∣ b) :

LO.Arith.LenBit i (a + b) ↔ LO.Arith.LenBit i a

theorem LO.Arith.LenBit.add_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {i : V} {a : V} (h : a < i) :

LO.Arith.LenBit i (a + i)

theorem LO.Arith.LenBit.add_self_of_not_lenbit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} {i : V} (pos : 0 < i) (h : ¬LO.Arith.LenBit i a) :

LO.Arith.LenBit i (a + i)

theorem LO.Arith.LenBit.add_self_of_lenbit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} {i : V} (pos : 0 < i) (h : LO.Arith.LenBit i a) :

¬LO.Arith.LenBit i (a + i)

theorem LO.Arith.LenBit.sub_self_of_lenbit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} {i : V} (pos : 0 < i) (h : LO.Arith.LenBit i a) :

¬LO.Arith.LenBit i (a - i)

theorem LO.Arith.Pow2.mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (ha : LO.Arith.Pow2 a) (hb : LO.Arith.Pow2 b) :

LO.Arith.Pow2 (a * b)

@[simp]

theorem LO.Arith.Pow2.mul_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} :

LO.Arith.Pow2 (a * b) ↔ LO.Arith.Pow2 a ∧ LO.Arith.Pow2 b

@[simp]

theorem LO.Arith.Pow2.sq_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} :

LO.Arith.Pow2 (a ^ 2) ↔ LO.Arith.Pow2 a

theorem LO.Arith.Pow2.sq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} :

LO.Arith.Pow2 a → LO.Arith.Pow2 (a ^ 2)

theorem LO.Arith.Pow2.dvd_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (ha : LO.Arith.Pow2 a) (hb : LO.Arith.Pow2 b) :

a ≤ b → a ∣ b

theorem LO.Arith.Pow2.le_iff_dvd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (ha : LO.Arith.Pow2 a) (hb : LO.Arith.Pow2 b) :

a ≤ b ↔ a ∣ b

theorem LO.Arith.Pow2.two_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} (pa : LO.Arith.Pow2 a) (ne1 : a ≠ 1) :

2 ≤ a

theorem LO.Arith.Pow2.le_iff_lt_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (ha : LO.Arith.Pow2 a) (hb : LO.Arith.Pow2 b) :

a ≤ b ↔ a < 2 * b

theorem LO.Arith.Pow2.lt_iff_two_mul_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (ha : LO.Arith.Pow2 a) (hb : LO.Arith.Pow2 b) :

a < b ↔ 2 * a ≤ b

theorem LO.Arith.Pow2.sq_or_dsq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} (pa : LO.Arith.Pow2 a) :

∃ (b : V), a = b ^ 2 ∨ a = 2 * b ^ 2

theorem LO.Arith.Pow2.sqrt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} (h : LO.Arith.Pow2 a) (hsq : (√a) ^ 2 = a) :

LO.Arith.Pow2 (√a)

@[simp]

theorem LO.Arith.Pow2.not_three {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

¬LO.Arith.Pow2 3

theorem LO.Arith.Pow2.four_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (hi : LO.Arith.Pow2 i) (lt : 2 < i) :

4 ≤ i

theorem LO.Arith.Pow2.mul_add_lt_of_mul_lt_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} {p : V} {q : V} (hp : LO.Arith.Pow2 p) (hq : LO.Arith.Pow2 q) (h : a * p < q) (hb : b < p) (hbq : b < q) :

a * p + b < q

theorem LO.Arith.LenBit.mod_pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} {j : V} (pi : LO.Arith.Pow2 i) (pj : LO.Arith.Pow2 j) (h : i < j) :

LO.Arith.LenBit i (a % j) ↔ LO.Arith.LenBit i a

theorem LO.Arith.LenBit.add_pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} {j : V} (pi : LO.Arith.Pow2 i) (pj : LO.Arith.Pow2 j) (h : i < j) :

LO.Arith.LenBit i (a + j) ↔ LO.Arith.LenBit i a

theorem LO.Arith.LenBit.add_pow2_iff_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} {j : V} (pi : LO.Arith.Pow2 i) (pj : LO.Arith.Pow2 j) (h : a < j) :

LO.Arith.LenBit i (a + j) ↔ i = j ∨ LO.Arith.LenBit i a

theorem LO.Arith.lenbit_iff_add_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} {a : V} (hi : LO.Arith.Pow2 i) :

LO.Arith.LenBit i a ↔ ∃ (k : V), ∃ r < i, a = k * (2 * i) + i + r

theorem LO.Arith.not_lenbit_iff_add_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} {a : V} (hi : LO.Arith.Pow2 i) :

¬LO.Arith.LenBit i a ↔ ∃ (k : V), ∃ r < i, a = k * (2 * i) + r

theorem LO.Arith.lenbit_mul_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} {j : V} {a : V} {r : V} (pi : LO.Arith.Pow2 i) (pj : LO.Arith.Pow2 j) (hr : r < j) :

LO.Arith.LenBit (i * j) (a * j + r) ↔ LO.Arith.LenBit i a

theorem LO.Arith.lenbit_add_pow2_iff_of_not_lenbit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} {j : V} (pi : LO.Arith.Pow2 i) (pj : LO.Arith.Pow2 j) (h : ¬LO.Arith.LenBit j a) :

LO.Arith.LenBit i (a + j) ↔ i = j ∨ LO.Arith.LenBit i a

theorem LO.Arith.lenbit_sub_pow2_iff_of_lenbit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} {j : V} (pi : LO.Arith.Pow2 i) (pj : LO.Arith.Pow2 j) (h : LO.Arith.LenBit j a) :

LO.Arith.LenBit i (a - j) ↔ i ≠ j ∧ LO.Arith.LenBit i a