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 ‘ ℝ )