Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: prime_nat x0.
Assume H1: prime_nat x1.
Assume H2: divides_int x0 x1.
Apply H0 with x0 = x1.
Assume H3: and (x0 ∈ omega) (1 ∈ x0).
Apply H3 with (∀ x2 . x2 ∈ omega ⟶ divides_nat x2 x0 ⟶ or (x2 = 1) (x2 = x0)) ⟶ x0 = x1.
Assume H4: x0 ∈ omega.
Assume H5: 1 ∈ x0.
Assume H6: ∀ x2 . x2 ∈ omega ⟶ divides_nat x2 x0 ⟶ or (x2 = 1) (x2 = x0).
Apply H1 with x0 = x1.
Assume H7: and (x1 ∈ omega) (1 ∈ x1).
Apply H7 with (∀ x2 . x2 ∈ omega ⟶ divides_nat x2 x1 ⟶ or (x2 = 1) (x2 = x1)) ⟶ x0 = x1.
Assume H8: x1 ∈ omega.
Assume H9: 1 ∈ x1.
Assume H10: ∀ x2 . x2 ∈ omega ⟶ divides_nat x2 x1 ⟶ or (x2 = 1) (x2 = x1).
Apply H10 with x0, x0 = x1 leaving 4 subgoals.
The subproof is completed by applying H4.
Apply divides_int_divides_nat with x0, x1 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
The subproof is completed by applying H2.
Assume H11: x0 = 1.
Apply FalseE with x0 = x1.
Apply In_irref with x0.
Apply H11 with λ x2 x3 . x3 ∈ x0.
The subproof is completed by applying H5.
Assume H11: x0 = x1.
The subproof is completed by applying H11.
■