Step |
Hyp |
Ref |
Expression |
1 |
|
inlinecirc02p.i |
โข ๐ผ = { 1 , 2 } |
2 |
|
inlinecirc02p.e |
โข ๐ธ = ( โ^ โ ๐ผ ) |
3 |
|
inlinecirc02p.p |
โข ๐ = ( โ โm ๐ผ ) |
4 |
|
inlinecirc02p.s |
โข ๐ = ( Sphere โ ๐ธ ) |
5 |
|
inlinecirc02p.0 |
โข 0 = ( ๐ผ ร { 0 } ) |
6 |
|
inlinecirc02p.l |
โข ๐ฟ = ( LineM โ ๐ธ ) |
7 |
|
inlinecirc02plem.q |
โข ๐ = ( ( ๐ด โ 2 ) + ( ๐ต โ 2 ) ) |
8 |
|
inlinecirc02plem.d |
โข ๐ท = ( ( ( ๐
โ 2 ) ยท ๐ ) โ ( ๐ถ โ 2 ) ) |
9 |
|
inlinecirc02plem.a |
โข ๐ด = ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) |
10 |
|
inlinecirc02plem.b |
โข ๐ต = ( ( ๐ โ 1 ) โ ( ๐ โ 1 ) ) |
11 |
|
inlinecirc02plem.c |
โข ๐ถ = ( ( ( ๐ โ 2 ) ยท ( ๐ โ 1 ) ) โ ( ( ๐ โ 1 ) ยท ( ๐ โ 2 ) ) ) |
12 |
|
simprr |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ 0 < ๐ท ) |
13 |
12
|
gt0ne0d |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ท โ 0 ) |
14 |
1 3
|
rrx2pyel |
โข ( ๐ โ ๐ โ ( ๐ โ 2 ) โ โ ) |
15 |
14
|
adantr |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ โ 2 ) โ โ ) |
16 |
1 3
|
rrx2pyel |
โข ( ๐ โ ๐ โ ( ๐ โ 2 ) โ โ ) |
17 |
16
|
adantl |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ โ 2 ) โ โ ) |
18 |
15 17
|
resubcld |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ๐ โ 2 ) โ ( ๐ โ 2 ) ) โ โ ) |
19 |
9 18
|
eqeltrid |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ด โ โ ) |
20 |
19
|
3adant3 |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ด โ โ ) |
21 |
20
|
adantr |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ด โ โ ) |
22 |
1 3
|
rrx2pxel |
โข ( ๐ โ ๐ โ ( ๐ โ 1 ) โ โ ) |
23 |
22
|
adantl |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ โ 1 ) โ โ ) |
24 |
1 3
|
rrx2pxel |
โข ( ๐ โ ๐ โ ( ๐ โ 1 ) โ โ ) |
25 |
24
|
adantr |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ โ 1 ) โ โ ) |
26 |
23 25
|
resubcld |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ๐ โ 1 ) โ ( ๐ โ 1 ) ) โ โ ) |
27 |
10 26
|
eqeltrid |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ต โ โ ) |
28 |
27
|
3adant3 |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ต โ โ ) |
29 |
28
|
adantr |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ต โ โ ) |
30 |
15 23
|
remulcld |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ๐ โ 2 ) ยท ( ๐ โ 1 ) ) โ โ ) |
31 |
25 17
|
remulcld |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ๐ โ 1 ) ยท ( ๐ โ 2 ) ) โ โ ) |
32 |
30 31
|
resubcld |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ( ๐ โ 2 ) ยท ( ๐ โ 1 ) ) โ ( ( ๐ โ 1 ) ยท ( ๐ โ 2 ) ) ) โ โ ) |
33 |
11 32
|
eqeltrid |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ถ โ โ ) |
34 |
33
|
3adant3 |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ถ โ โ ) |
35 |
34
|
adantr |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ถ โ โ ) |
36 |
19 27 33
|
3jca |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) ) |
37 |
36
|
3adant3 |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) ) |
38 |
|
rpre |
โข ( ๐
โ โ+ โ ๐
โ โ ) |
39 |
38
|
adantr |
โข ( ( ๐
โ โ+ โง 0 < ๐ท ) โ ๐
โ โ ) |
40 |
7 8
|
itsclc0lem3 |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ๐
โ โ ) โ ๐ท โ โ ) |
41 |
37 39 40
|
syl2an |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ท โ โ ) |
42 |
41 12
|
elrpd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ท โ โ+ ) |
43 |
42
|
rprege0d |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ๐ท โ โ โง 0 โค ๐ท ) ) |
44 |
7
|
resum2sqcl |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ๐ โ โ ) |
45 |
19 27 44
|
syl2anc |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ โ โ ) |
46 |
45
|
3adant3 |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ โ โ ) |
47 |
1 3 10 9
|
rrx2pnedifcoorneorr |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ต โ 0 โจ ๐ด โ 0 ) ) |
48 |
47
|
orcomd |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ด โ 0 โจ ๐ต โ 0 ) ) |
49 |
7
|
resum2sqorgt0 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ด โ 0 โจ ๐ต โ 0 ) ) โ 0 < ๐ ) |
50 |
20 28 48 49
|
syl3anc |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ 0 < ๐ ) |
51 |
50
|
gt0ne0d |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ๐ โ 0 ) |
52 |
46 51
|
jca |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ โ โ โง ๐ โ 0 ) ) |
53 |
52
|
adantr |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ๐ โ โ โง ๐ โ 0 ) ) |
54 |
|
itsclc0lem1 |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ท โ โ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) |
55 |
21 29 35 43 53 54
|
syl311anc |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) |
56 |
|
itsclc0lem2 |
โข ( ( ( ๐ต โ โ โง ๐ด โ โ โง ๐ถ โ โ ) โง ( ๐ท โ โ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) |
57 |
29 21 35 43 53 56
|
syl311anc |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) |
58 |
55 57
|
jca |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ โง ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) ) |
59 |
58
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ โง ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) ) |
60 |
1 3
|
prelrrx2 |
โข ( ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ โง ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ ) |
61 |
59 60
|
syl |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ ) |
62 |
|
itsclc0lem2 |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โง ( ๐ท โ โ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) |
63 |
21 29 35 43 53 62
|
syl311anc |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) |
64 |
|
itsclc0lem1 |
โข ( ( ( ๐ต โ โ โง ๐ด โ โ โง ๐ถ โ โ ) โง ( ๐ท โ โ โง 0 โค ๐ท ) โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) |
65 |
29 21 35 43 53 64
|
syl311anc |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) |
66 |
63 65
|
jca |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ โง ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) ) |
67 |
66
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ โง ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) ) |
68 |
1 3
|
prelrrx2 |
โข ( ( ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ โง ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ โ ) โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ ) |
69 |
67 68
|
syl |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ ) |
70 |
|
simpl |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) ) |
71 |
|
simprl |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐
โ โ+ ) |
72 |
|
0red |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ 0 โ โ ) |
73 |
72 41 12
|
ltled |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ 0 โค ๐ท ) |
74 |
70 71 73
|
jca32 |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) ) |
75 |
74
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) ) |
76 |
1 2 3 4 5 7 8 6 9 10 11
|
itsclinecirc0in |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 โค ๐ท ) ) โ ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } } ) |
77 |
75 76
|
syl |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } } ) |
78 |
|
opex |
โข โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V |
79 |
|
opex |
โข โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V |
80 |
|
opex |
โข โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V |
81 |
|
opex |
โข โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V |
82 |
80 81
|
pm3.2i |
โข ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V ) |
83 |
48
|
adantr |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ๐ด โ 0 โจ ๐ต โ 0 ) ) |
84 |
83
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ๐ด โ 0 โจ ๐ต โ 0 ) ) |
85 |
|
orcom |
โข ( ( ๐ด โ 0 โจ ๐ต โ 0 ) โ ( ๐ต โ 0 โจ ๐ด โ 0 ) ) |
86 |
21
|
recnd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ด โ โ ) |
87 |
86
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ๐ด โ โ ) |
88 |
35
|
recnd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ถ โ โ ) |
89 |
88
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ๐ถ โ โ ) |
90 |
87 89
|
mulcld |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ๐ด ยท ๐ถ ) โ โ ) |
91 |
29
|
recnd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ต โ โ ) |
92 |
91
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ๐ต โ โ ) |
93 |
41
|
recnd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ท โ โ ) |
94 |
93
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ๐ท โ โ ) |
95 |
94
|
sqrtcld |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( โ โ ๐ท ) โ โ ) |
96 |
92 95
|
mulcld |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ๐ต ยท ( โ โ ๐ท ) ) โ โ ) |
97 |
90 96
|
addcld |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) โ โ ) |
98 |
90 96
|
subcld |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) โ โ ) |
99 |
46
|
adantr |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ โ โ ) |
100 |
99
|
recnd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ โ โ ) |
101 |
51
|
adantr |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ๐ โ 0 ) |
102 |
100 101
|
jca |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ๐ โ โ โง ๐ โ 0 ) ) |
103 |
102
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ๐ โ โ โง ๐ โ 0 ) ) |
104 |
|
div11 |
โข ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) โ โ โง ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) โ โ โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) = ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) ) ) |
105 |
97 98 103 104
|
syl3anc |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) = ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) ) ) |
106 |
|
addsubeq0 |
โข ( ( ( ๐ด ยท ๐ถ ) โ โ โง ( ๐ต ยท ( โ โ ๐ท ) ) โ โ ) โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) = ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) โ ( ๐ต ยท ( โ โ ๐ท ) ) = 0 ) ) |
107 |
90 96 106
|
syl2anc |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) = ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) โ ( ๐ต ยท ( โ โ ๐ท ) ) = 0 ) ) |
108 |
41 73
|
resqrtcld |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( โ โ ๐ท ) โ โ ) |
109 |
108
|
recnd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( โ โ ๐ท ) โ โ ) |
110 |
91 109
|
mul0ord |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ๐ต ยท ( โ โ ๐ท ) ) = 0 โ ( ๐ต = 0 โจ ( โ โ ๐ท ) = 0 ) ) ) |
111 |
110
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ( ๐ต ยท ( โ โ ๐ท ) ) = 0 โ ( ๐ต = 0 โจ ( โ โ ๐ท ) = 0 ) ) ) |
112 |
|
eqneqall |
โข ( ๐ต = 0 โ ( ๐ต โ 0 โ ๐ท = 0 ) ) |
113 |
112
|
com12 |
โข ( ๐ต โ 0 โ ( ๐ต = 0 โ ๐ท = 0 ) ) |
114 |
113
|
adantl |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ๐ต = 0 โ ๐ท = 0 ) ) |
115 |
|
sqrt00 |
โข ( ( ๐ท โ โ โง 0 โค ๐ท ) โ ( ( โ โ ๐ท ) = 0 โ ๐ท = 0 ) ) |
116 |
41 73 115
|
syl2anc |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( โ โ ๐ท ) = 0 โ ๐ท = 0 ) ) |
117 |
116
|
biimpd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( โ โ ๐ท ) = 0 โ ๐ท = 0 ) ) |
118 |
117
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ( โ โ ๐ท ) = 0 โ ๐ท = 0 ) ) |
119 |
114 118
|
jaod |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ( ๐ต = 0 โจ ( โ โ ๐ท ) = 0 ) โ ๐ท = 0 ) ) |
120 |
111 119
|
sylbid |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ( ๐ต ยท ( โ โ ๐ท ) ) = 0 โ ๐ท = 0 ) ) |
121 |
107 120
|
sylbid |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) = ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) โ ๐ท = 0 ) ) |
122 |
105 121
|
sylbid |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ๐ท = 0 ) ) |
123 |
122
|
necon3d |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ต โ 0 ) โ ( ๐ท โ 0 โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
124 |
123
|
impancom |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ๐ต โ 0 โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
125 |
124
|
imp |
โข ( ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โง ๐ต โ 0 ) โ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) |
126 |
125
|
olcd |
โข ( ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โง ๐ต โ 0 ) โ ( 1 โ 1 โจ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
127 |
|
1ex |
โข 1 โ V |
128 |
|
ovex |
โข ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ V |
129 |
127 128
|
opthne |
โข ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ ( 1 โ 1 โจ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
130 |
126 129
|
sylibr |
โข ( ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โง ๐ต โ 0 ) โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) |
131 |
|
1ne2 |
โข 1 โ 2 |
132 |
131
|
orci |
โข ( 1 โ 2 โจ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) |
133 |
127 128
|
opthne |
โข ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ ( 1 โ 2 โจ ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
134 |
132 133
|
mpbir |
โข โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ |
135 |
130 134
|
jctir |
โข ( ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โง ๐ต โ 0 ) โ ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) ) |
136 |
135
|
ex |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ๐ต โ 0 โ ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) ) ) |
137 |
27 33
|
remulcld |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ต ยท ๐ถ ) โ โ ) |
138 |
137
|
3adant3 |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ๐ต ยท ๐ถ ) โ โ ) |
139 |
138
|
adantr |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ๐ต ยท ๐ถ ) โ โ ) |
140 |
21 108
|
remulcld |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ๐ด ยท ( โ โ ๐ท ) ) โ โ ) |
141 |
139 140
|
resubcld |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) โ โ ) |
142 |
141
|
recnd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) โ โ ) |
143 |
142
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) โ โ ) |
144 |
29 35
|
remulcld |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ๐ต ยท ๐ถ ) โ โ ) |
145 |
144 140
|
readdcld |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) โ โ ) |
146 |
145
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) โ โ ) |
147 |
146
|
recnd |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) โ โ ) |
148 |
102
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ๐ โ โ โง ๐ โ 0 ) ) |
149 |
|
div11 |
โข ( ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) โ โ โง ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) โ โ โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ( ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) ) ) |
150 |
143 147 148 149
|
syl3anc |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) ) ) |
151 |
139
|
recnd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ๐ต ยท ๐ถ ) โ โ ) |
152 |
140
|
recnd |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ๐ด ยท ( โ โ ๐ท ) ) โ โ ) |
153 |
151 152
|
jca |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ๐ต ยท ๐ถ ) โ โ โง ( ๐ด ยท ( โ โ ๐ท ) ) โ โ ) ) |
154 |
153
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ๐ต ยท ๐ถ ) โ โ โง ( ๐ด ยท ( โ โ ๐ท ) ) โ โ ) ) |
155 |
|
eqcom |
โข ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) โ ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) ) |
156 |
|
addsubeq0 |
โข ( ( ( ๐ต ยท ๐ถ ) โ โ โง ( ๐ด ยท ( โ โ ๐ท ) ) โ โ ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) โ ( ๐ด ยท ( โ โ ๐ท ) ) = 0 ) ) |
157 |
155 156
|
bitrid |
โข ( ( ( ๐ต ยท ๐ถ ) โ โ โง ( ๐ด ยท ( โ โ ๐ท ) ) โ โ ) โ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) โ ( ๐ด ยท ( โ โ ๐ท ) ) = 0 ) ) |
158 |
154 157
|
syl |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) โ ( ๐ด ยท ( โ โ ๐ท ) ) = 0 ) ) |
159 |
86 109
|
mul0ord |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( ( ๐ด ยท ( โ โ ๐ท ) ) = 0 โ ( ๐ด = 0 โจ ( โ โ ๐ท ) = 0 ) ) ) |
160 |
159
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ๐ด ยท ( โ โ ๐ท ) ) = 0 โ ( ๐ด = 0 โจ ( โ โ ๐ท ) = 0 ) ) ) |
161 |
|
eqneqall |
โข ( ๐ด = 0 โ ( ๐ด โ 0 โ ๐ท = 0 ) ) |
162 |
161
|
com12 |
โข ( ๐ด โ 0 โ ( ๐ด = 0 โ ๐ท = 0 ) ) |
163 |
162
|
adantl |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ๐ด = 0 โ ๐ท = 0 ) ) |
164 |
117
|
adantr |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( โ โ ๐ท ) = 0 โ ๐ท = 0 ) ) |
165 |
163 164
|
jaod |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ๐ด = 0 โจ ( โ โ ๐ท ) = 0 ) โ ๐ท = 0 ) ) |
166 |
160 165
|
sylbid |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ๐ด ยท ( โ โ ๐ท ) ) = 0 โ ๐ท = 0 ) ) |
167 |
158 166
|
sylbid |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) = ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) โ ๐ท = 0 ) ) |
168 |
150 167
|
sylbid |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) = ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ๐ท = 0 ) ) |
169 |
168
|
necon3d |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ด โ 0 ) โ ( ๐ท โ 0 โ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
170 |
169
|
impancom |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ๐ด โ 0 โ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
171 |
170
|
imp |
โข ( ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โง ๐ด โ 0 ) โ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) |
172 |
171
|
olcd |
โข ( ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โง ๐ด โ 0 ) โ ( 2 โ 2 โจ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
173 |
|
2ex |
โข 2 โ V |
174 |
|
ovex |
โข ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ V |
175 |
173 174
|
opthne |
โข ( โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ ( 2 โ 2 โจ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
176 |
172 175
|
sylibr |
โข ( ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โง ๐ด โ 0 ) โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) |
177 |
131
|
necomi |
โข 2 โ 1 |
178 |
177
|
orci |
โข ( 2 โ 1 โจ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) |
179 |
173 174
|
opthne |
โข ( โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ ( 2 โ 1 โจ ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โ ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) ) ) |
180 |
178 179
|
mpbir |
โข โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ |
181 |
176 180
|
jctil |
โข ( ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โง ๐ด โ 0 ) โ ( โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) ) |
182 |
181
|
ex |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ๐ด โ 0 โ ( โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) ) ) |
183 |
136 182
|
orim12d |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ( ๐ต โ 0 โจ ๐ด โ 0 ) โ ( ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) โจ ( โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) ) ) ) |
184 |
85 183
|
biimtrid |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ( ๐ด โ 0 โจ ๐ต โ 0 ) โ ( ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) โจ ( โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) ) ) ) |
185 |
84 184
|
mpd |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) โจ ( โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) ) ) |
186 |
|
prneimg |
โข ( ( ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V ) โง ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V ) ) โ ( ( ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) โจ ( โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) ) โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } ) ) |
187 |
186
|
imp |
โข ( ( ( ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V ) โง ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ V ) ) โง ( ( โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) โจ ( โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โง โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ โ โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ ) ) ) โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } ) |
188 |
78 79 82 185 187
|
mpsyl4anc |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } ) |
189 |
77 188
|
jca |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } } โง { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } ) ) |
190 |
61 69 189
|
3jca |
โข ( ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โง ๐ท โ 0 ) โ ( { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ โง { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ โง ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } } โง { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } ) ) ) |
191 |
13 190
|
mpdan |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ ( { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ โง { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ โง ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } } โง { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } ) ) ) |
192 |
|
preq1 |
โข ( ๐ = { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { ๐ , ๐ } = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , ๐ } ) |
193 |
192
|
eqeq2d |
โข ( ๐ = { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { ๐ , ๐ } โ ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , ๐ } ) ) |
194 |
|
neeq1 |
โข ( ๐ = { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ( ๐ โ ๐ โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ ) ) |
195 |
193 194
|
anbi12d |
โข ( ๐ = { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ( ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { ๐ , ๐ } โง ๐ โ ๐ ) โ ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , ๐ } โง { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ ) ) ) |
196 |
|
preq2 |
โข ( ๐ = { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , ๐ } = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } } ) |
197 |
196
|
eqeq2d |
โข ( ๐ = { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , ๐ } โ ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } } ) ) |
198 |
|
neeq2 |
โข ( ๐ = { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ( { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } ) ) |
199 |
197 198
|
anbi12d |
โข ( ๐ = { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ( ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , ๐ } โง { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ ) โ ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } } โง { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } ) ) ) |
200 |
195 199
|
rspc2ev |
โข ( ( { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ โง { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ ๐ โง ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } , { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } } โง { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) + ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) โ ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } โ { โจ 1 , ( ( ( ๐ด ยท ๐ถ ) โ ( ๐ต ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ , โจ 2 , ( ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ( โ โ ๐ท ) ) ) / ๐ ) โฉ } ) ) โ โ ๐ โ ๐ โ ๐ โ ๐ ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { ๐ , ๐ } โง ๐ โ ๐ ) ) |
201 |
191 200
|
syl |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐
โ โ+ โง 0 < ๐ท ) ) โ โ ๐ โ ๐ โ ๐ โ ๐ ( ( ( 0 ๐ ๐
) โฉ ( ๐ ๐ฟ ๐ ) ) = { ๐ , ๐ } โง ๐ โ ๐ ) ) |