I want to rewrite the following proposition in mathematical language (and by mathematical language I mean symbols such as: $\forall , \exists, (, ), \implies$ and so on).
Proposition: Every non-trivial quadratic equation with real coefficients and whose determinant is positive has two different solutions.
My attempt: $$\forall a, b, c,x\in\mathbb{R}\exists y=ax^2+bx+c\left[\left(a\neq 0~ \land ~b^2-4ac>0\right)\implies\left(x=\frac{-b\pm\sqrt{b^2-4ac}}{2a}\right)\right]$$
I think this might be wrong but that is what I have done so far. In case my attempt is wrong, then how can I solve it? Thanks in advance
It should be written as follows.
$$\forall a, b, c,x\in\mathbb{R}\left[ \begin{array}{l} \left(ax^2+bx+c=0\wedge a\neq 0 \wedge b^2-4ac>0\right)\implies\\ \exists x_1\in\mathbb{R}\exists x_2\in\mathbb{R}(x_1\neq x_2 \wedge a{x_1}^2+bx_1+c=0\wedge a{x_2}^2+bx_2+c=0) \end{array} \right].$$
More accurately, it should be written as follows where $(\mathbb{R},+,\cdot,0)$ is a first order structure.
$$(\mathbb{R},+,\cdot,0)\vDash\forall a, b, c\left[ \begin{array}{l} \left(ax^2+bx+c=0\wedge a\neq 0 \wedge b^2-4ac>0\right)\implies\\ \exists x_1\exists x_2(x_1\neq x_2 \wedge a{x_1}^2+bx_1+c=0\wedge a{x_2}^2+bx_2+c=0) \end{array} \right].$$