Metamath Proof Explorer

Theorem sqrtrrnpoly

Description: Real square root is not a polynomial with real coefficients, because its value is imaginary for negative arguments. (Contributed by Ender Ting, 22-Jul-2026)

Ref Expression
Assertion sqrtrrnpoly ⊢ ¬ √ ∈ Poly ⁡ ℝ

Proof

Step Hyp Ref Expression
1 neg1rr ⊢ − 1 ∈ ℝ
2 fvres ⊢ − 1 ∈ ℝ → √ ↾ ℝ ⁡ − 1 = − 1
3 1 2 ax-mp ⊢ √ ↾ ℝ ⁡ − 1 = − 1
4 sqrtm1 ⊢ i = − 1
5 4 eqcomi ⊢ − 1 = i
6 inelr ⊢ ¬ i ∈ ℝ
7 5 6 eqneltri ⊢ ¬ − 1 ∈ ℝ
8 3 7 eqneltri ⊢ ¬ √ ↾ ℝ ⁡ − 1 ∈ ℝ
9 ffvelcdm ⊢ √ ↾ ℝ : ℝ ⟶ ℝ ∧ − 1 ∈ ℝ → √ ↾ ℝ ⁡ − 1 ∈ ℝ
10 1 9 mpan2 ⊢ √ ↾ ℝ : ℝ ⟶ ℝ → √ ↾ ℝ ⁡ − 1 ∈ ℝ
11 8 10 mto ⊢ ¬ √ ↾ ℝ : ℝ ⟶ ℝ
12 plyreres ⊢ √ ∈ Poly ⁡ ℝ → √ ↾ ℝ : ℝ ⟶ ℝ
13 11 12 mto ⊢ ¬ √ ∈ Poly ⁡ ℝ