Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_ind with λ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ nat_p (x1 x2)) ⟶ ∀ x2 . x2 ∈ x0 ⟶ divides_nat (x1 x2) (nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) x0) leaving 2 subgoals.
Let x0 of type ι → ι be given.
Assume H0: ∀ x1 . x1 ∈ 0 ⟶ nat_p (x0 x1).
Let x1 of type ι be given.
Assume H1: x1 ∈ 0.
Apply FalseE with divides_nat (x0 x1) (nat_primrec 1 (λ x2 x3 . mul_nat (x0 x2) x3) 0).
Apply EmptyE with x1.
The subproof is completed by applying H1.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ nat_p (x1 x2)) ⟶ ∀ x2 . x2 ∈ x0 ⟶ divides_nat (x1 x2) (nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) x0).
Let x1 of type ι → ι be given.
Assume H2: ∀ x2 . x2 ∈ ordsucc x0 ⟶ nat_p (x1 x2).
Let x2 of type ι be given.
Assume H3: x2 ∈ ordsucc x0.
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Apply ordsuccE with x0, x2, divides_nat (x1 x2) (nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) (ordsucc x0)) leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H8: x2 ∈ x0.
Apply unknownprop_f799b99d854d7bca6941dc7751c0c00a5bf29ac2d7e070aa318a7a7ed9ce8fa0 with x1 x2, nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) x0, nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) (ordsucc x0) leaving 2 subgoals.
Apply H1 with x1, x2 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H8.
Apply and3I with nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) x0 ∈ omega, nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) (ordsucc x0) ∈ omega, ∃ x3 . and (x3 ∈ omega) (mul_nat (nat_primrec 1 (λ x4 x5 . mul_nat (x1 x4) x5) x0) x3 = nat_primrec 1 (λ x4 x5 . mul_nat (x1 x4) x5) (ordsucc x0)) leaving 3 subgoals.
Apply nat_p_omega with nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) x0.
The subproof is completed by applying L6.
Apply nat_p_omega with nat_primrec 1 (λ x3 x4 . mul_nat (x1 x3) x4) (ordsucc x0).
Apply unknownprop_6acf4d775f3657f6657248067c81d93f75e7e3c111f6937130fc5b44c841c89f with ordsucc x0, x1 leaving 2 subgoals.
Apply nat_ordsucc with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Let x3 of type ο be given.
Assume H9: ∀ x4 . and (x4 ∈ omega) (mul_nat (nat_primrec 1 (λ x5 x6 . mul_nat (x1 x5) x6) x0) x4 = nat_primrec 1 (λ x5 x6 . mul_nat (x1 x5) x6) (ordsucc x0)) ⟶ x3.
Apply H9 with x1 x0.
Apply andI with x1 x0 ∈ omega, mul_nat (nat_primrec 1 (λ x4 x5 . mul_nat (x1 x4) x5) x0) (x1 x0) = nat_primrec 1 (λ x4 x5 . mul_nat (x1 x4) x5) (ordsucc x0) leaving 2 subgoals.
Apply nat_p_omega with x1 x0.
The subproof is completed by applying L5.
Apply mul_nat_com with nat_primrec 1 (λ x4 x5 . mul_nat (x1 x4) x5) ..., ..., ... leaving 3 subgoals.
...
...
...
...
■