Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιι be given.
Apply nat_ind with λ x1 . (∀ x2 . x2x1nat_p (x0 x2))∀ x2 . x2x1divides_nat (x0 x2) (Pi_nat x0 x1) leaving 2 subgoals.
Assume H0: ∀ x1 . x10nat_p (x0 x1).
Let x1 of type ι be given.
Assume H1: x10.
Apply FalseE with divides_nat (x0 x1) (Pi_nat x0 0).
Apply EmptyE with x1.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H0: nat_p x1.
Assume H1: (∀ x2 . x2x1nat_p (x0 x2))∀ x2 . x2x1divides_nat (x0 x2) (Pi_nat x0 x1).
Assume H2: ∀ x2 . x2ordsucc x1nat_p (x0 x2).
Claim L3: ∀ x2 . x2x1nat_p (x0 x2)
Let x2 of type ι be given.
Assume H3: x2x1.
Apply H2 with x2.
Apply ordsuccI1 with x1, x2.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H4: x2ordsucc x1.
Apply Pi_nat_S with x0, x1, λ x3 x4 . divides_nat (x0 x2) x4 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordsuccE with x1, x2, divides_nat (x0 x2) (mul_nat (Pi_nat x0 x1) (x0 x1)) leaving 3 subgoals.
The subproof is completed by applying H4.
Assume H5: x2x1.
Apply unknownprop_f799b99d854d7bca6941dc7751c0c00a5bf29ac2d7e070aa318a7a7ed9ce8fa0 with x0 x2, Pi_nat x0 x1, mul_nat (Pi_nat x0 x1) (x0 x1) leaving 2 subgoals.
Apply H1 with x2 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H5.
Apply divides_nat_mulR with Pi_nat x0 x1, x0 x1 leaving 2 subgoals.
Apply nat_p_omega with Pi_nat x0 x1.
Apply Pi_nat_p with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply nat_p_omega with x0 x1.
Apply H2 with x1.
The subproof is completed by applying ordsuccI2 with x1.
Assume H5: x2 = x1.
Apply H5 with λ x3 x4 . divides_nat (x0 x4) (mul_nat (Pi_nat x0 x1) (x0 x1)).
Apply divides_nat_mulL with Pi_nat x0 x1, x0 x1 leaving 2 subgoals.
Apply nat_p_omega with Pi_nat x0 x1.
Apply Pi_nat_p with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply nat_p_omega with x0 x1.
Apply H2 with x1.
The subproof is completed by applying ordsuccI2 with x1.