Metamath Proof Explorer

Theorem dquartlem1

Description: Lemma for dquart . (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses dquart.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
dquart.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
dquart.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
dquart.s ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
dquart.m ⊢ ( 𝜑 → 𝑀 = ( ( 2 · 𝑆 ) ↑ 2 ) )
dquart.m0 ⊢ ( 𝜑 → 𝑀 ≠ 0 )
dquart.i ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
dquart.i2 ⊢ ( 𝜑 → ( 𝐼 ↑ 2 ) = ( ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) + ( ( 𝐶 / 4 ) / 𝑆 ) ) )
Assertion dquartlem1 ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) = 0 ↔ ( 𝑋 = ( - 𝑆 + 𝐼 ) ∨ 𝑋 = ( - 𝑆 − 𝐼 ) ) ) )

Proof

Step Hyp Ref Expression
1 dquart.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
2 dquart.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
3 dquart.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4 dquart.s ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
5 dquart.m ⊢ ( 𝜑 → 𝑀 = ( ( 2 · 𝑆 ) ↑ 2 ) )
6 dquart.m0 ⊢ ( 𝜑 → 𝑀 ≠ 0 )
7 dquart.i ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
8 dquart.i2 ⊢ ( 𝜑 → ( 𝐼 ↑ 2 ) = ( ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) + ( ( 𝐶 / 4 ) / 𝑆 ) ) )
9 3 sqcld ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
10 2cn ⊢ 2 ∈ ℂ
11 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( 2 · 𝑆 ) ∈ ℂ )
12 10 4 11 sylancr ⊢ ( 𝜑 → ( 2 · 𝑆 ) ∈ ℂ )
13 12 sqcld ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) ↑ 2 ) ∈ ℂ )
14 5 13 eqeltrd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
15 14 1 addcld ⊢ ( 𝜑 → ( 𝑀 + 𝐵 ) ∈ ℂ )
16 15 halfcld ⊢ ( 𝜑 → ( ( 𝑀 + 𝐵 ) / 2 ) ∈ ℂ )
17 9 16 addcld ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) ∈ ℂ )
18 14 halfcld ⊢ ( 𝜑 → ( 𝑀 / 2 ) ∈ ℂ )
19 18 3 mulcld ⊢ ( 𝜑 → ( ( 𝑀 / 2 ) · 𝑋 ) ∈ ℂ )
20 4cn ⊢ 4 ∈ ℂ
21 20 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
22 4ne0 ⊢ 4 ≠ 0
23 22 a1i ⊢ ( 𝜑 → 4 ≠ 0 )
24 2 21 23 divcld ⊢ ( 𝜑 → ( 𝐶 / 4 ) ∈ ℂ )
25 19 24 subcld ⊢ ( 𝜑 → ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) ∈ ℂ )
26 5 6 eqnetrrd ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) ↑ 2 ) ≠ 0 )
27 sqne0 ⊢ ( ( 2 · 𝑆 ) ∈ ℂ → ( ( ( 2 · 𝑆 ) ↑ 2 ) ≠ 0 ↔ ( 2 · 𝑆 ) ≠ 0 ) )
28 12 27 syl ⊢ ( 𝜑 → ( ( ( 2 · 𝑆 ) ↑ 2 ) ≠ 0 ↔ ( 2 · 𝑆 ) ≠ 0 ) )
29 26 28 mpbid ⊢ ( 𝜑 → ( 2 · 𝑆 ) ≠ 0 )
30 mulne0b ⊢ ( ( 2 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( ( 2 ≠ 0 ∧ 𝑆 ≠ 0 ) ↔ ( 2 · 𝑆 ) ≠ 0 ) )
31 10 4 30 sylancr ⊢ ( 𝜑 → ( ( 2 ≠ 0 ∧ 𝑆 ≠ 0 ) ↔ ( 2 · 𝑆 ) ≠ 0 ) )
32 29 31 mpbird ⊢ ( 𝜑 → ( 2 ≠ 0 ∧ 𝑆 ≠ 0 ) )
33 32 simprd ⊢ ( 𝜑 → 𝑆 ≠ 0 )
34 25 4 33 divcld ⊢ ( 𝜑 → ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ∈ ℂ )
35 17 34 addcld ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) ∈ ℂ )
36 10 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
37 2ne0 ⊢ 2 ≠ 0
38 37 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
39 35 36 38 diveq0ad ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) / 2 ) = 0 ↔ ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) = 0 ) )
40 9 16 34 addassd ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) = ( ( 𝑋 ↑ 2 ) + ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) ) )
41 40 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) / 2 ) = ( ( ( 𝑋 ↑ 2 ) + ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) ) / 2 ) )
42 16 34 addcld ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) ∈ ℂ )
43 9 42 36 38 divdird ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) ) / 2 ) = ( ( ( 𝑋 ↑ 2 ) / 2 ) + ( ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) / 2 ) ) )
44 9 36 38 divrec2d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) / 2 ) = ( ( 1 / 2 ) · ( 𝑋 ↑ 2 ) ) )
45 19 24 4 33 divsubdird ⊢ ( 𝜑 → ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) = ( ( ( ( 𝑀 / 2 ) · 𝑋 ) / 𝑆 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) )
46 18 3 4 33 div23d ⊢ ( 𝜑 → ( ( ( 𝑀 / 2 ) · 𝑋 ) / 𝑆 ) = ( ( ( 𝑀 / 2 ) / 𝑆 ) · 𝑋 ) )
47 4 sqvald ⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) = ( 𝑆 · 𝑆 ) )
48 47 oveq2d ⊢ ( 𝜑 → ( 2 · ( 𝑆 ↑ 2 ) ) = ( 2 · ( 𝑆 · 𝑆 ) ) )
49 sqmul ⊢ ( ( 2 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( ( 2 · 𝑆 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑆 ↑ 2 ) ) )
50 10 4 49 sylancr ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑆 ↑ 2 ) ) )
51 10 sqvali ⊢ ( 2 ↑ 2 ) = ( 2 · 2 )
52 51 oveq1i ⊢ ( ( 2 ↑ 2 ) · ( 𝑆 ↑ 2 ) ) = ( ( 2 · 2 ) · ( 𝑆 ↑ 2 ) )
53 50 52 eqtrdi ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) ↑ 2 ) = ( ( 2 · 2 ) · ( 𝑆 ↑ 2 ) ) )
54 4 sqcld ⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℂ )
55 36 36 54 mulassd ⊢ ( 𝜑 → ( ( 2 · 2 ) · ( 𝑆 ↑ 2 ) ) = ( 2 · ( 2 · ( 𝑆 ↑ 2 ) ) ) )
56 5 53 55 3eqtrd ⊢ ( 𝜑 → 𝑀 = ( 2 · ( 2 · ( 𝑆 ↑ 2 ) ) ) )
57 56 oveq1d ⊢ ( 𝜑 → ( 𝑀 / 2 ) = ( ( 2 · ( 2 · ( 𝑆 ↑ 2 ) ) ) / 2 ) )
58 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑆 ↑ 2 ) ∈ ℂ ) → ( 2 · ( 𝑆 ↑ 2 ) ) ∈ ℂ )
59 10 54 58 sylancr ⊢ ( 𝜑 → ( 2 · ( 𝑆 ↑ 2 ) ) ∈ ℂ )
60 59 36 38 divcan3d ⊢ ( 𝜑 → ( ( 2 · ( 2 · ( 𝑆 ↑ 2 ) ) ) / 2 ) = ( 2 · ( 𝑆 ↑ 2 ) ) )
61 57 60 eqtrd ⊢ ( 𝜑 → ( 𝑀 / 2 ) = ( 2 · ( 𝑆 ↑ 2 ) ) )
62 36 4 4 mulassd ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) · 𝑆 ) = ( 2 · ( 𝑆 · 𝑆 ) ) )
63 48 61 62 3eqtr4d ⊢ ( 𝜑 → ( 𝑀 / 2 ) = ( ( 2 · 𝑆 ) · 𝑆 ) )
64 63 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 / 2 ) / 𝑆 ) = ( ( ( 2 · 𝑆 ) · 𝑆 ) / 𝑆 ) )
65 12 4 33 divcan4d ⊢ ( 𝜑 → ( ( ( 2 · 𝑆 ) · 𝑆 ) / 𝑆 ) = ( 2 · 𝑆 ) )
66 64 65 eqtrd ⊢ ( 𝜑 → ( ( 𝑀 / 2 ) / 𝑆 ) = ( 2 · 𝑆 ) )
67 66 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑀 / 2 ) / 𝑆 ) · 𝑋 ) = ( ( 2 · 𝑆 ) · 𝑋 ) )
68 46 67 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 / 2 ) · 𝑋 ) / 𝑆 ) = ( ( 2 · 𝑆 ) · 𝑋 ) )
69 68 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑀 / 2 ) · 𝑋 ) / 𝑆 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) = ( ( ( 2 · 𝑆 ) · 𝑋 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) )
70 45 69 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) = ( ( ( 2 · 𝑆 ) · 𝑋 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) )
71 70 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) = ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( 2 · 𝑆 ) · 𝑋 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) ) )
72 12 3 mulcld ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) · 𝑋 ) ∈ ℂ )
73 24 4 33 divcld ⊢ ( 𝜑 → ( ( 𝐶 / 4 ) / 𝑆 ) ∈ ℂ )
74 16 72 73 addsub12d ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( 2 · 𝑆 ) · 𝑋 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) ) = ( ( ( 2 · 𝑆 ) · 𝑋 ) + ( ( ( 𝑀 + 𝐵 ) / 2 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) ) )
75 71 74 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) = ( ( ( 2 · 𝑆 ) · 𝑋 ) + ( ( ( 𝑀 + 𝐵 ) / 2 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) ) )
76 75 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) / 2 ) = ( ( ( ( 2 · 𝑆 ) · 𝑋 ) + ( ( ( 𝑀 + 𝐵 ) / 2 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) ) / 2 ) )
77 16 73 subcld ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) / 2 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) ∈ ℂ )
78 72 77 36 38 divdird ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑆 ) · 𝑋 ) + ( ( ( 𝑀 + 𝐵 ) / 2 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) ) / 2 ) = ( ( ( ( 2 · 𝑆 ) · 𝑋 ) / 2 ) + ( ( ( ( 𝑀 + 𝐵 ) / 2 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) / 2 ) ) )
79 36 4 3 mulassd ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) · 𝑋 ) = ( 2 · ( 𝑆 · 𝑋 ) ) )
80 79 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝑆 ) · 𝑋 ) / 2 ) = ( ( 2 · ( 𝑆 · 𝑋 ) ) / 2 ) )
81 4 3 mulcld ⊢ ( 𝜑 → ( 𝑆 · 𝑋 ) ∈ ℂ )
82 81 36 38 divcan3d ⊢ ( 𝜑 → ( ( 2 · ( 𝑆 · 𝑋 ) ) / 2 ) = ( 𝑆 · 𝑋 ) )
83 80 82 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑆 ) · 𝑋 ) / 2 ) = ( 𝑆 · 𝑋 ) )
84 54 negcld ⊢ ( 𝜑 → - ( 𝑆 ↑ 2 ) ∈ ℂ )
85 1 halfcld ⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℂ )
86 84 85 subcld ⊢ ( 𝜑 → ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) ∈ ℂ )
87 54 86 73 subsub4d ⊢ ( 𝜑 → ( ( ( 𝑆 ↑ 2 ) − ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) = ( ( 𝑆 ↑ 2 ) − ( ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) + ( ( 𝐶 / 4 ) / 𝑆 ) ) ) )
88 14 1 36 38 divdird ⊢ ( 𝜑 → ( ( 𝑀 + 𝐵 ) / 2 ) = ( ( 𝑀 / 2 ) + ( 𝐵 / 2 ) ) )
89 54 2timesd ⊢ ( 𝜑 → ( 2 · ( 𝑆 ↑ 2 ) ) = ( ( 𝑆 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )
90 61 89 eqtrd ⊢ ( 𝜑 → ( 𝑀 / 2 ) = ( ( 𝑆 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )
91 90 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 / 2 ) + ( 𝐵 / 2 ) ) = ( ( ( 𝑆 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) + ( 𝐵 / 2 ) ) )
92 88 91 eqtrd ⊢ ( 𝜑 → ( ( 𝑀 + 𝐵 ) / 2 ) = ( ( ( 𝑆 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) + ( 𝐵 / 2 ) ) )
93 54 54 85 addassd ⊢ ( 𝜑 → ( ( ( 𝑆 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) + ( 𝐵 / 2 ) ) = ( ( 𝑆 ↑ 2 ) + ( ( 𝑆 ↑ 2 ) + ( 𝐵 / 2 ) ) ) )
94 54 85 addcld ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) + ( 𝐵 / 2 ) ) ∈ ℂ )
95 54 94 subnegd ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) − - ( ( 𝑆 ↑ 2 ) + ( 𝐵 / 2 ) ) ) = ( ( 𝑆 ↑ 2 ) + ( ( 𝑆 ↑ 2 ) + ( 𝐵 / 2 ) ) ) )
96 54 85 negdi2d ⊢ ( 𝜑 → - ( ( 𝑆 ↑ 2 ) + ( 𝐵 / 2 ) ) = ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) )
97 96 oveq2d ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) − - ( ( 𝑆 ↑ 2 ) + ( 𝐵 / 2 ) ) ) = ( ( 𝑆 ↑ 2 ) − ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) ) )
98 95 97 eqtr3d ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) + ( ( 𝑆 ↑ 2 ) + ( 𝐵 / 2 ) ) ) = ( ( 𝑆 ↑ 2 ) − ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) ) )
99 92 93 98 3eqtrd ⊢ ( 𝜑 → ( ( 𝑀 + 𝐵 ) / 2 ) = ( ( 𝑆 ↑ 2 ) − ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) ) )
100 99 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) / 2 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) = ( ( ( 𝑆 ↑ 2 ) − ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) )
101 8 oveq2d ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) = ( ( 𝑆 ↑ 2 ) − ( ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) + ( ( 𝐶 / 4 ) / 𝑆 ) ) ) )
102 87 100 101 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑀 + 𝐵 ) / 2 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) = ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) )
103 102 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) / 2 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) / 2 ) = ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) )
104 83 103 oveq12d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑆 ) · 𝑋 ) / 2 ) + ( ( ( ( 𝑀 + 𝐵 ) / 2 ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) / 2 ) ) = ( ( 𝑆 · 𝑋 ) + ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) )
105 76 78 104 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) / 2 ) = ( ( 𝑆 · 𝑋 ) + ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) )
106 44 105 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) / 2 ) + ( ( ( ( 𝑀 + 𝐵 ) / 2 ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) / 2 ) ) = ( ( ( 1 / 2 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑆 · 𝑋 ) + ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) ) )
107 41 43 106 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) / 2 ) = ( ( ( 1 / 2 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑆 · 𝑋 ) + ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) ) )
108 107 eqeq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) / 2 ) = 0 ↔ ( ( ( 1 / 2 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑆 · 𝑋 ) + ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) ) = 0 ) )
109 39 108 bitr3d ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) = 0 ↔ ( ( ( 1 / 2 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑆 · 𝑋 ) + ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) ) = 0 ) )
110 ax-1cn ⊢ 1 ∈ ℂ
111 halfcl ⊢ ( 1 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
112 110 111 mp1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
113 ax-1ne0 ⊢ 1 ≠ 0
114 110 10 113 37 divne0i ⊢ ( 1 / 2 ) ≠ 0
115 114 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ≠ 0 )
116 7 sqcld ⊢ ( 𝜑 → ( 𝐼 ↑ 2 ) ∈ ℂ )
117 54 116 subcld ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) ∈ ℂ )
118 117 halfcld ⊢ ( 𝜑 → ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ∈ ℂ )
119 110 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
120 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
121 120 a1i ⊢ ( 𝜑 → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
122 divmuldiv ⊢ ( ( ( 1 ∈ ℂ ∧ ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) ∈ ℂ ) ∧ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) ) → ( ( 1 / 2 ) · ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) = ( ( 1 · ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) ) / ( 2 · 2 ) ) )
123 119 117 121 121 122 syl22anc ⊢ ( 𝜑 → ( ( 1 / 2 ) · ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) = ( ( 1 · ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) ) / ( 2 · 2 ) ) )
124 117 mulid2d ⊢ ( 𝜑 → ( 1 · ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) ) = ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) )
125 2t2e4 ⊢ ( 2 · 2 ) = 4
126 125 a1i ⊢ ( 𝜑 → ( 2 · 2 ) = 4 )
127 124 126 oveq12d ⊢ ( 𝜑 → ( ( 1 · ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) ) / ( 2 · 2 ) ) = ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 4 ) )
128 123 127 eqtrd ⊢ ( 𝜑 → ( ( 1 / 2 ) · ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) = ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 4 ) )
129 128 oveq2d ⊢ ( 𝜑 → ( 4 · ( ( 1 / 2 ) · ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) ) = ( 4 · ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 4 ) ) )
130 117 21 23 divcan2d ⊢ ( 𝜑 → ( 4 · ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 4 ) ) = ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) )
131 129 130 eqtrd ⊢ ( 𝜑 → ( 4 · ( ( 1 / 2 ) · ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) ) = ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) )
132 131 oveq2d ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) − ( 4 · ( ( 1 / 2 ) · ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) ) ) = ( ( 𝑆 ↑ 2 ) − ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) ) )
133 54 116 nncand ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) − ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) ) = ( 𝐼 ↑ 2 ) )
134 132 133 eqtr2d ⊢ ( 𝜑 → ( 𝐼 ↑ 2 ) = ( ( 𝑆 ↑ 2 ) − ( 4 · ( ( 1 / 2 ) · ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) ) ) )
135 112 115 4 118 3 7 134 quad2 ⊢ ( 𝜑 → ( ( ( ( 1 / 2 ) · ( 𝑋 ↑ 2 ) ) + ( ( 𝑆 · 𝑋 ) + ( ( ( 𝑆 ↑ 2 ) − ( 𝐼 ↑ 2 ) ) / 2 ) ) ) = 0 ↔ ( 𝑋 = ( ( - 𝑆 + 𝐼 ) / ( 2 · ( 1 / 2 ) ) ) ∨ 𝑋 = ( ( - 𝑆 − 𝐼 ) / ( 2 · ( 1 / 2 ) ) ) ) ) )
136 10 37 recidi ⊢ ( 2 · ( 1 / 2 ) ) = 1
137 136 oveq2i ⊢ ( ( - 𝑆 + 𝐼 ) / ( 2 · ( 1 / 2 ) ) ) = ( ( - 𝑆 + 𝐼 ) / 1 )
138 4 negcld ⊢ ( 𝜑 → - 𝑆 ∈ ℂ )
139 138 7 addcld ⊢ ( 𝜑 → ( - 𝑆 + 𝐼 ) ∈ ℂ )
140 139 div1d ⊢ ( 𝜑 → ( ( - 𝑆 + 𝐼 ) / 1 ) = ( - 𝑆 + 𝐼 ) )
141 137 140 syl5eq ⊢ ( 𝜑 → ( ( - 𝑆 + 𝐼 ) / ( 2 · ( 1 / 2 ) ) ) = ( - 𝑆 + 𝐼 ) )
142 141 eqeq2d ⊢ ( 𝜑 → ( 𝑋 = ( ( - 𝑆 + 𝐼 ) / ( 2 · ( 1 / 2 ) ) ) ↔ 𝑋 = ( - 𝑆 + 𝐼 ) ) )
143 136 oveq2i ⊢ ( ( - 𝑆 − 𝐼 ) / ( 2 · ( 1 / 2 ) ) ) = ( ( - 𝑆 − 𝐼 ) / 1 )
144 138 7 subcld ⊢ ( 𝜑 → ( - 𝑆 − 𝐼 ) ∈ ℂ )
145 144 div1d ⊢ ( 𝜑 → ( ( - 𝑆 − 𝐼 ) / 1 ) = ( - 𝑆 − 𝐼 ) )
146 143 145 syl5eq ⊢ ( 𝜑 → ( ( - 𝑆 − 𝐼 ) / ( 2 · ( 1 / 2 ) ) ) = ( - 𝑆 − 𝐼 ) )
147 146 eqeq2d ⊢ ( 𝜑 → ( 𝑋 = ( ( - 𝑆 − 𝐼 ) / ( 2 · ( 1 / 2 ) ) ) ↔ 𝑋 = ( - 𝑆 − 𝐼 ) ) )
148 142 147 orbi12d ⊢ ( 𝜑 → ( ( 𝑋 = ( ( - 𝑆 + 𝐼 ) / ( 2 · ( 1 / 2 ) ) ) ∨ 𝑋 = ( ( - 𝑆 − 𝐼 ) / ( 2 · ( 1 / 2 ) ) ) ) ↔ ( 𝑋 = ( - 𝑆 + 𝐼 ) ∨ 𝑋 = ( - 𝑆 − 𝐼 ) ) ) )
149 109 135 148 3bitrd ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 2 ) + ( ( 𝑀 + 𝐵 ) / 2 ) ) + ( ( ( ( 𝑀 / 2 ) · 𝑋 ) − ( 𝐶 / 4 ) ) / 𝑆 ) ) = 0 ↔ ( 𝑋 = ( - 𝑆 + 𝐼 ) ∨ 𝑋 = ( - 𝑆 − 𝐼 ) ) ) )