Search for blocks/addresses/...

Proofgold Proof

pf
Apply int_SNo_cases with λ x0 . ∀ x1 . x1 ∈ int ⟶ mul_SNo x0 x1 ∈ int leaving 2 subgoals.
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Apply int_SNo_cases with λ x1 . mul_SNo x0 x1 ∈ int leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1: x1 ∈ omega.
Apply Subq_omega_int 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 H1.
Let x1 of type ι be given.
Assume H1: x1 ∈ omega.
Apply mul_SNo_com with x0, minus_SNo x1, λ x2 x3 . x3 ∈ int leaving 3 subgoals.
Apply ordinal_SNo with x0.
Apply nat_p_ordinal with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with x1.
Apply ordinal_SNo with x1.
Apply nat_p_ordinal with x1.
Apply omega_nat_p with x1.
The subproof is completed by applying H1.
Apply mul_SNo_minus_distrL with x1, x0, λ x2 x3 . x3 ∈ int leaving 3 subgoals.
Apply ordinal_SNo with x1.
Apply nat_p_ordinal with x1.
Apply omega_nat_p with x1.
The subproof is completed by applying H1.
Apply ordinal_SNo with x0.
Apply nat_p_ordinal with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Apply int_minus_SNo with mul_SNo x1 x0.
Apply Subq_omega_int with mul_SNo x1 x0.
Apply mul_SNo_In_omega with x1, x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Claim L1: SNo x0
Apply ordinal_SNo with x0.
Apply nat_p_ordinal with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Apply int_SNo_cases with λ x1 . mul_SNo (minus_SNo x0) x1 ∈ int leaving 2 subgoals.
Let x1 of type ι be given.
Assume H2: x1 ∈ omega.
Apply mul_SNo_minus_distrL with x0, x1, λ x2 x3 . x3 ∈ int leaving 3 subgoals.
The subproof is completed by applying L1.
Apply ordinal_SNo with x1.
Apply nat_p_ordinal with x1.
Apply omega_nat_p with x1.
The subproof is completed by applying H2.
Apply int_minus_SNo with mul_SNo x0 x1.
Apply Subq_omega_int 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 H2.
Let x1 of type ι be given.
Assume H2: x1 ∈ omega.
Claim L3: SNo x1
Apply ordinal_SNo with x1.
Apply nat_p_ordinal with x1.
Apply omega_nat_p with x1.
The subproof is completed by applying H2.
Apply mul_SNo_minus_distrL with x0, minus_SNo x1, λ x2 x3 . x3 ∈ int leaving 3 subgoals.
The subproof is completed by applying L1.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying L3.
Apply mul_SNo_com with x0, minus_SNo x1, λ x2 x3 . minus_SNo x3 ∈ int leaving 3 subgoals.
The subproof is completed by applying L1.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying L3.
Apply mul_SNo_minus_distrL with x1, x0, λ x2 x3 . minus_SNo x3 ∈ int leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L1.
Apply minus_SNo_invol with mul_SNo x1 x0, λ x2 x3 . x3 ∈ int leaving 2 subgoals.
Apply SNo_mul_SNo with x1, x0 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L1.
Apply Subq_omega_int with mul_SNo x1 x0.
Apply mul_SNo_In_omega with x1, x0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
■