Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Let x1 of type ι be given.
Assume H1: x1 ∈ omega.
Assume H2: divides_int x0 x1.
Apply H2 with divides_nat x0 x1.
Assume H3: and (x0 ∈ int) (x1 ∈ int).
Assume H4: ∃ x2 . and (x2 ∈ int) (mul_SNo x0 x2 = x1).
Apply H4 with divides_nat x0 x1.
Let x2 of type ι be given.
Assume H5: (λ x3 . and (x3 ∈ int) (mul_SNo x0 x3 = x1)) x2.
Apply H5 with divides_nat x0 x1.
Assume H6: x2 ∈ int.
Assume H7: mul_SNo x0 x2 = x1.
Claim L8: ...
...
Claim L9: ...
...
Apply SNoLeE with 0, x0, divides_nat x0 x1 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L8.
Apply unknownprop_72fc13f59561a486e7f04b4e6ad6c40ec1d48eeac6e68c47cb50fa618c19e933 with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Assume H10: SNoLt 0 x0.
Claim L11: ∀ x3 . nat_p x3 ⟶ mul_SNo x0 (minus_SNo x3) = x1 ⟶ x3 = 0
Apply nat_inv_impred with λ x3 . mul_SNo x0 (minus_SNo x3) = x1 ⟶ x3 = 0 leaving 2 subgoals.
Assume H11: mul_SNo x0 (minus_SNo 0) = x1.
Let x3 of type ι → ι → ο be given.
Assume H12: x3 0 0.
The subproof is completed by applying H12.
Let x3 of type ι be given.
Assume H11: nat_p x3.
Claim L12: ...
...
Claim L13: ...
...
Apply ordinal_ordsucc_SNo_eq with x3, λ x4 x5 . mul_SNo x0 (minus_SNo x5) = x1 ⟶ x5 = 0 leaving 2 subgoals.
Apply nat_p_ordinal with x3.
The subproof is completed by applying H11.
Apply minus_add_SNo_distr with 1, x3, λ x4 x5 . mul_SNo x0 x5 = x1 ⟶ add_SNo 1 x3 = 0 leaving 3 subgoals.
The subproof is completed by applying SNo_1.
Apply nat_p_SNo with x3.
The subproof is completed by applying H11.
Apply mul_SNo_distrL with x0, minus_SNo 1, minus_SNo x3, λ x4 x5 . x5 = x1 ⟶ add_SNo 1 x3 = 0 leaving 4 subgoals.
The subproof is completed by applying L8.
Apply SNo_minus_SNo with 1.
The subproof is completed by applying SNo_1.
Apply SNo_minus_SNo with x3.
The subproof is completed by applying L12.
Apply mul_SNo_minus_distrR with x0, 1, λ x4 x5 . add_SNo x5 (mul_SNo x0 (minus_SNo ...)) = ... ⟶ add_SNo 1 x3 = 0 leaving 3 subgoals.
...
...
...
Claim L12: ∀ x3 . x3 ∈ int ⟶ mul_SNo x0 x3 = x1 ⟶ x3 ∈ omega
Apply int_SNo_cases with λ x3 . mul_SNo x0 x3 = x1 ⟶ x3 ∈ omega leaving 2 subgoals.
Let x3 of type ι be given.
Assume H12: x3 ∈ omega.
Assume H13: mul_SNo x0 x3 = x1.
The subproof is completed by applying H12.
Let x3 of type ι be given.
Assume H12: x3 ∈ omega.
Assume H13: mul_SNo x0 (minus_SNo x3) = x1.
Apply L11 with x3, λ x4 x5 . minus_SNo x5 ∈ omega leaving 3 subgoals.
Apply omega_nat_p with x3.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
Apply minus_SNo_0 with λ x4 x5 . x5 ∈ omega.
Apply nat_p_omega with 0.
The subproof is completed by applying nat_0.
Claim L13: x2 ∈ omega
Apply L12 with x2 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Apply and3I with x0 ∈ omega, x1 ∈ omega, ∃ x3 . and (x3 ∈ omega) (mul_nat x0 x3 = x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x3 of type ο be given.
Assume H14: ∀ x4 . and (x4 ∈ omega) (mul_nat x0 x4 = x1) ⟶ x3.
Apply H14 with x2.
Apply andI with x2 ∈ omega, mul_nat x0 x2 = x1 leaving 2 subgoals.
The subproof is completed by applying L13.
Apply mul_nat_mul_SNo with x0, x2, λ x4 x5 . x5 = x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L13.
The subproof is completed by applying H7.
...
■