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	|- -. sqrt e. ( Poly ` RR )

Proof

Step	Hyp	Ref	Expression
1		neg1rr	|- -u 1 e. RR
2		fvres	|- ( -u 1 e. RR -> ( ( sqrt |` RR ) ` -u 1 ) = ( sqrt ` -u 1 ) )
3	1 2	ax-mp	|- ( ( sqrt |` RR ) ` -u 1 ) = ( sqrt ` -u 1 )
4		sqrtm1	|- _i = ( sqrt ` -u 1 )
5	4	eqcomi	|- ( sqrt ` -u 1 ) = _i
6		inelr	|- -. _i e. RR
7	5 6	eqneltri	|- -. ( sqrt ` -u 1 ) e. RR
8	3 7	eqneltri	|- -. ( ( sqrt |` RR ) ` -u 1 ) e. RR
9		ffvelcdm	|- ( ( ( sqrt |` RR ) : RR --> RR /\ -u 1 e. RR ) -> ( ( sqrt |` RR ) ` -u 1 ) e. RR )
10	1 9	mpan2	|- ( ( sqrt |` RR ) : RR --> RR -> ( ( sqrt |` RR ) ` -u 1 ) e. RR )
11	8 10	mto	|- -. ( sqrt |` RR ) : RR --> RR
12		plyreres	|- ( sqrt e. ( Poly ` RR ) -> ( sqrt |` RR ) : RR --> RR )
13	11 12	mto	|- -. sqrt e. ( Poly ` RR )