Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: int_lin_comb x0 x1 x2.
Assume H1: SNoLt 0 x2.
Assume H2: ∀ x3 . int_lin_comb x0 x1 x3 ⟶ SNoLt 0 x3 ⟶ SNoLe x2 x3.
Apply int_lin_comb_E with x0, x1, x2, divides_int x2 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H3: x0 ∈ int.
Assume H4: x1 ∈ int.
Assume H5: x2 ∈ int.
Let x3 of type ι be given.
Assume H6: x3 ∈ int.
Let x4 of type ι be given.
Assume H7: x4 ∈ int.
Assume H8: add_SNo (mul_SNo x3 x0) (mul_SNo x4 x1) = x2.
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
Apply quotient_remainder_int with x2, x0, divides_int x2 x0 leaving 3 subgoals.
Apply setminusI with omega, Sing 0, x2 leaving 2 subgoals.
Apply nat_p_omega with x2.
The subproof is completed by applying L13.
Assume H15: x2 ∈ Sing 0.
Apply SNoLt_irref with 0.
Apply SingE with 0, x2, λ x5 x6 . SNoLt 0 x5 leaving 2 subgoals.
The subproof is completed by applying H15.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Let x5 of type ι be given.
Assume H15: (λ x6 . and (x6 ∈ int) (∃ x7 . and (x7 ∈ x2) (x0 = add_SNo (mul_SNo x6 x2) x7))) x5.
Apply H15 with divides_int x2 x0.
Assume H16: x5 ∈ int.
Assume H17: ∃ x6 . and (x6 ∈ x2) (x0 = add_SNo (mul_SNo x5 x2) x6).
Apply H17 with divides_int x2 x0.
Let x6 of type ι be given.
Assume H18: (λ x7 . and (x7 ∈ x2) (x0 = add_SNo (mul_SNo x5 x2) x7)) x6.
Apply H18 with divides_int x2 x0.
Assume H19: x6 ∈ x2.
Assume H20: x0 = add_SNo (mul_SNo x5 x2) x6.
Claim L21: ...
...
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Apply and3I with x2 ∈ int, x0 ∈ int, ∃ x7 . and (x7 ∈ int) (mul_SNo x2 x7 = x0) leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H3.
Let x7 of type ο be given.
Assume H26: ∀ x8 . and (x8 ∈ int) (mul_SNo x2 x8 = x0) ⟶ x7.
Apply H26 with x5.
Apply andI with x5 ∈ int, mul_SNo x2 x5 = x0 leaving 2 subgoals.
The subproof is completed by applying H16.
Apply H20 with λ x8 x9 . mul_SNo x2 x5 = x9.
Apply SNoLeE with 0, x6, x6 = 0, λ x8 x9 . mul_SNo x2 x5 = add_SNo (mul_SNo x5 x2) x9 leaving 6 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L25.
Apply omega_nonneg with x6.
Apply nat_p_omega with x6.
The subproof is completed by applying L23.
Assume H27: SNoLt 0 x6.
Apply FalseE with x6 = 0.
Apply SNoLt_irref with x6.
Apply SNoLtLe_tra with x6, x2, x6 leaving 5 subgoals.
The subproof is completed by applying L25.
The subproof is completed by applying L14.
The subproof is completed by applying L25.
Apply ordinal_In_SNoLt with x2, x6 leaving 2 subgoals.
Apply nat_p_ordinal with x2.
The subproof is completed by applying L13.
The subproof is completed by applying H19.
Apply H2 with x6 leaving 2 subgoals.
Apply and4I with x0 ∈ int, x1 ∈ int, x6 ∈ int, ∃ x8 . and (x8 ∈ int) (∃ x9 . and (x9 ∈ int) (add_SNo (mul_SNo x8 x0) (mul_SNo x9 x1) = x6)) leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply Subq_omega_int with x6.
Apply nat_p_omega with x6.
The subproof is completed by applying L23.
Let x8 of type ο be given.
Assume H28: ∀ x9 . and (x9 ∈ int) (∃ x10 . and (x10 ∈ int) (add_SNo (mul_SNo x9 x0) (mul_SNo x10 x1) = x6)) ⟶ x8.
...
...
...
...
■