Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Assume H1: prime_nat x0.
Assume H2: b3e62.. x0 1 4.
Apply unknownprop_19a26ef39c10368cbf6a4da444f473007201f73a30e6058e59b44809197f519a with x0, ∃ x1 . and (x1 ∈ omega) (∃ x2 . and (x2 ∈ omega) (x0 = add_nat (mul_nat x1 x1) (mul_nat x2 x2))) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Assume H3: (λ x2 . and (x2 ∈ omega) (∃ x3 . and (x3 ∈ omega) (x0 = add_SNo (mul_SNo x2 x2) (mul_SNo x3 x3)))) x1.
Apply H3 with ∃ x2 . and (x2 ∈ omega) (∃ x3 . and (x3 ∈ omega) (x0 = add_nat (mul_nat x2 x2) (mul_nat x3 x3))).
Assume H4: x1 ∈ omega.
Assume H5: ∃ x2 . and (x2 ∈ omega) (x0 = add_SNo (mul_SNo x1 x1) (mul_SNo x2 x2)).
Apply H5 with ∃ x2 . and (x2 ∈ omega) (∃ x3 . and (x3 ∈ omega) (x0 = add_nat (mul_nat x2 x2) (mul_nat x3 x3))).
Let x2 of type ι be given.
Assume H6: (λ x3 . and (x3 ∈ omega) (x0 = add_SNo (mul_SNo x1 x1) (mul_SNo x3 x3))) x2.
Apply H6 with ∃ x3 . and (x3 ∈ omega) (∃ x4 . and (x4 ∈ omega) (x0 = add_nat (mul_nat x3 x3) (mul_nat x4 x4))).
Assume H7: x2 ∈ omega.
Assume H8: x0 = add_SNo (mul_SNo x1 x1) (mul_SNo x2 x2).
Let x3 of type ο be given.
Assume H9: ∀ x4 . and (x4 ∈ omega) (∃ x5 . and (x5 ∈ omega) (x0 = add_nat (mul_nat x4 x4) (mul_nat x5 x5))) ⟶ x3.
Apply H9 with x1.
Apply andI with x1 ∈ omega, ∃ x4 . and (x4 ∈ omega) (x0 = add_nat (mul_nat x1 x1) (mul_nat x4 x4)) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x4 of type ο be given.
Assume H10: ∀ x5 . and (x5 ∈ omega) (x0 = add_nat (mul_nat x1 x1) (mul_nat x5 x5)) ⟶ x4.
Apply H10 with x2.
Apply andI with x2 ∈ omega, x0 = add_nat (mul_nat x1 x1) (mul_nat x2 x2) leaving 2 subgoals.
The subproof is completed by applying H7.
Apply mul_nat_mul_SNo with x1, x1, λ x5 x6 . x0 = add_nat x6 (mul_nat x2 x2) leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H4.
Apply mul_nat_mul_SNo with x2, x2, λ x5 x6 . x0 = add_nat (mul_SNo x1 x1) x6 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H7.
Apply add_nat_add_SNo with mul_SNo x1 x1, mul_SNo x2 x2, λ x5 x6 . x0 = x6 leaving 3 subgoals.
Apply mul_SNo_In_omega with x1, x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H4.
Apply mul_SNo_In_omega with x2, x2 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
■