Metamath Proof Explorer

Theorem quadfac

Description: The solution of a quadratic equation via factoring. (Contributed by Luke Murphy, 10-Jul-2026)

Ref Expression
Hypotheses quadfac.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
quadfac.z ⊢ ( 𝜑 → 𝐴 ≠ 0 )
quadfac.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
quadfac.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
quadfac.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
quadfac.m ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
quadfac.n ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
quadfac.mpn ⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) = - ( 𝐵 / 𝐴 ) )
quadfac.mtn ⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) = ( 𝐶 / 𝐴 ) )
Assertion quadfac ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ↔ ( 𝑋 = 𝑀 ∨ 𝑋 = 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 quadfac.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 quadfac.z ⊢ ( 𝜑 → 𝐴 ≠ 0 )
3 quadfac.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4 quadfac.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 quadfac.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
6 quadfac.m ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
7 quadfac.n ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
8 quadfac.mpn ⊢ ( 𝜑 → ( 𝑀 + 𝑁 ) = - ( 𝐵 / 𝐴 ) )
9 quadfac.mtn ⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) = ( 𝐶 / 𝐴 ) )
10 5 6 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝑀 ) ∈ ℂ )
11 5 7 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝑁 ) ∈ ℂ )
12 10 11 mul0ord ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝑀 ) · ( 𝑋 − 𝑁 ) ) = 0 ↔ ( ( 𝑋 − 𝑀 ) = 0 ∨ ( 𝑋 − 𝑁 ) = 0 ) ) )
13 olc ⊢ ( ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 → ( 𝐴 = 0 ∨ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) )
14 2 neneqd ⊢ ( 𝜑 → ¬ 𝐴 = 0 )
15 id ⊢ ( 𝐴 = 0 → 𝐴 = 0 )
16 falim ⊢ ( ⊥ → 𝐴 = 0 )
17 15 16 pm5.21ni ⊢ ( ¬ 𝐴 = 0 → ( 𝐴 = 0 ↔ ⊥ ) )
18 14 17 syl ⊢ ( 𝜑 → ( 𝐴 = 0 ↔ ⊥ ) )
19 18 orbi1d ⊢ ( 𝜑 → ( ( 𝐴 = 0 ∨ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) ↔ ( ⊥ ∨ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) ) )
20 falim ⊢ ( ⊥ → ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 )
21 id ⊢ ( ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 → ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 )
22 20 21 jaoi ⊢ ( ( ⊥ ∨ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 )
23 22 a1i ⊢ ( 𝜑 → ( ( ⊥ ∨ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) )
24 19 23 sylbid ⊢ ( 𝜑 → ( ( 𝐴 = 0 ∨ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) )
25 13 24 impbid2 ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ↔ ( 𝐴 = 0 ∨ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) ) )
26 5 6 5 7 mulsubd ⊢ ( 𝜑 → ( ( 𝑋 − 𝑀 ) · ( 𝑋 − 𝑁 ) ) = ( ( ( 𝑋 · 𝑋 ) + ( 𝑁 · 𝑀 ) ) − ( ( 𝑋 · 𝑁 ) + ( 𝑋 · 𝑀 ) ) ) )
27 5 sqvald ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) = ( 𝑋 · 𝑋 ) )
28 27 eqcomd ⊢ ( 𝜑 → ( 𝑋 · 𝑋 ) = ( 𝑋 ↑ 2 ) )
29 6 7 mulcomd ⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) = ( 𝑁 · 𝑀 ) )
30 29 9 eqtr3d ⊢ ( 𝜑 → ( 𝑁 · 𝑀 ) = ( 𝐶 / 𝐴 ) )
31 28 30 oveq12d ⊢ ( 𝜑 → ( ( 𝑋 · 𝑋 ) + ( 𝑁 · 𝑀 ) ) = ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) )
32 7 6 addcomd ⊢ ( 𝜑 → ( 𝑁 + 𝑀 ) = ( 𝑀 + 𝑁 ) )
33 32 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 + 𝑀 ) · 𝑋 ) = ( ( 𝑀 + 𝑁 ) · 𝑋 ) )
34 7 5 mulcomd ⊢ ( 𝜑 → ( 𝑁 · 𝑋 ) = ( 𝑋 · 𝑁 ) )
35 6 5 mulcomd ⊢ ( 𝜑 → ( 𝑀 · 𝑋 ) = ( 𝑋 · 𝑀 ) )
36 34 35 oveq12d ⊢ ( 𝜑 → ( ( 𝑁 · 𝑋 ) + ( 𝑀 · 𝑋 ) ) = ( ( 𝑋 · 𝑁 ) + ( 𝑋 · 𝑀 ) ) )
37 7 5 6 36 joinlmuladdmuld ⊢ ( 𝜑 → ( ( 𝑁 + 𝑀 ) · 𝑋 ) = ( ( 𝑋 · 𝑁 ) + ( 𝑋 · 𝑀 ) ) )
38 8 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( - ( 𝐵 / 𝐴 ) · 𝑋 ) )
39 33 37 38 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑋 · 𝑁 ) + ( 𝑋 · 𝑀 ) ) = ( - ( 𝐵 / 𝐴 ) · 𝑋 ) )
40 31 39 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝑋 ) + ( 𝑁 · 𝑀 ) ) − ( ( 𝑋 · 𝑁 ) + ( 𝑋 · 𝑀 ) ) ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) − ( - ( 𝐵 / 𝐴 ) · 𝑋 ) ) )
41 26 40 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 − 𝑀 ) · ( 𝑋 − 𝑁 ) ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) − ( - ( 𝐵 / 𝐴 ) · 𝑋 ) ) )
42 41 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝑀 ) · ( 𝑋 − 𝑁 ) ) = 0 ↔ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) − ( - ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) )
43 3 1 2 divcld ⊢ ( 𝜑 → ( 𝐵 / 𝐴 ) ∈ ℂ )
44 43 5 mulneg1d ⊢ ( 𝜑 → ( - ( 𝐵 / 𝐴 ) · 𝑋 ) = - ( ( 𝐵 / 𝐴 ) · 𝑋 ) )
45 44 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) − ( - ( 𝐵 / 𝐴 ) · 𝑋 ) ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) − - ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) )
46 45 eqeq1d ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) − ( - ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ↔ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) − - ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) )
47 5 sqcld ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
48 4 1 2 divcld ⊢ ( 𝜑 → ( 𝐶 / 𝐴 ) ∈ ℂ )
49 47 48 addcld ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) ∈ ℂ )
50 43 5 mulcld ⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · 𝑋 ) ∈ ℂ )
51 49 50 subnegd ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) − - ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) )
52 51 eqeq1d ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) − - ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ↔ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) )
53 42 46 52 3bitrd ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝑀 ) · ( 𝑋 − 𝑁 ) ) = 0 ↔ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) )
54 49 50 addcld ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) ∈ ℂ )
55 1 54 mul0ord ⊢ ( 𝜑 → ( ( 𝐴 · ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) ) = 0 ↔ ( 𝐴 = 0 ∨ ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = 0 ) ) )
56 25 53 55 3bitr4d ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝑀 ) · ( 𝑋 − 𝑁 ) ) = 0 ↔ ( 𝐴 · ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) ) = 0 ) )
57 1 49 50 adddid ⊢ ( 𝜑 → ( 𝐴 · ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) ) = ( ( 𝐴 · ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) ) + ( 𝐴 · ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) ) )
58 57 eqeq1d ⊢ ( 𝜑 → ( ( 𝐴 · ( ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) ) = 0 ↔ ( ( 𝐴 · ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) ) + ( 𝐴 · ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) ) = 0 ) )
59 1 47 48 adddid ⊢ ( 𝜑 → ( 𝐴 · ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) ) = ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐴 · ( 𝐶 / 𝐴 ) ) ) )
60 4 1 2 divcan2d ⊢ ( 𝜑 → ( 𝐴 · ( 𝐶 / 𝐴 ) ) = 𝐶 )
61 60 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐴 · ( 𝐶 / 𝐴 ) ) ) = ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + 𝐶 ) )
62 59 61 eqtrd ⊢ ( 𝜑 → ( 𝐴 · ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) ) = ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + 𝐶 ) )
63 1 43 5 mulassd ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝐵 / 𝐴 ) ) · 𝑋 ) = ( 𝐴 · ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) )
64 3 1 2 divcan2d ⊢ ( 𝜑 → ( 𝐴 · ( 𝐵 / 𝐴 ) ) = 𝐵 )
65 64 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝐵 / 𝐴 ) ) · 𝑋 ) = ( 𝐵 · 𝑋 ) )
66 63 65 eqtr3d ⊢ ( 𝜑 → ( 𝐴 · ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = ( 𝐵 · 𝑋 ) )
67 62 66 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 · ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) ) + ( 𝐴 · ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) ) = ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + 𝐶 ) + ( 𝐵 · 𝑋 ) ) )
68 67 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( ( 𝑋 ↑ 2 ) + ( 𝐶 / 𝐴 ) ) ) + ( 𝐴 · ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) ) = 0 ↔ ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + 𝐶 ) + ( 𝐵 · 𝑋 ) ) = 0 ) )
69 56 58 68 3bitrd ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝑀 ) · ( 𝑋 − 𝑁 ) ) = 0 ↔ ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + 𝐶 ) + ( 𝐵 · 𝑋 ) ) = 0 ) )
70 1 47 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
71 3 5 mulcld ⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ ℂ )
72 70 4 71 addassd ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + 𝐶 ) + ( 𝐵 · 𝑋 ) ) = ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐶 + ( 𝐵 · 𝑋 ) ) ) )
73 72 eqeq1d ⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + 𝐶 ) + ( 𝐵 · 𝑋 ) ) = 0 ↔ ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐶 + ( 𝐵 · 𝑋 ) ) ) = 0 ) )
74 4 71 addcomd ⊢ ( 𝜑 → ( 𝐶 + ( 𝐵 · 𝑋 ) ) = ( ( 𝐵 · 𝑋 ) + 𝐶 ) )
75 74 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐶 + ( 𝐵 · 𝑋 ) ) ) = ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) )
76 75 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐶 + ( 𝐵 · 𝑋 ) ) ) = 0 ↔ ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ) )
77 69 73 76 3bitrd ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝑀 ) · ( 𝑋 − 𝑁 ) ) = 0 ↔ ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ) )
78 5 6 subeq0ad ⊢ ( 𝜑 → ( ( 𝑋 − 𝑀 ) = 0 ↔ 𝑋 = 𝑀 ) )
79 5 7 subeq0ad ⊢ ( 𝜑 → ( ( 𝑋 − 𝑁 ) = 0 ↔ 𝑋 = 𝑁 ) )
80 78 79 orbi12d ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝑀 ) = 0 ∨ ( 𝑋 − 𝑁 ) = 0 ) ↔ ( 𝑋 = 𝑀 ∨ 𝑋 = 𝑁 ) ) )
81 12 77 80 3bitr3d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 ↔ ( 𝑋 = 𝑀 ∨ 𝑋 = 𝑁 ) ) )