Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0e523d...
Let x1 of type ι be given.
Assume H1: x1e523d...
Claim L2: 28f8d.. x0real
Apply unknownprop_bf35ed077052d180738002d3131b9c960f2105b6fc771a9376424dc88c5accaa with x0.
The subproof is completed by applying H0.
Claim L3: d634d.. x0real
Apply unknownprop_f4589932e78557c04376dc773ac7e96363fb72f89bfabb77016339bd41fdf147 with x0.
The subproof is completed by applying H0.
Claim L4: 28f8d.. x1real
Apply unknownprop_bf35ed077052d180738002d3131b9c960f2105b6fc771a9376424dc88c5accaa with x1.
The subproof is completed by applying H1.
Claim L5: d634d.. x1real
Apply unknownprop_f4589932e78557c04376dc773ac7e96363fb72f89bfabb77016339bd41fdf147 with x1.
The subproof is completed by applying H1.
Apply unknownprop_ab5523330112f607e055e625ca3ec71bcb7369b53cba9b5f845ed34015ce25b3 with add_SNo (mul_SNo (28f8d.. x0) (28f8d.. x1)) (minus_SNo (mul_SNo (d634d.. x0) (d634d.. x1))), add_SNo (mul_SNo (28f8d.. x0) (d634d.. x1)) (mul_SNo (d634d.. x0) (28f8d.. x1)) leaving 2 subgoals.
Apply real_add_SNo with mul_SNo (28f8d.. x0) (28f8d.. x1), minus_SNo (mul_SNo (d634d.. x0) (d634d.. x1)) leaving 2 subgoals.
Apply real_mul_SNo with 28f8d.. x0, 28f8d.. x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L4.
Apply real_minus_SNo with mul_SNo (d634d.. x0) (d634d.. x1).
Apply real_mul_SNo with d634d.. x0, d634d.. x1 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L5.
Apply real_add_SNo with mul_SNo (28f8d.. x0) (d634d.. x1), mul_SNo (d634d.. x0) (28f8d.. x1) leaving 2 subgoals.
Apply real_mul_SNo with 28f8d.. x0, d634d.. x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L5.
Apply real_mul_SNo with d634d.. x0, 28f8d.. x1 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.