Step | Hyp | Ref
| Expression |
1 | | sharhght.a |
. . . . . . . . 9
โข (๐ โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) |
2 | 1 | simp3d 1145 |
. . . . . . . 8
โข (๐ โ ๐ถ โ โ) |
3 | 1 | simp1d 1143 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
4 | 2, 3 | subcld 11519 |
. . . . . . 7
โข (๐ โ (๐ถ โ ๐ด) โ โ) |
5 | 4 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ต = ๐ท) โ (๐ถ โ ๐ด) โ โ) |
6 | | sharhght.b |
. . . . . . . . 9
โข (๐ โ (๐ท โ โ โง ((๐ด โ ๐ท)๐บ(๐ต โ ๐ท)) = 0)) |
7 | 6 | simpld 496 |
. . . . . . . 8
โข (๐ โ ๐ท โ โ) |
8 | 7, 3 | subcld 11519 |
. . . . . . 7
โข (๐ โ (๐ท โ ๐ด) โ โ) |
9 | 8 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ต = ๐ท) โ (๐ท โ ๐ด) โ โ) |
10 | | sharhght.sigar |
. . . . . . 7
โข ๐บ = (๐ฅ โ โ, ๐ฆ โ โ โฆ
(โโ((โโ๐ฅ) ยท ๐ฆ))) |
11 | 10 | sigarim 45166 |
. . . . . 6
โข (((๐ถ โ ๐ด) โ โ โง (๐ท โ ๐ด) โ โ) โ ((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) โ โ) |
12 | 5, 9, 11 | syl2anc 585 |
. . . . 5
โข ((๐ โง ๐ต = ๐ท) โ ((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) โ โ) |
13 | 12 | recnd 11190 |
. . . 4
โข ((๐ โง ๐ต = ๐ท) โ ((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) โ โ) |
14 | 13 | mul01d 11361 |
. . 3
โข ((๐ โง ๐ต = ๐ท) โ (((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) ยท 0) = 0) |
15 | 1 | simp2d 1144 |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
16 | 15 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ต = ๐ท) โ ๐ต โ โ) |
17 | | simpr 486 |
. . . . 5
โข ((๐ โง ๐ต = ๐ท) โ ๐ต = ๐ท) |
18 | 16, 17 | subeq0bd 11588 |
. . . 4
โข ((๐ โง ๐ต = ๐ท) โ (๐ต โ ๐ท) = 0) |
19 | 18 | oveq2d 7378 |
. . 3
โข ((๐ โง ๐ต = ๐ท) โ (((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) ยท (๐ต โ ๐ท)) = (((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) ยท 0)) |
20 | 2, 15 | subcld 11519 |
. . . . . . . 8
โข (๐ โ (๐ถ โ ๐ต) โ โ) |
21 | 20 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ต = ๐ท) โ (๐ถ โ ๐ต) โ โ) |
22 | 7, 15 | subcld 11519 |
. . . . . . . 8
โข (๐ โ (๐ท โ ๐ต) โ โ) |
23 | 22 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ต = ๐ท) โ (๐ท โ ๐ต) โ โ) |
24 | 10 | sigarval 45165 |
. . . . . . 7
โข (((๐ถ โ ๐ต) โ โ โง (๐ท โ ๐ต) โ โ) โ ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) = (โโ((โโ(๐ถ โ ๐ต)) ยท (๐ท โ ๐ต)))) |
25 | 21, 23, 24 | syl2anc 585 |
. . . . . 6
โข ((๐ โง ๐ต = ๐ท) โ ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) = (โโ((โโ(๐ถ โ ๐ต)) ยท (๐ท โ ๐ต)))) |
26 | 7 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ต = ๐ท) โ ๐ท โ โ) |
27 | 17 | eqcomd 2743 |
. . . . . . . . . 10
โข ((๐ โง ๐ต = ๐ท) โ ๐ท = ๐ต) |
28 | 26, 27 | subeq0bd 11588 |
. . . . . . . . 9
โข ((๐ โง ๐ต = ๐ท) โ (๐ท โ ๐ต) = 0) |
29 | 28 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โง ๐ต = ๐ท) โ ((โโ(๐ถ โ ๐ต)) ยท (๐ท โ ๐ต)) = ((โโ(๐ถ โ ๐ต)) ยท 0)) |
30 | 21 | cjcld 15088 |
. . . . . . . . 9
โข ((๐ โง ๐ต = ๐ท) โ (โโ(๐ถ โ ๐ต)) โ โ) |
31 | 30 | mul01d 11361 |
. . . . . . . 8
โข ((๐ โง ๐ต = ๐ท) โ ((โโ(๐ถ โ ๐ต)) ยท 0) = 0) |
32 | 29, 31 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง ๐ต = ๐ท) โ ((โโ(๐ถ โ ๐ต)) ยท (๐ท โ ๐ต)) = 0) |
33 | 32 | fveq2d 6851 |
. . . . . 6
โข ((๐ โง ๐ต = ๐ท) โ
(โโ((โโ(๐ถ โ ๐ต)) ยท (๐ท โ ๐ต))) = (โโ0)) |
34 | | 0red 11165 |
. . . . . . 7
โข ((๐ โง ๐ต = ๐ท) โ 0 โ โ) |
35 | 34 | reim0d 15117 |
. . . . . 6
โข ((๐ โง ๐ต = ๐ท) โ (โโ0) =
0) |
36 | 25, 33, 35 | 3eqtrd 2781 |
. . . . 5
โข ((๐ โง ๐ต = ๐ท) โ ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) = 0) |
37 | 36 | oveq1d 7377 |
. . . 4
โข ((๐ โง ๐ต = ๐ท) โ (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ด โ ๐ท)) = (0 ยท (๐ด โ ๐ท))) |
38 | 3 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ต = ๐ท) โ ๐ด โ โ) |
39 | 38, 26 | subcld 11519 |
. . . . 5
โข ((๐ โง ๐ต = ๐ท) โ (๐ด โ ๐ท) โ โ) |
40 | 39 | mul02d 11360 |
. . . 4
โข ((๐ โง ๐ต = ๐ท) โ (0 ยท (๐ด โ ๐ท)) = 0) |
41 | 37, 40 | eqtrd 2777 |
. . 3
โข ((๐ โง ๐ต = ๐ท) โ (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ด โ ๐ท)) = 0) |
42 | 14, 19, 41 | 3eqtr4d 2787 |
. 2
โข ((๐ โง ๐ต = ๐ท) โ (((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) ยท (๐ต โ ๐ท)) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ด โ ๐ท))) |
43 | 2 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ๐ถ โ โ) |
44 | 15 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ๐ต โ โ) |
45 | 3 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ๐ด โ โ) |
46 | 43, 44, 45 | npncand 11543 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ถ โ ๐ต) + (๐ต โ ๐ด)) = (๐ถ โ ๐ด)) |
47 | 46 | oveq1d 7377 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ถ โ ๐ต) + (๐ต โ ๐ด))๐บ(๐ท โ ๐ด)) = ((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด))) |
48 | 43, 44 | subcld 11519 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (๐ถ โ ๐ต) โ โ) |
49 | 8 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (๐ท โ ๐ด) โ โ) |
50 | 44, 45 | subcld 11519 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (๐ต โ ๐ด) โ โ) |
51 | 10 | sigaraf 45168 |
. . . . . . . 8
โข (((๐ถ โ ๐ต) โ โ โง (๐ท โ ๐ด) โ โ โง (๐ต โ ๐ด) โ โ) โ (((๐ถ โ ๐ต) + (๐ต โ ๐ด))๐บ(๐ท โ ๐ด)) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด)) + ((๐ต โ ๐ด)๐บ(๐ท โ ๐ด)))) |
52 | 48, 49, 50, 51 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ถ โ ๐ต) + (๐ต โ ๐ด))๐บ(๐ท โ ๐ด)) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด)) + ((๐ต โ ๐ด)๐บ(๐ท โ ๐ด)))) |
53 | 47, 52 | eqtr3d 2779 |
. . . . . 6
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด)) + ((๐ต โ ๐ด)๐บ(๐ท โ ๐ด)))) |
54 | 6 | simprd 497 |
. . . . . . . . 9
โข (๐ โ ((๐ด โ ๐ท)๐บ(๐ต โ ๐ท)) = 0) |
55 | 54 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ด โ ๐ท)๐บ(๐ต โ ๐ท)) = 0) |
56 | 7 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ๐ท โ โ) |
57 | 10 | sigarperm 45175 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โ ((๐ด โ ๐ท)๐บ(๐ต โ ๐ท)) = ((๐ต โ ๐ด)๐บ(๐ท โ ๐ด))) |
58 | 45, 44, 56, 57 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ด โ ๐ท)๐บ(๐ต โ ๐ท)) = ((๐ต โ ๐ด)๐บ(๐ท โ ๐ด))) |
59 | 55, 58 | eqtr3d 2779 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ต = ๐ท) โ 0 = ((๐ต โ ๐ด)๐บ(๐ท โ ๐ด))) |
60 | 59 | oveq2d 7378 |
. . . . . 6
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด)) + 0) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด)) + ((๐ต โ ๐ด)๐บ(๐ท โ ๐ด)))) |
61 | 10 | sigarim 45166 |
. . . . . . . . 9
โข (((๐ถ โ ๐ต) โ โ โง (๐ท โ ๐ด) โ โ) โ ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด)) โ โ) |
62 | 48, 49, 61 | syl2anc 585 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด)) โ โ) |
63 | 62 | recnd 11190 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด)) โ โ) |
64 | 63 | addid1d 11362 |
. . . . . 6
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด)) + 0) = ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด))) |
65 | 53, 60, 64 | 3eqtr2d 2783 |
. . . . 5
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) = ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด))) |
66 | 44, 56 | negsubdi2d 11535 |
. . . . . . . . . . . 12
โข ((๐ โง ยฌ ๐ต = ๐ท) โ -(๐ต โ ๐ท) = (๐ท โ ๐ต)) |
67 | 66 | eqcomd 2743 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (๐ท โ ๐ต) = -(๐ต โ ๐ท)) |
68 | 67 | oveq1d 7377 |
. . . . . . . . . 10
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ท โ ๐ต) / (๐ต โ ๐ท)) = (-(๐ต โ ๐ท) / (๐ต โ ๐ท))) |
69 | 44, 56 | subcld 11519 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (๐ต โ ๐ท) โ โ) |
70 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ยฌ ๐ต = ๐ท) |
71 | 70 | neqned 2951 |
. . . . . . . . . . . 12
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ๐ต โ ๐ท) |
72 | 44, 56, 71 | subne0d 11528 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (๐ต โ ๐ท) โ 0) |
73 | 69, 69, 72 | divnegd 11951 |
. . . . . . . . . 10
โข ((๐ โง ยฌ ๐ต = ๐ท) โ -((๐ต โ ๐ท) / (๐ต โ ๐ท)) = (-(๐ต โ ๐ท) / (๐ต โ ๐ท))) |
74 | 69, 72 | dividd 11936 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ต โ ๐ท) / (๐ต โ ๐ท)) = 1) |
75 | 74 | negeqd 11402 |
. . . . . . . . . 10
โข ((๐ โง ยฌ ๐ต = ๐ท) โ -((๐ต โ ๐ท) / (๐ต โ ๐ท)) = -1) |
76 | 68, 73, 75 | 3eqtr2d 2783 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ท โ ๐ต) / (๐ต โ ๐ท)) = -1) |
77 | 76 | oveq1d 7377 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ท โ ๐ต) / (๐ต โ ๐ท)) ยท (๐ด โ ๐ท)) = (-1 ยท (๐ด โ ๐ท))) |
78 | 45, 56 | subcld 11519 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (๐ด โ ๐ท) โ โ) |
79 | 78 | mulm1d 11614 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (-1 ยท (๐ด โ ๐ท)) = -(๐ด โ ๐ท)) |
80 | 45, 56 | negsubdi2d 11535 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ -(๐ด โ ๐ท) = (๐ท โ ๐ด)) |
81 | 77, 79, 80 | 3eqtrd 2781 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ท โ ๐ต) / (๐ต โ ๐ท)) ยท (๐ด โ ๐ท)) = (๐ท โ ๐ด)) |
82 | 56, 44 | subcld 11519 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (๐ท โ ๐ต) โ โ) |
83 | 82, 69, 78, 72 | div32d 11961 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ท โ ๐ต) / (๐ต โ ๐ท)) ยท (๐ด โ ๐ท)) = ((๐ท โ ๐ต) ยท ((๐ด โ ๐ท) / (๐ต โ ๐ท)))) |
84 | 81, 83 | eqtr3d 2779 |
. . . . . 6
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (๐ท โ ๐ด) = ((๐ท โ ๐ต) ยท ((๐ด โ ๐ท) / (๐ต โ ๐ท)))) |
85 | 84 | oveq2d 7378 |
. . . . 5
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ด)) = ((๐ถ โ ๐ต)๐บ((๐ท โ ๐ต) ยท ((๐ด โ ๐ท) / (๐ต โ ๐ท))))) |
86 | 56, 45, 44 | 3jca 1129 |
. . . . . . 7
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (๐ท โ โ โง ๐ด โ โ โง ๐ต โ โ)) |
87 | 10, 86, 70, 55 | sigardiv 45176 |
. . . . . 6
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ด โ ๐ท) / (๐ต โ ๐ท)) โ โ) |
88 | 10 | sigarls 45172 |
. . . . . 6
โข (((๐ถ โ ๐ต) โ โ โง (๐ท โ ๐ต) โ โ โง ((๐ด โ ๐ท) / (๐ต โ ๐ท)) โ โ) โ ((๐ถ โ ๐ต)๐บ((๐ท โ ๐ต) ยท ((๐ด โ ๐ท) / (๐ต โ ๐ท)))) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท ((๐ด โ ๐ท) / (๐ต โ ๐ท)))) |
89 | 48, 82, 87, 88 | syl3anc 1372 |
. . . . 5
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ถ โ ๐ต)๐บ((๐ท โ ๐ต) ยท ((๐ด โ ๐ท) / (๐ต โ ๐ท)))) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท ((๐ด โ ๐ท) / (๐ต โ ๐ท)))) |
90 | 65, 85, 89 | 3eqtrd 2781 |
. . . 4
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท ((๐ด โ ๐ท) / (๐ต โ ๐ท)))) |
91 | 90 | oveq1d 7377 |
. . 3
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) ยท (๐ต โ ๐ท)) = ((((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท ((๐ด โ ๐ท) / (๐ต โ ๐ท))) ยท (๐ต โ ๐ท))) |
92 | 10 | sigarim 45166 |
. . . . . 6
โข (((๐ถ โ ๐ต) โ โ โง (๐ท โ ๐ต) โ โ) โ ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) โ โ) |
93 | 92 | recnd 11190 |
. . . . 5
โข (((๐ถ โ ๐ต) โ โ โง (๐ท โ ๐ต) โ โ) โ ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) โ โ) |
94 | 48, 82, 93 | syl2anc 585 |
. . . 4
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) โ โ) |
95 | 78, 69, 72 | divcld 11938 |
. . . 4
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((๐ด โ ๐ท) / (๐ต โ ๐ท)) โ โ) |
96 | 94, 95, 69 | mulassd 11185 |
. . 3
โข ((๐ โง ยฌ ๐ต = ๐ท) โ ((((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท ((๐ด โ ๐ท) / (๐ต โ ๐ท))) ยท (๐ต โ ๐ท)) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (((๐ด โ ๐ท) / (๐ต โ ๐ท)) ยท (๐ต โ ๐ท)))) |
97 | 78, 69, 72 | divcan1d 11939 |
. . . 4
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ด โ ๐ท) / (๐ต โ ๐ท)) ยท (๐ต โ ๐ท)) = (๐ด โ ๐ท)) |
98 | 97 | oveq2d 7378 |
. . 3
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (((๐ด โ ๐ท) / (๐ต โ ๐ท)) ยท (๐ต โ ๐ท))) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ด โ ๐ท))) |
99 | 91, 96, 98 | 3eqtrd 2781 |
. 2
โข ((๐ โง ยฌ ๐ต = ๐ท) โ (((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) ยท (๐ต โ ๐ท)) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ด โ ๐ท))) |
100 | 42, 99 | pm2.61dan 812 |
1
โข (๐ โ (((๐ถ โ ๐ด)๐บ(๐ท โ ๐ด)) ยท (๐ต โ ๐ท)) = (((๐ถ โ ๐ต)๐บ(๐ท โ ๐ต)) ยท (๐ด โ ๐ท))) |