Step | Hyp | Ref
| Expression |
1 | | sigarcol.sigar |
. . . . 5
โข ๐บ = (๐ฅ โ โ, ๐ฆ โ โ โฆ
(โโ((โโ๐ฅ) ยท ๐ฆ))) |
2 | | sigarcol.a |
. . . . . . . 8
โข (๐ โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) |
3 | 2 | simp2d 1143 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
4 | 2 | simp3d 1144 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
5 | 2 | simp1d 1142 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
6 | 3, 4, 5 | 3jca 1128 |
. . . . . 6
โข (๐ โ (๐ต โ โ โง ๐ถ โ โ โง ๐ด โ โ)) |
7 | 6 | adantr 481 |
. . . . 5
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ (๐ต โ โ โง ๐ถ โ โ โง ๐ด โ โ)) |
8 | | sigarcol.b |
. . . . . 6
โข (๐ โ ยฌ ๐ด = ๐ต) |
9 | 8 | adantr 481 |
. . . . 5
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ ยฌ ๐ด = ๐ต) |
10 | 1 | sigarperm 45002 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = ((๐ต โ ๐ด)๐บ(๐ถ โ ๐ด))) |
11 | 2, 10 | syl 17 |
. . . . . . . 8
โข (๐ โ ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = ((๐ต โ ๐ด)๐บ(๐ถ โ ๐ด))) |
12 | 1 | sigarperm 45002 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ถ โ โ โง ๐ด โ โ) โ ((๐ต โ ๐ด)๐บ(๐ถ โ ๐ด)) = ((๐ถ โ ๐ต)๐บ(๐ด โ ๐ต))) |
13 | 6, 12 | syl 17 |
. . . . . . . 8
โข (๐ โ ((๐ต โ ๐ด)๐บ(๐ถ โ ๐ด)) = ((๐ถ โ ๐ต)๐บ(๐ด โ ๐ต))) |
14 | 11, 13 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = ((๐ถ โ ๐ต)๐บ(๐ด โ ๐ต))) |
15 | 14 | eqeq1d 2739 |
. . . . . 6
โข (๐ โ (((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0 โ ((๐ถ โ ๐ต)๐บ(๐ด โ ๐ต)) = 0)) |
16 | 15 | biimpa 477 |
. . . . 5
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ ((๐ถ โ ๐ต)๐บ(๐ด โ ๐ต)) = 0) |
17 | 1, 7, 9, 16 | sigardiv 45003 |
. . . 4
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ ((๐ถ โ ๐ต) / (๐ด โ ๐ต)) โ โ) |
18 | 4, 3 | subcld 11470 |
. . . . . . . 8
โข (๐ โ (๐ถ โ ๐ต) โ โ) |
19 | 18 | adantr 481 |
. . . . . . 7
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ (๐ถ โ ๐ต) โ โ) |
20 | 5, 3 | subcld 11470 |
. . . . . . . 8
โข (๐ โ (๐ด โ ๐ต) โ โ) |
21 | 20 | adantr 481 |
. . . . . . 7
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ (๐ด โ ๐ต) โ โ) |
22 | 5 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ ๐ด โ โ) |
23 | 3 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ ๐ต โ โ) |
24 | 9 | neqned 2948 |
. . . . . . . 8
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ ๐ด โ ๐ต) |
25 | 22, 23, 24 | subne0d 11479 |
. . . . . . 7
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ (๐ด โ ๐ต) โ 0) |
26 | 19, 21, 25 | divcan1d 11890 |
. . . . . 6
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ (((๐ถ โ ๐ต) / (๐ด โ ๐ต)) ยท (๐ด โ ๐ต)) = (๐ถ โ ๐ต)) |
27 | 26 | oveq2d 7367 |
. . . . 5
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ (๐ต + (((๐ถ โ ๐ต) / (๐ด โ ๐ต)) ยท (๐ด โ ๐ต))) = (๐ต + (๐ถ โ ๐ต))) |
28 | 4 | adantr 481 |
. . . . . 6
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ ๐ถ โ โ) |
29 | 23, 28 | pncan3d 11473 |
. . . . 5
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ (๐ต + (๐ถ โ ๐ต)) = ๐ถ) |
30 | 27, 29 | eqtr2d 2778 |
. . . 4
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ ๐ถ = (๐ต + (((๐ถ โ ๐ต) / (๐ด โ ๐ต)) ยท (๐ด โ ๐ต)))) |
31 | | oveq1 7358 |
. . . . . 6
โข (๐ก = ((๐ถ โ ๐ต) / (๐ด โ ๐ต)) โ (๐ก ยท (๐ด โ ๐ต)) = (((๐ถ โ ๐ต) / (๐ด โ ๐ต)) ยท (๐ด โ ๐ต))) |
32 | 31 | oveq2d 7367 |
. . . . 5
โข (๐ก = ((๐ถ โ ๐ต) / (๐ด โ ๐ต)) โ (๐ต + (๐ก ยท (๐ด โ ๐ต))) = (๐ต + (((๐ถ โ ๐ต) / (๐ด โ ๐ต)) ยท (๐ด โ ๐ต)))) |
33 | 32 | rspceeqv 3593 |
. . . 4
โข ((((๐ถ โ ๐ต) / (๐ด โ ๐ต)) โ โ โง ๐ถ = (๐ต + (((๐ถ โ ๐ต) / (๐ด โ ๐ต)) ยท (๐ด โ ๐ต)))) โ โ๐ก โ โ ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) |
34 | 17, 30, 33 | syl2anc 584 |
. . 3
โข ((๐ โง ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) โ โ๐ก โ โ ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) |
35 | 34 | ex 413 |
. 2
โข (๐ โ (((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0 โ โ๐ก โ โ ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต))))) |
36 | 14 | 3ad2ant1 1133 |
. . . 4
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = ((๐ถ โ ๐ต)๐บ(๐ด โ ๐ต))) |
37 | 3 | 3ad2ant1 1133 |
. . . . . . 7
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ๐ต โ โ) |
38 | | simp2 1137 |
. . . . . . . . 9
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ๐ก โ โ) |
39 | 38 | recnd 11141 |
. . . . . . . 8
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ๐ก โ โ) |
40 | 5 | 3ad2ant1 1133 |
. . . . . . . . 9
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ๐ด โ โ) |
41 | 40, 37 | subcld 11470 |
. . . . . . . 8
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ (๐ด โ ๐ต) โ โ) |
42 | 39, 41 | mulcld 11133 |
. . . . . . 7
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ (๐ก ยท (๐ด โ ๐ต)) โ โ) |
43 | | simp3 1138 |
. . . . . . 7
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) |
44 | 37, 42, 43 | mvrladdd 11526 |
. . . . . 6
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ (๐ถ โ ๐ต) = (๐ก ยท (๐ด โ ๐ต))) |
45 | 44 | oveq1d 7366 |
. . . . 5
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ((๐ถ โ ๐ต)๐บ(๐ด โ ๐ต)) = ((๐ก ยท (๐ด โ ๐ต))๐บ(๐ด โ ๐ต))) |
46 | 39, 41 | mulcomd 11134 |
. . . . . 6
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ (๐ก ยท (๐ด โ ๐ต)) = ((๐ด โ ๐ต) ยท ๐ก)) |
47 | 46 | oveq1d 7366 |
. . . . 5
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ((๐ก ยท (๐ด โ ๐ต))๐บ(๐ด โ ๐ต)) = (((๐ด โ ๐ต) ยท ๐ก)๐บ(๐ด โ ๐ต))) |
48 | 45, 47 | eqtrd 2777 |
. . . 4
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ((๐ถ โ ๐ต)๐บ(๐ด โ ๐ต)) = (((๐ด โ ๐ต) ยท ๐ก)๐บ(๐ด โ ๐ต))) |
49 | 41, 39 | mulcld 11133 |
. . . . . 6
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ((๐ด โ ๐ต) ยท ๐ก) โ โ) |
50 | 1 | sigarac 44994 |
. . . . . 6
โข ((((๐ด โ ๐ต) ยท ๐ก) โ โ โง (๐ด โ ๐ต) โ โ) โ (((๐ด โ ๐ต) ยท ๐ก)๐บ(๐ด โ ๐ต)) = -((๐ด โ ๐ต)๐บ((๐ด โ ๐ต) ยท ๐ก))) |
51 | 49, 41, 50 | syl2anc 584 |
. . . . 5
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ (((๐ด โ ๐ต) ยท ๐ก)๐บ(๐ด โ ๐ต)) = -((๐ด โ ๐ต)๐บ((๐ด โ ๐ต) ยท ๐ก))) |
52 | 1 | sigarls 44999 |
. . . . . . . 8
โข (((๐ด โ ๐ต) โ โ โง (๐ด โ ๐ต) โ โ โง ๐ก โ โ) โ ((๐ด โ ๐ต)๐บ((๐ด โ ๐ต) ยท ๐ก)) = (((๐ด โ ๐ต)๐บ(๐ด โ ๐ต)) ยท ๐ก)) |
53 | 41, 41, 38, 52 | syl3anc 1371 |
. . . . . . 7
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ((๐ด โ ๐ต)๐บ((๐ด โ ๐ต) ยท ๐ก)) = (((๐ด โ ๐ต)๐บ(๐ด โ ๐ต)) ยท ๐ก)) |
54 | 1 | sigarid 45000 |
. . . . . . . . 9
โข ((๐ด โ ๐ต) โ โ โ ((๐ด โ ๐ต)๐บ(๐ด โ ๐ต)) = 0) |
55 | 41, 54 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ((๐ด โ ๐ต)๐บ(๐ด โ ๐ต)) = 0) |
56 | 55 | oveq1d 7366 |
. . . . . . 7
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ (((๐ด โ ๐ต)๐บ(๐ด โ ๐ต)) ยท ๐ก) = (0 ยท ๐ก)) |
57 | 39 | mul02d 11311 |
. . . . . . 7
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ (0 ยท ๐ก) = 0) |
58 | 53, 56, 57 | 3eqtrd 2781 |
. . . . . 6
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ((๐ด โ ๐ต)๐บ((๐ด โ ๐ต) ยท ๐ก)) = 0) |
59 | 58 | negeqd 11353 |
. . . . 5
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ -((๐ด โ ๐ต)๐บ((๐ด โ ๐ต) ยท ๐ก)) = -0) |
60 | | neg0 11405 |
. . . . . 6
โข -0 =
0 |
61 | 60 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ -0 = 0) |
62 | 51, 59, 61 | 3eqtrd 2781 |
. . . 4
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ (((๐ด โ ๐ต) ยท ๐ก)๐บ(๐ด โ ๐ต)) = 0) |
63 | 36, 48, 62 | 3eqtrd 2781 |
. . 3
โข ((๐ โง ๐ก โ โ โง ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต)))) โ ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0) |
64 | 63 | rexlimdv3a 3154 |
. 2
โข (๐ โ (โ๐ก โ โ ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต))) โ ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0)) |
65 | 35, 64 | impbid 211 |
1
โข (๐ โ (((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = 0 โ โ๐ก โ โ ๐ถ = (๐ต + (๐ก ยท (๐ด โ ๐ต))))) |