Step | Hyp | Ref
| Expression |
1 | | brbtwn2 28690 |
. . 3
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ด Btwn โจ๐ต, ๐ถโฉ โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
2 | | brbtwn2 28690 |
. . . . 5
โข ((๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐) โง ๐ด โ (๐ผโ๐)) โ (๐ต Btwn โจ๐ถ, ๐ดโฉ โ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐)))))) |
3 | 2 | 3comr 1123 |
. . . 4
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ต Btwn โจ๐ถ, ๐ดโฉ โ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐)))))) |
4 | | colinearalglem3 28693 |
. . . . . 6
โข ((๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐) โง ๐ด โ (๐ผโ๐)) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โ โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
5 | 4 | 3comr 1123 |
. . . . 5
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โ โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
6 | 5 | anbi2d 628 |
. . . 4
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ ((โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐)))) โ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
7 | 3, 6 | bitrd 279 |
. . 3
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ต Btwn โจ๐ถ, ๐ดโฉ โ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
8 | | brbtwn2 28690 |
. . . . 5
โข ((๐ถ โ (๐ผโ๐) โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (๐ถ Btwn โจ๐ด, ๐ตโฉ โ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) = (((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐)))))) |
9 | | colinearalglem2 28692 |
. . . . . 6
โข ((๐ถ โ (๐ผโ๐) โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) = (((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โ โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
10 | 9 | anbi2d 628 |
. . . . 5
โข ((๐ถ โ (๐ผโ๐) โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ ((โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) = (((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐)))) โ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
11 | 8, 10 | bitrd 279 |
. . . 4
โข ((๐ถ โ (๐ผโ๐) โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (๐ถ Btwn โจ๐ด, ๐ตโฉ โ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
12 | 11 | 3coml 1125 |
. . 3
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ถ Btwn โจ๐ด, ๐ตโฉ โ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
13 | 1, 7, 12 | 3orbi123d 1432 |
. 2
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ ((๐ด Btwn โจ๐ต, ๐ถโฉ โจ ๐ต Btwn โจ๐ถ, ๐ดโฉ โจ ๐ถ Btwn โจ๐ด, ๐ตโฉ) โ ((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))))) |
14 | | fveecn 28687 |
. . . . . . . . . . . . 13
โข ((๐ต โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
15 | | fveecn 28687 |
. . . . . . . . . . . . 13
โข ((๐ถ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
16 | | subid 11495 |
. . . . . . . . . . . . . . . 16
โข ((๐ถโ๐) โ โ โ ((๐ถโ๐) โ (๐ถโ๐)) = 0) |
17 | 16 | oveq2d 7430 |
. . . . . . . . . . . . . . 15
โข ((๐ถโ๐) โ โ โ (((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) = (((๐ตโ๐) โ (๐ถโ๐)) ยท 0)) |
18 | 17 | adantl 481 |
. . . . . . . . . . . . . 14
โข (((๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) = (((๐ตโ๐) โ (๐ถโ๐)) ยท 0)) |
19 | | subcl 11475 |
. . . . . . . . . . . . . . 15
โข (((๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((๐ตโ๐) โ (๐ถโ๐)) โ โ) |
20 | 19 | mul01d 11429 |
. . . . . . . . . . . . . 14
โข (((๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (((๐ตโ๐) โ (๐ถโ๐)) ยท 0) = 0) |
21 | 18, 20 | eqtrd 2767 |
. . . . . . . . . . . . 13
โข (((๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) = 0) |
22 | 14, 15, 21 | syl2an 595 |
. . . . . . . . . . . 12
โข (((๐ต โ (๐ผโ๐) โง ๐ โ (1...๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ โ (1...๐))) โ (((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) = 0) |
23 | 22 | anandirs 678 |
. . . . . . . . . . 11
โข (((๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) = 0) |
24 | | 0le0 12329 |
. . . . . . . . . . 11
โข 0 โค
0 |
25 | 23, 24 | eqbrtrdi 5181 |
. . . . . . . . . 10
โข (((๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) โค 0) |
26 | 25 | ralrimiva 3141 |
. . . . . . . . 9
โข ((๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) โค 0) |
27 | 26 | 3adant1 1128 |
. . . . . . . 8
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) โค 0) |
28 | | fveq1 6890 |
. . . . . . . . . . . 12
โข (๐ถ = ๐ด โ (๐ถโ๐) = (๐ดโ๐)) |
29 | 28 | oveq2d 7430 |
. . . . . . . . . . 11
โข (๐ถ = ๐ด โ ((๐ตโ๐) โ (๐ถโ๐)) = ((๐ตโ๐) โ (๐ดโ๐))) |
30 | 28 | oveq2d 7430 |
. . . . . . . . . . 11
โข (๐ถ = ๐ด โ ((๐ถโ๐) โ (๐ถโ๐)) = ((๐ถโ๐) โ (๐ดโ๐))) |
31 | 29, 30 | oveq12d 7432 |
. . . . . . . . . 10
โข (๐ถ = ๐ด โ (((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
32 | 31 | breq1d 5152 |
. . . . . . . . 9
โข (๐ถ = ๐ด โ ((((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) โค 0 โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0)) |
33 | 32 | ralbidv 3172 |
. . . . . . . 8
โข (๐ถ = ๐ด โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ถโ๐)) ยท ((๐ถโ๐) โ (๐ถโ๐))) โค 0 โ โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0)) |
34 | 27, 33 | syl5ibcom 244 |
. . . . . . 7
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ถ = ๐ด โ โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0)) |
35 | | 3mix1 1328 |
. . . . . . 7
โข
(โ๐ โ
(1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0)) |
36 | 34, 35 | syl6 35 |
. . . . . 6
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ถ = ๐ด โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0))) |
37 | 36 | a1dd 50 |
. . . . 5
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ถ = ๐ด โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0)))) |
38 | | simp3 1136 |
. . . . . . . . 9
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ ๐ถ โ (๐ผโ๐)) |
39 | | simp1 1134 |
. . . . . . . . 9
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ ๐ด โ (๐ผโ๐)) |
40 | | eqeefv 28688 |
. . . . . . . . 9
โข ((๐ถ โ (๐ผโ๐) โง ๐ด โ (๐ผโ๐)) โ (๐ถ = ๐ด โ โ๐ โ (1...๐)(๐ถโ๐) = (๐ดโ๐))) |
41 | 38, 39, 40 | syl2anc 583 |
. . . . . . . 8
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ถ = ๐ด โ โ๐ โ (1...๐)(๐ถโ๐) = (๐ดโ๐))) |
42 | 41 | necon3abid 2972 |
. . . . . . 7
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ถ โ ๐ด โ ยฌ โ๐ โ (1...๐)(๐ถโ๐) = (๐ดโ๐))) |
43 | | df-ne 2936 |
. . . . . . . . 9
โข ((๐ถโ๐) โ (๐ดโ๐) โ ยฌ (๐ถโ๐) = (๐ดโ๐)) |
44 | 43 | rexbii 3089 |
. . . . . . . 8
โข
(โ๐ โ
(1...๐)(๐ถโ๐) โ (๐ดโ๐) โ โ๐ โ (1...๐) ยฌ (๐ถโ๐) = (๐ดโ๐)) |
45 | | rexnal 3095 |
. . . . . . . 8
โข
(โ๐ โ
(1...๐) ยฌ (๐ถโ๐) = (๐ดโ๐) โ ยฌ โ๐ โ (1...๐)(๐ถโ๐) = (๐ดโ๐)) |
46 | 44, 45 | bitr2i 276 |
. . . . . . 7
โข (ยฌ
โ๐ โ (1...๐)(๐ถโ๐) = (๐ดโ๐) โ โ๐ โ (1...๐)(๐ถโ๐) โ (๐ดโ๐)) |
47 | 42, 46 | bitrdi 287 |
. . . . . 6
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ถ โ ๐ด โ โ๐ โ (1...๐)(๐ถโ๐) โ (๐ดโ๐))) |
48 | | ralcom 3281 |
. . . . . . . 8
โข
(โ๐ โ
(1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
49 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐ถโ๐) = (๐ถโ๐)) |
50 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
51 | 49, 50 | oveq12d 7432 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((๐ถโ๐) โ (๐ดโ๐)) = ((๐ถโ๐) โ (๐ดโ๐))) |
52 | 51 | oveq2d 7430 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
53 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐ตโ๐) = (๐ตโ๐)) |
54 | 53, 50 | oveq12d 7432 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((๐ตโ๐) โ (๐ดโ๐)) = ((๐ตโ๐) โ (๐ดโ๐))) |
55 | 54 | oveq1d 7429 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
56 | 52, 55 | eqeq12d 2743 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
57 | 56 | ralbidv 3172 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
58 | 57 | rspcv 3603 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
59 | 58 | ad2antrl 727 |
. . . . . . . . 9
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง (๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
60 | | fveere 28686 |
. . . . . . . . . . . . . 14
โข ((๐ด โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
61 | 60 | 3ad2antl1 1183 |
. . . . . . . . . . . . 13
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
62 | | fveere 28686 |
. . . . . . . . . . . . . 14
โข ((๐ต โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
63 | 62 | 3ad2antl2 1184 |
. . . . . . . . . . . . 13
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
64 | | fveere 28686 |
. . . . . . . . . . . . . 14
โข ((๐ถ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
65 | 64 | 3ad2antl3 1185 |
. . . . . . . . . . . . 13
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
66 | 61, 63, 65 | 3jca 1126 |
. . . . . . . . . . . 12
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) |
67 | 66 | anim1i 614 |
. . . . . . . . . . 11
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โง (๐ถโ๐) โ (๐ดโ๐)) โ (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐))) |
68 | 67 | anasss 466 |
. . . . . . . . . 10
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง (๐ถโ๐) โ (๐ดโ๐))) โ (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐))) |
69 | | fveecn 28687 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
70 | 69 | 3ad2antl1 1183 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (๐ดโ๐) โ โ) |
71 | 14 | 3ad2antl2 1184 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (๐ตโ๐) โ โ) |
72 | 15 | 3ad2antl3 1185 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
73 | 70, 71, 72 | 3jca 1126 |
. . . . . . . . . . . . . 14
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐ โ (1...๐)) โ ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) |
74 | 73 | adantlr 714 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐))) โง ๐ โ (1...๐)) โ ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) |
75 | | recn 11214 |
. . . . . . . . . . . . . . . 16
โข ((๐ดโ๐) โ โ โ (๐ดโ๐) โ โ) |
76 | | recn 11214 |
. . . . . . . . . . . . . . . 16
โข ((๐ตโ๐) โ โ โ (๐ตโ๐) โ โ) |
77 | | recn 11214 |
. . . . . . . . . . . . . . . 16
โข ((๐ถโ๐) โ โ โ (๐ถโ๐) โ โ) |
78 | 75, 76, 77 | 3anim123i 1149 |
. . . . . . . . . . . . . . 15
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) |
79 | 78 | adantr 480 |
. . . . . . . . . . . . . 14
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) |
80 | 79 | ad2antlr 726 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐))) โง ๐ โ (1...๐)) โ ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) |
81 | | simplrr 777 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐))) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ (๐ดโ๐)) |
82 | | eqcom 2734 |
. . . . . . . . . . . . . 14
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) = (๐ตโ๐)) |
83 | | simp12 1202 |
. . . . . . . . . . . . . . . 16
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (๐ตโ๐) โ โ) |
84 | | simp11 1201 |
. . . . . . . . . . . . . . . 16
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (๐ดโ๐) โ โ) |
85 | | simp22 1205 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (๐ตโ๐) โ โ) |
86 | | simp21 1204 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (๐ดโ๐) โ โ) |
87 | 85, 86 | subcld 11587 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((๐ตโ๐) โ (๐ดโ๐)) โ โ) |
88 | | simp23 1206 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (๐ถโ๐) โ โ) |
89 | 88, 86 | subcld 11587 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
90 | | simpr3 1194 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (๐ถโ๐) โ โ) |
91 | | simpr1 1192 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (๐ดโ๐) โ โ) |
92 | 90, 91 | subeq0ad 11597 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ถโ๐) โ (๐ดโ๐)) = 0 โ (๐ถโ๐) = (๐ดโ๐))) |
93 | 92 | necon3bid 2980 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ)) โ (((๐ถโ๐) โ (๐ดโ๐)) โ 0 โ (๐ถโ๐) โ (๐ดโ๐))) |
94 | 93 | biimp3ar 1467 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((๐ถโ๐) โ (๐ดโ๐)) โ 0) |
95 | 87, 89, 94 | divcld 12006 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
96 | | simp13 1203 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (๐ถโ๐) โ โ) |
97 | 96, 84 | subcld 11587 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
98 | 95, 97 | mulcld 11250 |
. . . . . . . . . . . . . . . 16
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
99 | | subadd2 11480 |
. . . . . . . . . . . . . . . . 17
โข (((๐ตโ๐) โ โ โง (๐ดโ๐) โ โ โง ((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) โ (((๐ตโ๐) โ (๐ดโ๐)) = ((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) = (๐ตโ๐))) |
100 | 99 | bicomd 222 |
. . . . . . . . . . . . . . . 16
โข (((๐ตโ๐) โ โ โง (๐ดโ๐) โ โ โง ((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) โ ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) = (๐ตโ๐) โ ((๐ตโ๐) โ (๐ดโ๐)) = ((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
101 | 83, 84, 98, 100 | syl3anc 1369 |
. . . . . . . . . . . . . . 15
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) = (๐ตโ๐) โ ((๐ตโ๐) โ (๐ดโ๐)) = ((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
102 | 87, 97, 89, 94 | div23d 12043 |
. . . . . . . . . . . . . . . 16
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) / ((๐ถโ๐) โ (๐ดโ๐))) = ((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
103 | 102 | eqeq2d 2738 |
. . . . . . . . . . . . . . 15
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (((๐ตโ๐) โ (๐ดโ๐)) = ((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) / ((๐ถโ๐) โ (๐ดโ๐))) โ ((๐ตโ๐) โ (๐ดโ๐)) = ((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
104 | | eqcom 2734 |
. . . . . . . . . . . . . . . 16
โข (((๐ตโ๐) โ (๐ดโ๐)) = ((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) / ((๐ถโ๐) โ (๐ดโ๐))) โ ((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) / ((๐ถโ๐) โ (๐ดโ๐))) = ((๐ตโ๐) โ (๐ดโ๐))) |
105 | 87, 97 | mulcld 11250 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
106 | 83, 84 | subcld 11587 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((๐ตโ๐) โ (๐ดโ๐)) โ โ) |
107 | 105, 89, 106, 94 | divmuld 12028 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) / ((๐ถโ๐) โ (๐ดโ๐))) = ((๐ตโ๐) โ (๐ดโ๐)) โ (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ตโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
108 | 89, 106 | mulcomd 11251 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ตโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
109 | 108 | eqeq1d 2729 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((((๐ถโ๐) โ (๐ดโ๐)) ยท ((๐ตโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
110 | 107, 109 | bitrd 279 |
. . . . . . . . . . . . . . . 16
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) / ((๐ถโ๐) โ (๐ดโ๐))) = ((๐ตโ๐) โ (๐ดโ๐)) โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
111 | 104, 110 | bitrid 283 |
. . . . . . . . . . . . . . 15
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (((๐ตโ๐) โ (๐ดโ๐)) = ((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) / ((๐ถโ๐) โ (๐ดโ๐))) โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
112 | 101, 103,
111 | 3bitr2d 307 |
. . . . . . . . . . . . . 14
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) = (๐ตโ๐) โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
113 | 82, 112 | bitrid 283 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง ((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
114 | 74, 80, 81, 113 | syl3anc 1369 |
. . . . . . . . . . . 12
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐))) โง ๐ โ (1...๐)) โ ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
115 | 114 | ralbidva 3170 |
. . . . . . . . . . 11
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
116 | | 3simpb 1147 |
. . . . . . . . . . . 12
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) |
117 | | simpl2 1190 |
. . . . . . . . . . . . . 14
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (๐ตโ๐) โ โ) |
118 | | simpl1 1189 |
. . . . . . . . . . . . . 14
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (๐ดโ๐) โ โ) |
119 | 117, 118 | resubcld 11658 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((๐ตโ๐) โ (๐ดโ๐)) โ โ) |
120 | | simpl3 1191 |
. . . . . . . . . . . . . 14
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (๐ถโ๐) โ โ) |
121 | 120, 118 | resubcld 11658 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((๐ถโ๐) โ (๐ดโ๐)) โ โ) |
122 | | simp3 1136 |
. . . . . . . . . . . . . . . . 17
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (๐ถโ๐) โ โ) |
123 | 122 | recnd 11258 |
. . . . . . . . . . . . . . . 16
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (๐ถโ๐) โ โ) |
124 | 75 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . 16
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (๐ดโ๐) โ โ) |
125 | 123, 124 | subeq0ad 11597 |
. . . . . . . . . . . . . . 15
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (((๐ถโ๐) โ (๐ดโ๐)) = 0 โ (๐ถโ๐) = (๐ดโ๐))) |
126 | 125 | necon3bid 2980 |
. . . . . . . . . . . . . 14
โข (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โ (((๐ถโ๐) โ (๐ดโ๐)) โ 0 โ (๐ถโ๐) โ (๐ดโ๐))) |
127 | 126 | biimpar 477 |
. . . . . . . . . . . . 13
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ ((๐ถโ๐) โ (๐ดโ๐)) โ 0) |
128 | 119, 121,
127 | redivcld 12058 |
. . . . . . . . . . . 12
โข ((((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐)) โ (((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) โ โ) |
129 | | colinearalglem4 28694 |
. . . . . . . . . . . . 13
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) โ โ) โ (โ๐ โ (1...๐)(((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0)) |
130 | | oveq1 7421 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ ((๐ตโ๐) โ (๐ดโ๐)) = ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐))) |
131 | 130 | oveq1d 7429 |
. . . . . . . . . . . . . . . . 17
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) |
132 | 131 | breq1d 5152 |
. . . . . . . . . . . . . . . 16
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ ((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โ (((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0)) |
133 | 132 | ralimi 3078 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
(1...๐)(๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ โ๐ โ (1...๐)((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โ (((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0)) |
134 | | ralbi 3098 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
(1...๐)((((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โ (((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โ โ๐ โ (1...๐)(((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0)) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
(1...๐)(๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โ โ๐ โ (1...๐)(((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0)) |
136 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ ((๐ถโ๐) โ (๐ตโ๐)) = ((๐ถโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) |
137 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ ((๐ดโ๐) โ (๐ตโ๐)) = ((๐ดโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) |
138 | 136, 137 | oveq12d 7432 |
. . . . . . . . . . . . . . . . 17
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))))) |
139 | 138 | breq1d 5152 |
. . . . . . . . . . . . . . . 16
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ ((((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โ (((๐ถโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0)) |
140 | 139 | ralimi 3078 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
(1...๐)(๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ โ๐ โ (1...๐)((((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โ (((๐ถโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0)) |
141 | | ralbi 3098 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
(1...๐)((((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โ (((๐ถโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0) โ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โ โ๐ โ (1...๐)(((๐ถโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0)) |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
(1...๐)(๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โ โ๐ โ (1...๐)(((๐ถโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0)) |
143 | | oveq1 7421 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ ((๐ตโ๐) โ (๐ถโ๐)) = ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) |
144 | 143 | oveq2d 7430 |
. . . . . . . . . . . . . . . . 17
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) = (((๐ดโ๐) โ (๐ถโ๐)) ยท ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐)))) |
145 | 144 | breq1d 5152 |
. . . . . . . . . . . . . . . 16
โข ((๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ ((((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โ (((๐ดโ๐) โ (๐ถโ๐)) ยท ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0)) |
146 | 145 | ralimi 3078 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
(1...๐)(๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ โ๐ โ (1...๐)((((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โ (((๐ดโ๐) โ (๐ถโ๐)) ยท ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0)) |
147 | | ralbi 3098 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
(1...๐)((((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โ (((๐ดโ๐) โ (๐ถโ๐)) ยท ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0) โ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0)) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
(1...๐)(๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0)) |
149 | 135, 142,
148 | 3orbi123d 1432 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
(1...๐)(๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ ((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0) โ (โ๐ โ (1...๐)(((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0))) |
150 | 129, 149 | syl5ibrcom 246 |
. . . . . . . . . . . 12
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) โ โ) โ (โ๐ โ (1...๐)(๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0))) |
151 | 116, 128,
150 | syl2an 595 |
. . . . . . . . . . 11
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(๐ตโ๐) = (((((๐ตโ๐) โ (๐ดโ๐)) / ((๐ถโ๐) โ (๐ดโ๐))) ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0))) |
152 | 115, 151 | sylbird 260 |
. . . . . . . . . 10
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (((๐ดโ๐) โ โ โง (๐ตโ๐) โ โ โง (๐ถโ๐) โ โ) โง (๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0))) |
153 | 68, 152 | syldan 590 |
. . . . . . . . 9
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง (๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0))) |
154 | 59, 153 | syld 47 |
. . . . . . . 8
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง (๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0))) |
155 | 48, 154 | biimtrid 241 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (1...๐) โง (๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0))) |
156 | 155 | rexlimdvaa 3151 |
. . . . . 6
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (โ๐ โ (1...๐)(๐ถโ๐) โ (๐ดโ๐) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0)))) |
157 | 47, 156 | sylbid 239 |
. . . . 5
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ถ โ ๐ด โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0)))) |
158 | 37, 157 | pm2.61dne 3023 |
. . . 4
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0))) |
159 | 158 | pm4.71rd 562 |
. . 3
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ ((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0) โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
160 | | andir 1007 |
. . . . 5
โข
(((โ๐ โ
(1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0) โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ ((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
161 | 160 | orbi1i 912 |
. . . 4
โข
((((โ๐ โ
(1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0) โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) โ (((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) โจ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
162 | | df-3or 1086 |
. . . . . 6
โข
((โ๐ โ
(1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0) โ ((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0) โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0)) |
163 | 162 | anbi1i 623 |
. . . . 5
โข
(((โ๐ โ
(1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0) โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ (((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0) โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0) โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
164 | | andir 1007 |
. . . . 5
โข
((((โ๐ โ
(1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0) โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0) โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ (((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0) โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
165 | 163, 164 | bitri 275 |
. . . 4
โข
(((โ๐ โ
(1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0) โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ (((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0) โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
166 | | df-3or 1086 |
. . . 4
โข
(((โ๐ โ
(1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) โ (((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) โจ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
167 | 161, 165,
166 | 3bitr4i 303 |
. . 3
โข
(((โ๐ โ
(1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0) โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โ ((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) |
168 | 159, 167 | bitr2di 288 |
. 2
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (((โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))) โจ (โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) โ โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |
169 | 13, 168 | bitrd 279 |
1
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ ((๐ด Btwn โจ๐ต, ๐ถโฉ โจ ๐ต Btwn โจ๐ถ, ๐ดโฉ โจ ๐ถ Btwn โจ๐ด, ๐ตโฉ) โ โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) |