Assume H1: finite primes.
Apply H1 to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω.
Assume H2: equip primes n.
Apply equip_sym primes n H2 to the current goal.
Let f be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hf1: ∀i ∈ n, f i ∈ primes.
Assume Hf2: ∀i j ∈ n, f i = f j → i = j.
Assume Hf3: ∀p ∈ primes, ∃i ∈ n, f i = p.
Set p to be the term ordsucc (Pi_nat f n).
We prove the intermediate claim L1: ∀i ∈ n, nat_p (f i).
Let i be given.
Assume Hi.
Apply omega_nat_p to the current goal.
We will prove f i ∈ ω.
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 H1: 0 ∈ primes.
Apply SepE2 ω prime_nat 0 H1 to the current goal.
Assume H _.
Apply H to the current goal.
Assume _.
Assume H2: 1 ∈ 0.
An exact proof term for the current goal is In_no2cycle 1 0 H2 In_0_1.
We prove the intermediate claim LPN: nat_p (Pi_nat f n).
An exact proof term for the current goal is Pi_nat_p f n (omega_nat_p n Hn) L1.
We prove the intermediate claim LpN: nat_p p.
Apply nat_ordsucc to the current goal.
An exact proof term for the current goal is LPN.
We prove the intermediate claim Lpo: p ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is LpN.
We prove the intermediate claim L3: ∀q, prime_nat q → ¬ divides_nat q p.
Let q be given.
Assume Hq: prime_nat q.
Assume Hqp: divides_nat q p.
We prove the intermediate claim LqP: q ∈ primes.
Apply Hq to the current goal.
Assume H _.
Apply H to the current goal.
Assume Hqo: q ∈ ω.
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.
Assume Hi: i ∈ n.
Assume H3: f i = q.
We prove the intermediate claim LfiP: f i ∈ primes.
An exact proof term for the current goal is Hf1 i Hi.
Apply SepE ω prime_nat (f i) LfiP to the current goal.
Assume H4: f i ∈ ω.
Assume H5: prime_nat (f i).
Apply H5 to the current goal.
Assume H.
Apply H to the current goal.
Assume _.
Assume H6: 1 ∈ f i.
Assume H7: ∀k ∈ ω, divides_nat k (f i) → k = 1 ∨ k = f i.
Apply nat_1In_not_divides_ordsucc (f i) (Pi_nat f n) H6 to the current goal.
We will prove divides_nat (f i) (Pi_nat f n).
An exact proof term for the current goal is Pi_nat_divides f n (omega_nat_p n Hn) L1 i Hi.
We will prove divides_nat (f i) p.
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.
We will prove 1 ∈ ordsucc (Pi_nat f n).
Apply nat_ordsucc_in_ordsucc (Pi_nat f n) LPN to the current goal.
We will prove 0 ∈ Pi_nat f n.
Apply ordinal_In_Or_Subq 0 (Pi_nat f n) ordinal_Empty (nat_p_ordinal (Pi_nat f n) LPN) to the current goal.
Assume H3: 0 ∈ Pi_nat f n.
An exact proof term for the current goal is H3.
Assume H3: Pi_nat f n ⊆ 0.
We prove the intermediate claim LP0: Pi_nat f n = 0.
An exact proof term for the current goal is Empty_Subq_eq (Pi_nat f n) H3.
Apply Pi_nat_0_inv f n (omega_nat_p n Hn) L1 LP0 to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ n.
Assume H4: f i = 0.
Apply L2 to the current goal.
We will prove 0 ∈ primes.
rewrite the current goal using H4 (from right to left).
We will prove f i ∈ primes.
An exact proof term for the current goal is Hf1 i Hi.
We prove the intermediate claim LpP: prime_nat p.
We will prove prime_nat p.
We will prove p ∈ ω ∧ 1 ∈ p ∧ ∀k ∈ ω, divides_nat k p → k = 1 ∨ k = 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.
Assume Hk: k ∈ ω.
Assume Hkp: divides_nat k p.
We will prove k = 1 ∨ k = p.
Apply orIL to the current goal.
We will prove k = 1.
Apply ordinal_In_Or_Subq 1 k (nat_p_ordinal 1 nat_1) (nat_p_ordinal k (omega_nat_p k Hk)) to the current goal.
Assume H3: 1 ∈ k.
Apply prime_nat_divisor_ex k (omega_nat_p k Hk) H3 to the current goal.
Let q be given.
Assume H.
Apply H to the current goal.
Assume Hq: prime_nat q.
Assume Hqk: divides_nat q k.
Apply L3 q Hq to the current goal.
We will prove divides_nat q p.
An exact proof term for the current goal is divides_nat_tra q k p Hqk Hkp.
Assume H3: k ⊆ 1.
Apply nat_le1_cases k (omega_nat_p k Hk) H3 to the current goal.
Assume H4: k = 0.
We will prove False.
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.
Assume Hm: m ∈ ω.
Assume Hkm: k * m = p.
We prove the intermediate claim Lp0: p = 0.
Use transitivity with and k * m.
We will prove p = k * m.
Use symmetry.
An exact proof term for the current goal is Hkm.
We will prove k * m = 0.
rewrite the current goal using H4 (from left to right).
We will prove 0 * m = 0.
An exact proof term for the current goal is mul_nat_0L m (omega_nat_p m Hm).
Apply In_no2cycle 0 1 In_0_1 to the current goal.
We will prove 1 ∈ 0.
rewrite the current goal using Lp0 (from right to left) at position 2.
An exact proof term for the current goal is L1p.
Assume H4: k = 1.
An exact proof term for the current goal is H4.
Apply L3 p LpP to the current goal.
We will prove divides_nat p p.
Apply divides_nat_ref to the current goal.
An exact proof term for the current goal is LpN.
∎