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 ⊢ ( 𝜑 → 𝐴 = 1 )
25or6to4.b ⊢ ( 𝜑 → 𝐵 = - ( 5 3 / 2 ) )
25or6to4.c ⊢ ( 𝜑 → 𝐶 = ( 7 5 / 2 ) )
25or6to4.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
Assertion 25or6to4 ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ↔ ( 𝑋 = 2 5 ∨ 𝑋 = ( 6 / 4 ) ) ) )

Proof

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