| pf |
|---|
Apply setminusI with real, rational, sqrt_SNo_nonneg 2 leaving 2 subgoals.
Apply sqrt_SNo_nonneg_real with 2 leaving 2 subgoals.
Apply SNoS_omega_real with 2.
Apply omega_SNoS_omega with 2.
Apply nat_p_omega with 2.
The subproof is completed by applying nat_2.
Apply SNoLtLe with 0, 2.
The subproof is completed by applying SNoLt_0_2.
Apply SepE with real, λ x0 . ∃ x1 . and (x1 ∈ int) (∃ x2 . and (x2 ∈ setminus omega (Sing 0)) (x0 = div_SNo x1 x2)), sqrt_SNo_nonneg 2, False leaving 2 subgoals.
The subproof is completed by applying H0.
Apply H2 with False.
Let x0 of type ι be given.
Apply H3 with False.
Apply H5 with False.
Let x1 of type ι be given.
Apply H6 with False.
Apply int_3_cases with x0, False leaving 4 subgoals.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Apply SNoLt_irref with 0.
Apply SNoLeLt_tra with 0, sqrt_SNo_nonneg 2, 0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L11.
The subproof is completed by applying SNo_0.
Apply sqrt_SNo_nonneg_nonneg with 2 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply SNoLtLe with 0, 2.
The subproof is completed by applying SNoLt_0_2.
Apply H8 with λ x3 x4 . SNoLt x4 0.
Apply div_SNo_neg_pos with x0, x1 leaving 4 subgoals.
Apply int_SNo with x0.
The subproof is completed by applying H4.
The subproof is completed by applying L10.
Apply H16 with λ x3 x4 . SNoLt x4 0.
Apply minus_SNo_Lt_contra1 with 0, ordsucc x2 leaving 3 subgoals.
The subproof is completed by applying SNo_0.
Apply omega_SNo with ordsucc x2.
Apply omega_ordsucc with x2.
The subproof is completed by applying H15.
Apply minus_SNo_0 with λ x3 x4 . SNoLt x4 (ordsucc x2).
Apply ordinal_ordsucc_SNo_eq with x2, λ x3 x4 . SNoLt 0 x4 leaving 2 subgoals.
Apply nat_p_ordinal with x2.
Apply omega_nat_p with x2.
The subproof is completed by applying H15.
Apply SNoLtLe_tra with 0, 1, add_SNo 1 x2 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_1.
Apply SNo_add_SNo with 1, x2 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply omega_SNo with x2.
The subproof is completed by applying H15.
The subproof is completed by applying SNoLt_0_1.
Apply add_SNo_0R with 1, λ x3 x4 . SNoLe x3 (add_SNo 1 x2) leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply add_SNo_Le2 with 1, 0, x2 leaving 4 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_0.
Apply omega_SNo with x2.
The subproof is completed by applying H15.
Apply omega_nonneg with x2.
The subproof is completed by applying H15.
The subproof is completed by applying L13.
Assume H15: x0 = 0.
Apply SNoLt_irref with 0.
Apply L14 with λ x2 x3 . x2 = 0, λ x2 x3 . SNoLt 0 x2 leaving 2 subgoals.
Apply H15 with λ x2 x3 . mul_SNo (sqrt_SNo_nonneg 2) x1 = x2, λ x2 x3 . mul_SNo x3 x3 = 0 leaving 2 subgoals.
The subproof is completed by applying L12.
Apply mul_SNo_zeroR with 0.
The subproof is completed by applying SNo_0.
Apply mul_SNo_pos_pos with 2, mul_SNo x1 x1 leaving 4 subgoals.
The subproof is completed by applying SNo_2.
Apply SNo_mul_SNo with x1, x1 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L10.
The subproof is completed by applying SNoLt_0_2.
Apply mul_SNo_pos_pos with x1, x1 leaving 4 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L10.
The subproof is completed by applying L13.
The subproof is completed by applying L13.
Let x2 of type ι be given.
Apply form100_1_v1 with x0, x1 leaving 3 subgoals.
Apply setminusI with omega, 1, x0 leaving 2 subgoals.
The subproof is completed by applying L17.
Assume H18: x0 ∈ 1.
Apply neq_ordsucc_0 with x2.
Apply H16 with λ x3 x4 . x3 = 0.
■ |
|