Step | Hyp | Ref
| Expression |
1 | | mulsunif2.1 |
. . 3
โข (๐ โ ๐ฟ <<s ๐
) |
2 | | mulsunif2.2 |
. . 3
โข (๐ โ ๐ <<s ๐) |
3 | | mulsunif2.3 |
. . 3
โข (๐ โ ๐ด = (๐ฟ |s ๐
)) |
4 | | mulsunif2.4 |
. . 3
โข (๐ โ ๐ต = (๐ |s ๐)) |
5 | 1, 2, 3, 4 | mulsunif 28005 |
. 2
โข (๐ โ (๐ด ยทs ๐ต) = (({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) |s ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}))) |
6 | 1 | scutcld 27691 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ฟ |s ๐
) โ No
) |
7 | 3, 6 | eqeltrd 2827 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ No
) |
8 | 2 | scutcld 27691 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ |s ๐) โ No
) |
9 | 4, 8 | eqeltrd 2827 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ No
) |
10 | 7, 9 | mulscld 27990 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด ยทs ๐ต) โ No
) |
11 | 10 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ด ยทs ๐ต) โ No
) |
12 | | ssltss1 27676 |
. . . . . . . . . . . . . . 15
โข (๐ฟ <<s ๐
โ ๐ฟ โ No
) |
13 | 1, 12 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ฟ โ No
) |
14 | 13 | sselda 3977 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ฟ) โ ๐ โ No
) |
15 | 14 | adantrr 714 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ โ No
) |
16 | 9 | adantr 480 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ต โ No
) |
17 | 15, 16 | mulscld 27990 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ ยทs ๐ต) โ No
) |
18 | 7 | adantr 480 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ด โ No
) |
19 | | ssltss1 27676 |
. . . . . . . . . . . . . . . 16
โข (๐ <<s ๐ โ ๐ โ No
) |
20 | 2, 19 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ No
) |
21 | 20 | sselda 3977 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ๐) โ ๐ โ No
) |
22 | 21 | adantrl 713 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ โ No
) |
23 | 18, 22 | mulscld 27990 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ด ยทs ๐) โ No
) |
24 | 15, 22 | mulscld 27990 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ ยทs ๐) โ No
) |
25 | 23, 24 | subscld 27928 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ด ยทs ๐) -s (๐ ยทs ๐)) โ No
) |
26 | 11, 17, 25 | subsubs4d 27956 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (((๐ด ยทs ๐ต) -s (๐ ยทs ๐ต)) -s ((๐ด ยทs ๐) -s (๐ ยทs ๐))) = ((๐ด ยทs ๐ต) -s ((๐ ยทs ๐ต) +s ((๐ด ยทs ๐) -s (๐ ยทs ๐))))) |
27 | 26 | oveq2d 7421 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ด ยทs ๐ต) -s (((๐ด ยทs ๐ต) -s (๐ ยทs ๐ต)) -s ((๐ด ยทs ๐) -s (๐ ยทs ๐)))) = ((๐ด ยทs ๐ต) -s ((๐ด ยทs ๐ต) -s ((๐ ยทs ๐ต) +s ((๐ด ยทs ๐) -s (๐ ยทs ๐)))))) |
28 | 17, 25 | addscld 27852 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ ยทs ๐ต) +s ((๐ด ยทs ๐) -s (๐ ยทs ๐))) โ No
) |
29 | 11, 28 | nncansd 27958 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ด ยทs ๐ต) -s ((๐ด ยทs ๐ต) -s ((๐ ยทs ๐ต) +s ((๐ด ยทs ๐) -s (๐ ยทs ๐))))) = ((๐ ยทs ๐ต) +s ((๐ด ยทs ๐) -s (๐ ยทs ๐)))) |
30 | 27, 29 | eqtrd 2766 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ด ยทs ๐ต) -s (((๐ด ยทs ๐ต) -s (๐ ยทs ๐ต)) -s ((๐ด ยทs ๐) -s (๐ ยทs ๐)))) = ((๐ ยทs ๐ต) +s ((๐ด ยทs ๐) -s (๐ ยทs ๐)))) |
31 | 18, 15 | subscld 27928 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ด -s ๐) โ No
) |
32 | 31, 16, 22 | subsdid 28013 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ด -s ๐) ยทs (๐ต -s ๐)) = (((๐ด -s ๐) ยทs ๐ต) -s ((๐ด -s ๐) ยทs ๐))) |
33 | 18, 15, 16 | subsdird 28014 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ด -s ๐) ยทs ๐ต) = ((๐ด ยทs ๐ต) -s (๐ ยทs ๐ต))) |
34 | 18, 15, 22 | subsdird 28014 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ด -s ๐) ยทs ๐) = ((๐ด ยทs ๐) -s (๐ ยทs ๐))) |
35 | 33, 34 | oveq12d 7423 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (((๐ด -s ๐) ยทs ๐ต) -s ((๐ด -s ๐) ยทs ๐)) = (((๐ด ยทs ๐ต) -s (๐ ยทs ๐ต)) -s ((๐ด ยทs ๐) -s (๐ ยทs ๐)))) |
36 | 32, 35 | eqtrd 2766 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ด -s ๐) ยทs (๐ต -s ๐)) = (((๐ด ยทs ๐ต) -s (๐ ยทs ๐ต)) -s ((๐ด ยทs ๐) -s (๐ ยทs ๐)))) |
37 | 36 | oveq2d 7421 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ด ยทs ๐ต) -s ((๐ด -s ๐) ยทs (๐ต -s ๐))) = ((๐ด ยทs ๐ต) -s (((๐ด ยทs ๐ต) -s (๐ ยทs ๐ต)) -s ((๐ด ยทs ๐) -s (๐ ยทs ๐))))) |
38 | 17, 23, 24 | addsubsassd 27944 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) = ((๐ ยทs ๐ต) +s ((๐ด ยทs ๐) -s (๐ ยทs ๐)))) |
39 | 30, 37, 38 | 3eqtr4rd 2777 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐) ยทs (๐ต -s ๐)))) |
40 | 39 | eqeq2d 2737 |
. . . . . 6
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐) ยทs (๐ต -s ๐))))) |
41 | 40 | 2rexbidva 3211 |
. . . . 5
โข (๐ โ (โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐) ยทs (๐ต -s ๐))))) |
42 | 41 | abbidv 2795 |
. . . 4
โข (๐ โ {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} = {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐) ยทs (๐ต -s ๐)))}) |
43 | 10 | adantr 480 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ด ยทs ๐ต) โ No
) |
44 | | ssltss2 27677 |
. . . . . . . . . . . . . . 15
โข (๐ฟ <<s ๐
โ ๐
โ No
) |
45 | 1, 44 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐
โ No
) |
46 | 45 | sselda 3977 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐
) โ ๐ โ No
) |
47 | 46 | adantrr 714 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ โ No
) |
48 | | ssltss2 27677 |
. . . . . . . . . . . . . . 15
โข (๐ <<s ๐ โ ๐ โ No
) |
49 | 2, 48 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ No
) |
50 | 49 | sselda 3977 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐) โ ๐ โ No
) |
51 | 50 | adantrl 713 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ โ No
) |
52 | 47, 51 | mulscld 27990 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ ยทs ๐ ) โ No
) |
53 | 7 | adantr 480 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ด โ No
) |
54 | 53, 51 | mulscld 27990 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ด ยทs ๐ ) โ No
) |
55 | 52, 54 | subscld 27928 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ ยทs ๐ ) -s (๐ด ยทs ๐ )) โ No
) |
56 | 9 | adantr 480 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ต โ No
) |
57 | 47, 56 | mulscld 27990 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ ยทs ๐ต) โ No
) |
58 | 57, 43 | subscld 27928 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต)) โ No
) |
59 | 43, 55, 58 | subsubs2d 27957 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ด ยทs ๐ต) -s (((๐ ยทs ๐ ) -s (๐ด ยทs ๐ )) -s ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต)))) = ((๐ด ยทs ๐ต) +s (((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต)) -s ((๐ ยทs ๐ ) -s (๐ด ยทs ๐ ))))) |
60 | 43, 58, 55 | addsubsassd 27944 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ด ยทs ๐ต) +s ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต))) -s ((๐ ยทs ๐ ) -s (๐ด ยทs ๐ ))) = ((๐ด ยทs ๐ต) +s (((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต)) -s ((๐ ยทs ๐ ) -s (๐ด ยทs ๐ ))))) |
61 | | pncan3s 27936 |
. . . . . . . . . . 11
โข (((๐ด ยทs ๐ต) โ
No โง (๐
ยทs ๐ต)
โ No ) โ ((๐ด ยทs ๐ต) +s ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต))) = (๐ ยทs ๐ต)) |
62 | 43, 57, 61 | syl2anc 583 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ด ยทs ๐ต) +s ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต))) = (๐ ยทs ๐ต)) |
63 | 62 | oveq1d 7420 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ด ยทs ๐ต) +s ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต))) -s ((๐ ยทs ๐ ) -s (๐ด ยทs ๐ ))) = ((๐ ยทs ๐ต) -s ((๐ ยทs ๐ ) -s (๐ด ยทs ๐ )))) |
64 | 59, 60, 63 | 3eqtr2d 2772 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ด ยทs ๐ต) -s (((๐ ยทs ๐ ) -s (๐ด ยทs ๐ )) -s ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต)))) = ((๐ ยทs ๐ต) -s ((๐ ยทs ๐ ) -s (๐ด ยทs ๐ )))) |
65 | 47, 53 | subscld 27928 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ -s ๐ด) โ No
) |
66 | 65, 51, 56 | subsdid 28013 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ -s ๐ด) ยทs (๐ -s ๐ต)) = (((๐ -s ๐ด) ยทs ๐ ) -s ((๐ -s ๐ด) ยทs ๐ต))) |
67 | 47, 53, 51 | subsdird 28014 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ -s ๐ด) ยทs ๐ ) = ((๐ ยทs ๐ ) -s (๐ด ยทs ๐ ))) |
68 | 47, 53, 56 | subsdird 28014 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ -s ๐ด) ยทs ๐ต) = ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต))) |
69 | 67, 68 | oveq12d 7423 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ -s ๐ด) ยทs ๐ ) -s ((๐ -s ๐ด) ยทs ๐ต)) = (((๐ ยทs ๐ ) -s (๐ด ยทs ๐ )) -s ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต)))) |
70 | 66, 69 | eqtrd 2766 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ -s ๐ด) ยทs (๐ -s ๐ต)) = (((๐ ยทs ๐ ) -s (๐ด ยทs ๐ )) -s ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต)))) |
71 | 70 | oveq2d 7421 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ด ยทs ๐ต) -s ((๐ -s ๐ด) ยทs (๐ -s ๐ต))) = ((๐ด ยทs ๐ต) -s (((๐ ยทs ๐ ) -s (๐ด ยทs ๐ )) -s ((๐ ยทs ๐ต) -s (๐ด ยทs ๐ต))))) |
72 | 57, 54, 52 | addsubsassd 27944 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) = ((๐ ยทs ๐ต) +s ((๐ด ยทs ๐ ) -s (๐ ยทs ๐ )))) |
73 | 57, 52, 54 | subsubs2d 27957 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ ยทs ๐ต) -s ((๐ ยทs ๐ ) -s (๐ด ยทs ๐ ))) = ((๐ ยทs ๐ต) +s ((๐ด ยทs ๐ ) -s (๐ ยทs ๐ )))) |
74 | 72, 73 | eqtr4d 2769 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) = ((๐ ยทs ๐ต) -s ((๐ ยทs ๐ ) -s (๐ด ยทs ๐ )))) |
75 | 64, 71, 74 | 3eqtr4rd 2777 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) = ((๐ด ยทs ๐ต) -s ((๐ -s ๐ด) ยทs (๐ -s ๐ต)))) |
76 | 75 | eqeq2d 2737 |
. . . . . 6
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ ๐ = ((๐ด ยทs ๐ต) -s ((๐ -s ๐ด) ยทs (๐ -s ๐ต))))) |
77 | 76 | 2rexbidva 3211 |
. . . . 5
โข (๐ โ (โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ โ๐ โ ๐
โ๐ โ ๐ ๐ = ((๐ด ยทs ๐ต) -s ((๐ -s ๐ด) ยทs (๐ -s ๐ต))))) |
78 | 77 | abbidv 2795 |
. . . 4
โข (๐ โ {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} = {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = ((๐ด ยทs ๐ต) -s ((๐ -s ๐ด) ยทs (๐ -s ๐ต)))}) |
79 | 42, 78 | uneq12d 4159 |
. . 3
โข (๐ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) = ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐) ยทs (๐ต -s ๐)))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = ((๐ด ยทs ๐ต) -s ((๐ -s ๐ด) ยทs (๐ -s ๐ต)))})) |
80 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ๐ด โ No
) |
81 | 49 | sselda 3977 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ข โ ๐) โ ๐ข โ No
) |
82 | 81 | adantrl 713 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ๐ข โ No
) |
83 | 80, 82 | mulscld 27990 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (๐ด ยทs ๐ข) โ No
) |
84 | 10 | adantr 480 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (๐ด ยทs ๐ต) โ No
) |
85 | 83, 84 | subscld 27928 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต)) โ No
) |
86 | 13 | sselda 3977 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ก โ ๐ฟ) โ ๐ก โ No
) |
87 | 86 | adantrr 714 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ๐ก โ No
) |
88 | 87, 82 | mulscld 27990 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (๐ก ยทs ๐ข) โ No
) |
89 | 9 | adantr 480 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ๐ต โ No
) |
90 | 87, 89 | mulscld 27990 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (๐ก ยทs ๐ต) โ No
) |
91 | 85, 88, 90 | subsubs2d 27957 |
. . . . . . . . . . 11
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต)) -s ((๐ก ยทs ๐ข) -s (๐ก ยทs ๐ต))) = (((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต)) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข)))) |
92 | 90, 88 | subscld 27928 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข)) โ No
) |
93 | 83, 92, 84 | addsubsd 27945 |
. . . . . . . . . . 11
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข))) -s (๐ด ยทs ๐ต)) = (((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต)) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข)))) |
94 | 91, 93 | eqtr4d 2769 |
. . . . . . . . . 10
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต)) -s ((๐ก ยทs ๐ข) -s (๐ก ยทs ๐ต))) = (((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข))) -s (๐ด ยทs ๐ต))) |
95 | 94 | oveq2d 7421 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ด ยทs ๐ต) +s (((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต)) -s ((๐ก ยทs ๐ข) -s (๐ก ยทs ๐ต)))) = ((๐ด ยทs ๐ต) +s (((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข))) -s (๐ด ยทs ๐ต)))) |
96 | 83, 92 | addscld 27852 |
. . . . . . . . . 10
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข))) โ No
) |
97 | | pncan3s 27936 |
. . . . . . . . . 10
โข (((๐ด ยทs ๐ต) โ
No โง ((๐ด
ยทs ๐ข)
+s ((๐ก
ยทs ๐ต)
-s (๐ก
ยทs ๐ข)))
โ No ) โ ((๐ด ยทs ๐ต) +s (((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข))) -s (๐ด ยทs ๐ต))) = ((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข)))) |
98 | 84, 96, 97 | syl2anc 583 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ด ยทs ๐ต) +s (((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข))) -s (๐ด ยทs ๐ต))) = ((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข)))) |
99 | 95, 98 | eqtrd 2766 |
. . . . . . . 8
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ด ยทs ๐ต) +s (((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต)) -s ((๐ก ยทs ๐ข) -s (๐ก ยทs ๐ต)))) = ((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข)))) |
100 | 82, 89 | subscld 27928 |
. . . . . . . . . . 11
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (๐ข -s ๐ต) โ No
) |
101 | 80, 87, 100 | subsdird 28014 |
. . . . . . . . . 10
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)) = ((๐ด ยทs (๐ข -s ๐ต)) -s (๐ก ยทs (๐ข -s ๐ต)))) |
102 | 80, 82, 89 | subsdid 28013 |
. . . . . . . . . . 11
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (๐ด ยทs (๐ข -s ๐ต)) = ((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต))) |
103 | 87, 82, 89 | subsdid 28013 |
. . . . . . . . . . 11
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (๐ก ยทs (๐ข -s ๐ต)) = ((๐ก ยทs ๐ข) -s (๐ก ยทs ๐ต))) |
104 | 102, 103 | oveq12d 7423 |
. . . . . . . . . 10
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ด ยทs (๐ข -s ๐ต)) -s (๐ก ยทs (๐ข -s ๐ต))) = (((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต)) -s ((๐ก ยทs ๐ข) -s (๐ก ยทs ๐ต)))) |
105 | 101, 104 | eqtrd 2766 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)) = (((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต)) -s ((๐ก ยทs ๐ข) -s (๐ก ยทs ๐ต)))) |
106 | 105 | oveq2d 7421 |
. . . . . . . 8
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))) = ((๐ด ยทs ๐ต) +s (((๐ด ยทs ๐ข) -s (๐ด ยทs ๐ต)) -s ((๐ก ยทs ๐ข) -s (๐ก ยทs ๐ต))))) |
107 | 90, 83 | addscomd 27839 |
. . . . . . . . . 10
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ ((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) = ((๐ด ยทs ๐ข) +s (๐ก ยทs ๐ต))) |
108 | 107 | oveq1d 7420 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) = (((๐ด ยทs ๐ข) +s (๐ก ยทs ๐ต)) -s (๐ก ยทs ๐ข))) |
109 | 83, 90, 88 | addsubsassd 27944 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (((๐ด ยทs ๐ข) +s (๐ก ยทs ๐ต)) -s (๐ก ยทs ๐ข)) = ((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข)))) |
110 | 108, 109 | eqtrd 2766 |
. . . . . . . 8
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) = ((๐ด ยทs ๐ข) +s ((๐ก ยทs ๐ต) -s (๐ก ยทs ๐ข)))) |
111 | 99, 106, 110 | 3eqtr4rd 2777 |
. . . . . . 7
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))) |
112 | 111 | eqeq2d 2737 |
. . . . . 6
โข ((๐ โง (๐ก โ ๐ฟ โง ๐ข โ ๐)) โ (๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ๐ = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))))) |
113 | 112 | 2rexbidva 3211 |
. . . . 5
โข (๐ โ (โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))))) |
114 | 113 | abbidv 2795 |
. . . 4
โข (๐ โ {๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} = {๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))}) |
115 | 45 | sselda 3977 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฃ โ ๐
) โ ๐ฃ โ No
) |
116 | 115 | adantrr 714 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ๐ฃ โ No
) |
117 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ๐ต โ No
) |
118 | 116, 117 | mulscld 27990 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (๐ฃ ยทs ๐ต) โ No
) |
119 | 20 | sselda 3977 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ค โ ๐) โ ๐ค โ No
) |
120 | 119 | adantrl 713 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ๐ค โ No
) |
121 | 116, 120 | mulscld 27990 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (๐ฃ ยทs ๐ค) โ No
) |
122 | 118, 121 | subscld 27928 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) โ No
) |
123 | 10 | adantr 480 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (๐ด ยทs ๐ต) โ No
) |
124 | 7 | adantr 480 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ๐ด โ No
) |
125 | 124, 120 | mulscld 27990 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (๐ด ยทs ๐ค) โ No
) |
126 | 122, 123,
125 | subsubs2d 27957 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) -s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ค))) = (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s ((๐ด ยทs ๐ค) -s (๐ด ยทs ๐ต)))) |
127 | 122, 125,
123 | addsubsassd 27944 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ((((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s (๐ด ยทs ๐ค)) -s (๐ด ยทs ๐ต)) = (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s ((๐ด ยทs ๐ค) -s (๐ด ยทs ๐ต)))) |
128 | 126, 127 | eqtr4d 2769 |
. . . . . . . . . 10
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) -s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ค))) = ((((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s (๐ด ยทs ๐ค)) -s (๐ด ยทs ๐ต))) |
129 | 128 | oveq2d 7421 |
. . . . . . . . 9
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ((๐ด ยทs ๐ต) +s (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) -s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ค)))) = ((๐ด ยทs ๐ต) +s ((((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s (๐ด ยทs ๐ค)) -s (๐ด ยทs ๐ต)))) |
130 | 122, 125 | addscld 27852 |
. . . . . . . . . 10
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s (๐ด ยทs ๐ค)) โ No
) |
131 | | pncan3s 27936 |
. . . . . . . . . 10
โข (((๐ด ยทs ๐ต) โ
No โง (((๐ฃ
ยทs ๐ต)
-s (๐ฃ
ยทs ๐ค))
+s (๐ด
ยทs ๐ค))
โ No ) โ ((๐ด ยทs ๐ต) +s ((((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s (๐ด ยทs ๐ค)) -s (๐ด ยทs ๐ต))) = (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s (๐ด ยทs ๐ค))) |
132 | 123, 130,
131 | syl2anc 583 |
. . . . . . . . 9
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ((๐ด ยทs ๐ต) +s ((((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s (๐ด ยทs ๐ค)) -s (๐ด ยทs ๐ต))) = (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s (๐ด ยทs ๐ค))) |
133 | 129, 132 | eqtrd 2766 |
. . . . . . . 8
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ((๐ด ยทs ๐ต) +s (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) -s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ค)))) = (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s (๐ด ยทs ๐ค))) |
134 | 117, 120 | subscld 27928 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (๐ต -s ๐ค) โ No
) |
135 | 116, 124,
134 | subsdird 28014 |
. . . . . . . . . 10
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ((๐ฃ -s ๐ด) ยทs (๐ต -s ๐ค)) = ((๐ฃ ยทs (๐ต -s ๐ค)) -s (๐ด ยทs (๐ต -s ๐ค)))) |
136 | 116, 117,
120 | subsdid 28013 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (๐ฃ ยทs (๐ต -s ๐ค)) = ((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค))) |
137 | 124, 117,
120 | subsdid 28013 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (๐ด ยทs (๐ต -s ๐ค)) = ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ค))) |
138 | 136, 137 | oveq12d 7423 |
. . . . . . . . . 10
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ((๐ฃ ยทs (๐ต -s ๐ค)) -s (๐ด ยทs (๐ต -s ๐ค))) = (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) -s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ค)))) |
139 | 135, 138 | eqtrd 2766 |
. . . . . . . . 9
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ((๐ฃ -s ๐ด) ยทs (๐ต -s ๐ค)) = (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) -s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ค)))) |
140 | 139 | oveq2d 7421 |
. . . . . . . 8
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ ((๐ด ยทs ๐ต) +s ((๐ฃ -s ๐ด) ยทs (๐ต -s ๐ค))) = ((๐ด ยทs ๐ต) +s (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) -s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ค))))) |
141 | 118, 125,
121 | addsubsd 27945 |
. . . . . . . 8
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) = (((๐ฃ ยทs ๐ต) -s (๐ฃ ยทs ๐ค)) +s (๐ด ยทs ๐ค))) |
142 | 133, 140,
141 | 3eqtr4rd 2777 |
. . . . . . 7
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) = ((๐ด ยทs ๐ต) +s ((๐ฃ -s ๐ด) ยทs (๐ต -s ๐ค)))) |
143 | 142 | eqeq2d 2737 |
. . . . . 6
โข ((๐ โง (๐ฃ โ ๐
โง ๐ค โ ๐)) โ (๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ๐ = ((๐ด ยทs ๐ต) +s ((๐ฃ -s ๐ด) ยทs (๐ต -s ๐ค))))) |
144 | 143 | 2rexbidva 3211 |
. . . . 5
โข (๐ โ (โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = ((๐ด ยทs ๐ต) +s ((๐ฃ -s ๐ด) ยทs (๐ต -s ๐ค))))) |
145 | 144 | abbidv 2795 |
. . . 4
โข (๐ โ {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))} = {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = ((๐ด ยทs ๐ต) +s ((๐ฃ -s ๐ด) ยทs (๐ต -s ๐ค)))}) |
146 | 114, 145 | uneq12d 4159 |
. . 3
โข (๐ โ ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) = ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))} โช {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = ((๐ด ยทs ๐ต) +s ((๐ฃ -s ๐ด) ยทs (๐ต -s ๐ค)))})) |
147 | 79, 146 | oveq12d 7423 |
. 2
โข (๐ โ (({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) |s ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) = (({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐) ยทs (๐ต -s ๐)))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = ((๐ด ยทs ๐ต) -s ((๐ -s ๐ด) ยทs (๐ -s ๐ต)))}) |s ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))} โช {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = ((๐ด ยทs ๐ต) +s ((๐ฃ -s ๐ด) ยทs (๐ต -s ๐ค)))}))) |
148 | 5, 147 | eqtrd 2766 |
1
โข (๐ โ (๐ด ยทs ๐ต) = (({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐) ยทs (๐ต -s ๐)))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = ((๐ด ยทs ๐ต) -s ((๐ -s ๐ด) ยทs (๐ -s ๐ต)))}) |s ({๐ โฃ โ๐ก โ ๐ฟ โ๐ข โ ๐ ๐ = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))} โช {๐ โฃ โ๐ฃ โ ๐
โ๐ค โ ๐ ๐ = ((๐ด ยทs ๐ต) +s ((๐ฃ -s ๐ด) ยทs (๐ต -s ๐ค)))}))) |