Search for blocks/addresses/...

Proofgold Proof

pf
Apply minus_OSNo_minus_HSNo with 1, λ x0 x1 . mul_OSNo Octonion_i3 Octonion_i3 = x1 leaving 2 subgoals.
The subproof is completed by applying HSNo_1.
Claim L0: OSNo (mul_OSNo Octonion_i3 Octonion_i3)
Apply OSNo_mul_OSNo with Octonion_i3, Octonion_i3 leaving 2 subgoals.
The subproof is completed by applying OSNo_Octonion_i3.
The subproof is completed by applying OSNo_Octonion_i3.
Claim L1: HSNo (minus_HSNo 1)
Apply HSNo_minus_HSNo with 1.
The subproof is completed by applying HSNo_1.
Apply OSNo_proj0proj1_split with mul_OSNo Octonion_i3 Octonion_i3, minus_HSNo 1 leaving 4 subgoals.
The subproof is completed by applying L0.
Apply HSNo_OSNo with minus_HSNo 1.
The subproof is completed by applying L1.
Apply HSNo_OSNo_proj0 with minus_HSNo 1, λ x0 x1 . OSNo_proj0 (mul_OSNo Octonion_i3 Octonion_i3) = x1 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply mul_OSNo_proj0 with Octonion_i3, Octonion_i3, λ x0 x1 . x1 = minus_HSNo 1 leaving 3 subgoals.
The subproof is completed by applying OSNo_Octonion_i3.
The subproof is completed by applying OSNo_Octonion_i3.
Apply OSNo_p0_i3 with λ x0 x1 . add_HSNo (mul_HSNo x1 x1) (minus_HSNo (mul_HSNo (conj_HSNo (OSNo_proj1 Octonion_i3)) (OSNo_proj1 Octonion_i3))) = minus_HSNo 1.
Apply OSNo_p1_i3 with λ x0 x1 . add_HSNo (mul_HSNo 0 0) (minus_HSNo (mul_HSNo (conj_HSNo x1) x1)) = minus_HSNo 1.
Apply mul_HSNo_0R with 0, λ x0 x1 . add_HSNo x1 (minus_HSNo (mul_HSNo (conj_HSNo (minus_HSNo Complex_i)) (minus_HSNo Complex_i))) = minus_HSNo 1 leaving 2 subgoals.
The subproof is completed by applying HSNo_0.
Apply conj_minus_HSNo with Complex_i, λ x0 x1 . add_HSNo 0 (minus_HSNo (mul_HSNo x1 (minus_HSNo Complex_i))) = minus_HSNo 1 leaving 2 subgoals.
The subproof is completed by applying HSNo_Complex_i.
Apply conj_HSNo_i with λ x0 x1 . add_HSNo 0 (minus_HSNo (mul_HSNo (minus_HSNo x1) (minus_HSNo Complex_i))) = minus_HSNo 1.
Apply minus_HSNo_invol with Complex_i, λ x0 x1 . add_HSNo 0 (minus_HSNo (mul_HSNo x1 (minus_HSNo Complex_i))) = minus_HSNo 1 leaving 2 subgoals.
The subproof is completed by applying HSNo_Complex_i.
Apply minus_mul_HSNo_distrR with Complex_i, Complex_i, λ x0 x1 . add_HSNo 0 (minus_HSNo x1) = minus_HSNo 1 leaving 3 subgoals.
The subproof is completed by applying HSNo_Complex_i.
The subproof is completed by applying HSNo_Complex_i.
Apply minus_HSNo_invol with mul_HSNo Complex_i Complex_i, λ x0 x1 . add_HSNo 0 x1 = minus_HSNo 1 leaving 2 subgoals.
Apply HSNo_mul_HSNo with Complex_i, Complex_i leaving 2 subgoals.
The subproof is completed by applying HSNo_Complex_i.
The subproof is completed by applying HSNo_Complex_i.
Apply Quaternion_i_sqr with λ x0 x1 . add_HSNo 0 x1 = minus_HSNo 1.
Apply add_HSNo_0L with minus_HSNo 1.
The subproof is completed by applying L1.
Apply HSNo_OSNo_proj1 with minus_HSNo 1, λ x0 x1 . OSNo_proj1 (mul_OSNo Octonion_i3 Octonion_i3) = x1 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply mul_OSNo_proj1 with Octonion_i3, Octonion_i3, λ x0 x1 . x1 = 0 leaving 3 subgoals.
The subproof is completed by applying OSNo_Octonion_i3.
The subproof is completed by applying OSNo_Octonion_i3.
Apply OSNo_p0_i3 with λ x0 x1 . add_HSNo (mul_HSNo (OSNo_proj1 Octonion_i3) x1) (mul_HSNo (OSNo_proj1 Octonion_i3) (conj_HSNo x1)) = 0.
Apply OSNo_p1_i3 with λ x0 x1 . add_HSNo (mul_HSNo x1 0) (mul_HSNo x1 (conj_HSNo 0)) = 0.
Apply conj_HSNo_id_SNo with 0, λ x0 x1 . add_HSNo (mul_HSNo (minus_HSNo Complex_i) 0) (mul_HSNo (minus_HSNo Complex_i) x1) = 0 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply mul_HSNo_0R with minus_HSNo Complex_i, λ x0 x1 . add_HSNo x1 x1 = 0 leaving 2 subgoals.
Apply HSNo_minus_HSNo with Complex_i.
The subproof is completed by applying HSNo_Complex_i.
Apply add_HSNo_0L with 0.
The subproof is completed by applying HSNo_0.
■