Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ setminus omega (Sing 0).
Apply setminusE with omega, Sing 0, x0, gcd_reln x0 x0 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: x0 ∈ omega.
Assume H2: nIn x0 (Sing 0).
Claim L3: ...
...
Claim L4: ...
...
Claim L5: SNoLt 0 x0
Apply SNoLeE with 0, x0, SNoLt 0 x0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L4.
Apply omega_nonneg with x0.
The subproof is completed by applying H1.
Assume H5: SNoLt 0 x0.
The subproof is completed by applying H5.
...
Apply and3I with divides_int x0 x0, divides_int x0 x0, ∀ x1 . divides_int x1 x0 ⟶ divides_int x1 x0 ⟶ SNoLe x1 x0 leaving 3 subgoals.
Apply divides_int_ref with x0.
The subproof is completed by applying L3.
Apply divides_int_ref with x0.
The subproof is completed by applying L3.
Let x1 of type ι be given.
Assume H6: divides_int x1 x0.
Assume H7: divides_int x1 x0.
Apply H6 with SNoLe x1 x0.
Assume H8: and (x1 ∈ int) (x0 ∈ int).
Apply H8 with (∃ x2 . and (x2 ∈ int) (mul_SNo x1 x2 = x0)) ⟶ SNoLe x1 x0.
Assume H9: x1 ∈ int.
Assume H10: x0 ∈ int.
Assume H11: ∃ x2 . and (x2 ∈ int) (mul_SNo x1 x2 = x0).
Apply H11 with SNoLe x1 x0.
Let x2 of type ι be given.
Assume H12: (λ x3 . and (x3 ∈ int) (mul_SNo x1 x3 = x0)) x2.
Apply H12 with SNoLe x1 x0.
Assume H13: x2 ∈ int.
Assume H14: mul_SNo x1 x2 = x0.
Claim L15: SNo x1
Apply int_SNo with x1.
The subproof is completed by applying H9.
Apply SNoLtLe_or with 0, x1, SNoLe x1 x0 leaving 4 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L15.
Assume H16: SNoLt 0 x1.
Apply SNoLtLe_or with x2, 0, SNoLe x1 x0 leaving 4 subgoals.
Apply int_SNo with x2.
The subproof is completed by applying H13.
The subproof is completed by applying SNo_0.
Assume H17: SNoLt x2 0.
Apply FalseE with SNoLe x1 x0.
Apply SNoLt_irref with x0.
Apply SNoLt_tra with x0, 0, x0 leaving 5 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L4.
Apply H14 with λ x3 x4 . SNoLt x3 0.
Apply mul_SNo_pos_neg with x1, x2 leaving 4 subgoals.
The subproof is completed by applying L15.
Apply int_SNo with x2.
The subproof is completed by applying H13.
The subproof is completed by applying H16.
The subproof is completed by applying H17.
The subproof is completed by applying L5.
Assume H17: SNoLe 0 x2.
Claim L18: nat_p x2
Apply unknownprop_17e526dd107b435f5416528d1c977ef8aa1ea06ba09d8b9ed0ca53424a454f1a with x2 leaving 2 subgoals.
The subproof is completed by applying H13.
The subproof is completed by applying H17.
Claim L19: nat_p x1
Apply unknownprop_17e526dd107b435f5416528d1c977ef8aa1ea06ba09d8b9ed0ca53424a454f1a with x1 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply SNoLtLe with 0, x1.
The subproof is completed by applying H16.
Apply unknownprop_bdf0eb0ad914e7080c1a90c10a5be5aadacffe01a001ae1e9b4568b2273272d9 with x1, x2, SNoLe x1 x0 leaving 4 subgoals.
The subproof is completed by applying L19.
The subproof is completed by applying L18.
Assume H20: x2 = 0.
Apply FalseE with SNoLe x1 x0.
Apply SNoLt_irref with x0.
Apply H14 with λ x3 x4 . SNoLt x3 x0.
Apply H20 with λ x3 x4 . SNoLt (mul_SNo x1 x4) x0.
Apply mul_SNo_zeroR with x1, λ x3 x4 . SNoLt x4 x0 leaving 2 subgoals.
The subproof is completed by applying L15.
The subproof is completed by applying L5.
Assume H20: x1 ⊆ mul_nat x1 x2.
Apply H14 with λ x3 x4 . SNoLe x1 x3.
Apply mul_nat_mul_SNo with x1, x2, λ x3 x4 . SNoLe x1 x3 leaving 3 subgoals.
Apply nat_p_omega with x1.
The subproof is completed by applying L19.
Apply nat_p_omega with x2.
The subproof is completed by applying L18.
Apply ordinal_Subq_SNoLe with x1, mul_nat x1 x2 leaving 3 subgoals.
Apply nat_p_ordinal with x1.
The subproof is completed by applying L19.
Apply nat_p_ordinal with mul_nat x1 x2.
Apply mul_nat_p with x1, x2 leaving 2 subgoals.
The subproof is completed by applying L19.
The subproof is completed by applying L18.
The subproof is completed by applying H20.
Assume H16: SNoLe x1 0.
Apply SNoLe_tra with x1, 0, x0 leaving 5 subgoals.
The subproof is completed by applying L15.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L4.
The subproof is completed by applying H16.
Apply SNoLtLe with 0, x0.
The subproof is completed by applying L5.
■