Let x0 of type ι be given.
Apply unknownprop_6cf9cf26662aea90389ac20eb34f002de2be0a449437f2aac80f306aa0a8256b with
x0.
The subproof is completed by applying H0.
Apply unknownprop_d0b18a67181e900ea67f7a0ba30a861268ef122d83dee9e0402983f02611aa3f with
x0,
41fb9.. x0 ∈ e523d.. leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply H4 with
λ x3 x4 . 28f8d.. x4 ∈ real.
Apply unknownprop_b9b7bfb6c9b892d1b6018106403bf15df7213abab01ccecd88c7179d2ef8e566 with
x1,
x2,
λ x3 x4 . x4 ∈ real leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
Apply H4 with
λ x3 x4 . d634d.. x4 ∈ real.
Apply unknownprop_fb49976af43b10d0ce8aeb3d9ab418005490959b10197c6c1e0102ac4ae81973 with
x1,
x2,
λ x3 x4 . x4 ∈ real leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H3.
Apply exp_SNo_nat_2 with
28f8d.. x0,
λ x3 x4 . x4 ∈ real leaving 2 subgoals.
Apply unknownprop_62ffbce17a1080b510b3d10f88e78f4b8e9088a2c54409ce0c70e91f74a9fd08 with
x0.
The subproof is completed by applying L1.
Apply real_mul_SNo with
28f8d.. x0,
28f8d.. x0 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L5.
Apply exp_SNo_nat_2 with
d634d.. x0,
λ x3 x4 . x4 ∈ real leaving 2 subgoals.
Apply unknownprop_f319423ed101339f42129d35c36f78ec84ab916352e52ec279686150bcbdfec5 with
x0.
The subproof is completed by applying L1.
Apply real_mul_SNo with
d634d.. x0,
d634d.. x0 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L6.
Apply real_add_SNo with
exp_SNo_nat (28f8d.. x0) 2,
exp_SNo_nat (d634d.. x0) 2 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L8.