Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: divides_int x0 x1.
Assume H1: SNoLt 0 x1.
Apply H0 with SNoLe x0 x1.
Assume H2: and (x0 ∈ int) (x1 ∈ int).
Assume H3: ∃ x2 . and (x2 ∈ int) (mul_SNo x0 x2 = x1).
Apply H2 with SNoLe x0 x1.
Assume H4: x0 ∈ int.
Assume H5: x1 ∈ int.
Apply int_SNo_cases with λ x2 . divides_int x2 x1 ⟶ SNoLe x2 x1, x0 leaving 4 subgoals.
Let x2 of type ι be given.
Assume H6: x2 ∈ omega.
Assume H7: divides_int x2 x1.
Apply H7 with SNoLe x2 x1.
Assume H8: and (x2 ∈ int) (x1 ∈ int).
Assume H9: ∃ x3 . and (x3 ∈ int) (mul_SNo x2 x3 = x1).
Apply H9 with SNoLe x2 x1.
Let x3 of type ι be given.
Assume H10: (λ x4 . and (x4 ∈ int) (mul_SNo x2 x4 = x1)) x3.
Apply H10 with SNoLe x2 x1.
Assume H11: x3 ∈ int.
Assume H12: mul_SNo x2 x3 = x1.
Claim L13: SNo x2
Apply omega_SNo with x2.
The subproof is completed by applying H6.
Claim L14: SNo x3
Apply int_SNo with x3.
The subproof is completed by applying H11.
Apply H12 with λ x4 x5 . SNoLe x2 x4.
Apply mul_SNo_oneR with x2, λ x4 x5 . SNoLe x4 (mul_SNo x2 x3) leaving 2 subgoals.
The subproof is completed by applying L13.
Apply nonneg_mul_SNo_Le with x2, 1, x3 leaving 5 subgoals.
The subproof is completed by applying L13.
Apply omega_nonneg with x2.
The subproof is completed by applying H6.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L14.
Apply SNoLtLe_or with x3, 1, SNoLe 1 x3 leaving 4 subgoals.
The subproof is completed by applying L14.
The subproof is completed by applying SNo_1.
Assume H15: SNoLt x3 1.
Apply FalseE with SNoLe 1 x3.
Apply SNoLt_irref with x1.
Apply H12 with λ x4 x5 . SNoLt x4 x1.
Apply SNoLeLt_tra with mul_SNo x2 x3, 0, x1 leaving 5 subgoals.
Apply SNo_mul_SNo with x2, x3 leaving 2 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
The subproof is completed by applying SNo_0.
Apply int_SNo with x1.
The subproof is completed by applying H5.
Apply mul_SNo_com with x2, x3, λ x4 x5 . SNoLe x5 0 leaving 3 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
Apply mul_SNo_nonpos_nonneg with x3, x2 leaving 4 subgoals.
The subproof is completed by applying L14.
The subproof is completed by applying L13.
Apply SNoLtLe_or with 0, x3, SNoLe x3 0 leaving 4 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L14.
Assume H16: SNoLt 0 x3.
Apply FalseE with SNoLe x3 0.
Claim L17: nat_p x3
Apply unknownprop_17e526dd107b435f5416528d1c977ef8aa1ea06ba09d8b9ed0ca53424a454f1a with x3 leaving 2 subgoals.
The subproof is completed by applying H11.
Apply SNoLtLe with 0, x3.
The subproof is completed by applying H16.
Apply SNoLt_irref with x3.
Apply SNoLtLe_tra with x3, 1, x3 leaving 5 subgoals.
The subproof is completed by applying L14.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L14.
The subproof is completed by applying H15.
Apply ordinal_Subq_SNoLe with 1, x3 leaving 3 subgoals.
Apply ordinal_ordsucc with 0.
The subproof is completed by applying ordinal_Empty.
Apply nat_p_ordinal with x3.
The subproof is completed by applying L17.
Apply ordinal_ordsucc_In_Subq with x3, 0 leaving 2 subgoals.
Apply nat_p_ordinal with x3.
The subproof is completed by applying L17.
Apply ordinal_SNoLt_In with 0, x3 leaving 3 subgoals.
The subproof is completed by applying ordinal_Empty.
Apply nat_p_ordinal with x3.
The subproof is completed by applying L17.
The subproof is completed by applying H16.
Assume H16: SNoLe x3 0.
The subproof is completed by applying H16.
Apply omega_nonneg with x2.
The subproof is completed by applying H6.
The subproof is completed by applying H1.
Assume H15: SNoLe 1 x3.
The subproof is completed by applying H15.
Let x2 of type ι be given.
Assume H6: x2 ∈ omega.
Assume H7: divides_int (minus_SNo x2) x1.
Apply SNoLe_tra with minus_SNo x2, 0, x1 leaving 5 subgoals.
Apply SNo_minus_SNo with x2.
Apply omega_SNo with x2.
The subproof is completed by applying H6.
The subproof is completed by applying SNo_0.
Apply int_SNo with x1.
The subproof is completed by applying H5.
Apply minus_SNo_0 with λ x3 x4 . SNoLe (minus_SNo x2) x3.
Apply minus_SNo_Le_contra with 0, x2 leaving 3 subgoals.
The subproof is completed by applying SNo_0.
Apply omega_SNo with x2.
The subproof is completed by applying H6.
Apply omega_nonneg with x2.
The subproof is completed by applying H6.
Apply SNoLtLe with 0, x1.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H0.
■