Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_2504c05a08587fe0873ed45685efc417625f0a904281d653d757d643896f9a70 with λ x0 . ∀ x1 . x1 ∈ int_alt1 ⟶ mul_SNo x0 x1 ∈ int_alt1 leaving 2 subgoals.
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Claim L1: nat_p x0
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Claim L2: ordinal x0
Apply nat_p_ordinal with x0.
The subproof is completed by applying L1.
Claim L3: SNo x0
Apply ordinal_SNo with x0.
The subproof is completed by applying L2.
Apply unknownprop_2504c05a08587fe0873ed45685efc417625f0a904281d653d757d643896f9a70 with λ x1 . mul_SNo x0 x1 ∈ int_alt1 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H4: x1 ∈ omega.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with mul_SNo x0 x1.
Apply mul_SNo_In_omega with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Assume H4: x1 ∈ omega.
Claim L5: nat_p x1
Apply omega_nat_p with x1.
The subproof is completed by applying H4.
Claim L6: ordinal x1
Apply nat_p_ordinal with x1.
The subproof is completed by applying L5.
Claim L7: SNo x1
Apply ordinal_SNo with x1.
The subproof is completed by applying L6.
Apply mul_SNo_com with x0, minus_SNo x1, λ x2 x3 . x3 ∈ int_alt1 leaving 3 subgoals.
The subproof is completed by applying L3.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying L7.
Apply mul_SNo_minus_distrL with x1, x0, λ x2 x3 . x3 ∈ int_alt1 leaving 3 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L3.
Apply unknownprop_66d7a7b7f8768657be1ea35e52473cc5e1846e635153a280e3783a8275062773 with mul_SNo x1 x0.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with mul_SNo x1 x0.
Apply mul_SNo_In_omega with x1, x0 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H0.
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Claim L1: nat_p x0
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Claim L2: ordinal x0
Apply nat_p_ordinal with x0.
The subproof is completed by applying L1.
Claim L3: SNo x0
Apply ordinal_SNo with x0.
The subproof is completed by applying L2.
Apply unknownprop_2504c05a08587fe0873ed45685efc417625f0a904281d653d757d643896f9a70 with λ x1 . mul_SNo (minus_SNo x0) x1 ∈ int_alt1 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H4: x1 ∈ omega.
Claim L5: nat_p x1
Apply omega_nat_p with x1.
The subproof is completed by applying H4.
Claim L6: ordinal x1
Apply nat_p_ordinal with x1.
The subproof is completed by applying L5.
Claim L7: SNo x1
Apply ordinal_SNo with x1.
The subproof is completed by applying L6.
Apply mul_SNo_minus_distrL with x0, x1, λ x2 x3 . x3 ∈ int_alt1 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L7.
Apply unknownprop_66d7a7b7f8768657be1ea35e52473cc5e1846e635153a280e3783a8275062773 with mul_SNo x0 x1.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with mul_SNo x0 x1.
Apply mul_SNo_In_omega with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Assume H4: x1 ∈ omega.
Claim L5: nat_p x1
Apply omega_nat_p with x1.
The subproof is completed by applying H4.
Claim L6: ordinal x1
Apply nat_p_ordinal with x1.
The subproof is completed by applying L5.
Claim L7: SNo x1
Apply ordinal_SNo with x1.
The subproof is completed by applying L6.
Apply mul_SNo_minus_distrL with x0, minus_SNo x1, λ x2 x3 . x3 ∈ int_alt1 leaving 3 subgoals.
The subproof is completed by applying L3.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying L7.
Apply mul_SNo_com with x0, minus_SNo x1, λ x2 x3 . minus_SNo x3 ∈ int_alt1 leaving 3 subgoals.
The subproof is completed by applying L3.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying L7.
Apply mul_SNo_minus_distrL with x1, x0, λ x2 x3 . minus_SNo x3 ∈ int_alt1 leaving 3 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L3.
Apply minus_SNo_invol with mul_SNo x1 x0, λ x2 x3 . x3 ∈ int_alt1 leaving 2 subgoals.
Apply SNo_mul_SNo with x1, x0 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L3.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with mul_SNo x1 x0.
Apply mul_SNo_In_omega with x1, x0 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H0.
■