Arithmetization.ISigmaZero.Exponential.Pow2

source

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

Prop

Equations

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

Instances For

source

def LO.FirstOrder.Arith.pow2Def :

𝚺₀.Semisentence 1

Equations

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

Instances For

source

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

𝚺₀ -Predicate Pow2 via FirstOrder.Arith.pow2Def

source

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

𝚺₀ -Predicate Pow2

source

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

0 < a

source

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

1 < r → r ∣ a → 2 ∣ r

source

@[simp]

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

Pow2 1

source

@[simp]

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

¬Pow2 0

source

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

2 ∣ a

source

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

2 ∣ a

source

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

Pow2 a → Pow2 b

source

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

Pow2 (2 * a) ↔ Pow2 a

source

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

Pow2 (4 * a) ↔ Pow2 a

source

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

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

source

@[simp]

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

Pow2 2

source

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

Pow2 (p / 2)

source

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

2 * (p / 2) = p

source

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

p / 2 * 2 = p

source

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

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

source

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

Prop

$\mathrm{LenBit} (2^i, a) \iff \text{$i$th-bit of $a$ is $1$}$.

Equations

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

Instances For

source

def LO.FirstOrder.Arith.lenbitDef :

𝚺₀.Semisentence 2

Equations

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

Instances For

source

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

𝚺₀ -Relation LenBit via FirstOrder.Arith.lenbitDef

source

@[simp]

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

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

source

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

𝚺₀ -Relation LenBit

source

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

i ≤ a

source

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

¬LenBit i a

source

@[simp]

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

¬LenBit 0 a

source

@[simp]

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

¬LenBit a 0

source

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

LenBit 1 a ↔ ¬2 ∣ a

source

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

LenBit i a ↔ a / i % 2 = 1

source

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

¬LenBit i a ↔ a / i % 2 = 0

source

@[simp]

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

LenBit a a

source

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

LenBit i (a % k) ↔ LenBit i a

source

@[simp]

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

LenBit i (a % (2 * i)) ↔ LenBit i a

source

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

LenBit i (a + b) ↔ LenBit i a

source

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

LenBit i (a + i)

source

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

LenBit i (a + i)

source

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

¬LenBit i (a + i)

source

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

¬LenBit i (a - i)

source

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

Pow2 (a * b)

source

@[simp]

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

Pow2 (a * b) ↔ Pow2 a ∧ Pow2 b

source

@[simp]

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

Pow2 (a ^ 2) ↔ Pow2 a

source

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

Pow2 a → Pow2 (a ^ 2)

source

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

a ≤ b → a ∣ b

source

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

a ≤ b ↔ a ∣ b

source

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

2 ≤ a

source

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

a ≤ b ↔ a < 2 * b

source

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

a < b ↔ 2 * a ≤ b

source

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

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

source

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

Pow2 (√a)

source

@[simp]

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

¬Pow2 3

source

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

4 ≤ i

source

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

a * p + b < q

source

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

LenBit i (a % j) ↔ LenBit i a

source

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

LenBit i (a + j) ↔ LenBit i a

source

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

LenBit i (a + j) ↔ i = j ∨ LenBit i a

source

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

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

source

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

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

source

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

LenBit (i * j) (a * j + r) ↔ LenBit i a

source

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

LenBit i (a + j) ↔ i = j ∨ LenBit i a

source

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

LenBit i (a - j) ↔ i ≠ j ∧ LenBit i a