Beginning of Section SurOctonions

(*** $I sig/Part1.mgs ***)

(*** $I sig/Part2.mgs ***)

(*** $I sig/Part3.mgs ***)

(*** $I sig/Part4.mgs ***)

(*** $I sig/Part5.mgs ***)

(*** $I sig/Part6.mgs ***)

(*** $I sig/Part7.mgs ***)

(*** $I sig/Part8.mgs ***)

(*** $I sig/Part9.mgs ***)

(*** $I sig/Part10.mgs ***)

(*** $I sig/Part11.mgs ***)

(*** $I sig/Part12.mgs ***)

(*** $I sig/Part13.mgs ***)

L16

Theorem. (octonion_tag_fresh)

∀x, HSNo x → ∀u ∈ x, {4} ∉ u

In Proofgold the corresponding term root is b25e72... and proposition id is 9cf79c...

Proof:
Proof not loaded.

(*** Part 14 ***)

L23

Definition. We define HSNo_pair to be pair_tag {4} of type set → set → set.

In Proofgold the corresponding term root is 62b543... and object id is 60b502...

L25

Theorem. (HSNo_pair_0)

∀x, HSNo_pair x 0 = x

In Proofgold the corresponding term root is 121f87... and proposition id is 367405...

Proof:
Proof not loaded.

L29

Theorem. (HSNo_pair_prop_1)

∀x1 y1 x2 y2, HSNo x1 → HSNo x2 → HSNo_pair x1 y1 = HSNo_pair x2 y2 → x1 = x2

In Proofgold the corresponding term root is 99dd5b... and proposition id is 30edd7...

Proof:
Proof not loaded.

L33

Theorem. (HSNo_pair_prop_2)

∀x1 y1 x2 y2, HSNo x1 → HSNo y1 → HSNo x2 → HSNo y2 → HSNo_pair x1 y1 = HSNo_pair x2 y2 → y1 = y2

In Proofgold the corresponding term root is 9a74c6... and proposition id is 9508dd...

Proof:
Proof not loaded.

L37

Definition. We define OSNo to be CD_carr {4} HSNo of type set → prop.

In Proofgold the corresponding term root is fbe446... and object id is e6b55c...

L39

Theorem. (OSNo_I)

∀x y, HSNo x → HSNo y → OSNo (HSNo_pair x y)

In Proofgold the corresponding term root is afb109... and proposition id is 1fdc97...

Proof:
Proof not loaded.

L43

Theorem. (OSNo_E)

∀z, OSNo z → ∀p : set → prop, (∀x y, HSNo x → HSNo y → z = HSNo_pair x y → p (HSNo_pair x y)) → p z

In Proofgold the corresponding term root is c2c632... and proposition id is 2673ee...

Proof:
Proof not loaded.

L50

Theorem. (HSNo_OSNo)

∀x, HSNo x → OSNo x

In Proofgold the corresponding term root is 4fae92... and proposition id is 097009...

Proof:
Proof not loaded.

L54

Theorem. (OSNo_0)

OSNo 0

In Proofgold the corresponding term root is 6ebd11... and proposition id is 819fb5...

Proof:
Proof not loaded.

L58

Theorem. (OSNo_1)

OSNo 1

In Proofgold the corresponding term root is 76552d... and proposition id is a6d6f8...

Proof:
Proof not loaded.

L62

Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {4}

Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.

L65

Theorem. (OSNo_ExtendedSNoElt_5)

∀z, OSNo z → ExtendedSNoElt_ 5 z

In Proofgold the corresponding term root is 5f1c66... and proposition id is 8a0ec8...

Proof:
Proof not loaded.

Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_HSNo.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_HSNo.

Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_HSNo.

Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_HSNo.

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term conj_HSNo.

L110

Let i ≝ Complex_i

L112

Let j ≝ Quaternion_j

L113

Let k ≝ Quaternion_k

L114

Definition. We define OSNo_proj0 to be CD_proj0 {4} HSNo of type set → set.

In Proofgold the corresponding term root is 13b462... and object id is a29720...

L116

Definition. We define OSNo_proj1 to be CD_proj1 {4} HSNo of type set → set.

In Proofgold the corresponding term root is c77647... and object id is 6492a3...

L117

Let p0 : set → set ≝ OSNo_proj0

L119

Let p1 : set → set ≝ OSNo_proj1

L120

Let pa : set → set → set ≝ HSNo_pair

L121

Theorem. (OSNo_proj0_1)

∀z, OSNo z → HSNo (p0 z) ∧ ∃y, HSNo y ∧ z = pa (p0 z) y

In Proofgold the corresponding term root is d56b4b... and proposition id is b5e6a4...

Proof:
Proof not loaded.

L125

Theorem. (OSNo_proj0_2)

∀x y, HSNo x → HSNo y → p0 (pa x y) = x

In Proofgold the corresponding term root is b97eaa... and proposition id is 37276d...

Proof:
Proof not loaded.

L129

Theorem. (OSNo_proj1_1)

∀z, OSNo z → HSNo (p1 z) ∧ z = pa (p0 z) (p1 z)

In Proofgold the corresponding term root is 8334fc... and proposition id is d28a24...

Proof:
Proof not loaded.

L133

Theorem. (OSNo_proj1_2)

∀x y, HSNo x → HSNo y → p1 (pa x y) = y

In Proofgold the corresponding term root is 00b55f... and proposition id is ad4890...

Proof:
Proof not loaded.

L137

Theorem. (OSNo_proj0R)

∀z, OSNo z → HSNo (p0 z)

In Proofgold the corresponding term root is d79361... and proposition id is bb9e47...

Proof:
Proof not loaded.

L141

Theorem. (OSNo_proj1R)

∀z, OSNo z → HSNo (p1 z)

In Proofgold the corresponding term root is 010b9d... and proposition id is 7e4dac...

Proof:
Proof not loaded.

L145

Theorem. (OSNo_proj0p1)

∀z, OSNo z → z = pa (p0 z) (p1 z)

In Proofgold the corresponding term root is 5c4035... and proposition id is d5f2d3...

Proof:
Proof not loaded.

L149

Theorem. (OSNo_proj0proj1_split)

∀z w, OSNo z → OSNo w → p0 z = p0 w → p1 z = p1 w → z = w

In Proofgold the corresponding term root is 9e9a0b... and proposition id is 2764ac...

Proof:
Proof not loaded.

L153

Definition. We define OSNoLev to be λz ⇒ HSNoLev (p0 z) ∪ HSNoLev (p1 z) of type set → set.

In Proofgold the corresponding term root is 26d397... and object id is 5ccbab...

L155

Theorem. (OSNoLev_ordinal)

∀z, OSNo z → ordinal (OSNoLev z)

In Proofgold the corresponding term root is 49d6e6... and proposition id is 9886f3...

Proof:
Proof not loaded.

L168

Definition. We define minus_OSNo to be CD_minus {4} HSNo minus_HSNo of type set → set.

In Proofgold the corresponding term root is ad664e... and object id is 656a9e...

L170

Definition. We define conj_OSNo to be CD_conj {4} HSNo minus_HSNo conj_HSNo of type set → set.

In Proofgold the corresponding term root is 6daad6... and object id is 78d882...

L171

Definition. We define add_OSNo to be CD_add {4} HSNo add_HSNo of type set → set → set.

In Proofgold the corresponding term root is fe136b... and object id is 298874...

L172

Definition. We define mul_OSNo to be CD_mul {4} HSNo minus_HSNo conj_HSNo add_HSNo mul_HSNo of type set → set → set.

In Proofgold the corresponding term root is a82d6b... and object id is cf582d...

L173

Definition. We define exp_OSNo_nat to be CD_exp_nat {4} HSNo minus_HSNo conj_HSNo add_HSNo mul_HSNo of type set → set → set.

In Proofgold the corresponding term root is 80e8fd... and object id is d6861c...

L174

Let plus' ≝ add_OSNo

L176

Let mult' ≝ mul_OSNo

Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term minus_OSNo.

Notation. We use '' as a postfix operator with priority 100 corresponding to applying term conj_OSNo.

Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_OSNo.

Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_OSNo.

Notation. We use :^: as an infix operator with priority 355 and which associates to the right corresponding to applying term exp_OSNo_nat.

L183

Theorem. (OSNo_minus_OSNo)

∀z, OSNo z → OSNo (minus_OSNo z)

In Proofgold the corresponding term root is 5239a5... and proposition id is 33ab42...

Proof:
Proof not loaded.

L187

Theorem. (minus_OSNo_proj0)

∀z, OSNo z → p0 (:-: z) = - p0 z

In Proofgold the corresponding term root is 537bbd... and proposition id is bf0daa...

Proof:
Proof not loaded.

L191

Theorem. (minus_OSNo_proj1)

∀z, OSNo z → p1 (:-: z) = - p1 z

In Proofgold the corresponding term root is 34ff58... and proposition id is 0637f8...

Proof:
Proof not loaded.

L195

Theorem. (OSNo_conj_OSNo)

∀z, OSNo z → OSNo (conj_OSNo z)

In Proofgold the corresponding term root is 0bd248... and proposition id is 4a891d...

Proof:
Proof not loaded.

L199

Theorem. (conj_OSNo_proj0)

∀z, OSNo z → p0 (z '') = (p0 z) '

In Proofgold the corresponding term root is 9f0c90... and proposition id is 9f6dc7...

Proof:
Proof not loaded.

L203

Theorem. (conj_OSNo_proj1)

∀z, OSNo z → p1 (z '') = - p1 z

In Proofgold the corresponding term root is 0b0356... and proposition id is 88571e...

Proof:
Proof not loaded.

L207

Theorem. (OSNo_add_OSNo)

∀z w, OSNo z → OSNo w → OSNo (add_OSNo z w)

In Proofgold the corresponding term root is d59847... and proposition id is 96e815...

Proof:
Proof not loaded.

L211

Theorem. (add_OSNo_proj0)

∀z w, OSNo z → OSNo w → p0 (plus' z w) = p0 z + p0 w

In Proofgold the corresponding term root is 2a7265... and proposition id is acc7f5...

Proof:
Proof not loaded.

L215

Theorem. (add_OSNo_proj1)

∀z w, OSNo z → OSNo w → p1 (plus' z w) = p1 z + p1 w

In Proofgold the corresponding term root is 1f76aa... and proposition id is dbcaac...

Proof:
Proof not loaded.

L219

Theorem. (OSNo_mul_OSNo)

∀z w, OSNo z → OSNo w → OSNo (z ⨯ w)

In Proofgold the corresponding term root is 121ca3... and proposition id is 965453...

Proof:
Proof not loaded.

L223

Theorem. (mul_OSNo_proj0)

∀z w, OSNo z → OSNo w → p0 (mult' z w) = p0 z * p0 w + - (p1 w ' * p1 z)

In Proofgold the corresponding term root is 34f083... and proposition id is 45d781...

Proof:
Proof not loaded.

L227

Theorem. (mul_OSNo_proj1)

∀z w, OSNo z → OSNo w → p1 (mult' z w) = p1 w * p0 z + p1 z * p0 w '

In Proofgold the corresponding term root is 587f08... and proposition id is 251060...

Proof:
Proof not loaded.

L231

Theorem. (HSNo_OSNo_proj0)

∀x, HSNo x → p0 x = x

In Proofgold the corresponding term root is 3841a4... and proposition id is 5dc42a...

Proof:
Proof not loaded.

L235

Theorem. (HSNo_OSNo_proj1)

∀x, HSNo x → p1 x = 0

In Proofgold the corresponding term root is c0d013... and proposition id is 1ce9ac...

Proof:
Proof not loaded.

L239

Theorem. (OSNo_p0_0)

p0 0 = 0

In Proofgold the corresponding term root is 6e03c2... and proposition id is 50bfb2...

Proof:
Proof not loaded.

L243

Theorem. (OSNo_p1_0)

p1 0 = 0

In Proofgold the corresponding term root is 6a2ee2... and proposition id is 5b3474...

Proof:
Proof not loaded.

L247

Theorem. (OSNo_p0_1)

p0 1 = 1

In Proofgold the corresponding term root is 6166b0... and proposition id is e0ed62...

Proof:
Proof not loaded.

L251

Theorem. (OSNo_p1_1)

p1 1 = 0

In Proofgold the corresponding term root is decdcd... and proposition id is 52bcba...

Proof:
Proof not loaded.

L255

Theorem. (OSNo_p0_i)

p0 i = i

In Proofgold the corresponding term root is d61cfb... and proposition id is 092df0...

Proof:
Proof not loaded.

L259

Theorem. (OSNo_p1_i)

p1 i = 0

In Proofgold the corresponding term root is 041303... and proposition id is 0ea4e3...

Proof:
Proof not loaded.

L263

Theorem. (OSNo_p0_j)

p0 j = j

In Proofgold the corresponding term root is abf3bd... and proposition id is a67029...

Proof:
Proof not loaded.

L267

Theorem. (OSNo_p1_j)

p1 j = 0

In Proofgold the corresponding term root is d50e95... and proposition id is 2eedc2...

Proof:
Proof not loaded.

L271

Theorem. (OSNo_p0_k)

p0 k = k

In Proofgold the corresponding term root is 7d823a... and proposition id is 669c9a...

Proof:
Proof not loaded.

L275

Theorem. (OSNo_p1_k)

p1 k = 0

In Proofgold the corresponding term root is 3ff0b5... and proposition id is 1b52cc...

Proof:
Proof not loaded.

L279

Theorem. (minus_OSNo_minus_HSNo)

∀x, HSNo x → :-: x = - x

In Proofgold the corresponding term root is ad664f... and proposition id is aba4f2...

Proof:
Proof not loaded.

L283

Theorem. (minus_OSNo_0)

:-: 0 = 0

In Proofgold the corresponding term root is 82bb0f... and proposition id is 86b97f...

Proof:
Proof not loaded.

L288

Theorem. (conj_OSNo_conj_HSNo)

∀x, HSNo x → x '' = x '

In Proofgold the corresponding term root is 8cc42b... and proposition id is 071fef...

Proof:
Proof not loaded.

L292

Theorem. (conj_OSNo_0)

0 '' = 0

In Proofgold the corresponding term root is 898c21... and proposition id is 41501c...

Proof:
Proof not loaded.

L297

Theorem. (conj_OSNo_1)

1 '' = 1

In Proofgold the corresponding term root is eb7536... and proposition id is 657772...

Proof:
Proof not loaded.

L302

Theorem. (add_OSNo_add_HSNo)

∀x y, HSNo x → HSNo y → x + y = x + y

In Proofgold the corresponding term root is c83899... and proposition id is b499cd...

Proof:
Proof not loaded.

L306

Theorem. (mul_OSNo_mul_HSNo)

∀x y, HSNo x → HSNo y → x ⨯ y = x * y

In Proofgold the corresponding term root is 7fa435... and proposition id is 1eaaef...

Proof:
Proof not loaded.

L310

Theorem. (minus_OSNo_invol)

∀z, OSNo z → :-: :-: z = z

In Proofgold the corresponding term root is 0a5f21... and proposition id is 101363...

Proof:
Proof not loaded.

L314

Theorem. (conj_OSNo_invol)

∀z, OSNo z → z '' '' = z

In Proofgold the corresponding term root is 93265e... and proposition id is 468f13...

Proof:
Proof not loaded.

L318

Theorem. (conj_minus_OSNo)

∀z, OSNo z → (:-: z) '' = :-: (z '')

In Proofgold the corresponding term root is 7ff953... and proposition id is 66cbb8...

Proof:
Proof not loaded.

L322

Theorem. (minus_add_OSNo)

∀z w, OSNo z → OSNo w → :-: (z + w) = :-: z + :-: w

In Proofgold the corresponding term root is 77b3e0... and proposition id is d27c28...

Proof:
Proof not loaded.

L326

Theorem. (conj_add_OSNo)

∀z w, OSNo z → OSNo w → (z + w) '' = z '' + w ''

In Proofgold the corresponding term root is 35c199... and proposition id is 02f2b8...

Proof:
Proof not loaded.

L330

Theorem. (add_OSNo_com)

∀z w, OSNo z → OSNo w → z + w = w + z

In Proofgold the corresponding term root is a80b65... and proposition id is 2dee60...

Proof:
Proof not loaded.

L334

Theorem. (add_OSNo_assoc)

∀z w v, OSNo z → OSNo w → OSNo v → (z + w) + v = z + (w + v)

In Proofgold the corresponding term root is 88229f... and proposition id is 1279b1...

Proof:
Proof not loaded.

L338

Theorem. (add_OSNo_0L)

∀z, OSNo z → add_OSNo 0 z = z

In Proofgold the corresponding term root is 7b12c3... and proposition id is cb288a...

Proof:
Proof not loaded.

L342

Theorem. (add_OSNo_0R)

∀z, OSNo z → add_OSNo z 0 = z

In Proofgold the corresponding term root is 206e65... and proposition id is 11264f...

Proof:
Proof not loaded.

L346

Theorem. (add_OSNo_minus_OSNo_linv)

∀z, OSNo z → add_OSNo (minus_OSNo z) z = 0

In Proofgold the corresponding term root is d558dc... and proposition id is 8767d9...

Proof:
Proof not loaded.

L350

Theorem. (add_OSNo_minus_OSNo_rinv)

∀z, OSNo z → add_OSNo z (minus_OSNo z) = 0

In Proofgold the corresponding term root is 67ef27... and proposition id is 1f6cac...

Proof:
Proof not loaded.

L354

Theorem. (mul_OSNo_0R)

∀z, OSNo z → z ⨯ 0 = 0

In Proofgold the corresponding term root is 4efeb2... and proposition id is ee156e...

Proof:
Proof not loaded.

L358

Theorem. (mul_OSNo_0L)

∀z, OSNo z → 0 ⨯ z = 0

In Proofgold the corresponding term root is 9ff46d... and proposition id is ea206a...

Proof:
Proof not loaded.

L362

Theorem. (mul_OSNo_1R)

∀z, OSNo z → z ⨯ 1 = z

In Proofgold the corresponding term root is 0cf2d9... and proposition id is 71047e...

Proof:
Proof not loaded.

L366

Theorem. (mul_OSNo_1L)

∀z, OSNo z → 1 ⨯ z = z

In Proofgold the corresponding term root is d299c9... and proposition id is 0048db...

Proof:
Proof not loaded.

L370

Theorem. (conj_mul_OSNo)

∀z w, OSNo z → OSNo w → (z ⨯ w) '' = w '' ⨯ z ''

In Proofgold the corresponding term root is 05d740... and proposition id is b7721c...

Proof:
Proof not loaded.

L374

Theorem. (mul_OSNo_distrL)

∀z w u, OSNo z → OSNo w → OSNo u → z ⨯ (w + u) = z ⨯ w + z ⨯ u

In Proofgold the corresponding term root is 78f00f... and proposition id is 0d8b00...

Proof:
Proof not loaded.

L378

Theorem. (mul_OSNo_distrR)

∀z w u, OSNo z → OSNo w → OSNo u → (z + w) ⨯ u = z ⨯ u + w ⨯ u

In Proofgold the corresponding term root is f3a994... and proposition id is 76bd4b...

Proof:
Proof not loaded.

L382

Theorem. (minus_mul_OSNo_distrR)

∀z w, OSNo z → OSNo w → z ⨯ (:-: w) = :-: z ⨯ w

In Proofgold the corresponding term root is 54ee0d... and proposition id is 65f43c...

Proof:
Proof not loaded.

L386

Theorem. (minus_mul_OSNo_distrL)

∀z w, OSNo z → OSNo w → (:-: z) ⨯ w = :-: z ⨯ w

In Proofgold the corresponding term root is bfdb51... and proposition id is 2ef898...

Proof:
Proof not loaded.

L390

Theorem. (exp_OSNo_nat_0)

∀z, z⁰ = 1

In Proofgold the corresponding term root is 469625... and proposition id is 0dfdbe...

Proof:
Proof not loaded.

L394

Theorem. (exp_OSNo_nat_S)

∀z n, nat_p n → z^{(ordsucc n)} = z ⨯ zⁿ

In Proofgold the corresponding term root is 340b9f... and proposition id is e25374...

Proof:
Proof not loaded.

L398

Theorem. (exp_OSNo_nat_1)

∀z, OSNo z → z¹ = z

In Proofgold the corresponding term root is f5712c... and proposition id is e64119...

Proof:
Proof not loaded.

L402

Theorem. (exp_OSNo_nat_2)

∀z, OSNo z → z² = z ⨯ z

In Proofgold the corresponding term root is 6ad2c8... and proposition id is b8a62a...

Proof:
Proof not loaded.

L406

Theorem. (OSNo_exp_OSNo_nat)

∀z, OSNo z → ∀n, nat_p n → OSNo (zⁿ)

In Proofgold the corresponding term root is 9fea84... and proposition id is ccc319...

Proof:
Proof not loaded.

L410

Theorem. (add_HSNo_com_3b_1_2)

∀x y z, HSNo x → HSNo y → HSNo z → (x + y) + z = (x + z) + y

In Proofgold the corresponding term root is dcf334... and proposition id is 57e838...

Proof:
Proof not loaded.

L423

Theorem. (add_HSNo_com_4_inner_mid)

∀x y z w, HSNo x → HSNo y → HSNo z → HSNo w → (x + y) + (z + w) = (x + z) + (y + w)

In Proofgold the corresponding term root is eac30d... and proposition id is 5eecfb...

Proof:
Proof not loaded.

L434

Theorem. (add_HSNo_rotate_4_0312)

∀x y z w, HSNo x → HSNo y → HSNo z → HSNo w → (x + y) + (z + w) = (x + w) + (y + z)

In Proofgold the corresponding term root is b2c7cb... and proposition id is 394006...

Proof:
Proof not loaded.

L441

Definition. We define Octonion_i0 to be pa 0 1 of type set.

In Proofgold the corresponding term root is 53fb1a... and object id is c8bb3f...

L443

Definition. We define Octonion_i3 to be pa 0 (- Complex_i) of type set.

In Proofgold the corresponding term root is ad3e24... and object id is f0f0f0...

L444

Definition. We define Octonion_i5 to be pa 0 (- Quaternion_k) of type set.

In Proofgold the corresponding term root is 23c235... and object id is 764d12...

L445

Definition. We define Octonion_i6 to be pa 0 (- Quaternion_j) of type set.

In Proofgold the corresponding term root is 6111ba... and object id is d882ec...

L446

Let i0 ≝ Octonion_i0

L448

Let i1 ≝ Complex_i

L449

Let i2 ≝ Quaternion_j

L450

Let i3 ≝ Octonion_i3

L451

Let i4 ≝ Quaternion_k

L452

Let i5 ≝ Octonion_i5

L453

Let i6 ≝ Octonion_i6

L454

Theorem. (OSNo_Complex_i)

OSNo i

In Proofgold the corresponding term root is af3f4b... and proposition id is 12bbc0...

Proof:
Proof not loaded.

L458

Theorem. (OSNo_Quaternion_j)

OSNo j

In Proofgold the corresponding term root is 77f80f... and proposition id is c8c165...

Proof:
Proof not loaded.

L462

Theorem. (OSNo_Quaternion_k)

OSNo k

In Proofgold the corresponding term root is 9b69f6... and proposition id is eba5fb...

Proof:
Proof not loaded.

L466

Theorem. (OSNo_Octonion_i0)

OSNo i0

In Proofgold the corresponding term root is e6c8dc... and proposition id is 45658b...

Proof:
Proof not loaded.

L470

Theorem. (OSNo_Octonion_i3)

OSNo i3

In Proofgold the corresponding term root is 39dd06... and proposition id is 428549...

Proof:
Proof not loaded.

L474

Theorem. (OSNo_Octonion_i5)

OSNo i5

In Proofgold the corresponding term root is 55ce63... and proposition id is e92a7a...

Proof:
Proof not loaded.

L478

Theorem. (OSNo_Octonion_i6)

OSNo i6

In Proofgold the corresponding term root is 73ed2a... and proposition id is d0f581...

Proof:
Proof not loaded.

L482

Theorem. (OSNo_p0_i0)

p0 i0 = 0

In Proofgold the corresponding term root is c9a02f... and proposition id is 444265...

Proof:
Proof not loaded.

L486

Theorem. (OSNo_p1_i0)

p1 i0 = 1

In Proofgold the corresponding term root is 6bb51f... and proposition id is 17a56f...

Proof:
Proof not loaded.

L490

Theorem. (OSNo_p0_i3)

p0 i3 = 0

In Proofgold the corresponding term root is 784dc9... and proposition id is 27f5a3...

Proof:
Proof not loaded.

L494

Theorem. (OSNo_p1_i3)

p1 i3 = - i

In Proofgold the corresponding term root is 097faa... and proposition id is 6371c8...

Proof:
Proof not loaded.

L498

Theorem. (OSNo_p0_i5)

p0 i5 = 0

In Proofgold the corresponding term root is 597589... and proposition id is c4b46c...

Proof:
Proof not loaded.

L502

Theorem. (OSNo_p1_i5)

p1 i5 = - k

In Proofgold the corresponding term root is ef1afc... and proposition id is 9bf42c...

Proof:
Proof not loaded.

L506

Theorem. (OSNo_p0_i6)

p0 i6 = 0

In Proofgold the corresponding term root is bf6e13... and proposition id is 183aad...

Proof:
Proof not loaded.

L510

Theorem. (OSNo_p1_i6)

p1 i6 = - j

In Proofgold the corresponding term root is 50991b... and proposition id is 78f3bd...

Proof:
Proof not loaded.

L514

Theorem. (Octonion_i1_sqr)

i1 ⨯ i1 = :-: 1

In Proofgold the corresponding term root is 2cf2b7... and proposition id is 701b4a...

Proof:
Proof not loaded.

L521

Theorem. (Octonion_i2_sqr)

i2 ⨯ i2 = :-: 1

In Proofgold the corresponding term root is 52dca5... and proposition id is 46db7e...

Proof:
Proof not loaded.

L528

Theorem. (Octonion_i4_sqr)

i4 ⨯ i4 = :-: 1

In Proofgold the corresponding term root is e85aa9... and proposition id is f8d60f...

Proof:
Proof not loaded.

L535

Theorem. (Octonion_i0_sqr)

i0 ⨯ i0 = :-: 1

In Proofgold the corresponding term root is 6e1738... and proposition id is 4f5642...

Proof:
Proof not loaded.

L568

Theorem. (Octonion_i3_sqr)

i3 ⨯ i3 = :-: 1

In Proofgold the corresponding term root is 8c0727... and proposition id is 24bf69...

Proof:
Proof not loaded.

L607

Theorem. (Octonion_i5_sqr)

i5 ⨯ i5 = :-: 1

In Proofgold the corresponding term root is 19b120... and proposition id is 474ccf...

Proof:
Proof not loaded.

L646

Theorem. (Octonion_i6_sqr)

i6 ⨯ i6 = :-: 1

In Proofgold the corresponding term root is 97f9e7... and proposition id is 12af41...

Proof:
Proof not loaded.

L685

Theorem. (Octonion_i1_i2)

i1 ⨯ i2 = i4

In Proofgold the corresponding term root is 54f62e... and proposition id is fd7e6b...

Proof:
Proof not loaded.

L713

Theorem. (Octonion_i2_i1)

i2 ⨯ i1 = :-: i4

In Proofgold the corresponding term root is a29e37... and proposition id is f1a9c7...

Proof:
Proof not loaded.

L742

Theorem. (Octonion_i2_i4)

i2 ⨯ i4 = i1

In Proofgold the corresponding term root is 32f52e... and proposition id is 60c4d4...

Proof:
Proof not loaded.

L770

Theorem. (Octonion_i4_i2)

i4 ⨯ i2 = :-: i1

In Proofgold the corresponding term root is 0c684d... and proposition id is 294b23...

Proof:
Proof not loaded.

L799

Theorem. (Octonion_i4_i1)

i4 ⨯ i1 = i2

In Proofgold the corresponding term root is fe2349... and proposition id is f00e84...

Proof:
Proof not loaded.

L827

Theorem. (Octonion_i1_i4)

i1 ⨯ i4 = :-: i2

In Proofgold the corresponding term root is 6ef84c... and proposition id is 48faff...

Proof:
Proof not loaded.

L856

Theorem. (Octonion_i2_i3)

i2 ⨯ i3 = i5

In Proofgold the corresponding term root is 69b316... and proposition id is 7ee827...

Proof:
Proof not loaded.

L885

Theorem. (Octonion_i3_i2)

i3 ⨯ i2 = :-: i5

In Proofgold the corresponding term root is 189ce1... and proposition id is ba3701...

Proof:
Proof not loaded.

L917

Theorem. (Octonion_i3_i5)

i3 ⨯ i5 = i2

In Proofgold the corresponding term root is 0c085c... and proposition id is 54e1ef...

Proof:
Proof not loaded.

L950

Theorem. (Octonion_i5_i3)

i5 ⨯ i3 = :-: i2

In Proofgold the corresponding term root is e8fde0... and proposition id is 9faab2...

Proof:
Proof not loaded.

L984

Theorem. (Octonion_i5_i2)

i5 ⨯ i2 = i3

In Proofgold the corresponding term root is 346b35... and proposition id is 40996f...

Proof:
Proof not loaded.

L1016

Theorem. (Octonion_i2_i5)

i2 ⨯ i5 = :-: i3

In Proofgold the corresponding term root is 2d78a7... and proposition id is f300cd...

Proof:
Proof not loaded.

L1046

Theorem. (Octonion_i3_i4)

i3 ⨯ i4 = i6

In Proofgold the corresponding term root is 511ac9... and proposition id is 73693c...

Proof:
Proof not loaded.

L1078

Theorem. (Octonion_i4_i3)

i4 ⨯ i3 = :-: i6

In Proofgold the corresponding term root is e373e5... and proposition id is b2ad1d...

Proof:
Proof not loaded.

L1109

Theorem. (Octonion_i4_i6)

i4 ⨯ i6 = i3

In Proofgold the corresponding term root is 620e03... and proposition id is 7c49f7...

Proof:
Proof not loaded.

L1138

Theorem. (Octonion_i6_i4)

i6 ⨯ i4 = :-: i3

In Proofgold the corresponding term root is 121f61... and proposition id is 0b4e69...

Proof:
Proof not loaded.

L1171

Theorem. (Octonion_i6_i3)

i6 ⨯ i3 = i4

In Proofgold the corresponding term root is d3cc9f... and proposition id is 9b6ce9...

Proof:
Proof not loaded.

L1204

Theorem. (Octonion_i3_i6)

i3 ⨯ i6 = :-: i4

In Proofgold the corresponding term root is 575da0... and proposition id is 517b53...

Proof:
Proof not loaded.

L1238

Theorem. (Octonion_i4_i5)

i4 ⨯ i5 = i0

In Proofgold the corresponding term root is 360332... and proposition id is fc370d...

Proof:
Proof not loaded.

L1268

Theorem. (Octonion_i5_i4)

i5 ⨯ i4 = :-: i0

In Proofgold the corresponding term root is beff8b... and proposition id is afcfe9...

Proof:
Proof not loaded.

L1302

Theorem. (Octonion_i5_i0)

i5 ⨯ i0 = i4

In Proofgold the corresponding term root is adfd5d... and proposition id is e39b44...

Proof:
Proof not loaded.

L1332

Theorem. (Octonion_i0_i5)

i0 ⨯ i5 = :-: i4

In Proofgold the corresponding term root is 498fb6... and proposition id is 0b796b...

Proof:
Proof not loaded.

L1364

Theorem. (Octonion_i0_i4)

i0 ⨯ i4 = i5

In Proofgold the corresponding term root is 133131... and proposition id is 3686a2...

Proof:
Proof not loaded.

L1395

Theorem. (Octonion_i4_i0)

i4 ⨯ i0 = :-: i5

In Proofgold the corresponding term root is 01a797... and proposition id is 529327...

Proof:
Proof not loaded.

L1424

Theorem. (Octonion_i5_i6)

i5 ⨯ i6 = i1

In Proofgold the corresponding term root is f51c6c... and proposition id is bd260d...

Proof:
Proof not loaded.

L1457

Theorem. (Octonion_i6_i5)

i6 ⨯ i5 = :-: i1

In Proofgold the corresponding term root is b9e439... and proposition id is b85ae9...

Proof:
Proof not loaded.

L1491

Theorem. (Octonion_i6_i1)

i6 ⨯ i1 = i5

In Proofgold the corresponding term root is e457ad... and proposition id is a0a7b9...

Proof:
Proof not loaded.

L1523

Theorem. (Octonion_i1_i6)

i1 ⨯ i6 = :-: i5

In Proofgold the corresponding term root is c1b4e0... and proposition id is bd93b5...

Proof:
Proof not loaded.

L1554

Theorem. (Octonion_i1_i5)

i1 ⨯ i5 = i6

In Proofgold the corresponding term root is 1e9e88... and proposition id is 3b1993...

Proof:
Proof not loaded.

L1583

Theorem. (Octonion_i5_i1)

i5 ⨯ i1 = :-: i6

In Proofgold the corresponding term root is 5e4738... and proposition id is 547b1a...

Proof:
Proof not loaded.

L1615

Theorem. (Octonion_i6_i0)

i6 ⨯ i0 = i2

In Proofgold the corresponding term root is 73d83a... and proposition id is c60735...

Proof:
Proof not loaded.

L1644

Theorem. (Octonion_i0_i6)

i0 ⨯ i6 = :-: i2

In Proofgold the corresponding term root is 7f039d... and proposition id is dc4654...

Proof:
Proof not loaded.

L1676

Theorem. (Octonion_i0_i2)

i0 ⨯ i2 = i6

In Proofgold the corresponding term root is 95da86... and proposition id is b659de...

Proof:
Proof not loaded.

L1706

Theorem. (Octonion_i2_i0)

i2 ⨯ i0 = :-: i6

In Proofgold the corresponding term root is cafa53... and proposition id is 330a2a...

Proof:
Proof not loaded.

L1735

Theorem. (Octonion_i2_i6)

i2 ⨯ i6 = i0

In Proofgold the corresponding term root is 787314... and proposition id is b9cfda...

Proof:
Proof not loaded.

L1765

Theorem. (Octonion_i6_i2)

i6 ⨯ i2 = :-: i0

In Proofgold the corresponding term root is 158a18... and proposition id is cd6dcf...

Proof:
Proof not loaded.

L1797

Theorem. (Octonion_i0_i1)

i0 ⨯ i1 = i3

In Proofgold the corresponding term root is b43708... and proposition id is 251b34...

Proof:
Proof not loaded.

L1826

Theorem. (Octonion_i1_i0)

i1 ⨯ i0 = :-: i3

In Proofgold the corresponding term root is 9cb018... and proposition id is 9165d8...

Proof:
Proof not loaded.

L1855

Theorem. (Octonion_i1_i3)

i1 ⨯ i3 = i0

In Proofgold the corresponding term root is 3cc4e3... and proposition id is f71c20...

Proof:
Proof not loaded.

L1887

Theorem. (Octonion_i3_i1)

i3 ⨯ i1 = :-: i0

In Proofgold the corresponding term root is 2603e9... and proposition id is 105f8c...

Proof:
Proof not loaded.

L1919

Theorem. (Octonion_i3_i0)

i3 ⨯ i0 = i1

In Proofgold the corresponding term root is 902425... and proposition id is cf0eac...

Proof:
Proof not loaded.

L1948

Theorem. (Octonion_i0_i3)

i0 ⨯ i3 = :-: i1

In Proofgold the corresponding term root is 73d689... and proposition id is c0f00e...

Proof:
Proof not loaded.

End of Section SurOctonions