Proof of Theorem quad3
Step | Hyp | Ref
| Expression |
1 | | 2cn 11803 |
. . . . . 6
⊢ 2 ∈
ℂ |
2 | | quad3.2 |
. . . . . 6
⊢ 𝐴 ∈ ℂ |
3 | 1, 2 | mulcli 10738 |
. . . . 5
⊢ (2
· 𝐴) ∈
ℂ |
4 | | quad3.1 |
. . . . . 6
⊢ 𝑋 ∈ ℂ |
5 | | quad3.4 |
. . . . . . 7
⊢ 𝐵 ∈ ℂ |
6 | | 2ne0 11832 |
. . . . . . . 8
⊢ 2 ≠
0 |
7 | | quad3.3 |
. . . . . . . 8
⊢ 𝐴 ≠ 0 |
8 | 1, 2, 6, 7 | mulne0i 11373 |
. . . . . . 7
⊢ (2
· 𝐴) ≠
0 |
9 | 5, 3, 8 | divcli 11472 |
. . . . . 6
⊢ (𝐵 / (2 · 𝐴)) ∈ ℂ |
10 | 4, 9 | addcli 10737 |
. . . . 5
⊢ (𝑋 + (𝐵 / (2 · 𝐴))) ∈ ℂ |
11 | 3, 10 | sqmuli 13651 |
. . . 4
⊢ (((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)) |
12 | 4, 9 | binom2i 13678 |
. . . . . . 7
⊢ ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)) |
13 | 4 | sqcli 13648 |
. . . . . . . . . . . 12
⊢ (𝑋↑2) ∈
ℂ |
14 | 2, 13 | mulcli 10738 |
. . . . . . . . . . 11
⊢ (𝐴 · (𝑋↑2)) ∈ ℂ |
15 | 5, 4 | mulcli 10738 |
. . . . . . . . . . 11
⊢ (𝐵 · 𝑋) ∈ ℂ |
16 | 14, 15, 2, 7 | divdiri 11487 |
. . . . . . . . . 10
⊢ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)) |
17 | 13, 2, 7 | divcan3i 11476 |
. . . . . . . . . . 11
⊢ ((𝐴 · (𝑋↑2)) / 𝐴) = (𝑋↑2) |
18 | 5, 4, 2, 7 | div23i 11488 |
. . . . . . . . . . 11
⊢ ((𝐵 · 𝑋) / 𝐴) = ((𝐵 / 𝐴) · 𝑋) |
19 | 17, 18 | oveq12i 7194 |
. . . . . . . . . 10
⊢ (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)) = ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) |
20 | 16, 19 | eqtr2i 2763 |
. . . . . . . . 9
⊢ ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) |
21 | 5, 2, 7 | divcli 11472 |
. . . . . . . . . . . 12
⊢ (𝐵 / 𝐴) ∈ ℂ |
22 | 21, 4 | mulcomi 10739 |
. . . . . . . . . . 11
⊢ ((𝐵 / 𝐴) · 𝑋) = (𝑋 · (𝐵 / 𝐴)) |
23 | 4, 21 | mulcli 10738 |
. . . . . . . . . . . 12
⊢ (𝑋 · (𝐵 / 𝐴)) ∈ ℂ |
24 | 23, 1, 6 | divcan2i 11473 |
. . . . . . . . . . 11
⊢ (2
· ((𝑋 ·
(𝐵 / 𝐴)) / 2)) = (𝑋 · (𝐵 / 𝐴)) |
25 | 4, 21, 1, 6 | divassi 11486 |
. . . . . . . . . . . . 13
⊢ ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · ((𝐵 / 𝐴) / 2)) |
26 | 2, 7 | pm3.2i 474 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) |
27 | 1, 6 | pm3.2i 474 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
28 | | divdiv1 11441 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((𝐵
/ 𝐴) / 2) = (𝐵 / (𝐴 · 2))) |
29 | 5, 26, 27, 28 | mp3an 1462 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 / 𝐴) / 2) = (𝐵 / (𝐴 · 2)) |
30 | 2, 1 | mulcomi 10739 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 · 2) = (2 · 𝐴) |
31 | 30 | oveq2i 7193 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 / (𝐴 · 2)) = (𝐵 / (2 · 𝐴)) |
32 | 29, 31 | eqtri 2762 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 / 𝐴) / 2) = (𝐵 / (2 · 𝐴)) |
33 | 32 | oveq2i 7193 |
. . . . . . . . . . . . 13
⊢ (𝑋 · ((𝐵 / 𝐴) / 2)) = (𝑋 · (𝐵 / (2 · 𝐴))) |
34 | 25, 33 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · (𝐵 / (2 · 𝐴))) |
35 | 34 | oveq2i 7193 |
. . . . . . . . . . 11
⊢ (2
· ((𝑋 ·
(𝐵 / 𝐴)) / 2)) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))) |
36 | 22, 24, 35 | 3eqtr2i 2768 |
. . . . . . . . . 10
⊢ ((𝐵 / 𝐴) · 𝑋) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))) |
37 | 36 | oveq2i 7193 |
. . . . . . . . 9
⊢ ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) |
38 | | quad3.5 |
. . . . . . . . . . . . . . 15
⊢ 𝐶 ∈ ℂ |
39 | 14, 15, 38 | addassi 10741 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) = ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) |
40 | 39 | eqcomi 2748 |
. . . . . . . . . . . . 13
⊢ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) |
41 | 40 | oveq1i 7192 |
. . . . . . . . . . . 12
⊢ (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = ((((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) − 𝐶) |
42 | 14, 15 | addcli 10737 |
. . . . . . . . . . . . 13
⊢ ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) ∈ ℂ |
43 | 42, 38 | pncan3oi 10992 |
. . . . . . . . . . . 12
⊢ ((((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) − 𝐶) = ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) |
44 | 41, 43 | eqtr2i 2763 |
. . . . . . . . . . 11
⊢ ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) |
45 | | quad3.6 |
. . . . . . . . . . . . 13
⊢ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 |
46 | 45 | oveq1i 7192 |
. . . . . . . . . . . 12
⊢ (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = (0 − 𝐶) |
47 | | df-neg 10963 |
. . . . . . . . . . . 12
⊢ -𝐶 = (0 − 𝐶) |
48 | 46, 47 | eqtr4i 2765 |
. . . . . . . . . . 11
⊢ (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = -𝐶 |
49 | 44, 48 | eqtri 2762 |
. . . . . . . . . 10
⊢ ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = -𝐶 |
50 | 49 | oveq1i 7192 |
. . . . . . . . 9
⊢ (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (-𝐶 / 𝐴) |
51 | 20, 37, 50 | 3eqtr3i 2770 |
. . . . . . . 8
⊢ ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) = (-𝐶 / 𝐴) |
52 | 51 | oveq1i 7192 |
. . . . . . 7
⊢ (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)) |
53 | 12, 52 | eqtri 2762 |
. . . . . 6
⊢ ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)) |
54 | 38 | negcli 11044 |
. . . . . . . 8
⊢ -𝐶 ∈ ℂ |
55 | 54, 2, 7 | divcli 11472 |
. . . . . . 7
⊢ (-𝐶 / 𝐴) ∈ ℂ |
56 | 9 | sqcli 13648 |
. . . . . . 7
⊢ ((𝐵 / (2 · 𝐴))↑2) ∈ ℂ |
57 | 55, 56 | addcomi 10921 |
. . . . . 6
⊢ ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)) = (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) |
58 | 5, 3, 8 | sqdivi 13652 |
. . . . . . . 8
⊢ ((𝐵 / (2 · 𝐴))↑2) = ((𝐵↑2) / ((2 · 𝐴)↑2)) |
59 | | 4cn 11813 |
. . . . . . . . . . 11
⊢ 4 ∈
ℂ |
60 | 59, 2 | mulcli 10738 |
. . . . . . . . . 10
⊢ (4
· 𝐴) ∈
ℂ |
61 | | 4ne0 11836 |
. . . . . . . . . . 11
⊢ 4 ≠
0 |
62 | 59, 2, 61, 7 | mulne0i 11373 |
. . . . . . . . . 10
⊢ (4
· 𝐴) ≠
0 |
63 | 60, 60, 54, 2, 62, 7 | divmuldivi 11490 |
. . . . . . . . 9
⊢ (((4
· 𝐴) / (4 ·
𝐴)) · (-𝐶 / 𝐴)) = (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)) |
64 | 60, 62 | dividi 11463 |
. . . . . . . . . . . 12
⊢ ((4
· 𝐴) / (4 ·
𝐴)) = 1 |
65 | 64 | eqcomi 2748 |
. . . . . . . . . . 11
⊢ 1 = ((4
· 𝐴) / (4 ·
𝐴)) |
66 | 65 | oveq1i 7192 |
. . . . . . . . . 10
⊢ (1
· (-𝐶 / 𝐴)) = (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) |
67 | 55 | mulid2i 10736 |
. . . . . . . . . 10
⊢ (1
· (-𝐶 / 𝐴)) = (-𝐶 / 𝐴) |
68 | 66, 67 | eqtr3i 2764 |
. . . . . . . . 9
⊢ (((4
· 𝐴) / (4 ·
𝐴)) · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴) |
69 | 38 | mulm1i 11175 |
. . . . . . . . . . . . . . 15
⊢ (-1
· 𝐶) = -𝐶 |
70 | 69 | eqcomi 2748 |
. . . . . . . . . . . . . 14
⊢ -𝐶 = (-1 · 𝐶) |
71 | 70 | oveq2i 7193 |
. . . . . . . . . . . . 13
⊢ ((4
· 𝐴) · -𝐶) = ((4 · 𝐴) · (-1 · 𝐶)) |
72 | | neg1cn 11842 |
. . . . . . . . . . . . . 14
⊢ -1 ∈
ℂ |
73 | 60, 72, 38 | mulassi 10742 |
. . . . . . . . . . . . 13
⊢ (((4
· 𝐴) · -1)
· 𝐶) = ((4 ·
𝐴) · (-1 ·
𝐶)) |
74 | 71, 73 | eqtr4i 2765 |
. . . . . . . . . . . 12
⊢ ((4
· 𝐴) · -𝐶) = (((4 · 𝐴) · -1) · 𝐶) |
75 | 60, 72 | mulcomi 10739 |
. . . . . . . . . . . . 13
⊢ ((4
· 𝐴) · -1) =
(-1 · (4 · 𝐴)) |
76 | 75 | oveq1i 7192 |
. . . . . . . . . . . 12
⊢ (((4
· 𝐴) · -1)
· 𝐶) = ((-1 ·
(4 · 𝐴)) ·
𝐶) |
77 | 72, 60, 38 | mulassi 10742 |
. . . . . . . . . . . 12
⊢ ((-1
· (4 · 𝐴))
· 𝐶) = (-1 ·
((4 · 𝐴) ·
𝐶)) |
78 | 74, 76, 77 | 3eqtri 2766 |
. . . . . . . . . . 11
⊢ ((4
· 𝐴) · -𝐶) = (-1 · ((4 ·
𝐴) · 𝐶)) |
79 | 59, 2, 38 | mulassi 10742 |
. . . . . . . . . . . 12
⊢ ((4
· 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)) |
80 | 79 | oveq2i 7193 |
. . . . . . . . . . 11
⊢ (-1
· ((4 · 𝐴)
· 𝐶)) = (-1 ·
(4 · (𝐴 ·
𝐶))) |
81 | 2, 38 | mulcli 10738 |
. . . . . . . . . . . . 13
⊢ (𝐴 · 𝐶) ∈ ℂ |
82 | 59, 81 | mulcli 10738 |
. . . . . . . . . . . 12
⊢ (4
· (𝐴 · 𝐶)) ∈
ℂ |
83 | 82 | mulm1i 11175 |
. . . . . . . . . . 11
⊢ (-1
· (4 · (𝐴
· 𝐶))) = -(4
· (𝐴 · 𝐶)) |
84 | 78, 80, 83 | 3eqtri 2766 |
. . . . . . . . . 10
⊢ ((4
· 𝐴) · -𝐶) = -(4 · (𝐴 · 𝐶)) |
85 | | 2t2e4 11892 |
. . . . . . . . . . . . . . . 16
⊢ (2
· 2) = 4 |
86 | 85 | eqcomi 2748 |
. . . . . . . . . . . . . . 15
⊢ 4 = (2
· 2) |
87 | 86 | oveq1i 7192 |
. . . . . . . . . . . . . 14
⊢ (4
· 𝐴) = ((2 ·
2) · 𝐴) |
88 | 87 | oveq1i 7192 |
. . . . . . . . . . . . 13
⊢ ((4
· 𝐴) · 𝐴) = (((2 · 2) ·
𝐴) · 𝐴) |
89 | 1, 1, 2 | mulassi 10742 |
. . . . . . . . . . . . . 14
⊢ ((2
· 2) · 𝐴) =
(2 · (2 · 𝐴)) |
90 | 89 | oveq1i 7192 |
. . . . . . . . . . . . 13
⊢ (((2
· 2) · 𝐴)
· 𝐴) = ((2 ·
(2 · 𝐴)) ·
𝐴) |
91 | 88, 90 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ ((4
· 𝐴) · 𝐴) = ((2 · (2 ·
𝐴)) · 𝐴) |
92 | 1, 3 | mulcomi 10739 |
. . . . . . . . . . . . 13
⊢ (2
· (2 · 𝐴)) =
((2 · 𝐴) ·
2) |
93 | 92 | oveq1i 7192 |
. . . . . . . . . . . 12
⊢ ((2
· (2 · 𝐴))
· 𝐴) = (((2 ·
𝐴) · 2) ·
𝐴) |
94 | 3, 1, 2 | mulassi 10742 |
. . . . . . . . . . . 12
⊢ (((2
· 𝐴) · 2)
· 𝐴) = ((2 ·
𝐴) · (2 ·
𝐴)) |
95 | 91, 93, 94 | 3eqtri 2766 |
. . . . . . . . . . 11
⊢ ((4
· 𝐴) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)) |
96 | 3 | sqvali 13647 |
. . . . . . . . . . 11
⊢ ((2
· 𝐴)↑2) = ((2
· 𝐴) · (2
· 𝐴)) |
97 | 95, 96 | eqtr4i 2765 |
. . . . . . . . . 10
⊢ ((4
· 𝐴) · 𝐴) = ((2 · 𝐴)↑2) |
98 | 84, 97 | oveq12i 7194 |
. . . . . . . . 9
⊢ (((4
· 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)) |
99 | 63, 68, 98 | 3eqtr3i 2770 |
. . . . . . . 8
⊢ (-𝐶 / 𝐴) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)) |
100 | 58, 99 | oveq12i 7194 |
. . . . . . 7
⊢ (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))) |
101 | 5 | sqcli 13648 |
. . . . . . . 8
⊢ (𝐵↑2) ∈
ℂ |
102 | 82 | negcli 11044 |
. . . . . . . 8
⊢ -(4
· (𝐴 · 𝐶)) ∈
ℂ |
103 | 3 | sqcli 13648 |
. . . . . . . 8
⊢ ((2
· 𝐴)↑2) ∈
ℂ |
104 | 3, 3, 8, 8 | mulne0i 11373 |
. . . . . . . . 9
⊢ ((2
· 𝐴) · (2
· 𝐴)) ≠
0 |
105 | 96, 104 | eqnetri 3005 |
. . . . . . . 8
⊢ ((2
· 𝐴)↑2) ≠
0 |
106 | 101, 102,
103, 105 | divdiri 11487 |
. . . . . . 7
⊢ (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))) |
107 | 101, 82 | negsubi 11054 |
. . . . . . . 8
⊢ ((𝐵↑2) + -(4 · (𝐴 · 𝐶))) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))) |
108 | 107 | oveq1i 7192 |
. . . . . . 7
⊢ (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) |
109 | 100, 106,
108 | 3eqtr2i 2768 |
. . . . . 6
⊢ (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) |
110 | 53, 57, 109 | 3eqtri 2766 |
. . . . 5
⊢ ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) |
111 | 110 | oveq2i 7193 |
. . . 4
⊢ (((2
· 𝐴)↑2)
· ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)) = (((2 · 𝐴)↑2) · (((𝐵↑2) − (4 ·
(𝐴 · 𝐶))) / ((2 · 𝐴)↑2))) |
112 | 101, 82 | subcli 11052 |
. . . . 5
⊢ ((𝐵↑2) − (4 ·
(𝐴 · 𝐶))) ∈
ℂ |
113 | 112, 103,
105 | divcan2i 11473 |
. . . 4
⊢ (((2
· 𝐴)↑2)
· (((𝐵↑2)
− (4 · (𝐴
· 𝐶))) / ((2
· 𝐴)↑2))) =
((𝐵↑2) − (4
· (𝐴 · 𝐶))) |
114 | 11, 111, 113 | 3eqtri 2766 |
. . 3
⊢ (((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))) |
115 | 3, 10 | mulcli 10738 |
. . . . 5
⊢ ((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ |
116 | 115, 112 | pm3.2i 474 |
. . . 4
⊢ (((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ ∧ ((𝐵↑2) − (4 ·
(𝐴 · 𝐶))) ∈
ℂ) |
117 | | eqsqrtor 14828 |
. . . 4
⊢ ((((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ ∧ ((𝐵↑2) − (4 ·
(𝐴 · 𝐶))) ∈ ℂ) → ((((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ↔ (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))))) |
118 | 116, 117 | ax-mp 5 |
. . 3
⊢ ((((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ↔ (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))))) |
119 | 114, 118 | mpbi 233 |
. 2
⊢ (((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) |
120 | | sqrtcl 14823 |
. . . . . . 7
⊢ (((𝐵↑2) − (4 ·
(𝐴 · 𝐶))) ∈ ℂ →
(√‘((𝐵↑2)
− (4 · (𝐴
· 𝐶)))) ∈
ℂ) |
121 | 112, 120 | ax-mp 5 |
. . . . . 6
⊢
(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ |
122 | 121, 3, 10, 8 | divmuli 11484 |
. . . . 5
⊢
(((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) = (𝑋 + (𝐵 / (2 · 𝐴))) ↔ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) |
123 | | eqcom 2746 |
. . . . 5
⊢
(((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) = (𝑋 + (𝐵 / (2 · 𝐴))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
124 | 122, 123 | bitr3i 280 |
. . . 4
⊢ (((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
125 | 121, 3, 8 | divcli 11472 |
. . . . . 6
⊢
((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ |
126 | 125, 9, 4 | subadd2i 11064 |
. . . . 5
⊢
((((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = 𝑋 ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
127 | | eqcom 2746 |
. . . . 5
⊢
((((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = 𝑋 ↔ 𝑋 = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))) |
128 | 126, 127 | bitr3i 280 |
. . . 4
⊢ ((𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))) |
129 | | divneg 11422 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ (2
· 𝐴) ∈ ℂ
∧ (2 · 𝐴) ≠
0) → -(𝐵 / (2 ·
𝐴)) = (-𝐵 / (2 · 𝐴))) |
130 | 5, 3, 8, 129 | mp3an 1462 |
. . . . . . . 8
⊢ -(𝐵 / (2 · 𝐴)) = (-𝐵 / (2 · 𝐴)) |
131 | 130 | oveq2i 7193 |
. . . . . . 7
⊢
(((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) |
132 | 125, 9 | negsubi 11054 |
. . . . . . 7
⊢
(((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) |
133 | 5 | negcli 11044 |
. . . . . . . . 9
⊢ -𝐵 ∈ ℂ |
134 | 133, 3, 8 | divcli 11472 |
. . . . . . . 8
⊢ (-𝐵 / (2 · 𝐴)) ∈ ℂ |
135 | 125, 134 | addcomi 10921 |
. . . . . . 7
⊢
(((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
136 | 131, 132,
135 | 3eqtr3i 2770 |
. . . . . 6
⊢
(((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
137 | 133, 121,
3, 8 | divdiri 11487 |
. . . . . 6
⊢ ((-𝐵 + (√‘((𝐵↑2) − (4 ·
(𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
138 | 136, 137 | eqtr4i 2765 |
. . . . 5
⊢
(((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) |
139 | 138 | eqeq2i 2752 |
. . . 4
⊢ (𝑋 = (((√‘((𝐵↑2) − (4 ·
(𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) ↔ 𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))) |
140 | 124, 128,
139 | 3bitri 300 |
. . 3
⊢ (((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ 𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))) |
141 | 121 | negcli 11044 |
. . . . . 6
⊢
-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ |
142 | 141, 3, 10, 8 | divmuli 11484 |
. . . . 5
⊢
((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) = (𝑋 + (𝐵 / (2 · 𝐴))) ↔ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) |
143 | | eqcom 2746 |
. . . . 5
⊢
((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) = (𝑋 + (𝐵 / (2 · 𝐴))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
144 | 142, 143 | bitr3i 280 |
. . . 4
⊢ (((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
145 | 141, 3, 8 | divcli 11472 |
. . . . . 6
⊢
(-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ |
146 | 145, 9, 4 | subadd2i 11064 |
. . . . 5
⊢
(((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = 𝑋 ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
147 | | eqcom 2746 |
. . . . 5
⊢
(((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = 𝑋 ↔ 𝑋 = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))) |
148 | 146, 147 | bitr3i 280 |
. . . 4
⊢ ((𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))) |
149 | 130 | oveq2i 7193 |
. . . . . . 7
⊢
((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) |
150 | 145, 9 | negsubi 11054 |
. . . . . . 7
⊢
((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) |
151 | 145, 134 | addcomi 10921 |
. . . . . . 7
⊢
((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
152 | 149, 150,
151 | 3eqtr3i 2770 |
. . . . . 6
⊢
((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
153 | 133, 141,
3, 8 | divdiri 11487 |
. . . . . 6
⊢ ((-𝐵 + -(√‘((𝐵↑2) − (4 ·
(𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))) |
154 | 133, 121 | negsubi 11054 |
. . . . . . 7
⊢ (-𝐵 + -(√‘((𝐵↑2) − (4 ·
(𝐴 · 𝐶))))) = (-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) |
155 | 154 | oveq1i 7192 |
. . . . . 6
⊢ ((-𝐵 + -(√‘((𝐵↑2) − (4 ·
(𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) |
156 | 152, 153,
155 | 3eqtr2i 2768 |
. . . . 5
⊢
((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) |
157 | 156 | eqeq2i 2752 |
. . . 4
⊢ (𝑋 = ((-(√‘((𝐵↑2) − (4 ·
(𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) ↔ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))) |
158 | 144, 148,
157 | 3bitri 300 |
. . 3
⊢ (((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))) |
159 | 140, 158 | orbi12i 914 |
. 2
⊢ ((((2
· 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) ↔ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))) |
160 | 119, 159 | mpbi 233 |
1
⊢ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))) |