Metamath Proof Explorer

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 
|- ( ph -> A = 1 )
25or6to4.b 
|- ( ph -> B = -u ( ; 5 3 / 2 ) )
25or6to4.c 
|- ( ph -> C = ( ; 7 5 / 2 ) )
25or6to4.x 
|- ( ph -> X e. CC )
Assertion 25or6to4 
|- ( ph -> ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 <-> ( X = ; 2 5 \/ X = ( 6 / 4 ) ) ) )

Proof

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