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: equiv_nat_mod x0 x1 x2.
Apply H0 with 6ccc6.. x0 x1 x2.
Assume H1: and (and (x0 ∈ omega) (x1 ∈ omega)) (x2 ∈ setminus omega 1).
Apply H1 with or (∃ x3 . and (x3 ∈ omega) (add_nat x0 (mul_nat x3 x2) = x1)) (∃ x3 . and (x3 ∈ omega) (add_nat x1 (mul_nat x3 x2) = x0)) ⟶ 6ccc6.. x0 x1 x2.
Assume H2: and (x0 ∈ omega) (x1 ∈ omega).
Apply H2 with x2 ∈ setminus omega 1 ⟶ or (∃ x3 . and (x3 ∈ omega) (add_nat x0 (mul_nat x3 x2) = x1)) (∃ x3 . and (x3 ∈ omega) (add_nat x1 (mul_nat x3 x2) = x0)) ⟶ 6ccc6.. x0 x1 x2.
Assume H3: x0 ∈ omega.
Assume H4: x1 ∈ omega.
Assume H5: x2 ∈ setminus omega 1.
Assume H6: or (∃ x3 . and (x3 ∈ omega) (add_nat x0 (mul_nat x3 x2) = x1)) (∃ x3 . and (x3 ∈ omega) (add_nat x1 (mul_nat x3 x2) = x0)).
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Apply and4I with x0 ∈ int_alt1, x1 ∈ int_alt1, x2 ∈ setminus omega 1, divides_int_alt1 x2 (add_SNo x0 (minus_SNo x1)) leaving 4 subgoals.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with x0.
The subproof is completed by applying H3.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with x1.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply and3I with x2 ∈ int_alt1, add_SNo x0 (minus_SNo x1) ∈ int_alt1, ∃ x3 . and (x3 ∈ int_alt1) (mul_SNo x2 x3 = add_SNo x0 (minus_SNo x1)) leaving 3 subgoals.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with x2.
The subproof is completed by applying L9.
Apply unknownprop_02609f82bf442d61fb8c6410818e7e4cbf8c67c9ea08bffcbf8a77c06b0f784a with x0, minus_SNo x1 leaving 2 subgoals.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with x0.
The subproof is completed by applying H3.
Apply unknownprop_66d7a7b7f8768657be1ea35e52473cc5e1846e635153a280e3783a8275062773 with x1.
Apply unknownprop_c213ff287d87049b1e6a47a232f87c366800922741a9eeadb1d3ac2fbadaf052 with x1.
The subproof is completed by applying H4.
Apply H6 with ∃ x3 . and (x3 ∈ int_alt1) (mul_SNo x2 x3 = add_SNo x0 (minus_SNo x1)) leaving 2 subgoals.
Assume H11: ∃ x3 . and (x3 ∈ omega) (add_nat x0 (mul_nat x3 x2) = x1).
Apply H11 with ∃ x3 . and (x3 ∈ int_alt1) (mul_SNo x2 x3 = add_SNo x0 (minus_SNo x1)).
Let x3 of type ι be given.
Assume H12: (λ x4 . and (x4 ∈ omega) (add_nat x0 (mul_nat x4 x2) = x1)) x3.
Apply H12 with ∃ x4 . and (x4 ∈ int_alt1) (mul_SNo x2 x4 = add_SNo x0 (minus_SNo x1)).
Assume H13: x3 ∈ omega.
Apply mul_nat_mul_SNo with x3, x2, λ x4 x5 . add_nat x0 x5 = x1 ⟶ ∃ x6 . and (x6 ∈ int_alt1) (mul_SNo x2 x6 = add_SNo x0 (minus_SNo x1)) leaving 3 subgoals.
The subproof is completed by applying H13.
The subproof is completed by applying L9.
Apply add_nat_add_SNo with x0, ..., ... leaving 3 subgoals.
...
...
...
...
■