MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dquart Structured version   Visualization version   GIF version

Theorem dquart 26896
Description: Solve a depressed quartic equation. To eliminate 𝑆, which is the square root of a solution 𝑀 to the resolvent cubic equation, apply cubic 26892 or one of its variants. (Contributed by Mario Carneiro, 6-May-2015.)
Hypotheses
Ref Expression
dquart.b (𝜑𝐵 ∈ ℂ)
dquart.c (𝜑𝐶 ∈ ℂ)
dquart.x (𝜑𝑋 ∈ ℂ)
dquart.s (𝜑𝑆 ∈ ℂ)
dquart.m (𝜑𝑀 = ((2 · 𝑆)↑2))
dquart.m0 (𝜑𝑀 ≠ 0)
dquart.i (𝜑𝐼 ∈ ℂ)
dquart.i2 (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆)))
dquart.d (𝜑𝐷 ∈ ℂ)
dquart.3 (𝜑 → (((𝑀↑3) + ((2 · 𝐵) · (𝑀↑2))) + ((((𝐵↑2) − (4 · 𝐷)) · 𝑀) + -(𝐶↑2))) = 0)
dquart.j (𝜑𝐽 ∈ ℂ)
dquart.j2 (𝜑 → (𝐽↑2) = ((-(𝑆↑2) − (𝐵 / 2)) − ((𝐶 / 4) / 𝑆)))
Assertion
Ref Expression
dquart (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ((𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆𝐼)) ∨ (𝑋 = (𝑆 + 𝐽) ∨ 𝑋 = (𝑆𝐽)))))

Proof of Theorem dquart
StepHypRef Expression
1 dquart.x . . . . . . . . 9 (𝜑𝑋 ∈ ℂ)
21sqcld 14184 . . . . . . . 8 (𝜑 → (𝑋↑2) ∈ ℂ)
3 dquart.m . . . . . . . . . . 11 (𝜑𝑀 = ((2 · 𝑆)↑2))
4 2cn 12341 . . . . . . . . . . . . 13 2 ∈ ℂ
5 dquart.s . . . . . . . . . . . . 13 (𝜑𝑆 ∈ ℂ)
6 mulcl 11239 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (2 · 𝑆) ∈ ℂ)
74, 5, 6sylancr 587 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑆) ∈ ℂ)
87sqcld 14184 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑆)↑2) ∈ ℂ)
93, 8eqeltrd 2841 . . . . . . . . . 10 (𝜑𝑀 ∈ ℂ)
10 dquart.b . . . . . . . . . 10 (𝜑𝐵 ∈ ℂ)
119, 10addcld 11280 . . . . . . . . 9 (𝜑 → (𝑀 + 𝐵) ∈ ℂ)
1211halfcld 12511 . . . . . . . 8 (𝜑 → ((𝑀 + 𝐵) / 2) ∈ ℂ)
13 binom2 14256 . . . . . . . 8 (((𝑋↑2) ∈ ℂ ∧ ((𝑀 + 𝐵) / 2) ∈ ℂ) → (((𝑋↑2) + ((𝑀 + 𝐵) / 2))↑2) = ((((𝑋↑2)↑2) + (2 · ((𝑋↑2) · ((𝑀 + 𝐵) / 2)))) + (((𝑀 + 𝐵) / 2)↑2)))
142, 12, 13syl2anc 584 . . . . . . 7 (𝜑 → (((𝑋↑2) + ((𝑀 + 𝐵) / 2))↑2) = ((((𝑋↑2)↑2) + (2 · ((𝑋↑2) · ((𝑀 + 𝐵) / 2)))) + (((𝑀 + 𝐵) / 2)↑2)))
15 2nn0 12543 . . . . . . . . . . . . 13 2 ∈ ℕ0
1615a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ∈ ℕ0)
171, 16, 16expmuld 14189 . . . . . . . . . . 11 (𝜑 → (𝑋↑(2 · 2)) = ((𝑋↑2)↑2))
18 2t2e4 12430 . . . . . . . . . . . 12 (2 · 2) = 4
1918oveq2i 7442 . . . . . . . . . . 11 (𝑋↑(2 · 2)) = (𝑋↑4)
2017, 19eqtr3di 2792 . . . . . . . . . 10 (𝜑 → ((𝑋↑2)↑2) = (𝑋↑4))
214a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ∈ ℂ)
2221, 2, 12mul12d 11470 . . . . . . . . . . 11 (𝜑 → (2 · ((𝑋↑2) · ((𝑀 + 𝐵) / 2))) = ((𝑋↑2) · (2 · ((𝑀 + 𝐵) / 2))))
23 2ne0 12370 . . . . . . . . . . . . . . 15 2 ≠ 0
2423a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ≠ 0)
2511, 21, 24divcan2d 12045 . . . . . . . . . . . . 13 (𝜑 → (2 · ((𝑀 + 𝐵) / 2)) = (𝑀 + 𝐵))
2625oveq2d 7447 . . . . . . . . . . . 12 (𝜑 → ((𝑋↑2) · (2 · ((𝑀 + 𝐵) / 2))) = ((𝑋↑2) · (𝑀 + 𝐵)))
272, 11mulcomd 11282 . . . . . . . . . . . 12 (𝜑 → ((𝑋↑2) · (𝑀 + 𝐵)) = ((𝑀 + 𝐵) · (𝑋↑2)))
2826, 27eqtrd 2777 . . . . . . . . . . 11 (𝜑 → ((𝑋↑2) · (2 · ((𝑀 + 𝐵) / 2))) = ((𝑀 + 𝐵) · (𝑋↑2)))
299, 10, 2adddird 11286 . . . . . . . . . . 11 (𝜑 → ((𝑀 + 𝐵) · (𝑋↑2)) = ((𝑀 · (𝑋↑2)) + (𝐵 · (𝑋↑2))))
3022, 28, 293eqtrd 2781 . . . . . . . . . 10 (𝜑 → (2 · ((𝑋↑2) · ((𝑀 + 𝐵) / 2))) = ((𝑀 · (𝑋↑2)) + (𝐵 · (𝑋↑2))))
3120, 30oveq12d 7449 . . . . . . . . 9 (𝜑 → (((𝑋↑2)↑2) + (2 · ((𝑋↑2) · ((𝑀 + 𝐵) / 2)))) = ((𝑋↑4) + ((𝑀 · (𝑋↑2)) + (𝐵 · (𝑋↑2)))))
32 4nn0 12545 . . . . . . . . . . 11 4 ∈ ℕ0
33 expcl 14120 . . . . . . . . . . 11 ((𝑋 ∈ ℂ ∧ 4 ∈ ℕ0) → (𝑋↑4) ∈ ℂ)
341, 32, 33sylancl 586 . . . . . . . . . 10 (𝜑 → (𝑋↑4) ∈ ℂ)
359, 2mulcld 11281 . . . . . . . . . 10 (𝜑 → (𝑀 · (𝑋↑2)) ∈ ℂ)
3610, 2mulcld 11281 . . . . . . . . . 10 (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
3734, 35, 36add12d 11488 . . . . . . . . 9 (𝜑 → ((𝑋↑4) + ((𝑀 · (𝑋↑2)) + (𝐵 · (𝑋↑2)))) = ((𝑀 · (𝑋↑2)) + ((𝑋↑4) + (𝐵 · (𝑋↑2)))))
3831, 37eqtrd 2777 . . . . . . . 8 (𝜑 → (((𝑋↑2)↑2) + (2 · ((𝑋↑2) · ((𝑀 + 𝐵) / 2)))) = ((𝑀 · (𝑋↑2)) + ((𝑋↑4) + (𝐵 · (𝑋↑2)))))
3938oveq1d 7446 . . . . . . 7 (𝜑 → ((((𝑋↑2)↑2) + (2 · ((𝑋↑2) · ((𝑀 + 𝐵) / 2)))) + (((𝑀 + 𝐵) / 2)↑2)) = (((𝑀 · (𝑋↑2)) + ((𝑋↑4) + (𝐵 · (𝑋↑2)))) + (((𝑀 + 𝐵) / 2)↑2)))
4034, 36addcld 11280 . . . . . . . 8 (𝜑 → ((𝑋↑4) + (𝐵 · (𝑋↑2))) ∈ ℂ)
4112sqcld 14184 . . . . . . . 8 (𝜑 → (((𝑀 + 𝐵) / 2)↑2) ∈ ℂ)
4235, 40, 41addassd 11283 . . . . . . 7 (𝜑 → (((𝑀 · (𝑋↑2)) + ((𝑋↑4) + (𝐵 · (𝑋↑2)))) + (((𝑀 + 𝐵) / 2)↑2)) = ((𝑀 · (𝑋↑2)) + (((𝑋↑4) + (𝐵 · (𝑋↑2))) + (((𝑀 + 𝐵) / 2)↑2))))
4314, 39, 423eqtrd 2781 . . . . . 6 (𝜑 → (((𝑋↑2) + ((𝑀 + 𝐵) / 2))↑2) = ((𝑀 · (𝑋↑2)) + (((𝑋↑4) + (𝐵 · (𝑋↑2))) + (((𝑀 + 𝐵) / 2)↑2))))
449halfcld 12511 . . . . . . . . . . . 12 (𝜑 → (𝑀 / 2) ∈ ℂ)
4544, 1mulcld 11281 . . . . . . . . . . 11 (𝜑 → ((𝑀 / 2) · 𝑋) ∈ ℂ)
46 dquart.c . . . . . . . . . . . 12 (𝜑𝐶 ∈ ℂ)
47 4cn 12351 . . . . . . . . . . . . 13 4 ∈ ℂ
4847a1i 11 . . . . . . . . . . . 12 (𝜑 → 4 ∈ ℂ)
49 4ne0 12374 . . . . . . . . . . . . 13 4 ≠ 0
5049a1i 11 . . . . . . . . . . . 12 (𝜑 → 4 ≠ 0)
5146, 48, 50divcld 12043 . . . . . . . . . . 11 (𝜑 → (𝐶 / 4) ∈ ℂ)
5245, 51subcld 11620 . . . . . . . . . 10 (𝜑 → (((𝑀 / 2) · 𝑋) − (𝐶 / 4)) ∈ ℂ)
53 dquart.m0 . . . . . . . . . . . . . 14 (𝜑𝑀 ≠ 0)
543, 53eqnetrrd 3009 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝑆)↑2) ≠ 0)
55 sqne0 14163 . . . . . . . . . . . . . 14 ((2 · 𝑆) ∈ ℂ → (((2 · 𝑆)↑2) ≠ 0 ↔ (2 · 𝑆) ≠ 0))
567, 55syl 17 . . . . . . . . . . . . 13 (𝜑 → (((2 · 𝑆)↑2) ≠ 0 ↔ (2 · 𝑆) ≠ 0))
5754, 56mpbid 232 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑆) ≠ 0)
58 mulne0b 11904 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((2 ≠ 0 ∧ 𝑆 ≠ 0) ↔ (2 · 𝑆) ≠ 0))
594, 5, 58sylancr 587 . . . . . . . . . . . 12 (𝜑 → ((2 ≠ 0 ∧ 𝑆 ≠ 0) ↔ (2 · 𝑆) ≠ 0))
6057, 59mpbird 257 . . . . . . . . . . 11 (𝜑 → (2 ≠ 0 ∧ 𝑆 ≠ 0))
6160simprd 495 . . . . . . . . . 10 (𝜑𝑆 ≠ 0)
6252, 5, 21, 61, 24divcan5d 12069 . . . . . . . . 9 (𝜑 → ((2 · (((𝑀 / 2) · 𝑋) − (𝐶 / 4))) / (2 · 𝑆)) = ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆))
6321, 45, 51subdid 11719 . . . . . . . . . . 11 (𝜑 → (2 · (((𝑀 / 2) · 𝑋) − (𝐶 / 4))) = ((2 · ((𝑀 / 2) · 𝑋)) − (2 · (𝐶 / 4))))
6421, 44, 1mulassd 11284 . . . . . . . . . . . . 13 (𝜑 → ((2 · (𝑀 / 2)) · 𝑋) = (2 · ((𝑀 / 2) · 𝑋)))
659, 21, 24divcan2d 12045 . . . . . . . . . . . . . 14 (𝜑 → (2 · (𝑀 / 2)) = 𝑀)
6665oveq1d 7446 . . . . . . . . . . . . 13 (𝜑 → ((2 · (𝑀 / 2)) · 𝑋) = (𝑀 · 𝑋))
6764, 66eqtr3d 2779 . . . . . . . . . . . 12 (𝜑 → (2 · ((𝑀 / 2) · 𝑋)) = (𝑀 · 𝑋))
6821, 46, 48, 50divassd 12078 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐶) / 4) = (2 · (𝐶 / 4)))
6918oveq2i 7442 . . . . . . . . . . . . . 14 ((2 · 𝐶) / (2 · 2)) = ((2 · 𝐶) / 4)
7046, 21, 21, 24, 24divcan5d 12069 . . . . . . . . . . . . . 14 (𝜑 → ((2 · 𝐶) / (2 · 2)) = (𝐶 / 2))
7169, 70eqtr3id 2791 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐶) / 4) = (𝐶 / 2))
7268, 71eqtr3d 2779 . . . . . . . . . . . 12 (𝜑 → (2 · (𝐶 / 4)) = (𝐶 / 2))
7367, 72oveq12d 7449 . . . . . . . . . . 11 (𝜑 → ((2 · ((𝑀 / 2) · 𝑋)) − (2 · (𝐶 / 4))) = ((𝑀 · 𝑋) − (𝐶 / 2)))
7463, 73eqtrd 2777 . . . . . . . . . 10 (𝜑 → (2 · (((𝑀 / 2) · 𝑋) − (𝐶 / 4))) = ((𝑀 · 𝑋) − (𝐶 / 2)))
7574oveq1d 7446 . . . . . . . . 9 (𝜑 → ((2 · (((𝑀 / 2) · 𝑋) − (𝐶 / 4))) / (2 · 𝑆)) = (((𝑀 · 𝑋) − (𝐶 / 2)) / (2 · 𝑆)))
7662, 75eqtr3d 2779 . . . . . . . 8 (𝜑 → ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆) = (((𝑀 · 𝑋) − (𝐶 / 2)) / (2 · 𝑆)))
7776oveq1d 7446 . . . . . . 7 (𝜑 → (((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)↑2) = ((((𝑀 · 𝑋) − (𝐶 / 2)) / (2 · 𝑆))↑2))
789, 1mulcld 11281 . . . . . . . . 9 (𝜑 → (𝑀 · 𝑋) ∈ ℂ)
7946halfcld 12511 . . . . . . . . 9 (𝜑 → (𝐶 / 2) ∈ ℂ)
8078, 79subcld 11620 . . . . . . . 8 (𝜑 → ((𝑀 · 𝑋) − (𝐶 / 2)) ∈ ℂ)
8180, 7, 57sqdivd 14199 . . . . . . 7 (𝜑 → ((((𝑀 · 𝑋) − (𝐶 / 2)) / (2 · 𝑆))↑2) = ((((𝑀 · 𝑋) − (𝐶 / 2))↑2) / ((2 · 𝑆)↑2)))
829sqcld 14184 . . . . . . . . . . 11 (𝜑 → (𝑀↑2) ∈ ℂ)
8382, 2mulcld 11281 . . . . . . . . . 10 (𝜑 → ((𝑀↑2) · (𝑋↑2)) ∈ ℂ)
8478, 46mulcld 11281 . . . . . . . . . 10 (𝜑 → ((𝑀 · 𝑋) · 𝐶) ∈ ℂ)
8583, 84subcld 11620 . . . . . . . . 9 (𝜑 → (((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)) ∈ ℂ)
8646sqcld 14184 . . . . . . . . . 10 (𝜑 → (𝐶↑2) ∈ ℂ)
8786, 48, 50divcld 12043 . . . . . . . . 9 (𝜑 → ((𝐶↑2) / 4) ∈ ℂ)
8885, 87, 9, 53divdird 12081 . . . . . . . 8 (𝜑 → (((((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)) + ((𝐶↑2) / 4)) / 𝑀) = (((((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)) / 𝑀) + (((𝐶↑2) / 4) / 𝑀)))
89 binom2sub 14259 . . . . . . . . . . 11 (((𝑀 · 𝑋) ∈ ℂ ∧ (𝐶 / 2) ∈ ℂ) → (((𝑀 · 𝑋) − (𝐶 / 2))↑2) = ((((𝑀 · 𝑋)↑2) − (2 · ((𝑀 · 𝑋) · (𝐶 / 2)))) + ((𝐶 / 2)↑2)))
9078, 79, 89syl2anc 584 . . . . . . . . . 10 (𝜑 → (((𝑀 · 𝑋) − (𝐶 / 2))↑2) = ((((𝑀 · 𝑋)↑2) − (2 · ((𝑀 · 𝑋) · (𝐶 / 2)))) + ((𝐶 / 2)↑2)))
919, 1sqmuld 14198 . . . . . . . . . . . 12 (𝜑 → ((𝑀 · 𝑋)↑2) = ((𝑀↑2) · (𝑋↑2)))
9221, 78, 79mul12d 11470 . . . . . . . . . . . . 13 (𝜑 → (2 · ((𝑀 · 𝑋) · (𝐶 / 2))) = ((𝑀 · 𝑋) · (2 · (𝐶 / 2))))
9346, 21, 24divcan2d 12045 . . . . . . . . . . . . . 14 (𝜑 → (2 · (𝐶 / 2)) = 𝐶)
9493oveq2d 7447 . . . . . . . . . . . . 13 (𝜑 → ((𝑀 · 𝑋) · (2 · (𝐶 / 2))) = ((𝑀 · 𝑋) · 𝐶))
9592, 94eqtrd 2777 . . . . . . . . . . . 12 (𝜑 → (2 · ((𝑀 · 𝑋) · (𝐶 / 2))) = ((𝑀 · 𝑋) · 𝐶))
9691, 95oveq12d 7449 . . . . . . . . . . 11 (𝜑 → (((𝑀 · 𝑋)↑2) − (2 · ((𝑀 · 𝑋) · (𝐶 / 2)))) = (((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)))
9746, 21, 24sqdivd 14199 . . . . . . . . . . . 12 (𝜑 → ((𝐶 / 2)↑2) = ((𝐶↑2) / (2↑2)))
98 sq2 14236 . . . . . . . . . . . . 13 (2↑2) = 4
9998oveq2i 7442 . . . . . . . . . . . 12 ((𝐶↑2) / (2↑2)) = ((𝐶↑2) / 4)
10097, 99eqtrdi 2793 . . . . . . . . . . 11 (𝜑 → ((𝐶 / 2)↑2) = ((𝐶↑2) / 4))
10196, 100oveq12d 7449 . . . . . . . . . 10 (𝜑 → ((((𝑀 · 𝑋)↑2) − (2 · ((𝑀 · 𝑋) · (𝐶 / 2)))) + ((𝐶 / 2)↑2)) = ((((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)) + ((𝐶↑2) / 4)))
10290, 101eqtr2d 2778 . . . . . . . . 9 (𝜑 → ((((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)) + ((𝐶↑2) / 4)) = (((𝑀 · 𝑋) − (𝐶 / 2))↑2))
103102, 3oveq12d 7449 . . . . . . . 8 (𝜑 → (((((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)) + ((𝐶↑2) / 4)) / 𝑀) = ((((𝑀 · 𝑋) − (𝐶 / 2))↑2) / ((2 · 𝑆)↑2)))
10483, 84, 9, 53divsubdird 12082 . . . . . . . . . . 11 (𝜑 → ((((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)) / 𝑀) = ((((𝑀↑2) · (𝑋↑2)) / 𝑀) − (((𝑀 · 𝑋) · 𝐶) / 𝑀)))
10582, 2, 9, 53div23d 12080 . . . . . . . . . . . . 13 (𝜑 → (((𝑀↑2) · (𝑋↑2)) / 𝑀) = (((𝑀↑2) / 𝑀) · (𝑋↑2)))
1069sqvald 14183 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
107106oveq1d 7446 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀↑2) / 𝑀) = ((𝑀 · 𝑀) / 𝑀))
1089, 9, 53divcan3d 12048 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀 · 𝑀) / 𝑀) = 𝑀)
109107, 108eqtrd 2777 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀↑2) / 𝑀) = 𝑀)
110109oveq1d 7446 . . . . . . . . . . . . 13 (𝜑 → (((𝑀↑2) / 𝑀) · (𝑋↑2)) = (𝑀 · (𝑋↑2)))
111105, 110eqtrd 2777 . . . . . . . . . . . 12 (𝜑 → (((𝑀↑2) · (𝑋↑2)) / 𝑀) = (𝑀 · (𝑋↑2)))
1129, 1, 46mul32d 11471 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀 · 𝑋) · 𝐶) = ((𝑀 · 𝐶) · 𝑋))
1139, 46, 1mulassd 11284 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀 · 𝐶) · 𝑋) = (𝑀 · (𝐶 · 𝑋)))
114112, 113eqtrd 2777 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 · 𝑋) · 𝐶) = (𝑀 · (𝐶 · 𝑋)))
115114oveq1d 7446 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 · 𝑋) · 𝐶) / 𝑀) = ((𝑀 · (𝐶 · 𝑋)) / 𝑀))
11646, 1mulcld 11281 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · 𝑋) ∈ ℂ)
117116, 9, 53divcan3d 12048 . . . . . . . . . . . . 13 (𝜑 → ((𝑀 · (𝐶 · 𝑋)) / 𝑀) = (𝐶 · 𝑋))
118115, 117eqtrd 2777 . . . . . . . . . . . 12 (𝜑 → (((𝑀 · 𝑋) · 𝐶) / 𝑀) = (𝐶 · 𝑋))
119111, 118oveq12d 7449 . . . . . . . . . . 11 (𝜑 → ((((𝑀↑2) · (𝑋↑2)) / 𝑀) − (((𝑀 · 𝑋) · 𝐶) / 𝑀)) = ((𝑀 · (𝑋↑2)) − (𝐶 · 𝑋)))
120104, 119eqtrd 2777 . . . . . . . . . 10 (𝜑 → ((((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)) / 𝑀) = ((𝑀 · (𝑋↑2)) − (𝐶 · 𝑋)))
121120oveq1d 7446 . . . . . . . . 9 (𝜑 → (((((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)) / 𝑀) + (((𝐶↑2) / 4) / 𝑀)) = (((𝑀 · (𝑋↑2)) − (𝐶 · 𝑋)) + (((𝐶↑2) / 4) / 𝑀)))
12287, 9, 53divcld 12043 . . . . . . . . . 10 (𝜑 → (((𝐶↑2) / 4) / 𝑀) ∈ ℂ)
12335, 116, 122subsubd 11648 . . . . . . . . 9 (𝜑 → ((𝑀 · (𝑋↑2)) − ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀))) = (((𝑀 · (𝑋↑2)) − (𝐶 · 𝑋)) + (((𝐶↑2) / 4) / 𝑀)))
124121, 123eqtr4d 2780 . . . . . . . 8 (𝜑 → (((((𝑀↑2) · (𝑋↑2)) − ((𝑀 · 𝑋) · 𝐶)) / 𝑀) + (((𝐶↑2) / 4) / 𝑀)) = ((𝑀 · (𝑋↑2)) − ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀))))
12588, 103, 1243eqtr3d 2785 . . . . . . 7 (𝜑 → ((((𝑀 · 𝑋) − (𝐶 / 2))↑2) / ((2 · 𝑆)↑2)) = ((𝑀 · (𝑋↑2)) − ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀))))
12677, 81, 1253eqtrd 2781 . . . . . 6 (𝜑 → (((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)↑2) = ((𝑀 · (𝑋↑2)) − ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀))))
12743, 126oveq12d 7449 . . . . 5 (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2))↑2) − (((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)↑2)) = (((𝑀 · (𝑋↑2)) + (((𝑋↑4) + (𝐵 · (𝑋↑2))) + (((𝑀 + 𝐵) / 2)↑2))) − ((𝑀 · (𝑋↑2)) − ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀)))))
12840, 41addcld 11280 . . . . . 6 (𝜑 → (((𝑋↑4) + (𝐵 · (𝑋↑2))) + (((𝑀 + 𝐵) / 2)↑2)) ∈ ℂ)
129116, 122subcld 11620 . . . . . 6 (𝜑 → ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀)) ∈ ℂ)
13035, 128, 129pnncand 11659 . . . . 5 (𝜑 → (((𝑀 · (𝑋↑2)) + (((𝑋↑4) + (𝐵 · (𝑋↑2))) + (((𝑀 + 𝐵) / 2)↑2))) − ((𝑀 · (𝑋↑2)) − ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀)))) = ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + (((𝑀 + 𝐵) / 2)↑2)) + ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀))))
131122negcld 11607 . . . . . . 7 (𝜑 → -(((𝐶↑2) / 4) / 𝑀) ∈ ℂ)
13240, 41, 116, 131add4d 11490 . . . . . 6 (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + (((𝑀 + 𝐵) / 2)↑2)) + ((𝐶 · 𝑋) + -(((𝐶↑2) / 4) / 𝑀))) = ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + (𝐶 · 𝑋)) + ((((𝑀 + 𝐵) / 2)↑2) + -(((𝐶↑2) / 4) / 𝑀))))
133116, 122negsubd 11626 . . . . . . 7 (𝜑 → ((𝐶 · 𝑋) + -(((𝐶↑2) / 4) / 𝑀)) = ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀)))
134133oveq2d 7447 . . . . . 6 (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + (((𝑀 + 𝐵) / 2)↑2)) + ((𝐶 · 𝑋) + -(((𝐶↑2) / 4) / 𝑀))) = ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + (((𝑀 + 𝐵) / 2)↑2)) + ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀))))
13541, 122negsubd 11626 . . . . . . . . 9 (𝜑 → ((((𝑀 + 𝐵) / 2)↑2) + -(((𝐶↑2) / 4) / 𝑀)) = ((((𝑀 + 𝐵) / 2)↑2) − (((𝐶↑2) / 4) / 𝑀)))
136 dquart.i . . . . . . . . . 10 (𝜑𝐼 ∈ ℂ)
137 dquart.i2 . . . . . . . . . 10 (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆)))
138 dquart.d . . . . . . . . . 10 (𝜑𝐷 ∈ ℂ)
139 dquart.3 . . . . . . . . . 10 (𝜑 → (((𝑀↑3) + ((2 · 𝐵) · (𝑀↑2))) + ((((𝐵↑2) − (4 · 𝐷)) · 𝑀) + -(𝐶↑2))) = 0)
14010, 46, 1, 5, 3, 53, 136, 137, 138, 139dquartlem2 26895 . . . . . . . . 9 (𝜑 → ((((𝑀 + 𝐵) / 2)↑2) − (((𝐶↑2) / 4) / 𝑀)) = 𝐷)
141135, 140eqtrd 2777 . . . . . . . 8 (𝜑 → ((((𝑀 + 𝐵) / 2)↑2) + -(((𝐶↑2) / 4) / 𝑀)) = 𝐷)
142141oveq2d 7447 . . . . . . 7 (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + (𝐶 · 𝑋)) + ((((𝑀 + 𝐵) / 2)↑2) + -(((𝐶↑2) / 4) / 𝑀))) = ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + (𝐶 · 𝑋)) + 𝐷))
14340, 116, 138addassd 11283 . . . . . . 7 (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + (𝐶 · 𝑋)) + 𝐷) = (((𝑋↑4) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
144142, 143eqtrd 2777 . . . . . 6 (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + (𝐶 · 𝑋)) + ((((𝑀 + 𝐵) / 2)↑2) + -(((𝐶↑2) / 4) / 𝑀))) = (((𝑋↑4) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
145132, 134, 1443eqtr3d 2785 . . . . 5 (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + (((𝑀 + 𝐵) / 2)↑2)) + ((𝐶 · 𝑋) − (((𝐶↑2) / 4) / 𝑀))) = (((𝑋↑4) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
146127, 130, 1453eqtrd 2781 . . . 4 (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2))↑2) − (((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)↑2)) = (((𝑋↑4) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
1472, 12addcld 11280 . . . . 5 (𝜑 → ((𝑋↑2) + ((𝑀 + 𝐵) / 2)) ∈ ℂ)
14852, 5, 61divcld 12043 . . . . 5 (𝜑 → ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆) ∈ ℂ)
149 subsq 14249 . . . . 5 ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) ∈ ℂ ∧ ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆) ∈ ℂ) → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2))↑2) − (((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)↑2)) = ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) · (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆))))
150147, 148, 149syl2anc 584 . . . 4 (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2))↑2) − (((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)↑2)) = ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) · (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆))))
151146, 150eqtr3d 2779 . . 3 (𝜑 → (((𝑋↑4) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) · (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆))))
152151eqeq1d 2739 . 2 (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) · (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆))) = 0))
153147, 148addcld 11280 . . 3 (𝜑 → (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) ∈ ℂ)
154147, 148subcld 11620 . . 3 (𝜑 → (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) ∈ ℂ)
155153, 154mul0ord 11913 . 2 (𝜑 → (((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) · (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆))) = 0 ↔ ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0 ∨ (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0)))
15610, 46, 1, 5, 3, 53, 136, 137dquartlem1 26894 . . 3 (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0 ↔ (𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆𝐼))))
1575negcld 11607 . . . . 5 (𝜑 → -𝑆 ∈ ℂ)
158 sqneg 14156 . . . . . . . 8 ((2 · 𝑆) ∈ ℂ → (-(2 · 𝑆)↑2) = ((2 · 𝑆)↑2))
1597, 158syl 17 . . . . . . 7 (𝜑 → (-(2 · 𝑆)↑2) = ((2 · 𝑆)↑2))
1603, 159eqtr4d 2780 . . . . . 6 (𝜑𝑀 = (-(2 · 𝑆)↑2))
161 mulneg2 11700 . . . . . . . 8 ((2 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (2 · -𝑆) = -(2 · 𝑆))
1624, 5, 161sylancr 587 . . . . . . 7 (𝜑 → (2 · -𝑆) = -(2 · 𝑆))
163162oveq1d 7446 . . . . . 6 (𝜑 → ((2 · -𝑆)↑2) = (-(2 · 𝑆)↑2))
164160, 163eqtr4d 2780 . . . . 5 (𝜑𝑀 = ((2 · -𝑆)↑2))
165 dquart.j . . . . 5 (𝜑𝐽 ∈ ℂ)
166 dquart.j2 . . . . . 6 (𝜑 → (𝐽↑2) = ((-(𝑆↑2) − (𝐵 / 2)) − ((𝐶 / 4) / 𝑆)))
1675sqcld 14184 . . . . . . . . 9 (𝜑 → (𝑆↑2) ∈ ℂ)
168167negcld 11607 . . . . . . . 8 (𝜑 → -(𝑆↑2) ∈ ℂ)
16910halfcld 12511 . . . . . . . 8 (𝜑 → (𝐵 / 2) ∈ ℂ)
170168, 169subcld 11620 . . . . . . 7 (𝜑 → (-(𝑆↑2) − (𝐵 / 2)) ∈ ℂ)
17151, 5, 61divcld 12043 . . . . . . 7 (𝜑 → ((𝐶 / 4) / 𝑆) ∈ ℂ)
172170, 171negsubd 11626 . . . . . 6 (𝜑 → ((-(𝑆↑2) − (𝐵 / 2)) + -((𝐶 / 4) / 𝑆)) = ((-(𝑆↑2) − (𝐵 / 2)) − ((𝐶 / 4) / 𝑆)))
173 sqneg 14156 . . . . . . . . . . 11 (𝑆 ∈ ℂ → (-𝑆↑2) = (𝑆↑2))
1745, 173syl 17 . . . . . . . . . 10 (𝜑 → (-𝑆↑2) = (𝑆↑2))
175174eqcomd 2743 . . . . . . . . 9 (𝜑 → (𝑆↑2) = (-𝑆↑2))
176175negeqd 11502 . . . . . . . 8 (𝜑 → -(𝑆↑2) = -(-𝑆↑2))
177176oveq1d 7446 . . . . . . 7 (𝜑 → (-(𝑆↑2) − (𝐵 / 2)) = (-(-𝑆↑2) − (𝐵 / 2)))
17851, 5, 61divneg2d 12057 . . . . . . 7 (𝜑 → -((𝐶 / 4) / 𝑆) = ((𝐶 / 4) / -𝑆))
179177, 178oveq12d 7449 . . . . . 6 (𝜑 → ((-(𝑆↑2) − (𝐵 / 2)) + -((𝐶 / 4) / 𝑆)) = ((-(-𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / -𝑆)))
180166, 172, 1793eqtr2d 2783 . . . . 5 (𝜑 → (𝐽↑2) = ((-(-𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / -𝑆)))
18110, 46, 1, 157, 164, 53, 165, 180dquartlem1 26894 . . . 4 (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / -𝑆)) = 0 ↔ (𝑋 = (--𝑆 + 𝐽) ∨ 𝑋 = (--𝑆𝐽))))
18252, 5, 61divneg2d 12057 . . . . . . 7 (𝜑 → -((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆) = ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / -𝑆))
183182oveq2d 7447 . . . . . 6 (𝜑 → (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + -((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / -𝑆)))
184147, 148negsubd 11626 . . . . . 6 (𝜑 → (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + -((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)))
185183, 184eqtr3d 2779 . . . . 5 (𝜑 → (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / -𝑆)) = (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)))
186185eqeq1d 2739 . . . 4 (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / -𝑆)) = 0 ↔ (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0))
1875negnegd 11611 . . . . . . 7 (𝜑 → --𝑆 = 𝑆)
188187oveq1d 7446 . . . . . 6 (𝜑 → (--𝑆 + 𝐽) = (𝑆 + 𝐽))
189188eqeq2d 2748 . . . . 5 (𝜑 → (𝑋 = (--𝑆 + 𝐽) ↔ 𝑋 = (𝑆 + 𝐽)))
190187oveq1d 7446 . . . . . 6 (𝜑 → (--𝑆𝐽) = (𝑆𝐽))
191190eqeq2d 2748 . . . . 5 (𝜑 → (𝑋 = (--𝑆𝐽) ↔ 𝑋 = (𝑆𝐽)))
192189, 191orbi12d 919 . . . 4 (𝜑 → ((𝑋 = (--𝑆 + 𝐽) ∨ 𝑋 = (--𝑆𝐽)) ↔ (𝑋 = (𝑆 + 𝐽) ∨ 𝑋 = (𝑆𝐽))))
193181, 186, 1923bitr3d 309 . . 3 (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0 ↔ (𝑋 = (𝑆 + 𝐽) ∨ 𝑋 = (𝑆𝐽))))
194156, 193orbi12d 919 . 2 (𝜑 → (((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0 ∨ (((𝑋↑2) + ((𝑀 + 𝐵) / 2)) − ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0) ↔ ((𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆𝐼)) ∨ (𝑋 = (𝑆 + 𝐽) ∨ 𝑋 = (𝑆𝐽)))))
195152, 155, 1943bitrd 305 1 (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ((𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆𝐼)) ∨ (𝑋 = (𝑆 + 𝐽) ∨ 𝑋 = (𝑆𝐽)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wcel 2108  wne 2940  (class class class)co 7431  cc 11153  0cc0 11155   + caddc 11158   · cmul 11160  cmin 11492  -cneg 11493   / cdiv 11920  2c2 12321  3c3 12322  4c4 12323  0cn0 12526  cexp 14102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-n0 12527  df-z 12614  df-uz 12879  df-seq 14043  df-exp 14103
This theorem is referenced by:  quart  26904
  Copyright terms: Public domain W3C validator