We prove the intermediate claim LS2R: sqrt_SNo_nonneg 2 ∈ real.
We will prove sqrt_SNo_nonneg 2 ∈ real.
Apply sqrt_SNo_nonneg_real 2 to the current goal.
We will prove 2 ∈ real.
Apply SNoS_omega_real to the current goal.
We will prove 2 ∈ SNoS_ ω.
Apply omega_SNoS_omega to the current goal.
We will prove 2 ∈ ω.
An exact proof term for the current goal is nat_p_omega 2 nat_2.
We will prove 0 ≤ 2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_0_2.
We prove the intermediate claim LS2: SNo (sqrt_SNo_nonneg 2).
Apply real_SNo to the current goal.
An exact proof term for the current goal is LS2R.
We prove the intermediate claim LS2nn: 0 ≤ sqrt_SNo_nonneg 2.
Apply sqrt_SNo_nonneg_nonneg to the current goal.
An exact proof term for the current goal is SNo_2.
We will prove 0 ≤ 2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_0_2.
We prove the intermediate claim LS2pos: 0 < sqrt_SNo_nonneg 2.
Apply SNoLeE 0 (sqrt_SNo_nonneg 2) SNo_0 LS2 LS2nn to the current goal.
Assume H1: 0 < sqrt_SNo_nonneg 2.
An exact proof term for the current goal is H1.
Assume H1: 0 = sqrt_SNo_nonneg 2.
We will prove False.
Apply neq_0_2 to the current goal.
We will prove 0 = 2.
rewrite the current goal using sqrt_SNo_nonneg_sqr 2 SNo_2 (SNoLtLe 0 2 SNoLt_0_2) (from right to left).
We will prove 0 = sqrt_SNo_nonneg 2 * sqrt_SNo_nonneg 2.
rewrite the current goal using H1 (from right to left).
We will prove 0 = 0 * 0.
Use symmetry.
An exact proof term for the current goal is mul_SNo_zeroR 0 SNo_0.
Apply setminusI to the current goal.
We will prove sqrt_SNo_nonneg 2 ∈ real.
An exact proof term for the current goal is LS2R.
Assume H1: sqrt_SNo_nonneg 2 ∈ rational.
Apply SepE real (λx ⇒ ∃m ∈ int, ∃n ∈ ω ∖ {0}, x = m :/: n) (sqrt_SNo_nonneg 2) H1 to the current goal.
Assume H2: sqrt_SNo_nonneg 2 ∈ real.
Assume H3: ∃m ∈ int, ∃n ∈ ω ∖ {0}, sqrt_SNo_nonneg 2 = m :/: n.
We prove the intermediate claim LnQ: ∀m ∈ int, ∀n ∈ ω ∖ {0}, sqrt_SNo_nonneg 2 ≠ m :/: n.
Apply int_SNo_cases to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Let n be given.
Assume Hn: n ∈ ω ∖ {0}.
Assume H4: sqrt_SNo_nonneg 2 = m :/: n.
We will prove False.
Apply setminusE ω {0} n Hn to the current goal.
Assume Hn1: n ∈ ω.
Assume Hn2: n ∉ {0}.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is omega_SNo m Hm.
We prove the intermediate claim LnN: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn1.
We prove the intermediate claim Ln1: n ∈ ω ∖ 1.
rewrite the current goal using eq_1_Sing0 (from left to right).
An exact proof term for the current goal is Hn.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is omega_SNo n Hn1.
Apply form100_1_lem2 m Hm n Ln1 to the current goal.
We will prove m * m = 2 * n * n.
We prove the intermediate claim L1: sqrt_SNo_nonneg 2 * n = m.
rewrite the current goal using H4 (from left to right).
We will prove (m :/: n) * n = m.
Apply mul_div_SNo_invL to the current goal.
We will prove SNo m.
An exact proof term for the current goal is LmS.
We will prove SNo n.
An exact proof term for the current goal is LnS.
We will prove n ≠ 0.
Assume Hn0: n = 0.
Apply Hn2 to the current goal.
We will prove n ∈ {0}.
rewrite the current goal using Hn0 (from left to right).
Apply SingI to the current goal.
rewrite the current goal using L1 (from right to left).
We will prove (sqrt_SNo_nonneg 2 * n) * (sqrt_SNo_nonneg 2 * n) = 2 * (n * n).
rewrite the current goal using mul_SNo_com_4_inner_mid (sqrt_SNo_nonneg 2) n (sqrt_SNo_nonneg 2) n LS2 LnS LS2 LnS (from left to right).
We will prove (sqrt_SNo_nonneg 2 * sqrt_SNo_nonneg 2) * (n * n) = 2 * (n * n).
Use f_equal.
We will prove sqrt_SNo_nonneg 2 * sqrt_SNo_nonneg 2 = 2.
Apply sqrt_SNo_nonneg_sqr to the current goal.
We will prove SNo 2.
An exact proof term for the current goal is SNo_2.
We will prove 0 ≤ 2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_0_2.
Let m be given.
Assume Hm: m ∈ ω.
Let n be given.
Assume Hn: n ∈ ω ∖ {0}.
Assume H4: sqrt_SNo_nonneg 2 = (- m) :/: n.
We will prove False.
Apply setminusE ω {0} n Hn to the current goal.
Assume Hn1: n ∈ ω.
Assume Hn2: n ∉ {0}.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is omega_SNo m Hm.
We prove the intermediate claim Lmnn: 0 ≤ m.
An exact proof term for the current goal is omega_nonneg m Hm.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is omega_SNo n Hn1.
We prove the intermediate claim Lnnn: 0 ≤ n.
An exact proof term for the current goal is omega_nonneg n Hn1.
We prove the intermediate claim Lnpos: 0 < n.
Apply SNoLeE 0 n SNo_0 LnS Lnnn to the current goal.
Assume H5: 0 < n.
An exact proof term for the current goal is H5.
Assume H5: 0 = n.
We will prove False.
Apply Hn2 to the current goal.
We will prove n ∈ {0}.
rewrite the current goal using H5 (from right to left).
Apply SingI to the current goal.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
Apply SNoLtLe_tra 0 (sqrt_SNo_nonneg 2) 0 SNo_0 LS2 SNo_0 LS2pos to the current goal.
We will prove sqrt_SNo_nonneg 2 ≤ 0.
rewrite the current goal using H4 (from left to right).
We will prove (- m) :/: n ≤ 0.
Apply SNoLeE 0 m SNo_0 LmS Lmnn to the current goal.
Assume H5: 0 < m.
Apply SNoLtLe to the current goal.
Apply div_SNo_neg_pos (- m) n (SNo_minus_SNo m LmS) LnS to the current goal.
We will prove - m < 0.
Apply minus_SNo_Lt_contra1 0 m SNo_0 LmS to the current goal.
We will prove - 0 < m.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is H5.
We will prove 0 < n.
An exact proof term for the current goal is Lnpos.
Assume H5: 0 = m.
rewrite the current goal using H5 (from right to left).
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using div_SNo_0_num n LnS (from left to right).
We will prove 0 ≤ 0.
Apply SNoLe_ref to the current goal.
Apply H3 to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω ∖ {0}.
Assume H4: sqrt_SNo_nonneg 2 = m :/: n.
An exact proof term for the current goal is LnQ m Hm n Hn H4.
∎