Apply H1 to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Let f be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim L1:
∀i ∈ n, nat_p (f i).
Let i be given.
Assume Hi.
An
exact proof term for the current goal is
SepE1 ω prime_nat (f i) (Hf1 i Hi).
We prove the intermediate
claim L2:
0 ∉ primes.
Assume H _.
Apply H to the current goal.
Assume _.
We prove the intermediate
claim LPN:
nat_p (Pi_nat f n).
We prove the intermediate
claim LpN:
nat_p p.
An exact proof term for the current goal is LPN.
We prove the intermediate
claim Lpo:
p ∈ ω.
An exact proof term for the current goal is LpN.
Let q be given.
We prove the intermediate
claim LqP:
q ∈ primes.
Apply Hq to the current goal.
Assume H _.
Apply H to the current goal.
Assume _.
An
exact proof term for the current goal is
SepI ω prime_nat q Hqo Hq.
Apply Hf3 q LqP to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim LfiP:
f i ∈ primes.
An exact proof term for the current goal is Hf1 i Hi.
Apply H5 to the current goal.
Assume H.
Apply H to the current goal.
Assume _.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is Hqp.
We prove the intermediate
claim L1p:
1 ∈ p.
An exact proof term for the current goal is H3.
We prove the intermediate
claim LP0:
Pi_nat f n = 0.
Let i be given.
Assume H.
Apply H to the current goal.
Apply L2 to the current goal.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hf1 i Hi.
We prove the intermediate
claim LpP:
prime_nat p.
Apply and3I to the current goal.
An exact proof term for the current goal is Lpo.
An exact proof term for the current goal is L1p.
Let k be given.
We will
prove k = 1 ∨ k = p.
Apply orIL to the current goal.
Let q be given.
Assume H.
Apply H to the current goal.
Apply L3 q Hq to the current goal.
Apply Hkp to the current goal.
Assume _ H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim Lp0:
p = 0.
Use transitivity with and
k * m.
Use symmetry.
An exact proof term for the current goal is Hkm.
rewrite the current goal using H4 (from left to right).
rewrite the current goal using Lp0 (from right to left) at position 2.
An exact proof term for the current goal is L1p.
An exact proof term for the current goal is H4.
Apply L3 p LpP to the current goal.
An exact proof term for the current goal is LpN.
∎