Search for blocks/addresses/...

Proofgold Proof

pf
Apply explicit_Field_I with complex, 0, 1, add_CSNo, mul_CSNo leaving 14 subgoals.
The subproof is completed by applying complex_add_CSNo.
Let x0 of type ι be given.
Assume H0: x0 ∈ complex.
Let x1 of type ι be given.
Assume H1: x1 ∈ complex.
Let x2 of type ι be given.
Assume H2: x2 ∈ complex.
Apply unknownprop_4dacc39fbff2a1eb7f64c88eae888b40bdb7083a731b4cd05ad435e42f13fcba with x0, x1, x2 leaving 3 subgoals.
Apply complex_CSNo with x0.
The subproof is completed by applying H0.
Apply complex_CSNo with x1.
The subproof is completed by applying H1.
Apply complex_CSNo with x2.
The subproof is completed by applying H2.
Let x0 of type ι be given.
Assume H0: x0 ∈ complex.
Let x1 of type ι be given.
Assume H1: x1 ∈ complex.
Apply unknownprop_6df04587a59e9b54f0549c96144213d94328d0b365474f739b895e743839c817 with x0, x1 leaving 2 subgoals.
Apply complex_CSNo with x0.
The subproof is completed by applying H0.
Apply complex_CSNo with x1.
The subproof is completed by applying H1.
The subproof is completed by applying complex_0.
Let x0 of type ι be given.
Assume H0: x0 ∈ complex.
Apply add_CSNo_0L with x0.
Apply complex_CSNo with x0.
The subproof is completed by applying H0.
Let x0 of type ι be given.
Assume H0: x0 ∈ complex.
Let x1 of type ο be given.
Assume H1: ∀ x2 . and (x2 ∈ complex) (add_CSNo x0 x2 = 0) ⟶ x1.
Apply H1 with minus_CSNo x0.
Apply andI with minus_CSNo x0 ∈ complex, add_CSNo x0 (minus_CSNo x0) = 0 leaving 2 subgoals.
Apply complex_minus_CSNo with x0.
The subproof is completed by applying H0.
Apply add_CSNo_minus_CSNo_rinv with x0.
Apply complex_CSNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying complex_mul_CSNo.
Let x0 of type ι be given.
Assume H0: x0 ∈ complex.
Let x1 of type ι be given.
Assume H1: x1 ∈ complex.
Let x2 of type ι be given.
Assume H2: x2 ∈ complex.
Apply unknownprop_f134758f39278620c60cfac6676dbfce170f8cc0cce849e07ba3004e259a9bbb with x0, x1, x2 leaving 3 subgoals.
Apply complex_CSNo with x0.
The subproof is completed by applying H0.
Apply complex_CSNo with x1.
The subproof is completed by applying H1.
Apply complex_CSNo with x2.
The subproof is completed by applying H2.
Let x0 of type ι be given.
Assume H0: x0 ∈ complex.
Let x1 of type ι be given.
Assume H1: x1 ∈ complex.
Apply unknownprop_4be0565ac5b41f138f7a30d0a9f34a5d126bb341d2eeaa545aa7f0c1552b9722 with x0, x1 leaving 2 subgoals.
Apply complex_CSNo with x0.
The subproof is completed by applying H0.
Apply complex_CSNo with x1.
The subproof is completed by applying H1.
The subproof is completed by applying complex_1.
The subproof is completed by applying neq_1_0.
Let x0 of type ι be given.
Assume H0: x0 ∈ complex.
Apply unknownprop_0d9bf92aa5eb4d4ae6bc10fbd993cadc9f48c429c82304b11a917b483aee3888 with x0.
Apply complex_CSNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying nonzero_complex_recip_ex.
Let x0 of type ι be given.
Assume H0: x0 ∈ complex.
Let x1 of type ι be given.
Assume H1: x1 ∈ complex.
Let x2 of type ι be given.
Assume H2: x2 ∈ complex.
Apply unknownprop_1a3b6d576749bdb66b853eab2e35cc4332be69b97fdfebcc7e17a4a552a3d204 with x0, x1, x2 leaving 3 subgoals.
Apply complex_CSNo with x0.
The subproof is completed by applying H0.
Apply complex_CSNo with x1.
The subproof is completed by applying H1.
Apply complex_CSNo with x2.
The subproof is completed by applying H2.
■