Theorem 25or6to4

Description: Question 67 of 68 from a lecture Prof. Loof Lirpa held last Saturday in Lincoln Park. When asked why the smaller root wasn't reduced to 3/2, Lirpa responded "It really doesn't matter anyhow." (Contributed by Luke Murphy, 10-Jul-2026)

	Ref	Expression
Hypotheses	25or6to4.a	$$⊢\phi \to A=1$$
	25or6to4.b	$$⊢\phi \to B=-\frac{53}{2}$$
	25or6to4.c	$$⊢\phi \to C=\frac{75}{2}$$
	25or6to4.x	$$⊢\phi \to X\in ℂ$$
Assertion	25or6to4	$$⊢\phi \to \left(A{X}^2+BX+C=0\leftrightarrow \left(X=25\vee X=\frac{6}{4}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		25or6to4.a	$$⊢\phi \to A=1$$
2		25or6to4.b	$$⊢\phi \to B=-\frac{53}{2}$$
3		25or6to4.c	$$⊢\phi \to C=\frac{75}{2}$$
4		25or6to4.x	$$⊢\phi \to X\in ℂ$$
5		ax-1cn	$$⊢1\in ℂ$$
6	1 5	eqeltrdi	$$⊢\phi \to A\in ℂ$$
7		ax-1ne0	$$⊢1\ne 0$$
8	7	a1i	$$⊢\phi \to 1\ne 0$$
9	1 8	eqnetrd	$$⊢\phi \to A\ne 0$$
10		df-dec	$$⊢53=\left(9+1\right)\cdot 5+3$$
11		9cn	$$⊢9\in ℂ$$
12	11 5	addcli	$$⊢9+1\in ℂ$$
13		5cn	$$⊢5\in ℂ$$
14	12 13	mulcli	$$⊢\left(9+1\right)\cdot 5\in ℂ$$
15		3cn	$$⊢3\in ℂ$$
16	14 15	addcli	$$⊢\left(9+1\right)\cdot 5+3\in ℂ$$
17	10 16	eqeltri	$$⊢53\in ℂ$$
18		2cn	$$⊢2\in ℂ$$
19		2ne0	$$⊢2\ne 0$$
20	17 18 19	divcli	$$⊢\frac{53}{2}\in ℂ$$
21	20	negcli	$$⊢-\frac{53}{2}\in ℂ$$
22	2 21	eqeltrdi	$$⊢\phi \to B\in ℂ$$
23		df-dec	$$⊢75=\left(9+1\right)\cdot 7+5$$
24		7cn	$$⊢7\in ℂ$$
25	12 24	mulcli	$$⊢\left(9+1\right)\cdot 7\in ℂ$$
26	25 13	addcli	$$⊢\left(9+1\right)\cdot 7+5\in ℂ$$
27	23 26	eqeltri	$$⊢75\in ℂ$$
28	27 18 19	divcli	$$⊢\frac{75}{2}\in ℂ$$
29	3 28	eqeltrdi	$$⊢\phi \to C\in ℂ$$
30		df-dec	$$⊢25=\left(9+1\right)\cdot 2+5$$
31	12 18	mulcli	$$⊢\left(9+1\right)\cdot 2\in ℂ$$
32	31 13	addcli	$$⊢\left(9+1\right)\cdot 2+5\in ℂ$$
33	30 32	eqeltri	$$⊢25\in ℂ$$
34	33	a1i	$$⊢\phi \to 25\in ℂ$$
35		6cn	$$⊢6\in ℂ$$
36		4cn	$$⊢4\in ℂ$$
37		4ne0	$$⊢4\ne 0$$
38	35 36 37	divcli	$$⊢\frac{6}{4}\in ℂ$$
39	38	a1i	$$⊢\phi \to \frac{6}{4}\in ℂ$$
40	33 18 19	divcan4i	$$⊢\frac{25\cdot 2}{2}=25$$
41		2nn0	$$⊢2\in {\mathbb{N}}_0$$
42		5nn0	$$⊢5\in {\mathbb{N}}_0$$
43		eqid	$$⊢25=25$$
44		0nn0	$$⊢0\in {\mathbb{N}}_0$$
45		1nn0	$$⊢1\in {\mathbb{N}}_0$$
46		2t2e4	$$⊢2\cdot 2=4$$
47	46	oveq1i	$$⊢2\cdot 2+1=4+1$$
48		4p1e5	$$⊢4+1=5$$
49	47 48	eqtri	$$⊢2\cdot 2+1=5$$
50		5t2e10	$$⊢5\cdot 2=10$$
51	41 41 42 43 44 45 49 50	decmul1c	$$⊢25\cdot 2=50$$
52	51	oveq1i	$$⊢\frac{25\cdot 2}{2}=\frac{50}{2}$$
53	40 52	eqtr3i	$$⊢25=\frac{50}{2}$$
54		6t2e12	$$⊢6\cdot 2=12$$
55		4t3e12	$$⊢4\cdot 3=12$$
56	36 15 55	mulcomli	$$⊢3\cdot 4=12$$
57	54 56	eqtr4i	$$⊢6\cdot 2=3\cdot 4$$
58	35 15	pm3.2i	$$⊢\left(6\in ℂ\wedge 3\in ℂ\right)$$
59	36 37	pm3.2i	$$⊢\left(4\in ℂ\wedge 4\ne 0\right)$$
60		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
61	59 60	pm3.2i	$$⊢\left(\left(4\in ℂ\wedge 4\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)$$
62	58 61	pm3.2i	$$⊢\left(\left(6\in ℂ\wedge 3\in ℂ\right)\wedge \left(\left(4\in ℂ\wedge 4\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\right)$$
63		divmuleq	$$⊢\left(\left(6\in ℂ\wedge 3\in ℂ\right)\wedge \left(\left(4\in ℂ\wedge 4\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\right)\to \left(\frac{6}{4}=\frac{3}{2}\leftrightarrow 6\cdot 2=3\cdot 4\right)$$
64	62 63	ax-mp	$$⊢\frac{6}{4}=\frac{3}{2}\leftrightarrow 6\cdot 2=3\cdot 4$$
65	57 64	mpbir	$$⊢\frac{6}{4}=\frac{3}{2}$$
66	53 65	oveq12i	$$⊢25+\left(\frac{6}{4}\right)=\left(\frac{50}{2}\right)+\left(\frac{3}{2}\right)$$
67		dfdec10	$$⊢53=10\cdot 5+3$$
68	42	dec0u	$$⊢10\cdot 5=50$$
69	68	oveq1i	$$⊢10\cdot 5+3=50+3$$
70	67 69	eqtri	$$⊢53=50+3$$
71	70	oveq1i	$$⊢\frac{53}{2}=\frac{50+3}{2}$$
72		df-dec	$$⊢50=\left(9+1\right)\cdot 5+0$$
73		0cn	$$⊢0\in ℂ$$
74	14 73	addcli	$$⊢\left(9+1\right)\cdot 5+0\in ℂ$$
75	72 74	eqeltri	$$⊢50\in ℂ$$
76	75 15 18 19	divdiri	$$⊢\frac{50+3}{2}=\left(\frac{50}{2}\right)+\left(\frac{3}{2}\right)$$
77	71 76	eqtri	$$⊢\frac{53}{2}=\left(\frac{50}{2}\right)+\left(\frac{3}{2}\right)$$
78	66 77	eqtr4i	$$⊢25+\left(\frac{6}{4}\right)=\frac{53}{2}$$
79	78 20	eqeltri	$$⊢25+\left(\frac{6}{4}\right)\in ℂ$$
80	79	negnegi	$$⊢-\left(-\left(25+\left(\frac{6}{4}\right)\right)\right)=25+\left(\frac{6}{4}\right)$$
81	78	negeqi	$$⊢-\left(25+\left(\frac{6}{4}\right)\right)=-\frac{53}{2}$$
82	21	div1i	$$⊢\frac{-\frac{53}{2}}{1}=-\frac{53}{2}$$
83	81 82	eqtr4i	$$⊢-\left(25+\left(\frac{6}{4}\right)\right)=\frac{-\frac{53}{2}}{1}$$
84	83	negeqi	$$⊢-\left(-\left(25+\left(\frac{6}{4}\right)\right)\right)=-\frac{-\frac{53}{2}}{1}$$
85	80 84	eqtr3i	$$⊢25+\left(\frac{6}{4}\right)=-\frac{-\frac{53}{2}}{1}$$
86	2 1	oveq12d	$$⊢\phi \to \frac{B}{A}=\frac{-\frac{53}{2}}{1}$$
87	86	negeqd	$$⊢\phi \to -\frac{B}{A}=-\frac{-\frac{53}{2}}{1}$$
88	85 87	eqtr4id	$$⊢\phi \to 25+\left(\frac{6}{4}\right)=-\frac{B}{A}$$
89	28	div1i	$$⊢\frac{\frac{75}{2}}{1}=\frac{75}{2}$$
90	33 15 18 19	divassi	$$⊢\frac{25\cdot 3}{2}=25\left(\frac{3}{2}\right)$$
91		3nn0	$$⊢3\in {\mathbb{N}}_0$$
92		2t3e6	$$⊢2\cdot 3=6$$
93	92	oveq1i	$$⊢2\cdot 3+1=6+1$$
94		6p1e7	$$⊢6+1=7$$
95	93 94	eqtri	$$⊢2\cdot 3+1=7$$
96		5t3e15	$$⊢5\cdot 3=15$$
97	91 41 42 43 42 45 95 96	decmul1c	$$⊢25\cdot 3=75$$
98	97	oveq1i	$$⊢\frac{25\cdot 3}{2}=\frac{75}{2}$$
99	90 98	eqtr3i	$$⊢25\left(\frac{3}{2}\right)=\frac{75}{2}$$
100	65	oveq2i	$$⊢25\left(\frac{6}{4}\right)=25\left(\frac{3}{2}\right)$$
101	100	eqcomi	$$⊢25\left(\frac{3}{2}\right)=25\left(\frac{6}{4}\right)$$
102	89 99 101	3eqtr2ri	$$⊢25\left(\frac{6}{4}\right)=\frac{\frac{75}{2}}{1}$$
103	3 1	oveq12d	$$⊢\phi \to \frac{C}{A}=\frac{\frac{75}{2}}{1}$$
104	102 103	eqtr4id	$$⊢\phi \to 25\left(\frac{6}{4}\right)=\frac{C}{A}$$
105	6 9 22 29 4 34 39 88 104	quadfac	$$⊢\phi \to \left(A{X}^2+BX+C=0\leftrightarrow \left(X=25\vee X=\frac{6}{4}\right)\right)$$