Step |
Hyp |
Ref |
Expression |
1 |
|
itscnhlc0yqe.q |
โข ๐ = ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) |
2 |
|
itsclc0yqsol.d |
โข ๐ท = ( ( ( ๐
โ 2 ) ยท ๐ ) โ ( ๐ถ โ 2 ) ) |
3 |
1 2
|
itschlc0xyqsol1 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) = ( ๐
โ 2 ) โง ( ( ๐ด ยท ๐ ) + ( ๐ต ยท ๐ ) ) = ๐ถ ) โ ( ๐ = ( ๐ถ / ๐ต ) โง ( ๐ = - ( ( โ โ ๐ท ) / ๐ต ) โจ ๐ = ( ( โ โ ๐ท ) / ๐ต ) ) ) ) ) |
4 |
|
orcom |
โข ( ( ๐ = - ( ( โ โ ๐ท ) / ๐ต ) โจ ๐ = ( ( โ โ ๐ท ) / ๐ต ) ) โ ( ๐ = ( ( โ โ ๐ท ) / ๐ต ) โจ ๐ = - ( ( โ โ ๐ท ) / ๐ต ) ) ) |
5 |
|
oveq1 |
โข ( ๐ด = 0 โ ( ๐ด ยท ๐ถ ) = ( 0 ยท ๐ถ ) ) |
6 |
5
|
ad2antrl |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โ ( ๐ด ยท ๐ถ ) = ( 0 ยท ๐ถ ) ) |
7 |
6
|
adantr |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ๐ด ยท ๐ถ ) = ( 0 ยท ๐ถ ) ) |
8 |
|
simpll3 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ๐ถ โ โ ) |
9 |
8
|
recnd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ๐ถ โ โ ) |
10 |
9
|
mul02d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( 0 ยท ๐ถ ) = 0 ) |
11 |
7 10
|
eqtrd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ๐ด ยท ๐ถ ) = 0 ) |
12 |
11
|
oveq1d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) = ( 0 + ( ๐ต ยท ( โ โ ๐ท ) ) ) ) |
13 |
|
simpll2 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ๐ต โ โ ) |
14 |
13
|
recnd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ๐ต โ โ ) |
15 |
|
rpre |
โข ( ๐
โ โ+ โ ๐
โ โ ) |
16 |
15
|
adantr |
โข ( ( ๐
โ โ+ โง 0 โค ๐ท ) โ ๐
โ โ ) |
17 |
16
|
recnd |
โข ( ( ๐
โ โ+ โง 0 โค ๐ท ) โ ๐
โ โ ) |
18 |
17
|
adantl |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ๐
โ โ ) |
19 |
18
|
sqcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ๐
โ 2 ) โ โ ) |
20 |
1
|
resum2sqcl |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ๐ โ โ ) |
21 |
20
|
recnd |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ๐ โ โ ) |
22 |
21
|
3adant3 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ๐ โ โ ) |
23 |
22
|
adantr |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โ ๐ โ โ ) |
24 |
23
|
adantr |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ๐ โ โ ) |
25 |
19 24
|
mulcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐
โ 2 ) ยท ๐ ) โ โ ) |
26 |
9
|
sqcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ๐ถ โ 2 ) โ โ ) |
27 |
25 26
|
subcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ( ๐
โ 2 ) ยท ๐ ) โ ( ๐ถ โ 2 ) ) โ โ ) |
28 |
2 27
|
eqeltrid |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ๐ท โ โ ) |
29 |
28
|
sqrtcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( โ โ ๐ท ) โ โ ) |
30 |
14 29
|
mulcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ๐ต ยท ( โ โ ๐ท ) ) โ โ ) |
31 |
30
|
addlidd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( 0 + ( ๐ต ยท ( โ โ ๐ท ) ) ) = ( ๐ต ยท ( โ โ ๐ท ) ) ) |
32 |
12 31
|
eqtrd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) = ( ๐ต ยท ( โ โ ๐ท ) ) ) |
33 |
32
|
oveq1d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( ๐ต ยท ( โ โ ๐ท ) ) / ๐ ) ) |
34 |
|
sq0i |
โข ( ๐ด = 0 โ ( ๐ด โ 2 ) = 0 ) |
35 |
34
|
ad2antrl |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โ ( ๐ด โ 2 ) = 0 ) |
36 |
35
|
oveq1d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โ ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) = ( 0 + ( ๐ต โ 2 ) ) ) |
37 |
|
simp2 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ๐ต โ โ ) |
38 |
37
|
recnd |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ๐ต โ โ ) |
39 |
38
|
sqcld |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ๐ต โ 2 ) โ โ ) |
40 |
39
|
addlidd |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( 0 + ( ๐ต โ 2 ) ) = ( ๐ต โ 2 ) ) |
41 |
38
|
sqvald |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ๐ต โ 2 ) = ( ๐ต ยท ๐ต ) ) |
42 |
40 41
|
eqtrd |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( 0 + ( ๐ต โ 2 ) ) = ( ๐ต ยท ๐ต ) ) |
43 |
42
|
adantr |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โ ( 0 + ( ๐ต โ 2 ) ) = ( ๐ต ยท ๐ต ) ) |
44 |
36 43
|
eqtrd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โ ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) = ( ๐ต ยท ๐ต ) ) |
45 |
1 44
|
eqtrid |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โ ๐ = ( ๐ต ยท ๐ต ) ) |
46 |
45
|
adantr |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ๐ = ( ๐ต ยท ๐ต ) ) |
47 |
46
|
oveq2d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ต ยท ( โ โ ๐ท ) ) / ๐ ) = ( ( ๐ต ยท ( โ โ ๐ท ) ) / ( ๐ต ยท ๐ต ) ) ) |
48 |
|
simplrr |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ๐ต โ 0 ) |
49 |
29 14 14 48 48
|
divcan5d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ต ยท ( โ โ ๐ท ) ) / ( ๐ต ยท ๐ต ) ) = ( ( โ โ ๐ท ) / ๐ต ) ) |
50 |
47 49
|
eqtrd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ต ยท ( โ โ ๐ท ) ) / ๐ ) = ( ( โ โ ๐ท ) / ๐ต ) ) |
51 |
33 50
|
eqtrd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( โ โ ๐ท ) / ๐ต ) ) |
52 |
51
|
3adant3 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( โ โ ๐ท ) / ๐ต ) ) |
53 |
52
|
adantr |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( โ โ ๐ท ) / ๐ต ) ) |
54 |
53
|
eqcomd |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ( โ โ ๐ท ) / ๐ต ) = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) |
55 |
54
|
eqeq2d |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ๐ = ( ( โ โ ๐ท ) / ๐ต ) โ ๐ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
56 |
55
|
biimpd |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ๐ = ( ( โ โ ๐ท ) / ๐ต ) โ ๐ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
57 |
|
oveq1 |
โข ( ๐ด = 0 โ ( ๐ด ยท ( โ โ ๐ท ) ) = ( 0 ยท ( โ โ ๐ท ) ) ) |
58 |
57
|
ad2antrl |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โ ( ๐ด ยท ( โ โ ๐ท ) ) = ( 0 ยท ( โ โ ๐ท ) ) ) |
59 |
58
|
adantr |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ๐ด ยท ( โ โ ๐ท ) ) = ( 0 ยท ( โ โ ๐ท ) ) ) |
60 |
29
|
mul02d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( 0 ยท ( โ โ ๐ท ) ) = 0 ) |
61 |
59 60
|
eqtrd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ๐ด ยท ( โ โ ๐ท ) ) = 0 ) |
62 |
61
|
oveq2d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) โ 0 ) ) |
63 |
14 9
|
mulcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ๐ต ยท ๐ถ ) โ โ ) |
64 |
63
|
subid1d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ต ยท ๐ถ ) โ 0 ) = ( ๐ต ยท ๐ถ ) ) |
65 |
62 64
|
eqtrd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ๐ต ยท ๐ถ ) ) |
66 |
65 46
|
oveq12d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( ๐ต ยท ๐ถ ) / ( ๐ต ยท ๐ต ) ) ) |
67 |
66
|
3adant3 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( ๐ต ยท ๐ถ ) / ( ๐ต ยท ๐ต ) ) ) |
68 |
9
|
3adant3 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ถ โ โ ) |
69 |
14
|
3adant3 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ต โ โ ) |
70 |
|
simp1rr |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ต โ 0 ) |
71 |
68 69 69 70 70
|
divcan5d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ๐ต ยท ๐ถ ) / ( ๐ต ยท ๐ต ) ) = ( ๐ถ / ๐ต ) ) |
72 |
67 71
|
eqtr2d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ๐ถ / ๐ต ) = ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) |
73 |
72
|
eqeq2d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ๐ = ( ๐ถ / ๐ต ) โ ๐ = ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
74 |
73
|
biimpa |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ๐ = ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) |
75 |
56 74
|
jctird |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ๐ = ( ( โ โ ๐ท ) / ๐ต ) โ ( ๐ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โง ๐ = ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) ) |
76 |
14 29
|
mulneg2d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ๐ต ยท - ( โ โ ๐ท ) ) = - ( ๐ต ยท ( โ โ ๐ท ) ) ) |
77 |
76
|
eqcomd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ - ( ๐ต ยท ( โ โ ๐ท ) ) = ( ๐ต ยท - ( โ โ ๐ท ) ) ) |
78 |
77 46
|
oveq12d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( - ( ๐ต ยท ( โ โ ๐ท ) ) / ๐ ) = ( ( ๐ต ยท - ( โ โ ๐ท ) ) / ( ๐ต ยท ๐ต ) ) ) |
79 |
29
|
negcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ - ( โ โ ๐ท ) โ โ ) |
80 |
79 14 14 48 48
|
divcan5d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ต ยท - ( โ โ ๐ท ) ) / ( ๐ต ยท ๐ต ) ) = ( - ( โ โ ๐ท ) / ๐ต ) ) |
81 |
78 80
|
eqtrd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( - ( ๐ต ยท ( โ โ ๐ท ) ) / ๐ ) = ( - ( โ โ ๐ท ) / ๐ต ) ) |
82 |
11
|
oveq1d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) = ( 0 โ ( ๐ต ยท ( โ โ ๐ท ) ) ) ) |
83 |
|
df-neg |
โข - ( ๐ต ยท ( โ โ ๐ท ) ) = ( 0 โ ( ๐ต ยท ( โ โ ๐ท ) ) ) |
84 |
82 83
|
eqtr4di |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) = - ( ๐ต ยท ( โ โ ๐ท ) ) ) |
85 |
84
|
oveq1d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( - ( ๐ต ยท ( โ โ ๐ท ) ) / ๐ ) ) |
86 |
29 14 48
|
divnegd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ - ( ( โ โ ๐ท ) / ๐ต ) = ( - ( โ โ ๐ท ) / ๐ต ) ) |
87 |
81 85 86
|
3eqtr4d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = - ( ( โ โ ๐ท ) / ๐ต ) ) |
88 |
87
|
3adant3 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = - ( ( โ โ ๐ท ) / ๐ต ) ) |
89 |
88
|
adantr |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = - ( ( โ โ ๐ท ) / ๐ต ) ) |
90 |
89
|
eqcomd |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ - ( ( โ โ ๐ท ) / ๐ต ) = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) |
91 |
90
|
eqeq2d |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ๐ = - ( ( โ โ ๐ท ) / ๐ต ) โ ๐ = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
92 |
91
|
biimpd |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ๐ = - ( ( โ โ ๐ท ) / ๐ต ) โ ๐ = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
93 |
58
|
3ad2ant1 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ๐ด ยท ( โ โ ๐ท ) ) = ( 0 ยท ( โ โ ๐ท ) ) ) |
94 |
17
|
3ad2ant2 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐
โ โ ) |
95 |
94
|
sqcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ๐
โ 2 ) โ โ ) |
96 |
23
|
3ad2ant1 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ โ โ ) |
97 |
95 96
|
mulcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ๐
โ 2 ) ยท ๐ ) โ โ ) |
98 |
|
simp1l3 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ถ โ โ ) |
99 |
98
|
recnd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ถ โ โ ) |
100 |
99
|
sqcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ๐ถ โ 2 ) โ โ ) |
101 |
97 100
|
subcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ( ๐
โ 2 ) ยท ๐ ) โ ( ๐ถ โ 2 ) ) โ โ ) |
102 |
2 101
|
eqeltrid |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ท โ โ ) |
103 |
102
|
sqrtcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( โ โ ๐ท ) โ โ ) |
104 |
103
|
mul02d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( 0 ยท ( โ โ ๐ท ) ) = 0 ) |
105 |
93 104
|
eqtrd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ๐ด ยท ( โ โ ๐ท ) ) = 0 ) |
106 |
105
|
oveq2d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + 0 ) ) |
107 |
|
simp1l2 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ต โ โ ) |
108 |
107
|
recnd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ต โ โ ) |
109 |
108 99
|
mulcld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ๐ต ยท ๐ถ ) โ โ ) |
110 |
109
|
addridd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ๐ต ยท ๐ถ ) + 0 ) = ( ๐ต ยท ๐ถ ) ) |
111 |
106 110
|
eqtrd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ๐ต ยท ๐ถ ) ) |
112 |
45
|
3ad2ant1 |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ = ( ๐ต ยท ๐ต ) ) |
113 |
111 112
|
oveq12d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( ๐ต ยท ๐ถ ) / ( ๐ต ยท ๐ต ) ) ) |
114 |
99 108 108 70 70
|
divcan5d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ๐ต ยท ๐ถ ) / ( ๐ต ยท ๐ต ) ) = ( ๐ถ / ๐ต ) ) |
115 |
113 114
|
eqtr2d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ๐ถ / ๐ต ) = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) |
116 |
115
|
eqeq2d |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ๐ = ( ๐ถ / ๐ต ) โ ๐ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
117 |
116
|
biimpa |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ๐ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) |
118 |
92 117
|
jctird |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ๐ = - ( ( โ โ ๐ท ) / ๐ต ) โ ( ๐ = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โง ๐ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) ) |
119 |
75 118
|
orim12d |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ( ๐ = ( ( โ โ ๐ท ) / ๐ต ) โจ ๐ = - ( ( โ โ ๐ท ) / ๐ต ) ) โ ( ( ๐ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โง ๐ = ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) โจ ( ๐ = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โง ๐ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) ) ) |
120 |
4 119
|
biimtrid |
โข ( ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ๐ = ( ๐ถ / ๐ต ) ) โ ( ( ๐ = - ( ( โ โ ๐ท ) / ๐ต ) โจ ๐ = ( ( โ โ ๐ท ) / ๐ต ) ) โ ( ( ๐ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โง ๐ = ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) โจ ( ๐ = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โง ๐ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) ) ) |
121 |
120
|
expimpd |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ๐ = ( ๐ถ / ๐ต ) โง ( ๐ = - ( ( โ โ ๐ท ) / ๐ต ) โจ ๐ = ( ( โ โ ๐ท ) / ๐ต ) ) ) โ ( ( ๐ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โง ๐ = ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) โจ ( ๐ = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โง ๐ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) ) ) |
122 |
3 121
|
syld |
โข ( ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ด = 0 โง ๐ต โ 0 ) ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ( ( ๐ โ 2 ) + ( ๐ โ 2 ) ) = ( ๐
โ 2 ) โง ( ( ๐ด ยท ๐ ) + ( ๐ต ยท ๐ ) ) = ๐ถ ) โ ( ( ๐ = ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โง ๐ = ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) โจ ( ๐ = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โง ๐ = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) ) ) |