Documentation

Foundation.FirstOrder.Arithmetic.Exponential.PPow2

On $\mathrm{PPow2}(x)$ #

$\mathrm{PPow2}(n)$ is a property that holds iff $n = 2^{2^i}$ for some $i$.

source
def LO.FirstOrder.Arithmetic.SPPow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (m : V) :
Prop
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def LO.FirstOrder.Arithmetic.sppow2Def :
    𝚺₀.Semisentence 1
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance LO.FirstOrder.Arithmetic.sppow2_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
      𝚺₀-Predicate SPPow2 via sppow2Def
      source
      def LO.FirstOrder.Arithmetic.PPow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (i : V) :
      Prop
      Equations
      Instances For
        source
        def LO.FirstOrder.Arithmetic.ppow2Def :
        𝚺₀.Semisentence 1
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance LO.FirstOrder.Arithmetic.ppow2_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          𝚺₀-Predicate PPow2 via ppow2Def
          source
          instance LO.FirstOrder.Arithmetic.ppow2_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          𝚺₀-Predicate PPow2
          source
          theorem LO.FirstOrder.Arithmetic.SPPow2.not_lenbit_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {m : V} (hm : SPPow2 m) :
          ¬LenBit 1 m
          source
          theorem LO.FirstOrder.Arithmetic.SPPow2.lenbit_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {m : V} (hm : SPPow2 m) :
          LenBit 2 m
          source
          theorem LO.FirstOrder.Arithmetic.SPPow2.lenbit_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (hi : i ≤ m) (pi : Pow2 i) (lt2 : 2 < i) :
          LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m
          source
          theorem LO.FirstOrder.Arithmetic.SPPow2.one_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (hi : LenBit i m) :
          1 < i
          source
          theorem LO.FirstOrder.Arithmetic.SPPow2.two_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (hi : LenBit i m) (ne2 : i ≠ 2) :
          2 < i
          source
          theorem LO.FirstOrder.Arithmetic.SPPow2.sqrt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (hi : LenBit i m) (pi : Pow2 i) (ne2 : i ≠ 2) :
          LenBit (√i) m
          source
          theorem LO.FirstOrder.Arithmetic.SPPow2.sq_sqrt_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (hi : LenBit i m) (pi : Pow2 i) (ne2 : i ≠ 2) :
          (√i) ^ 2 = i
          source
          theorem LO.FirstOrder.Arithmetic.SPPow2.of_sqrt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (pi : Pow2 i) (him : i ≤ m) (hsqi : (√i) ^ 2 = i) (hi : LenBit (√i) m) :
          LenBit i m
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.SPPow2.two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          SPPow2 2
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.SPPow2.not_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          ¬SPPow2 0
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.SPPow2.not_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          ¬SPPow2 1
          source
          theorem LO.FirstOrder.Arithmetic.SPPow2.sq_le_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {m : V} (hm : SPPow2 m) {i j : V} (pi : Pow2 i) (pj : Pow2 j) (hi : LenBit i m) (hj : LenBit j m) :
          i < j → i ^ 2 ≤ j
          source
          theorem LO.FirstOrder.Arithmetic.SPPow2.last_uniq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {m : V} (hm : SPPow2 m) {i j : V} (pi : Pow2 i) (pj : Pow2 j) (hi : LenBit i m) (hj : LenBit j m) (hsqi : m < i ^ 2) (hsqj : m < j ^ 2) :
          i = j
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.pow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (h : PPow2 i) :
          Pow2 i
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (ppi : PPow2 i) :
          0 < i
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.one_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (ppi : PPow2 i) :
          1 < i
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.sq_sqrt_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (ppi : PPow2 i) (ne2 : i ≠ 2) :
          (√i) ^ 2 = i
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.sqrt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (ppi : PPow2 i) (ne2 : i ≠ 2) :
          PPow2 (√i)
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.exists_spp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (h : PPow2 i) :
          ∃ m < 2 * i, SPPow2 m ∧ LenBit i m
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (ppi : PPow2 i) :
          PPow2 (i ^ 2)
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.PPow2.two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          PPow2 2
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.PPow2.not_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          ¬PPow2 0
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.PPow2.not_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          ¬PPow2 1
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.elim {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} :
          PPow2 i ↔ i = 2 ∨ ∃ (b : V), i = b ^ 2 ∧ PPow2 b
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.elim' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} :
          PPow2 i ↔ i = 2 ∨ 2 < i ∧ ∃ (j : V), i = j ^ 2 ∧ PPow2 j
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.PPow2.four {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          PPow2 4
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.two_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (hi : PPow2 i) :
          2 ≤ i
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.not_three {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          ¬PPow2 3
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.two_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (hi : PPow2 i) (ne : i ≠ 2) :
          2 < i
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.four_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (hi : PPow2 i) (ne : i ≠ 2) :
          4 ≤ i
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.four_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (hi : PPow2 i) (ne2 : i ≠ 2) (ne4 : i ≠ 4) :
          4 < i
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.sq_ne_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (hi : PPow2 i) :
          i ^ 2 ≠ 2
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.sqrt_ne_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (hi : PPow2 i) (ne2 : i ≠ 2) (ne4 : i ≠ 4) :
          √i ≠ 2
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.sq_ne_four {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (hi : PPow2 i) (ne2 : i ≠ 2) :
          i ^ 2 ≠ 4
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.sq_le_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i j : V} (hi : PPow2 i) (hj : PPow2 j) :
          i < j → i ^ 2 ≤ j
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.sq_uniq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y i j : V} (py : Pow2 y) (ppi : PPow2 i) (ppj : PPow2 j) (hi : y < i ∧ i ≤ y ^ 2) (hj : y < j ∧ j ≤ y ^ 2) :
          i = j
          source
          theorem LO.FirstOrder.Arithmetic.PPow2.two_mul_sq_uniq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y i j : V} (py : Pow2 y) (ppi : PPow2 i) (ppj : PPow2 j) (hi : y < i ∧ i ≤ 2 * y ^ 2) (hj : y < j ∧ j ≤ 2 * y ^ 2) :
          i = j