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 
|- ( ph -> A e. CC )
quadfac.z 
|- ( ph -> A =/= 0 )
quadfac.b 
|- ( ph -> B e. CC )
quadfac.c 
|- ( ph -> C e. CC )
quadfac.x 
|- ( ph -> X e. CC )
quadfac.m 
|- ( ph -> M e. CC )
quadfac.n 
|- ( ph -> N e. CC )
quadfac.mpn 
|- ( ph -> ( M + N ) = -u ( B / A ) )
quadfac.mtn 
|- ( ph -> ( M x. N ) = ( C / A ) )
Assertion quadfac 
|- ( ph -> ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 <-> ( X = M \/ X = N ) ) )

Proof

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