Let x0 of type ι be given.

Assume H0: nat_p x0.

Let x1 of type ι be given.

Assume H1: nat_p x1.

Apply unknownprop_6e151b9a51dc2ccfd71a98193c35cce693d1058fdc6a7b01e42e0782a75b29b2 with x1, λ x2 . mul_nat x0 x2 = 1 ⟶ and (x0 = 1) (x2 = 1) leaving 4 subgoals.

The subproof is completed by applying H1.

Apply mul_nat_0R with x0, λ x2 x3 . x3 = 1 ⟶ and (x0 = 1) (0 = 1).

Assume H2: 0 = 1.

Apply FalseE with and (x0 = 1) (0 = 1).

Apply neq_0_1.

The subproof is completed by applying H2.

Apply mul_nat_1R with x0, λ x2 x3 . x3 = 1 ⟶ and (x0 = 1) (1 = 1).

Assume H2: x0 = 1.

Apply andI with x0 = 1, 1 = 1 leaving 2 subgoals.

The subproof is completed by applying H2.

Let x2 of type ι → ι → ο be given.

Assume H3: x2 1 1.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H2: x2 ∈ setminus omega 2.

Apply setminusE with omega, 2, x2, (λ x3 . mul_nat x0 x3 = 1 ⟶ and (x0 = 1) (x3 = 1)) x2 leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H3: x2 ∈ omega.

Assume H4: nIn x2 2.

Claim L5: nat_p x2

Apply omega_nat_p with x2.

The subproof is completed by applying H3.

Claim L6: ∀ x3 . nat_p x3 ⟶ mul_nat x3 x2 = 1 ⟶ ∀ x4 : ο . x4

Let x3 of type ι be given.

Assume H6: nat_p x3.

Apply unknownprop_4dc51657821ef9793a5942e4da5b6631bdf7777ea8b0485605c5b11a0d0dabff with x3, λ x4 . mul_nat x4 x2 = 1 ⟶ ∀ x5 : ο . x5 leaving 3 subgoals.

The subproof is completed by applying H6.

Apply mul_nat_0L with x2, λ x4 x5 . x5 = 1 ⟶ ∀ x6 : ο . x6 leaving 2 subgoals.

The subproof is completed by applying L5.

The subproof is completed by applying neq_0_1.

Let x4 of type ι be given.

Assume H7: x4 ∈ setminus omega 1.

Apply unknownprop_e18849ea271b9fad1d1f55210e57a4e42a5b850b4f5bda4268b35baef08a0fd5 with x4, mul_nat x4 x2 = 1 ⟶ ∀ x5 : ο . x5 leaving 2 subgoals.

The subproof is completed by applying H7.

Let x5 of type ι be given.

Assume H8: x5 ∈ omega.

Assume H9: x4 = ordsucc x5.

Apply H9 with λ x6 x7 . mul_nat x7 x2 = 1 ⟶ ∀ x8 : ο . x8.

Apply mul_nat_SL with x5, x2, λ x6 x7 . x7 = 1 ⟶ ∀ x8 : ο . x8 leaving 3 subgoals.

Apply omega_nat_p with x5.

The subproof is completed by applying H8.

The subproof is completed by applying L5.

Apply unknownprop_9231c5823fa809fed9bf1ca5a2fc1ace2b76ed48a659fcd88b50f5e2f09a86ab with x2, add_nat (mul_nat x5 x2) x2 = 1 ⟶ ∀ x6 : ο . x6 leaving 2 subgoals.

The subproof is completed by applying H2.

Let x6 of type ι be given.

Assume H10: x6 ∈ omega.

Assume H11: x2 = ordsucc (ordsucc x6).

Apply H11 with λ x7 x8 . add_nat (mul_nat x5 x2) x8 = 1 ⟶ ∀ x9 : ο . x9.

Apply add_nat_SR with mul_nat x5 x2, ordsucc x6, λ x7 x8 . x8 = 1 ⟶ ∀ x9 : ο . x9 leaving 2 subgoals.

Apply nat_ordsucc with x6.

Apply omega_nat_p with x6.

The subproof is completed by applying H10.

Apply ordsucc_inj_contra with add_nat (mul_nat x5 x2) (ordsucc x6), 0.

Apply add_nat_SR with mul_nat x5 x2, x6, λ x7 x8 . x8 = 0 ⟶ ∀ x9 : ο . x9 leaving 2 subgoals.

Apply omega_nat_p with x6.

The subproof is completed by applying H10.

The subproof is completed by applying neq_ordsucc_0 with add_nat (mul_nat x5 x2) x6.

Assume H7: mul_nat x0 x2 = 1.

Apply FalseE with and (x0 = 1) (x2 = 1).

Apply L6 with x0 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H7.

■

Proofgold Proof