Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: x0 ⊆ real.

Assume H1: x1 ⊆ real.

Assume H2: x2 ∈ real.

Let x3 of type ι be given.

Assume H3: x3 ∈ famunion x0 (λ x4 . {div_SNo (add_SNo x2 (mul_SNo x4 x5)) (add_SNo x4 x5)|x5 ∈ x1,SNoLt 0 (add_SNo x4 x5)}).

Apply famunionE_impred with x0, λ x4 . {div_SNo (add_SNo x2 (mul_SNo x4 x5)) (add_SNo x4 x5)|x5 ∈ x1,SNoLt 0 (add_SNo x4 x5)}, x3, x3 ∈ real leaving 2 subgoals.

The subproof is completed by applying H3.

Let x4 of type ι be given.

Assume H4: x4 ∈ x0.

Assume H5: x3 ∈ {div_SNo (add_SNo x2 (mul_SNo x4 x5)) (add_SNo x4 x5)|x5 ∈ x1,SNoLt 0 (add_SNo x4 x5)}.

Apply ReplSepE_impred with x1, λ x5 . SNoLt 0 (add_SNo x4 x5), λ x5 . div_SNo (add_SNo x2 (mul_SNo x4 x5)) (add_SNo x4 x5), x3, x3 ∈ real leaving 2 subgoals.

The subproof is completed by applying H5.

Let x5 of type ι be given.

Assume H6: x5 ∈ x1.

Assume H7: SNoLt 0 (add_SNo x4 x5).

Assume H8: x3 = div_SNo (add_SNo x2 (mul_SNo x4 x5)) (add_SNo x4 x5).

Apply H8 with λ x6 x7 . x7 ∈ real.

Apply real_div_SNo with add_SNo x2 (mul_SNo x4 x5), add_SNo x4 x5 leaving 2 subgoals.

Apply real_add_SNo with x2, mul_SNo x4 x5 leaving 2 subgoals.

The subproof is completed by applying H2.

Apply real_mul_SNo with x4, x5 leaving 2 subgoals.

Apply H0 with x4.

The subproof is completed by applying H4.

Apply H1 with x5.

The subproof is completed by applying H6.

Apply real_add_SNo with x4, x5 leaving 2 subgoals.

Apply H0 with x4.

The subproof is completed by applying H4.

Apply H1 with x5.

The subproof is completed by applying H6.

■

Proofgold Proof