Let a, b, c and p be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Assume Hbne: b ≠ 0.
Assume Hsign: same_sign_nonzero_R a b.
Assume HpL: p ∈ affine_line_R2 a b c.
We will prove {p} ∈ subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c).
We prove the intermediate claim HdefTL: subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c) = {U0 ∈ 𝒫 (affine_line_R2 a b c)|∃V0 ∈ (product_topology R R_lower_limit_topology R R_lower_limit_topology), U0 = V0 ∩ (affine_line_R2 a b c)}.
Use reflexivity.
rewrite the current goal using HdefTL (from left to right).
Apply (SepI (𝒫 (affine_line_R2 a b c)) (λU0 : set ⇒ ∃V0 ∈ (product_topology R R_lower_limit_topology R R_lower_limit_topology), U0 = V0 ∩ (affine_line_R2 a b c)) {p}) to the current goal.
Apply PowerI (affine_line_R2 a b c) {p} to the current goal.
Let q be given.
Assume Hq: q ∈ {p}.
We will prove q ∈ affine_line_R2 a b c.
We prove the intermediate claim Hqeq: q = p.
An exact proof term for the current goal is (SingE p q Hq).
rewrite the current goal using Hqeq (from left to right).
An exact proof term for the current goal is HpL.
We prove the intermediate claim HpRR: p ∈ setprod R R.
An exact proof term for the current goal is (affine_line_R2_subset_R2 a b c p HpL).
Set x to be the term p 0.
Set y to be the term p 1.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p HpRR).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) p HpRR).
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim HxReal: x ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
We prove the intermediate claim HyReal: y ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HyR.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxReal).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyReal).
Set x1 to be the term add_SNo x 1.
Set y1 to be the term add_SNo y 1.
We prove the intermediate claim Hx1Real: x1 ∈ real.
An exact proof term for the current goal is (real_add_SNo x HxReal 1 real_1).
We prove the intermediate claim Hy1Real: y1 ∈ real.
An exact proof term for the current goal is (real_add_SNo y HyReal 1 real_1).
We prove the intermediate claim Hx1R: x1 ∈ R.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hx1Real.
We prove the intermediate claim Hy1R: y1 ∈ R.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hy1Real.
We prove the intermediate claim Hx1def: x1 = add_SNo x 1.
Use reflexivity.
We prove the intermediate claim Hy1def: y1 = add_SNo y 1.
Use reflexivity.
We prove the intermediate claim Hxltx1: x < x1.
We will prove x < x1.
rewrite the current goal using Hx1def (from left to right).
We prove the intermediate claim H0S: SNo 0.
An exact proof term for the current goal is SNo_0.
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is SNo_1.
We prove the intermediate claim H0lt1: 0 < 1.
An exact proof term for the current goal is SNoLt_0_1.
We prove the intermediate claim Hx0ltx1: add_SNo x 0 < add_SNo x 1.
An exact proof term for the current goal is (add_SNo_Lt2 x 0 1 HxS H0S H1S H0lt1).
rewrite the current goal using (add_SNo_0R x HxS) (from right to left) at position 1.
An exact proof term for the current goal is Hx0ltx1.
We prove the intermediate claim Hylt1: y < y1.
We will prove y < y1.
rewrite the current goal using Hy1def (from left to right).
We prove the intermediate claim H0S: SNo 0.
An exact proof term for the current goal is SNo_0.
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is SNo_1.
We prove the intermediate claim H0lt1: 0 < 1.
An exact proof term for the current goal is SNoLt_0_1.
We prove the intermediate claim Hy0lty1: add_SNo y 0 < add_SNo y 1.
An exact proof term for the current goal is (add_SNo_Lt2 y 0 1 HyS H0S H1S H0lt1).
rewrite the current goal using (add_SNo_0R y HyS) (from right to left) at position 1.
An exact proof term for the current goal is Hy0lty1.
We prove the intermediate claim HRlt_x_x1: Rlt x x1.
An exact proof term for the current goal is (RltI x x1 HxR Hx1R Hxltx1).
We prove the intermediate claim HRlt_y_y1: Rlt y y1.
An exact proof term for the current goal is (RltI y y1 HyR Hy1R Hylt1).
Set U to be the term halfopen_interval_left x x1.
Set V to be the term halfopen_interval_left y y1.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (halfopen_interval_left_leftmem x x1 HRlt_x_x1).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (halfopen_interval_left_leftmem y y1 HRlt_y_y1).
We prove the intermediate claim HUinBasis: U ∈ R_lower_limit_basis.
We will prove U ∈ R_lower_limit_basis.
We prove the intermediate claim HUfam: U ∈ {halfopen_interval_left x b0|b0 ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ halfopen_interval_left x b0) x1 Hx1R).
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {halfopen_interval_left a0 b0|b0 ∈ R}) x U HxR HUfam).
We prove the intermediate claim HVinBasis: V ∈ R_lower_limit_basis.
We will prove V ∈ R_lower_limit_basis.
We prove the intermediate claim HVfam: V ∈ {halfopen_interval_left y b0|b0 ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ halfopen_interval_left y b0) y1 Hy1R).
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {halfopen_interval_left a0 b0|b0 ∈ R}) y V HyR HVfam).
We prove the intermediate claim HBasis: basis_on R R_lower_limit_basis.
An exact proof term for the current goal is R_lower_limit_basis_is_basis_local.
We prove the intermediate claim HUopen: U ∈ R_lower_limit_topology.
An exact proof term for the current goal is (generated_topology_contains_basis R R_lower_limit_basis HBasis U HUinBasis).
We prove the intermediate claim HVopen: V ∈ R_lower_limit_topology.
An exact proof term for the current goal is (generated_topology_contains_basis R R_lower_limit_basis HBasis V HVinBasis).
We prove the intermediate claim HWsub: rectangle_set U V ∈ product_subbasis R R_lower_limit_topology R R_lower_limit_topology.
We will prove rectangle_set U V ∈ product_subbasis R R_lower_limit_topology R R_lower_limit_topology.
We prove the intermediate claim HWV: rectangle_set U V ∈ {rectangle_set U V0|V0 ∈ R_lower_limit_topology}.
An exact proof term for the current goal is (ReplI R_lower_limit_topology (λV0 : set ⇒ rectangle_set U V0) V HVopen).
An exact proof term for the current goal is (famunionI R_lower_limit_topology (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ R_lower_limit_topology}) U (rectangle_set U V) HUopen HWV).
We prove the intermediate claim HBsub: basis_on (setprod R R) (product_subbasis R R_lower_limit_topology R R_lower_limit_topology).
An exact proof term for the current goal is (product_subbasis_is_basis R R_lower_limit_topology R R_lower_limit_topology R_lower_limit_topology_is_topology R_lower_limit_topology_is_topology).
We prove the intermediate claim HWopen: rectangle_set U V ∈ product_topology R R_lower_limit_topology R R_lower_limit_topology.
An exact proof term for the current goal is (generated_topology_contains_basis (setprod R R) (product_subbasis R R_lower_limit_topology R R_lower_limit_topology) HBsub (rectangle_set U V) HWsub).
We prove the intermediate claim HsingEq: {p} = (rectangle_set U V) ∩ affine_line_R2 a b c.
Apply set_ext to the current goal.
Let q be given.
Assume Hq: q ∈ {p}.
We will prove q ∈ (rectangle_set U V) ∩ affine_line_R2 a b c.
We prove the intermediate claim Hqeq: q = p.
An exact proof term for the current goal is (SingE p q Hq).
rewrite the current goal using Hqeq (from left to right).
Apply binintersectI to the current goal.
We prove the intermediate claim Hpeta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta R R p HpRR).
We prove the intermediate claim Hxdef: x = p 0.
Use reflexivity.
We prove the intermediate claim Hydef: y = p 1.
Use reflexivity.
We prove the intermediate claim Hp0U: p 0 ∈ U.
rewrite the current goal using Hxdef (from right to left).
An exact proof term for the current goal is HxU.
We prove the intermediate claim Hp1V: p 1 ∈ V.
rewrite the current goal using Hydef (from right to left).
An exact proof term for the current goal is HyV.
rewrite the current goal using Hpeta (from left to right) at position 1.
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U V (p 0) (p 1) Hp0U Hp1V).
An exact proof term for the current goal is HpL.
Let q be given.
Assume Hq: q ∈ (rectangle_set U V) ∩ affine_line_R2 a b c.
We will prove q ∈ {p}.
We prove the intermediate claim HqL: q ∈ affine_line_R2 a b c.
An exact proof term for the current goal is (binintersectE2 (rectangle_set U V) (affine_line_R2 a b c) q Hq).
We prove the intermediate claim HqW: q ∈ rectangle_set U V.
An exact proof term for the current goal is (binintersectE1 (rectangle_set U V) (affine_line_R2 a b c) q Hq).
We prove the intermediate claim HqUV: q ∈ setprod U V.
An exact proof term for the current goal is HqW.
Set qx to be the term q 0.
Set qy to be the term q 1.
We prove the intermediate claim HqRR: q ∈ setprod R R.
An exact proof term for the current goal is (affine_line_R2_subset_R2 a b c q HqL).
We prove the intermediate claim HqxR: qx ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) q HqRR).
We prove the intermediate claim HqyR: qy ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) q HqRR).
We prove the intermediate claim HqxS: SNo qx.
We prove the intermediate claim HqxReal: qx ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HqxR.
An exact proof term for the current goal is (real_SNo qx HqxReal).
We prove the intermediate claim HqyS: SNo qy.
We prove the intermediate claim HqyReal: qy ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HqyR.
An exact proof term for the current goal is (real_SNo qy HqyReal).
We prove the intermediate claim HqxU: qx ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λ_ : set ⇒ V) q HqUV).
We prove the intermediate claim HqyV: qy ∈ V.
An exact proof term for the current goal is (ap1_Sigma U (λ_ : set ⇒ V) q HqUV).
We prove the intermediate claim HqxCond: ¬ (Rlt qx x) ∧ Rlt qx x1.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t x) ∧ Rlt t x1) qx HqxU).
We prove the intermediate claim HqyCond: ¬ (Rlt qy y) ∧ Rlt qy y1.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t y) ∧ Rlt t y1) qy HqyV).
We prove the intermediate claim HnotRlt_qx_x: ¬ (Rlt qx x).
An exact proof term for the current goal is (andEL (¬ (Rlt qx x)) (Rlt qx x1) HqxCond).
We prove the intermediate claim HnotRlt_qy_y: ¬ (Rlt qy y).
An exact proof term for the current goal is (andEL (¬ (Rlt qy y)) (Rlt qy y1) HqyCond).
We prove the intermediate claim Hnotlt_qx_x: ¬ (qx < x).
Assume Hlt: qx < x.
Apply HnotRlt_qx_x to the current goal.
An exact proof term for the current goal is (RltI qx x HqxR HxR Hlt).
We prove the intermediate claim Hqeq: q = p.
Apply (SNoLt_trichotomy_or_impred qx x HqxS HxS (q = p)) to the current goal.
Assume Hqxlt: qx < x.
We will prove q = p.
Apply FalseE to the current goal.
Apply Hnotlt_qx_x to the current goal.
An exact proof term for the current goal is Hqxlt.
Assume HqxEq: qx = x.
We will prove q = p.
Set f to be the term affine_line_R2_param_by_x a b c.
We prove the intermediate claim Hpx: apply_fun f x = p.
We prove the intermediate claim Happ1p: apply_fun (projection1 R R) p = x.
rewrite the current goal using (projection1_apply R R p HpRR) (from left to right).
Use reflexivity.
rewrite the current goal using Happ1p (from right to left).
An exact proof term for the current goal is (affine_line_R2_param_by_x_after_projection1_on_line a b c p HaR HbR HcR Hbne HpL).
We prove the intermediate claim Hqpx: apply_fun f qx = q.
We prove the intermediate claim Happ1q: apply_fun (projection1 R R) q = qx.
rewrite the current goal using (projection1_apply R R q HqRR) (from left to right).
Use reflexivity.
rewrite the current goal using Happ1q (from right to left).
An exact proof term for the current goal is (affine_line_R2_param_by_x_after_projection1_on_line a b c q HaR HbR HcR Hbne HqL).
rewrite the current goal using Hqpx (from right to left).
rewrite the current goal using Hpx (from right to left).
rewrite the current goal using HqxEq (from left to right).
Use reflexivity.
Assume Hxlt: x < qx.
We will prove q = p.
Apply FalseE to the current goal.
Set f to be the term affine_line_R2_param_by_x a b c.
Set yx to be the term div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b.
Set yq to be the term div_SNo (add_SNo c (minus_SNo (mul_SNo a qx))) b.
We prove the intermediate claim Hyxdef: yx = div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b.
Use reflexivity.
We prove the intermediate claim Hyqdef: yq = div_SNo (add_SNo c (minus_SNo (mul_SNo a qx))) b.
Use reflexivity.
We prove the intermediate claim Hpx: apply_fun f x = p.
We prove the intermediate claim Happ1p: apply_fun (projection1 R R) p = x.
rewrite the current goal using (projection1_apply R R p HpRR) (from left to right).
Use reflexivity.
rewrite the current goal using Happ1p (from right to left).
An exact proof term for the current goal is (affine_line_R2_param_by_x_after_projection1_on_line a b c p HaR HbR HcR Hbne HpL).
We prove the intermediate claim Hqpx: apply_fun f qx = q.
We prove the intermediate claim Happ1q: apply_fun (projection1 R R) q = qx.
rewrite the current goal using (projection1_apply R R q HqRR) (from left to right).
Use reflexivity.
rewrite the current goal using Happ1q (from right to left).
An exact proof term for the current goal is (affine_line_R2_param_by_x_after_projection1_on_line a b c q HaR HbR HcR Hbne HqL).
We prove the intermediate claim Hpeta: p = (x,y).
An exact proof term for the current goal is (setprod_eta R R p HpRR).
We prove the intermediate claim Hqeta: q = (qx,qy).
An exact proof term for the current goal is (setprod_eta R R q HqRR).
We prove the intermediate claim HpairP: (x,yx) = (x,y).
We prove the intermediate claim Hfx: apply_fun f x = (x,yx).
rewrite the current goal using (affine_line_R2_param_by_x_apply a b c x HxR) (from left to right).
rewrite the current goal using Hyxdef (from right to left).
Use reflexivity.
rewrite the current goal using Hpeta (from right to left).
rewrite the current goal using Hfx (from right to left).
An exact proof term for the current goal is Hpx.
We prove the intermediate claim HyxEq: yx = y.
An exact proof term for the current goal is (andER (x = x) (yx = y) (tuple_eq_coords x yx x y HpairP)).
We prove the intermediate claim HpairQ: (qx,yq) = (qx,qy).
We prove the intermediate claim Hfq: apply_fun f qx = (qx,yq).
rewrite the current goal using (affine_line_R2_param_by_x_apply a b c qx HqxR) (from left to right).
rewrite the current goal using Hyqdef (from right to left).
Use reflexivity.
rewrite the current goal using Hqeta (from right to left).
rewrite the current goal using Hfq (from right to left).
An exact proof term for the current goal is Hqpx.
We prove the intermediate claim HyqEq: yq = qy.
An exact proof term for the current goal is (andER (qx = qx) (yq = qy) (tuple_eq_coords qx yq qx qy HpairQ)).
We prove the intermediate claim HRlt_x_qx: Rlt x qx.
An exact proof term for the current goal is (RltI x qx HxR HqxR Hxlt).
We prove the intermediate claim HRlt_yq_yx: Rlt yq yx.
An exact proof term for the current goal is (affine_line_R2_param_by_x_y_decreases_same_sign a b c x qx HaR HbR HcR Hbne Hsign HxR HqxR HRlt_x_qx).
We prove the intermediate claim Hbad: Rlt qy y.
rewrite the current goal using HyqEq (from right to left).
rewrite the current goal using HyxEq (from right to left).
An exact proof term for the current goal is HRlt_yq_yx.
Apply HnotRlt_qy_y to the current goal.
An exact proof term for the current goal is Hbad.
rewrite the current goal using Hqeq (from left to right).
An exact proof term for the current goal is (SingI p).
We use (rectangle_set U V) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HWopen.
An exact proof term for the current goal is HsingEq.
∎