Proof of Theorem requad1
Step | Hyp | Ref
| Expression |
1 | | requad2.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | recnd 10861 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | 2 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℂ) |
4 | | requad2.z |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≠ 0) |
5 | 4 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝐴 ≠ 0) |
6 | | requad2.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
7 | 6 | recnd 10861 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
8 | 7 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℂ) |
9 | | requad2.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) |
10 | 9 | recnd 10861 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
11 | 10 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝐶 ∈ ℂ) |
12 | | recn 10819 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
13 | 12 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
14 | | requad2.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) |
15 | 14 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) |
16 | 3, 5, 8, 11, 13, 15 | quad 25723 |
. . . . 5
⊢ (((𝜑 ∧ 0 ≤ 𝐷) ∧ 𝑥 ∈ ℝ) → (((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))) |
17 | 16 | reubidva 3300 |
. . . 4
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ∃!𝑥 ∈ ℝ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))) |
18 | 6 | renegcld 11259 |
. . . . . . . 8
⊢ (𝜑 → -𝐵 ∈ ℝ) |
19 | 18 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → -𝐵 ∈ ℝ) |
20 | 6 | resqcld 13817 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵↑2) ∈ ℝ) |
21 | | 4re 11914 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 4 ∈
ℝ) |
23 | 1, 9 | remulcld 10863 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℝ) |
24 | 22, 23 | remulcld 10863 |
. . . . . . . . . 10
⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℝ) |
25 | 20, 24 | resubcld 11260 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℝ) |
26 | 14, 25 | eqeltrd 2838 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℝ) |
27 | | resqrtcl 14817 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℝ ∧ 0 ≤
𝐷) →
(√‘𝐷) ∈
ℝ) |
28 | 26, 27 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (√‘𝐷) ∈ ℝ) |
29 | 19, 28 | readdcld 10862 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (-𝐵 + (√‘𝐷)) ∈ ℝ) |
30 | | 2re 11904 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ) |
32 | 31, 1 | remulcld 10863 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐴) ∈
ℝ) |
33 | 32 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ∈ ℝ) |
34 | | 2cnd 11908 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℂ) |
35 | | 2ne0 11934 |
. . . . . . . . 9
⊢ 2 ≠
0 |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ≠ 0) |
37 | 34, 2, 36, 4 | mulne0d 11484 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐴) ≠ 0) |
38 | 37 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ≠ 0) |
39 | 29, 33, 38 | redivcld 11660 |
. . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ) |
40 | 19, 28 | resubcld 11260 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (-𝐵 − (√‘𝐷)) ∈ ℝ) |
41 | 40, 33, 38 | redivcld 11660 |
. . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ∈ ℝ) |
42 | | euoreqb 44273 |
. . . . 5
⊢
((((-𝐵 +
(√‘𝐷)) / (2
· 𝐴)) ∈ ℝ
∧ ((-𝐵 −
(√‘𝐷)) / (2
· 𝐴)) ∈
ℝ) → (∃!𝑥
∈ ℝ (𝑥 =
((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) ↔ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))) |
43 | 39, 41, 42 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑥 ∈ ℝ (𝑥 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑥 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))) ↔ ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))) |
44 | 7 | negcld 11176 |
. . . . . . . 8
⊢ (𝜑 → -𝐵 ∈ ℂ) |
45 | 26 | recnd 10861 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℂ) |
46 | 45 | sqrtcld 15001 |
. . . . . . . 8
⊢ (𝜑 → (√‘𝐷) ∈
ℂ) |
47 | 32 | recnd 10861 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝐴) ∈
ℂ) |
48 | 44, 46, 47, 37 | divdird 11646 |
. . . . . . 7
⊢ (𝜑 → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴)))) |
49 | 48 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴)))) |
50 | 44, 46, 47, 37 | divsubdird 11647 |
. . . . . . . 8
⊢ (𝜑 → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) − ((√‘𝐷) / (2 · 𝐴)))) |
51 | 50 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) − ((√‘𝐷) / (2 · 𝐴)))) |
52 | 44, 47, 37 | divcld 11608 |
. . . . . . . . 9
⊢ (𝜑 → (-𝐵 / (2 · 𝐴)) ∈ ℂ) |
53 | 52 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (-𝐵 / (2 · 𝐴)) ∈ ℂ) |
54 | 46, 47, 37 | divcld 11608 |
. . . . . . . . 9
⊢ (𝜑 → ((√‘𝐷) / (2 · 𝐴)) ∈
ℂ) |
55 | 54 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) / (2 · 𝐴)) ∈ ℂ) |
56 | 53, 55 | negsubd 11195 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 / (2 · 𝐴)) + -((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) − ((√‘𝐷) / (2 · 𝐴)))) |
57 | 46 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (√‘𝐷) ∈ ℂ) |
58 | 47 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (2 · 𝐴) ∈ ℂ) |
59 | 57, 58, 38 | divnegd 11621 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → -((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴))) |
60 | 59 | oveq2d 7229 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 / (2 · 𝐴)) + -((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴)))) |
61 | 51, 56, 60 | 3eqtr2d 2783 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴)))) |
62 | 49, 61 | eqeq12d 2753 |
. . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ ((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴))))) |
63 | 46 | negcld 11176 |
. . . . . . . . 9
⊢ (𝜑 → -(√‘𝐷) ∈
ℂ) |
64 | 63, 47, 37 | divcld 11608 |
. . . . . . . 8
⊢ (𝜑 → (-(√‘𝐷) / (2 · 𝐴)) ∈
ℂ) |
65 | 64 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (-(√‘𝐷) / (2 · 𝐴)) ∈ ℂ) |
66 | 53, 55, 65 | addcand 11035 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴))) ↔ ((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴)))) |
67 | | div11 11518 |
. . . . . . . 8
⊢
(((√‘𝐷)
∈ ℂ ∧ -(√‘𝐷) ∈ ℂ ∧ ((2 · 𝐴) ∈ ℂ ∧ (2
· 𝐴) ≠ 0)) →
(((√‘𝐷) / (2
· 𝐴)) =
(-(√‘𝐷) / (2
· 𝐴)) ↔
(√‘𝐷) =
-(√‘𝐷))) |
68 | 46, 63, 47, 37, 67 | syl112anc 1376 |
. . . . . . 7
⊢ (𝜑 → (((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴)) ↔ (√‘𝐷) = -(√‘𝐷))) |
69 | 68 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((√‘𝐷) / (2 · 𝐴)) = (-(√‘𝐷) / (2 · 𝐴)) ↔ (√‘𝐷) = -(√‘𝐷))) |
70 | 57 | eqnegd 11553 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) = -(√‘𝐷) ↔ (√‘𝐷) = 0)) |
71 | | sqrt00 14827 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℝ ∧ 0 ≤
𝐷) →
((√‘𝐷) = 0
↔ 𝐷 =
0)) |
72 | 26, 71 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) = 0 ↔ 𝐷 = 0)) |
73 | 70, 72 | bitrd 282 |
. . . . . 6
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → ((√‘𝐷) = -(√‘𝐷) ↔ 𝐷 = 0)) |
74 | 66, 69, 73 | 3bitrd 308 |
. . . . 5
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 / (2 · 𝐴)) + ((√‘𝐷) / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘𝐷) / (2 · 𝐴))) ↔ 𝐷 = 0)) |
75 | 62, 74 | bitrd 282 |
. . . 4
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)) ↔ 𝐷 = 0)) |
76 | 17, 43, 75 | 3bitrd 308 |
. . 3
⊢ ((𝜑 ∧ 0 ≤ 𝐷) → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0)) |
77 | 76 | expcom 417 |
. 2
⊢ (0 ≤
𝐷 → (𝜑 → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0))) |
78 | 1, 4, 6, 9, 14 | requad01 44746 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 0 ≤ 𝐷)) |
79 | 78 | notbid 321 |
. . . . . . 7
⊢ (𝜑 → (¬ ∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ ¬ 0 ≤ 𝐷)) |
80 | 79 | biimparc 483 |
. . . . . 6
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → ¬ ∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) |
81 | | reurex 3338 |
. . . . . 6
⊢
(∃!𝑥 ∈
ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → ∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) |
82 | 80, 81 | nsyl 142 |
. . . . 5
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → ¬ ∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) |
83 | 82 | pm2.21d 121 |
. . . 4
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 → 𝐷 = 0)) |
84 | | 0red 10836 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
85 | 26, 84 | ltnled 10979 |
. . . . . . 7
⊢ (𝜑 → (𝐷 < 0 ↔ ¬ 0 ≤ 𝐷)) |
86 | 85 | biimparc 483 |
. . . . . 6
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → 𝐷 < 0) |
87 | 86 | lt0ne0d 11397 |
. . . . 5
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → 𝐷 ≠ 0) |
88 | | eqneqall 2951 |
. . . . 5
⊢ (𝐷 = 0 → (𝐷 ≠ 0 → ∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0)) |
89 | 87, 88 | syl5com 31 |
. . . 4
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → (𝐷 = 0 → ∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0)) |
90 | 83, 89 | impbid 215 |
. . 3
⊢ ((¬ 0
≤ 𝐷 ∧ 𝜑) → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0)) |
91 | 90 | ex 416 |
. 2
⊢ (¬ 0
≤ 𝐷 → (𝜑 → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0))) |
92 | 77, 91 | pm2.61i 185 |
1
⊢ (𝜑 → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0)) |