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 0 x0 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: x0 ∈ omega.
Assume H2: nIn x0 (Sing 0).
Apply gcd_id with x0, gcd_reln 0 x0 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H3: and (divides_int x0 x0) (divides_int x0 x0).
Apply H3 with (∀ x1 . divides_int x1 x0 ⟶ divides_int x1 x0 ⟶ SNoLe x1 x0) ⟶ gcd_reln 0 x0 x0.
Assume H4: divides_int x0 x0.
Assume H5: divides_int x0 x0.
Assume H6: ∀ x1 . divides_int x1 x0 ⟶ divides_int x1 x0 ⟶ SNoLe x1 x0.
Apply and3I with divides_int x0 0, divides_int x0 x0, ∀ x1 . divides_int x1 0 ⟶ divides_int x1 x0 ⟶ SNoLe x1 x0 leaving 3 subgoals.
Apply divides_int_0 with x0.
Apply Subq_omega_int with x0.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Assume H7: divides_int x1 0.
Assume H8: divides_int x1 x0.
Apply H6 with x1 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H8.
■