Step | Hyp | Ref
| Expression |
1 | | requad2.a |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
2 | 1 | recnd 11242 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
3 | 2 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ ๐ด โ โ) |
4 | | requad2.z |
. . . . . 6
โข (๐ โ ๐ด โ 0) |
5 | 4 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ ๐ด โ 0) |
6 | | requad2.b |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
7 | 6 | recnd 11242 |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
8 | 7 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ ๐ต โ โ) |
9 | | requad2.c |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
10 | 9 | recnd 11242 |
. . . . . 6
โข (๐ โ ๐ถ โ โ) |
11 | 10 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ ๐ถ โ โ) |
12 | | recn 11200 |
. . . . . 6
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
13 | 12 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ ๐ฅ โ โ) |
14 | | requad2.d |
. . . . . 6
โข (๐ โ ๐ท = ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ)))) |
15 | 14 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ ๐ท = ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ)))) |
16 | 3, 5, 8, 11, 13, 15 | quad 26345 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ (((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0 โ (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โจ ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))))) |
17 | | eleq1 2822 |
. . . . . . . . . 10
โข (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ (๐ฅ โ โ โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ โ)) |
18 | 17 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) โ (๐ฅ โ โ โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ โ)) |
19 | | 2re 12286 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 2 โ
โ) |
21 | 20, 1 | remulcld 11244 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 ยท ๐ด) โ
โ) |
22 | 21 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ยฌ 0 โค ๐ท) โ (2 ยท ๐ด) โ
โ) |
23 | 7 | negcld 11558 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ -๐ต โ โ) |
24 | 6 | resqcld 14090 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ตโ2) โ โ) |
25 | | 4re 12296 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 4 โ
โ |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ 4 โ
โ) |
27 | 1, 9 | remulcld 11244 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ด ยท ๐ถ) โ โ) |
28 | 26, 27 | remulcld 11244 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (4 ยท (๐ด ยท ๐ถ)) โ โ) |
29 | 24, 28 | resubcld 11642 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ))) โ โ) |
30 | 14, 29 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ท โ โ) |
31 | 30 | recnd 11242 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ท โ โ) |
32 | 31 | sqrtcld 15384 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ๐ท) โ
โ) |
33 | 23, 32 | addcld 11233 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (-๐ต + (โโ๐ท)) โ โ) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ยฌ 0 โค ๐ท) โ (-๐ต + (โโ๐ท)) โ โ) |
35 | 6 | renegcld 11641 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ -๐ต โ โ) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ยฌ 0 โค ๐ท) โ -๐ต โ โ) |
37 | 32 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ยฌ 0 โค ๐ท) โ (โโ๐ท) โ
โ) |
38 | 31 | negnegd 11562 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ --๐ท = ๐ท) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ยฌ 0 โค ๐ท) โ --๐ท = ๐ท) |
40 | 39 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ยฌ 0 โค ๐ท) โ ๐ท = --๐ท) |
41 | 40 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ยฌ 0 โค ๐ท) โ (โโ๐ท) = (โโ--๐ท)) |
42 | 30 | renegcld 11641 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ -๐ท โ โ) |
43 | 42 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ยฌ 0 โค ๐ท) โ -๐ท โ โ) |
44 | | 0red 11217 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ 0 โ
โ) |
45 | 30, 44 | ltnled 11361 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (๐ท < 0 โ ยฌ 0 โค ๐ท)) |
46 | | ltle 11302 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ท โ โ โง 0 โ
โ) โ (๐ท < 0
โ ๐ท โค
0)) |
47 | 30, 44, 46 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (๐ท < 0 โ ๐ท โค 0)) |
48 | 45, 47 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (ยฌ 0 โค ๐ท โ ๐ท โค 0)) |
49 | 48 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ยฌ 0 โค ๐ท) โ ๐ท โค 0) |
50 | 30 | le0neg1d 11785 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐ท โค 0 โ 0 โค -๐ท)) |
51 | 50 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ยฌ 0 โค ๐ท) โ (๐ท โค 0 โ 0 โค -๐ท)) |
52 | 49, 51 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ยฌ 0 โค ๐ท) โ 0 โค -๐ท) |
53 | 43, 52 | sqrtnegd 15368 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ยฌ 0 โค ๐ท) โ (โโ--๐ท) = (i ยท
(โโ-๐ท))) |
54 | 41, 53 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ยฌ 0 โค ๐ท) โ (โโ๐ท) = (i ยท
(โโ-๐ท))) |
55 | | ax-icn 11169 |
. . . . . . . . . . . . . . . . . . . . . 22
โข i โ
โ |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ยฌ 0 โค ๐ท) โ i โ
โ) |
57 | 31 | negcld 11558 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ -๐ท โ โ) |
58 | 57 | sqrtcld 15384 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โโ-๐ท) โ
โ) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ยฌ 0 โค ๐ท) โ (โโ-๐ท) โ
โ) |
60 | 56, 59 | mulcomd 11235 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ยฌ 0 โค ๐ท) โ (i ยท
(โโ-๐ท)) =
((โโ-๐ท)
ยท i)) |
61 | 43, 52 | resqrtcld 15364 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ยฌ 0 โค ๐ท) โ (โโ-๐ท) โ
โ) |
62 | | inelr 12202 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ยฌ i
โ โ |
63 | | eldif 3959 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (i โ
(โ โ โ) โ (i โ โ โง ยฌ i โ
โ)) |
64 | 55, 62, 63 | mpbir2an 710 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข i โ
(โ โ โ) |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ยฌ 0 โค ๐ท) โ i โ (โ
โ โ)) |
66 | 30 | lt0neg1d 11783 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ (๐ท < 0 โ 0 < -๐ท)) |
67 | | ltne 11311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((0
โ โ โง 0 < -๐ท) โ -๐ท โ 0) |
68 | 44, 67 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โง 0 < -๐ท) โ -๐ท โ 0) |
69 | 42 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โง 0 < -๐ท) โ -๐ท โ โ) |
70 | | ltle 11302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข ((0
โ โ โง -๐ท
โ โ) โ (0 < -๐ท โ 0 โค -๐ท)) |
71 | 44, 42, 70 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ โ (0 < -๐ท โ 0 โค -๐ท)) |
72 | 71 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ โง 0 < -๐ท) โ 0 โค -๐ท) |
73 | | sqrt00 15210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((-๐ท โ โ โง 0 โค
-๐ท) โ
((โโ-๐ท) = 0
โ -๐ท =
0)) |
74 | 69, 72, 73 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ โง 0 < -๐ท) โ ((โโ-๐ท) = 0 โ -๐ท = 0)) |
75 | 74 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โง 0 < -๐ท) โ (-๐ท = 0 โ (โโ-๐ท) = 0)) |
76 | 75 | necon3bid 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โง 0 < -๐ท) โ (-๐ท โ 0 โ (โโ-๐ท) โ 0)) |
77 | 68, 76 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โง 0 < -๐ท) โ (โโ-๐ท) โ 0) |
78 | 77 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ (0 < -๐ท โ (โโ-๐ท) โ 0)) |
79 | 66, 78 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ (๐ท < 0 โ (โโ-๐ท) โ 0)) |
80 | 45, 79 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (ยฌ 0 โค ๐ท โ (โโ-๐ท) โ 0)) |
81 | 80 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ยฌ 0 โค ๐ท) โ (โโ-๐ท) โ 0) |
82 | 61, 65, 81 | recnmulnred 46013 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ยฌ 0 โค ๐ท) โ ((โโ-๐ท) ยท i) โ
โ) |
83 | | df-nel 3048 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((โโ-๐ท)
ยท i) โ โ โ ยฌ ((โโ-๐ท) ยท i) โ
โ) |
84 | 82, 83 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ยฌ 0 โค ๐ท) โ ยฌ
((โโ-๐ท)
ยท i) โ โ) |
85 | 60, 84 | eqneltrd 2854 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ยฌ 0 โค ๐ท) โ ยฌ (i ยท
(โโ-๐ท)) โ
โ) |
86 | 54, 85 | eqneltrd 2854 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ยฌ 0 โค ๐ท) โ ยฌ
(โโ๐ท) โ
โ) |
87 | 37, 86 | eldifd 3960 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ยฌ 0 โค ๐ท) โ (โโ๐ท) โ (โ โ
โ)) |
88 | 36, 87 | readdcnnred 46011 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ยฌ 0 โค ๐ท) โ (-๐ต + (โโ๐ท)) โ โ) |
89 | | df-nel 3048 |
. . . . . . . . . . . . . . . 16
โข ((-๐ต + (โโ๐ท)) โ โ โ ยฌ
(-๐ต + (โโ๐ท)) โ
โ) |
90 | 88, 89 | sylib 217 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ยฌ 0 โค ๐ท) โ ยฌ (-๐ต + (โโ๐ท)) โ
โ) |
91 | 34, 90 | eldifd 3960 |
. . . . . . . . . . . . . 14
โข ((๐ โง ยฌ 0 โค ๐ท) โ (-๐ต + (โโ๐ท)) โ (โ โ
โ)) |
92 | | 2cnd 12290 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 2 โ
โ) |
93 | | 2ne0 12316 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
0 |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 2 โ 0) |
95 | 92, 2, 94, 4 | mulne0d 11866 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 ยท ๐ด) โ 0) |
96 | 95 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ยฌ 0 โค ๐ท) โ (2 ยท ๐ด) โ 0) |
97 | 22, 91, 96 | cndivrenred 46014 |
. . . . . . . . . . . . 13
โข ((๐ โง ยฌ 0 โค ๐ท) โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ โ) |
98 | | df-nel 3048 |
. . . . . . . . . . . . 13
โข (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ โ โ ยฌ
((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ
โ) |
99 | 97, 98 | sylib 217 |
. . . . . . . . . . . 12
โข ((๐ โง ยฌ 0 โค ๐ท) โ ยฌ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ
โ) |
100 | 99 | ex 414 |
. . . . . . . . . . 11
โข (๐ โ (ยฌ 0 โค ๐ท โ ยฌ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ
โ)) |
101 | 100 | con4d 115 |
. . . . . . . . . 10
โข (๐ โ (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ โ โ 0 โค ๐ท)) |
102 | 101 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) โ (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ โ โ 0 โค ๐ท)) |
103 | 18, 102 | sylbid 239 |
. . . . . . . 8
โข ((๐ โง ๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) โ (๐ฅ โ โ โ 0 โค ๐ท)) |
104 | 103 | ex 414 |
. . . . . . 7
โข (๐ โ (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ (๐ฅ โ โ โ 0 โค ๐ท))) |
105 | | eleq1 2822 |
. . . . . . . . . 10
โข (๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ (๐ฅ โ โ โ ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ โ)) |
106 | 105 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))) โ (๐ฅ โ โ โ ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ โ)) |
107 | 23, 32 | subcld 11571 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (-๐ต โ (โโ๐ท)) โ โ) |
108 | 107 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ยฌ 0 โค ๐ท) โ (-๐ต โ (โโ๐ท)) โ โ) |
109 | 36, 87 | resubcnnred 46012 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ยฌ 0 โค ๐ท) โ (-๐ต โ (โโ๐ท)) โ โ) |
110 | | df-nel 3048 |
. . . . . . . . . . . . . . . 16
โข ((-๐ต โ (โโ๐ท)) โ โ โ ยฌ
(-๐ต โ
(โโ๐ท)) โ
โ) |
111 | 109, 110 | sylib 217 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ยฌ 0 โค ๐ท) โ ยฌ (-๐ต โ (โโ๐ท)) โ
โ) |
112 | 108, 111 | eldifd 3960 |
. . . . . . . . . . . . . 14
โข ((๐ โง ยฌ 0 โค ๐ท) โ (-๐ต โ (โโ๐ท)) โ (โ โ
โ)) |
113 | 22, 112, 96 | cndivrenred 46014 |
. . . . . . . . . . . . 13
โข ((๐ โง ยฌ 0 โค ๐ท) โ ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ โ) |
114 | | df-nel 3048 |
. . . . . . . . . . . . 13
โข (((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ โ โ ยฌ
((-๐ต โ
(โโ๐ท)) / (2
ยท ๐ด)) โ
โ) |
115 | 113, 114 | sylib 217 |
. . . . . . . . . . . 12
โข ((๐ โง ยฌ 0 โค ๐ท) โ ยฌ ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ
โ) |
116 | 115 | ex 414 |
. . . . . . . . . . 11
โข (๐ โ (ยฌ 0 โค ๐ท โ ยฌ ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ
โ)) |
117 | 116 | con4d 115 |
. . . . . . . . . 10
โข (๐ โ (((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ โ โ 0 โค ๐ท)) |
118 | 117 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))) โ (((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ โ โ 0 โค ๐ท)) |
119 | 106, 118 | sylbid 239 |
. . . . . . . 8
โข ((๐ โง ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))) โ (๐ฅ โ โ โ 0 โค ๐ท)) |
120 | 119 | ex 414 |
. . . . . . 7
โข (๐ โ (๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)) โ (๐ฅ โ โ โ 0 โค ๐ท))) |
121 | 104, 120 | jaod 858 |
. . . . . 6
โข (๐ โ ((๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โจ ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))) โ (๐ฅ โ โ โ 0 โค ๐ท))) |
122 | 121 | com23 86 |
. . . . 5
โข (๐ โ (๐ฅ โ โ โ ((๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โจ ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))) โ 0 โค ๐ท))) |
123 | 122 | imp 408 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ ((๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โจ ๐ฅ = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))) โ 0 โค ๐ท)) |
124 | 16, 123 | sylbid 239 |
. . 3
โข ((๐ โง ๐ฅ โ โ) โ (((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0 โ 0 โค ๐ท)) |
125 | 124 | rexlimdva 3156 |
. 2
โข (๐ โ (โ๐ฅ โ โ ((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0 โ 0 โค ๐ท)) |
126 | 35 | adantr 482 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ -๐ต โ โ) |
127 | 30 | adantr 482 |
. . . . . . 7
โข ((๐ โง 0 โค ๐ท) โ ๐ท โ โ) |
128 | | simpr 486 |
. . . . . . 7
โข ((๐ โง 0 โค ๐ท) โ 0 โค ๐ท) |
129 | 127, 128 | resqrtcld 15364 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ (โโ๐ท) โ โ) |
130 | 126, 129 | readdcld 11243 |
. . . . 5
โข ((๐ โง 0 โค ๐ท) โ (-๐ต + (โโ๐ท)) โ โ) |
131 | 19 | a1i 11 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ 2 โ โ) |
132 | 1 | adantr 482 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ ๐ด โ โ) |
133 | 131, 132 | remulcld 11244 |
. . . . 5
โข ((๐ โง 0 โค ๐ท) โ (2 ยท ๐ด) โ โ) |
134 | 95 | adantr 482 |
. . . . 5
โข ((๐ โง 0 โค ๐ท) โ (2 ยท ๐ด) โ 0) |
135 | 130, 133,
134 | redivcld 12042 |
. . . 4
โข ((๐ โง 0 โค ๐ท) โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ โ) |
136 | | oveq1 7416 |
. . . . . . . 8
โข (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ (๐ฅโ2) = (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))โ2)) |
137 | 136 | oveq2d 7425 |
. . . . . . 7
โข (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ (๐ด ยท (๐ฅโ2)) = (๐ด ยท (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))โ2))) |
138 | | oveq2 7417 |
. . . . . . . 8
โข (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ (๐ต ยท ๐ฅ) = (๐ต ยท ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)))) |
139 | 138 | oveq1d 7424 |
. . . . . . 7
โข (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ ((๐ต ยท ๐ฅ) + ๐ถ) = ((๐ต ยท ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) + ๐ถ)) |
140 | 137, 139 | oveq12d 7427 |
. . . . . 6
โข (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ ((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = ((๐ด ยท (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))โ2)) + ((๐ต ยท ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) + ๐ถ))) |
141 | 140 | eqeq1d 2735 |
. . . . 5
โข (๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ (((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0 โ ((๐ด ยท (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))โ2)) + ((๐ต ยท ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) + ๐ถ)) = 0)) |
142 | 141 | adantl 483 |
. . . 4
โข (((๐ โง 0 โค ๐ท) โง ๐ฅ = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) โ (((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0 โ ((๐ด ยท (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))โ2)) + ((๐ต ยท ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) + ๐ถ)) = 0)) |
143 | | eqidd 2734 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) |
144 | 143 | orcd 872 |
. . . . 5
โข ((๐ โง 0 โค ๐ท) โ (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โจ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด)))) |
145 | 2 | adantr 482 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ ๐ด โ โ) |
146 | 4 | adantr 482 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ ๐ด โ 0) |
147 | 7 | adantr 482 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ ๐ต โ โ) |
148 | 10 | adantr 482 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ ๐ถ โ โ) |
149 | 92, 2 | mulcld 11234 |
. . . . . . . 8
โข (๐ โ (2 ยท ๐ด) โ
โ) |
150 | 33, 149, 95 | divcld 11990 |
. . . . . . 7
โข (๐ โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ โ) |
151 | 150 | adantr 482 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โ โ) |
152 | 14 | adantr 482 |
. . . . . 6
โข ((๐ โง 0 โค ๐ท) โ ๐ท = ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ)))) |
153 | 145, 146,
147, 148, 151, 152 | quad 26345 |
. . . . 5
โข ((๐ โง 0 โค ๐ท) โ (((๐ด ยท (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))โ2)) + ((๐ต ยท ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) + ๐ถ)) = 0 โ (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) โจ ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด)) = ((-๐ต โ (โโ๐ท)) / (2 ยท ๐ด))))) |
154 | 144, 153 | mpbird 257 |
. . . 4
โข ((๐ โง 0 โค ๐ท) โ ((๐ด ยท (((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))โ2)) + ((๐ต ยท ((-๐ต + (โโ๐ท)) / (2 ยท ๐ด))) + ๐ถ)) = 0) |
155 | 135, 142,
154 | rspcedvd 3615 |
. . 3
โข ((๐ โง 0 โค ๐ท) โ โ๐ฅ โ โ ((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0) |
156 | 155 | ex 414 |
. 2
โข (๐ โ (0 โค ๐ท โ โ๐ฅ โ โ ((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0)) |
157 | 125, 156 | impbid 211 |
1
โข (๐ โ (โ๐ฅ โ โ ((๐ด ยท (๐ฅโ2)) + ((๐ต ยท ๐ฅ) + ๐ถ)) = 0 โ 0 โค ๐ท)) |