Step | Hyp | Ref
| Expression |
1 | | mulscl 27974 |
. . . . 5
โข ((๐ด โ
No โง ๐ต โ
No ) โ (๐ด ยทs ๐ต) โ No
) |
2 | 1 | adantr 480 |
. . . 4
โข (((๐ด โ
No โง ๐ต โ
No ) โง ((โ๐ โ โs (( -us
โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}))
โง (โ๐ โ
โs (( -us โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}))))
โ (๐ด
ยทs ๐ต)
โ No ) |
3 | | remulscllem2 28169 |
. . . . . . 7
โข (((๐ด โ
No โง ๐ต โ
No ) โง ((๐ โ โs โง ๐ โ โs)
โง ((( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)))) โ โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐)) |
4 | 3 | expr 456 |
. . . . . 6
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ โ โs โง ๐ โ โs))
โ (((( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)) โ โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐))) |
5 | 4 | rexlimdvva 3203 |
. . . . 5
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ โ โs โ๐ โ โs (((
-us โ๐)
<s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)) โ โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐))) |
6 | | simpl 482 |
. . . . . . 7
โข
((โ๐ โ
โs (( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}))
โ โ๐ โ
โs (( -us โ๐) <s ๐ด โง ๐ด <s ๐)) |
7 | | simpl 482 |
. . . . . . 7
โข
((โ๐ โ
โs (( -us โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}))
โ โ๐ โ
โs (( -us โ๐) <s ๐ต โง ๐ต <s ๐)) |
8 | 6, 7 | anim12i 612 |
. . . . . 6
โข
(((โ๐ โ
โs (( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}))
โง (โ๐ โ
โs (( -us โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))
โ (โ๐ โ
โs (( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง โ๐ โ โs (( -us
โ๐) <s ๐ต โง ๐ต <s ๐))) |
9 | | reeanv 3218 |
. . . . . 6
โข
(โ๐ โ
โs โ๐ โ โs (((
-us โ๐)
<s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐)) โ (โ๐ โ โs (( -us
โ๐) <s ๐ด โง ๐ด <s ๐) โง โ๐ โ โs (( -us
โ๐) <s ๐ต โง ๐ต <s ๐))) |
10 | 8, 9 | sylibr 233 |
. . . . 5
โข
(((โ๐ โ
โs (( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}))
โง (โ๐ โ
โs (( -us โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))
โ โ๐ โ
โs โ๐ โ โs (((
-us โ๐)
<s ๐ด โง ๐ด <s ๐) โง (( -us โ๐) <s ๐ต โง ๐ต <s ๐))) |
11 | 5, 10 | impel 505 |
. . . 4
โข (((๐ด โ
No โง ๐ต โ
No ) โง ((โ๐ โ โs (( -us
โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}))
โง (โ๐ โ
โs (( -us โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}))))
โ โ๐ โ
โs (( -us โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐)) |
12 | | simpr 484 |
. . . . . 6
โข
((โ๐ โ
โs (( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}))
โ ๐ด = ({๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})) |
13 | | simpr 484 |
. . . . . 6
โข
((โ๐ โ
โs (( -us โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}))
โ ๐ต = ({๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})) |
14 | 12, 13 | anim12i 612 |
. . . . 5
โข
(((โ๐ โ
โs (( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}))
โง (โ๐ โ
โs (( -us โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))
โ (๐ด = ({๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})
โง ๐ต = ({๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}))) |
15 | | recut 28164 |
. . . . . . . . 9
โข (๐ด โ
No โ {๐ฅ
โฃ โ๐ โ
โs ๐ฅ =
(๐ด -s (
1s /su ๐))} <<s {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}) |
16 | 15 | adantr 480 |
. . . . . . . 8
โข ((๐ด โ
No โง ๐ต โ
No ) โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}
<<s {๐ฅ โฃ
โ๐ โ
โs ๐ฅ =
(๐ด +s (
1s /su ๐))}) |
17 | 16 | adantr 480 |
. . . . . . 7
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})
โง ๐ต = ({๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))
โ {๐ฅ โฃ
โ๐ โ
โs ๐ฅ =
(๐ด -s (
1s /su ๐))} <<s {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}) |
18 | | recut 28164 |
. . . . . . . 8
โข (๐ต โ
No โ {๐ฆ
โฃ โ๐ โ
โs ๐ฆ =
(๐ต -s (
1s /su ๐))} <<s {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}) |
19 | 18 | ad2antlr 724 |
. . . . . . 7
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})
โง ๐ต = ({๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))
โ {๐ฆ โฃ
โ๐ โ
โs ๐ฆ =
(๐ต -s (
1s /su ๐))} <<s {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}) |
20 | | simprl 768 |
. . . . . . 7
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})
โง ๐ต = ({๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))
โ ๐ด = ({๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})) |
21 | | simprr 770 |
. . . . . . 7
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})
โง ๐ต = ({๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))
โ ๐ต = ({๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})) |
22 | 17, 19, 20, 21 | mulsunif2 28010 |
. . . . . 6
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})
โง ๐ต = ({๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))
โ (๐ด
ยทs ๐ต) =
(({๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))} โช {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))}) |s ({๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))} โช {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))}))) |
23 | | r19.41v 3180 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
โs (๐ก =
(๐ด -s (
1s /su ๐)) โง โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))) โ (โ๐ โ โs ๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข))))) |
24 | 23 | exbii 1842 |
. . . . . . . . . . . . 13
โข
(โ๐กโ๐ โ โs (๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))) โ โ๐ก(โ๐ โ โs ๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข))))) |
25 | | rexcom4 3277 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
โs โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))) โ โ๐กโ๐ โ โs (๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข))))) |
26 | | eqeq1 2728 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ก โ (๐ฅ = (๐ด -s ( 1s
/su ๐))
โ ๐ก = (๐ด -s ( 1s
/su ๐)))) |
27 | 26 | rexbidv 3170 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ก โ (โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))
โ โ๐ โ
โs ๐ก =
(๐ด -s (
1s /su ๐)))) |
28 | 27 | rexab 3683 |
. . . . . . . . . . . . 13
โข
(โ๐ก โ
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข))) โ โ๐ก(โ๐ โ โs ๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข))))) |
29 | 24, 25, 28 | 3bitr4ri 304 |
. . . . . . . . . . . 12
โข
(โ๐ก โ
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข))) โ โ๐ โ โs โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข))))) |
30 | | ovex 7435 |
. . . . . . . . . . . . . . . . 17
โข (๐ด -s ( 1s
/su ๐))
โ V |
31 | | oveq2 7410 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ก = (๐ด -s ( 1s
/su ๐))
โ (๐ด -s
๐ก) = (๐ด -s (๐ด -s ( 1s
/su ๐)))) |
32 | 31 | oveq1d 7417 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ก = (๐ด -s ( 1s
/su ๐))
โ ((๐ด -s
๐ก) ยทs
(๐ต -s ๐ข)) = ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))) |
33 | 32 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ก = (๐ด -s ( 1s
/su ๐))
โ ((๐ด
ยทs ๐ต)
-s ((๐ด
-s ๐ก)
ยทs (๐ต
-s ๐ข))) =
((๐ด ยทs
๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข)))) |
34 | 33 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . 18
โข (๐ก = (๐ด -s ( 1s
/su ๐))
โ (๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข))) โ ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))))) |
35 | 34 | rexbidv 3170 |
. . . . . . . . . . . . . . . . 17
โข (๐ก = (๐ด -s ( 1s
/su ๐))
โ (โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข))) โ โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))))) |
36 | 30, 35 | ceqsexv 3518 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))) โ โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข)))) |
37 | | r19.41v 3180 |
. . . . . . . . . . . . . . . . . 18
โข
(โ๐ โ
โs (๐ข =
(๐ต -s (
1s /su ๐)) โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข)))) โ
(โ๐ โ
โs ๐ข =
(๐ต -s (
1s /su ๐)) โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))))) |
38 | 37 | exbii 1842 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ขโ๐ โ โs (๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข)))) โ
โ๐ข(โ๐ โ โs
๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))))) |
39 | | rexcom4 3277 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ โ
โs โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข)))) โ
โ๐ขโ๐ โ โs
(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))))) |
40 | | eqeq1 2728 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ = ๐ข โ (๐ฆ = (๐ต -s ( 1s
/su ๐))
โ ๐ข = (๐ต -s ( 1s
/su ๐)))) |
41 | 40 | rexbidv 3170 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ = ๐ข โ (โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))
โ โ๐ โ
โs ๐ข =
(๐ต -s (
1s /su ๐)))) |
42 | 41 | rexab 3683 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))) โ
โ๐ข(โ๐ โ โs
๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))))) |
43 | 38, 39, 42 | 3bitr4ri 304 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))) โ
โ๐ โ
โs โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))))) |
44 | 36, 43 | bitri 275 |
. . . . . . . . . . . . . . 15
โข
(โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))) โ โ๐ โ โs โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))))) |
45 | | ovex 7435 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต -s ( 1s
/su ๐))
โ V |
46 | | oveq2 7410 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ข = (๐ต -s ( 1s
/su ๐))
โ (๐ต -s
๐ข) = (๐ต -s (๐ต -s ( 1s
/su ๐)))) |
47 | 46 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ข = (๐ต -s ( 1s
/su ๐))
โ ((๐ด -s
(๐ด -s (
1s /su ๐))) ยทs (๐ต -s ๐ข)) = ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s (๐ต
-s ( 1s /su ๐))))) |
48 | 47 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ข = (๐ต -s ( 1s
/su ๐))
โ ((๐ด
ยทs ๐ต)
-s ((๐ด
-s (๐ด
-s ( 1s /su ๐))) ยทs (๐ต -s ๐ข))) = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s (๐ต
-s ( 1s /su ๐)))))) |
49 | 48 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . 18
โข (๐ข = (๐ต -s ( 1s
/su ๐))
โ (๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข))) โ
๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s (๐ต
-s ( 1s /su ๐))))))) |
50 | 45, 49 | ceqsexv 3518 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข)))) โ
๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s (๐ต
-s ( 1s /su ๐)))))) |
51 | | simplll 772 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ๐ด โ No ) |
52 | | 1sno 27700 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
1s โ No |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ 1s โ No ) |
54 | | nnsno 28136 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โs
โ ๐ โ No ) |
55 | 54 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ๐ โ No ) |
56 | | nnne0s 28145 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โs
โ ๐ โ 0s
) |
57 | 56 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ๐ โ 0s
) |
58 | 53, 55, 57 | divscld 28062 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ( 1s /su ๐) โ No
) |
59 | 51, 58 | nncansd 27943 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (๐ด -s
(๐ด -s (
1s /su ๐))) = ( 1s /su
๐)) |
60 | | simpllr 773 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ๐ต โ No ) |
61 | | nnsno 28136 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โs
โ ๐ โ No ) |
62 | 61 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ๐ โ No ) |
63 | | nnne0s 28145 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โs
โ ๐ โ 0s
) |
64 | 63 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ๐ โ 0s
) |
65 | 53, 62, 64 | divscld 28062 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ( 1s /su ๐) โ No
) |
66 | 60, 65 | nncansd 27943 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (๐ต -s
(๐ต -s (
1s /su ๐))) = ( 1s /su
๐)) |
67 | 59, 66 | oveq12d 7420 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ((๐ด -s
(๐ด -s (
1s /su ๐))) ยทs (๐ต -s (๐ต -s ( 1s
/su ๐)))) =
(( 1s /su ๐) ยทs ( 1s
/su ๐))) |
68 | 67 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ((๐ด
ยทs ๐ต)
-s ((๐ด
-s (๐ด
-s ( 1s /su ๐))) ยทs (๐ต -s (๐ต -s ( 1s
/su ๐))))) =
((๐ด ยทs
๐ต) -s ((
1s /su ๐) ยทs ( 1s
/su ๐)))) |
69 | 68 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s (๐ต
-s ( 1s /su ๐))))) โ ๐ง = ((๐ด ยทs ๐ต) -s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
70 | 50, 69 | bitrid 283 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข)))) โ
๐ง = ((๐ด ยทs ๐ต) -s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
71 | 70 | rexbidva 3168 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โ
(โ๐ โ
โs โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ต
-s ๐ข)))) โ
โ๐ โ
โs ๐ง =
((๐ด ยทs
๐ต) -s ((
1s /su ๐) ยทs ( 1s
/su ๐))))) |
72 | 44, 71 | bitrid 283 |
. . . . . . . . . . . . . 14
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โ
(โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
73 | 72 | rexbidva 3168 |
. . . . . . . . . . . . 13
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ โ โs โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))) โ โ๐ โ โs โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) -s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
74 | | remulscllem1 28168 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
โs โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s (( 1s
/su ๐)
ยทs ( 1s /su ๐))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))) |
75 | 73, 74 | bitrdi 287 |
. . . . . . . . . . . 12
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ โ โs โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐)))) |
76 | 29, 75 | bitrid 283 |
. . . . . . . . . . 11
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐)))) |
77 | 76 | abbidv 2793 |
. . . . . . . . . 10
โข ((๐ด โ
No โง ๐ต โ
No ) โ {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))} = {๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))}) |
78 | | r19.41v 3180 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
โs (๐ก =
(๐ด +s (
1s /su ๐)) โง โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))) โ (โ๐ โ โs ๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต))))) |
79 | 78 | exbii 1842 |
. . . . . . . . . . . . 13
โข
(โ๐กโ๐ โ โs (๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))) โ โ๐ก(โ๐ โ โs ๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต))))) |
80 | | rexcom4 3277 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
โs โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))) โ โ๐กโ๐ โ โs (๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต))))) |
81 | | eqeq1 2728 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ก โ (๐ฅ = (๐ด +s ( 1s
/su ๐))
โ ๐ก = (๐ด +s ( 1s
/su ๐)))) |
82 | 81 | rexbidv 3170 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ก โ (โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))
โ โ๐ โ
โs ๐ก =
(๐ด +s (
1s /su ๐)))) |
83 | 82 | rexab 3683 |
. . . . . . . . . . . . 13
โข
(โ๐ก โ
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต))) โ โ๐ก(โ๐ โ โs ๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต))))) |
84 | 79, 80, 83 | 3bitr4ri 304 |
. . . . . . . . . . . 12
โข
(โ๐ก โ
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต))) โ โ๐ โ โs โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต))))) |
85 | | ovex 7435 |
. . . . . . . . . . . . . . . . 17
โข (๐ด +s ( 1s
/su ๐))
โ V |
86 | | oveq1 7409 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ก = (๐ด +s ( 1s
/su ๐))
โ (๐ก -s
๐ด) = ((๐ด +s ( 1s
/su ๐))
-s ๐ด)) |
87 | 86 | oveq1d 7417 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ก = (๐ด +s ( 1s
/su ๐))
โ ((๐ก -s
๐ด) ยทs
(๐ข -s ๐ต)) = (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))) |
88 | 87 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ก = (๐ด +s ( 1s
/su ๐))
โ ((๐ด
ยทs ๐ต)
-s ((๐ก
-s ๐ด)
ยทs (๐ข
-s ๐ต))) =
((๐ด ยทs
๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต)))) |
89 | 88 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . 18
โข (๐ก = (๐ด +s ( 1s
/su ๐))
โ (๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต))) โ ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))))) |
90 | 89 | rexbidv 3170 |
. . . . . . . . . . . . . . . . 17
โข (๐ก = (๐ด +s ( 1s
/su ๐))
โ (โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต))) โ โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))))) |
91 | 85, 90 | ceqsexv 3518 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))) โ โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต)))) |
92 | | r19.41v 3180 |
. . . . . . . . . . . . . . . . . 18
โข
(โ๐ โ
โs (๐ข =
(๐ต +s (
1s /su ๐)) โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต)))) โ
(โ๐ โ
โs ๐ข =
(๐ต +s (
1s /su ๐)) โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))))) |
93 | 92 | exbii 1842 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ขโ๐ โ โs (๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต)))) โ
โ๐ข(โ๐ โ โs
๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))))) |
94 | | rexcom4 3277 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ โ
โs โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต)))) โ
โ๐ขโ๐ โ โs
(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))))) |
95 | | eqeq1 2728 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ = ๐ข โ (๐ฆ = (๐ต +s ( 1s
/su ๐))
โ ๐ข = (๐ต +s ( 1s
/su ๐)))) |
96 | 95 | rexbidv 3170 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ = ๐ข โ (โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))
โ โ๐ โ
โs ๐ข =
(๐ต +s (
1s /su ๐)))) |
97 | 96 | rexab 3683 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))) โ
โ๐ข(โ๐ โ โs
๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))))) |
98 | 93, 94, 97 | 3bitr4ri 304 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))) โ
โ๐ โ
โs โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))))) |
99 | 91, 98 | bitri 275 |
. . . . . . . . . . . . . . 15
โข
(โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))) โ โ๐ โ โs โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))))) |
100 | | ovex 7435 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต +s ( 1s
/su ๐))
โ V |
101 | | oveq1 7409 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ข = (๐ต +s ( 1s
/su ๐))
โ (๐ข -s
๐ต) = ((๐ต +s ( 1s
/su ๐))
-s ๐ต)) |
102 | 101 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ข = (๐ต +s ( 1s
/su ๐))
โ (((๐ด +s (
1s /su ๐)) -s ๐ด) ยทs (๐ข -s ๐ต)) = (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs ((๐ต
+s ( 1s /su ๐)) -s ๐ต))) |
103 | 102 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ข = (๐ต +s ( 1s
/su ๐))
โ ((๐ด
ยทs ๐ต)
-s (((๐ด
+s ( 1s /su ๐)) -s ๐ด) ยทs (๐ข -s ๐ต))) = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs ((๐ต
+s ( 1s /su ๐)) -s ๐ต)))) |
104 | 103 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . 18
โข (๐ข = (๐ต +s ( 1s
/su ๐))
โ (๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต))) โ
๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs ((๐ต
+s ( 1s /su ๐)) -s ๐ต))))) |
105 | 100, 104 | ceqsexv 3518 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต)))) โ
๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs ((๐ต
+s ( 1s /su ๐)) -s ๐ต)))) |
106 | | pncan2s 27922 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ
No โง ( 1s /su ๐) โ No )
โ ((๐ด +s (
1s /su ๐)) -s ๐ด) = ( 1s /su ๐)) |
107 | 51, 58, 106 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ((๐ด +s (
1s /su ๐)) -s ๐ด) = ( 1s /su ๐)) |
108 | | pncan2s 27922 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ต โ
No โง ( 1s /su ๐) โ No )
โ ((๐ต +s (
1s /su ๐)) -s ๐ต) = ( 1s /su ๐)) |
109 | 60, 65, 108 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ((๐ต +s (
1s /su ๐)) -s ๐ต) = ( 1s /su ๐)) |
110 | 107, 109 | oveq12d 7420 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (((๐ด +s (
1s /su ๐)) -s ๐ด) ยทs ((๐ต +s ( 1s
/su ๐))
-s ๐ต)) = ((
1s /su ๐) ยทs ( 1s
/su ๐))) |
111 | 110 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ((๐ด
ยทs ๐ต)
-s (((๐ด
+s ( 1s /su ๐)) -s ๐ด) ยทs ((๐ต +s ( 1s
/su ๐))
-s ๐ต))) =
((๐ด ยทs
๐ต) -s ((
1s /su ๐) ยทs ( 1s
/su ๐)))) |
112 | 111 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs ((๐ต
+s ( 1s /su ๐)) -s ๐ต))) โ ๐ง = ((๐ด ยทs ๐ต) -s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
113 | 105, 112 | bitrid 283 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต)))) โ
๐ง = ((๐ด ยทs ๐ต) -s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
114 | 113 | rexbidva 3168 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โ
(โ๐ โ
โs โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ข
-s ๐ต)))) โ
โ๐ โ
โs ๐ง =
((๐ด ยทs
๐ต) -s ((
1s /su ๐) ยทs ( 1s
/su ๐))))) |
115 | 99, 114 | bitrid 283 |
. . . . . . . . . . . . . 14
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โ
(โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
116 | 115 | rexbidva 3168 |
. . . . . . . . . . . . 13
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ โ โs โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))) โ โ๐ โ โs โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) -s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
117 | 116, 74 | bitrdi 287 |
. . . . . . . . . . . 12
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ โ โs โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐)))) |
118 | 84, 117 | bitrid 283 |
. . . . . . . . . . 11
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐)))) |
119 | 118 | abbidv 2793 |
. . . . . . . . . 10
โข ((๐ด โ
No โง ๐ต โ
No ) โ {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))} = {๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))}) |
120 | 77, 119 | uneq12d 4157 |
. . . . . . . . 9
โข ((๐ด โ
No โง ๐ต โ
No ) โ ({๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))} โช {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))}) = ({๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))}
โช {๐ง โฃ
โ๐ โ
โs ๐ง =
((๐ด ยทs
๐ต) -s (
1s /su ๐))})) |
121 | | unidm 4145 |
. . . . . . . . 9
โข ({๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))}
โช {๐ง โฃ
โ๐ โ
โs ๐ง =
((๐ด ยทs
๐ต) -s (
1s /su ๐))}) = {๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))} |
122 | 120, 121 | eqtrdi 2780 |
. . . . . . . 8
โข ((๐ด โ
No โง ๐ต โ
No ) โ ({๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))} โช {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))}) = {๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))}) |
123 | | r19.41v 3180 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
โs (๐ก =
(๐ด -s (
1s /su ๐)) โง โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))) โ (โ๐ โ โs ๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))))) |
124 | 123 | exbii 1842 |
. . . . . . . . . . . . 13
โข
(โ๐กโ๐ โ โs (๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))) โ โ๐ก(โ๐ โ โs ๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))))) |
125 | | rexcom4 3277 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
โs โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))) โ โ๐กโ๐ โ โs (๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))))) |
126 | 27 | rexab 3683 |
. . . . . . . . . . . . 13
โข
(โ๐ก โ
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))) โ โ๐ก(โ๐ โ โs ๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))))) |
127 | 124, 125,
126 | 3bitr4ri 304 |
. . . . . . . . . . . 12
โข
(โ๐ก โ
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))) โ โ๐ โ โs โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))))) |
128 | 31 | oveq1d 7417 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ก = (๐ด -s ( 1s
/su ๐))
โ ((๐ด -s
๐ก) ยทs
(๐ข -s ๐ต)) = ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))) |
129 | 128 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ก = (๐ด -s ( 1s
/su ๐))
โ ((๐ด
ยทs ๐ต)
+s ((๐ด
-s ๐ก)
ยทs (๐ข
-s ๐ต))) =
((๐ด ยทs
๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต)))) |
130 | 129 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . 18
โข (๐ก = (๐ด -s ( 1s
/su ๐))
โ (๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))) โ ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))))) |
131 | 130 | rexbidv 3170 |
. . . . . . . . . . . . . . . . 17
โข (๐ก = (๐ด -s ( 1s
/su ๐))
โ (โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))) โ โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))))) |
132 | 30, 131 | ceqsexv 3518 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))) โ โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต)))) |
133 | | r19.41v 3180 |
. . . . . . . . . . . . . . . . . 18
โข
(โ๐ โ
โs (๐ข =
(๐ต +s (
1s /su ๐)) โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต)))) โ
(โ๐ โ
โs ๐ข =
(๐ต +s (
1s /su ๐)) โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))))) |
134 | 133 | exbii 1842 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ขโ๐ โ โs (๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต)))) โ
โ๐ข(โ๐ โ โs
๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))))) |
135 | | rexcom4 3277 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ โ
โs โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต)))) โ
โ๐ขโ๐ โ โs
(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))))) |
136 | 96 | rexab 3683 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))) โ
โ๐ข(โ๐ โ โs
๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))))) |
137 | 134, 135,
136 | 3bitr4ri 304 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))) โ
โ๐ โ
โs โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))))) |
138 | 132, 137 | bitri 275 |
. . . . . . . . . . . . . . 15
โข
(โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))) โ โ๐ โ โs โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))))) |
139 | 101 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ข = (๐ต +s ( 1s
/su ๐))
โ ((๐ด -s
(๐ด -s (
1s /su ๐))) ยทs (๐ข -s ๐ต)) = ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs ((๐ต
+s ( 1s /su ๐)) -s ๐ต))) |
140 | 139 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ข = (๐ต +s ( 1s
/su ๐))
โ ((๐ด
ยทs ๐ต)
+s ((๐ด
-s (๐ด
-s ( 1s /su ๐))) ยทs (๐ข -s ๐ต))) = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs ((๐ต
+s ( 1s /su ๐)) -s ๐ต)))) |
141 | 140 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . 18
โข (๐ข = (๐ต +s ( 1s
/su ๐))
โ (๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต))) โ
๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs ((๐ต
+s ( 1s /su ๐)) -s ๐ต))))) |
142 | 100, 141 | ceqsexv 3518 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต)))) โ
๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs ((๐ต
+s ( 1s /su ๐)) -s ๐ต)))) |
143 | 59, 109 | oveq12d 7420 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ((๐ด -s
(๐ด -s (
1s /su ๐))) ยทs ((๐ต +s ( 1s
/su ๐))
-s ๐ต)) = ((
1s /su ๐) ยทs ( 1s
/su ๐))) |
144 | 143 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ((๐ด
ยทs ๐ต)
+s ((๐ด
-s (๐ด
-s ( 1s /su ๐))) ยทs ((๐ต +s ( 1s
/su ๐))
-s ๐ต))) =
((๐ด ยทs
๐ต) +s ((
1s /su ๐) ยทs ( 1s
/su ๐)))) |
145 | 144 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs ((๐ต
+s ( 1s /su ๐)) -s ๐ต))) โ ๐ง = ((๐ด ยทs ๐ต) +s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
146 | 142, 145 | bitrid 283 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต)))) โ
๐ง = ((๐ด ยทs ๐ต) +s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
147 | 146 | rexbidva 3168 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โ
(โ๐ โ
โs โ๐ข(๐ข = (๐ต +s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s
/su ๐)))
ยทs (๐ข
-s ๐ต)))) โ
โ๐ โ
โs ๐ง =
((๐ด ยทs
๐ต) +s ((
1s /su ๐) ยทs ( 1s
/su ๐))))) |
148 | 138, 147 | bitrid 283 |
. . . . . . . . . . . . . 14
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โ
(โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
149 | 148 | rexbidva 3168 |
. . . . . . . . . . . . 13
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ โ โs โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))) โ โ๐ โ โs โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) +s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
150 | | remulscllem1 28168 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
โs โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s (( 1s
/su ๐)
ยทs ( 1s /su ๐))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))) |
151 | 149, 150 | bitrdi 287 |
. . . . . . . . . . . 12
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ โ โs โ๐ก(๐ก = (๐ด -s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐)))) |
152 | 127, 151 | bitrid 283 |
. . . . . . . . . . 11
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐)))) |
153 | 152 | abbidv 2793 |
. . . . . . . . . 10
โข ((๐ด โ
No โง ๐ต โ
No ) โ {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))} = {๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))}) |
154 | | r19.41v 3180 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
โs (๐ก =
(๐ด +s (
1s /su ๐)) โง โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))) โ (โ๐ โ โs ๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข))))) |
155 | 154 | exbii 1842 |
. . . . . . . . . . . . 13
โข
(โ๐กโ๐ โ โs (๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))) โ โ๐ก(โ๐ โ โs ๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข))))) |
156 | | rexcom4 3277 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
โs โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))) โ โ๐กโ๐ โ โs (๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข))))) |
157 | 82 | rexab 3683 |
. . . . . . . . . . . . 13
โข
(โ๐ก โ
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข))) โ โ๐ก(โ๐ โ โs ๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข))))) |
158 | 155, 156,
157 | 3bitr4ri 304 |
. . . . . . . . . . . 12
โข
(โ๐ก โ
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข))) โ โ๐ โ โs โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข))))) |
159 | 86 | oveq1d 7417 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ก = (๐ด +s ( 1s
/su ๐))
โ ((๐ก -s
๐ด) ยทs
(๐ต -s ๐ข)) = (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))) |
160 | 159 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ก = (๐ด +s ( 1s
/su ๐))
โ ((๐ด
ยทs ๐ต)
+s ((๐ก
-s ๐ด)
ยทs (๐ต
-s ๐ข))) =
((๐ด ยทs
๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข)))) |
161 | 160 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . 18
โข (๐ก = (๐ด +s ( 1s
/su ๐))
โ (๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข))) โ ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))))) |
162 | 161 | rexbidv 3170 |
. . . . . . . . . . . . . . . . 17
โข (๐ก = (๐ด +s ( 1s
/su ๐))
โ (โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข))) โ โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))))) |
163 | 85, 162 | ceqsexv 3518 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))) โ โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข)))) |
164 | | r19.41v 3180 |
. . . . . . . . . . . . . . . . . 18
โข
(โ๐ โ
โs (๐ข =
(๐ต -s (
1s /su ๐)) โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข)))) โ
(โ๐ โ
โs ๐ข =
(๐ต -s (
1s /su ๐)) โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))))) |
165 | 164 | exbii 1842 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ขโ๐ โ โs (๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข)))) โ
โ๐ข(โ๐ โ โs
๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))))) |
166 | | rexcom4 3277 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ โ
โs โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข)))) โ
โ๐ขโ๐ โ โs
(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))))) |
167 | 41 | rexab 3683 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))) โ
โ๐ข(โ๐ โ โs
๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))))) |
168 | 165, 166,
167 | 3bitr4ri 304 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))) โ
โ๐ โ
โs โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))))) |
169 | 163, 168 | bitri 275 |
. . . . . . . . . . . . . . 15
โข
(โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))) โ โ๐ โ โs โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))))) |
170 | 46 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ข = (๐ต -s ( 1s
/su ๐))
โ (((๐ด +s (
1s /su ๐)) -s ๐ด) ยทs (๐ต -s ๐ข)) = (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s (๐ต
-s ( 1s /su ๐))))) |
171 | 170 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ข = (๐ต -s ( 1s
/su ๐))
โ ((๐ด
ยทs ๐ต)
+s (((๐ด
+s ( 1s /su ๐)) -s ๐ด) ยทs (๐ต -s ๐ข))) = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s (๐ต
-s ( 1s /su ๐)))))) |
172 | 171 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . 18
โข (๐ข = (๐ต -s ( 1s
/su ๐))
โ (๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข))) โ
๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s (๐ต
-s ( 1s /su ๐))))))) |
173 | 45, 172 | ceqsexv 3518 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข)))) โ
๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s (๐ต
-s ( 1s /su ๐)))))) |
174 | 107, 66 | oveq12d 7420 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (((๐ด +s (
1s /su ๐)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s
/su ๐)))) =
(( 1s /su ๐) ยทs ( 1s
/su ๐))) |
175 | 174 | oveq2d 7418 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ ((๐ด
ยทs ๐ต)
+s (((๐ด
+s ( 1s /su ๐)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s
/su ๐))))) =
((๐ด ยทs
๐ต) +s ((
1s /su ๐) ยทs ( 1s
/su ๐)))) |
176 | 175 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s (๐ต
-s ( 1s /su ๐))))) โ ๐ง = ((๐ด ยทs ๐ต) +s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
177 | 173, 176 | bitrid 283 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โง ๐ โ โs)
โ (โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข)))) โ
๐ง = ((๐ด ยทs ๐ต) +s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
178 | 177 | rexbidva 3168 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โ
(โ๐ โ
โs โ๐ข(๐ข = (๐ต -s ( 1s
/su ๐))
โง ๐ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s
/su ๐))
-s ๐ด)
ยทs (๐ต
-s ๐ข)))) โ
โ๐ โ
โs ๐ง =
((๐ด ยทs
๐ต) +s ((
1s /su ๐) ยทs ( 1s
/su ๐))))) |
179 | 169, 178 | bitrid 283 |
. . . . . . . . . . . . . 14
โข (((๐ด โ
No โง ๐ต โ
No ) โง ๐ โ โs) โ
(โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
180 | 179 | rexbidva 3168 |
. . . . . . . . . . . . 13
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ โ โs โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))) โ โ๐ โ โs โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) +s (( 1s
/su ๐)
ยทs ( 1s /su ๐))))) |
181 | 180, 150 | bitrdi 287 |
. . . . . . . . . . . 12
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ โ โs โ๐ก(๐ก = (๐ด +s ( 1s
/su ๐))
โง โ๐ข โ
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐)))) |
182 | 158, 181 | bitrid 283 |
. . . . . . . . . . 11
โข ((๐ด โ
No โง ๐ต โ
No ) โ (โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข))) โ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐)))) |
183 | 182 | abbidv 2793 |
. . . . . . . . . 10
โข ((๐ด โ
No โง ๐ต โ
No ) โ {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))} = {๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))}) |
184 | 153, 183 | uneq12d 4157 |
. . . . . . . . 9
โข ((๐ด โ
No โง ๐ต โ
No ) โ ({๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))} โช {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))}) = ({๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))}
โช {๐ง โฃ
โ๐ โ
โs ๐ง =
((๐ด ยทs
๐ต) +s (
1s /su ๐))})) |
185 | | unidm 4145 |
. . . . . . . . 9
โข ({๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))}
โช {๐ง โฃ
โ๐ โ
โs ๐ง =
((๐ด ยทs
๐ต) +s (
1s /su ๐))}) = {๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))} |
186 | 184, 185 | eqtrdi 2780 |
. . . . . . . 8
โข ((๐ด โ
No โง ๐ต โ
No ) โ ({๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))} โช {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))}) = {๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))}) |
187 | 122, 186 | oveq12d 7420 |
. . . . . . 7
โข ((๐ด โ
No โง ๐ต โ
No ) โ (({๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))} โช {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))}) |s ({๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))} โช {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))})) = ({๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))} |s
{๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))})) |
188 | 187 | adantr 480 |
. . . . . 6
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})
โง ๐ต = ({๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))
โ (({๐ง โฃ
โ๐ก โ {๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐ก) ยทs (๐ต -s ๐ข)))} โช {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) -s ((๐ก -s ๐ด) ยทs (๐ข -s ๐ต)))}) |s ({๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต +s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐ก) ยทs (๐ข -s ๐ต)))} โช {๐ง โฃ โ๐ก โ {๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด +s ( 1s
/su ๐))}โ๐ข โ {๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))}๐ง = ((๐ด ยทs ๐ต) +s ((๐ก -s ๐ด) ยทs (๐ต -s ๐ข)))})) = ({๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))} |s
{๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))})) |
189 | 22, 188 | eqtrd 2764 |
. . . . 5
โข (((๐ด โ
No โง ๐ต โ
No ) โง (๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})
โง ๐ต = ({๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))
โ (๐ด
ยทs ๐ต) =
({๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))} |s
{๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))})) |
190 | 14, 189 | sylan2 592 |
. . . 4
โข (((๐ด โ
No โง ๐ต โ
No ) โง ((โ๐ โ โs (( -us
โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}))
โง (โ๐ โ
โs (( -us โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}))))
โ (๐ด
ยทs ๐ต) =
({๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))} |s
{๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))})) |
191 | 2, 11, 190 | jca32 515 |
. . 3
โข (((๐ด โ
No โง ๐ต โ
No ) โง ((โ๐ โ โs (( -us
โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))}))
โง (โ๐ โ
โs (( -us โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}))))
โ ((๐ด
ยทs ๐ต)
โ No โง (โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐) โง (๐ด ยทs ๐ต) = ({๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))} |s
{๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))})))) |
192 | 191 | an4s 657 |
. 2
โข (((๐ด โ
No โง (โ๐
โ โs (( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})))
โง (๐ต โ No โง (โ๐ โ โs (( -us
โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}))))
โ ((๐ด
ยทs ๐ต)
โ No โง (โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐) โง (๐ด ยทs ๐ต) = ({๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))} |s
{๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))})))) |
193 | | elreno 28163 |
. . 3
โข (๐ด โ โs
โ (๐ด โ No โง (โ๐ โ โs (( -us
โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})))) |
194 | | elreno 28163 |
. . 3
โข (๐ต โ โs
โ (๐ต โ No โง (โ๐ โ โs (( -us
โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))})))) |
195 | 193, 194 | anbi12i 626 |
. 2
โข ((๐ด โ โs
โง ๐ต โ
โs) โ ((๐ด โ No
โง (โ๐ โ
โs (( -us โ๐) <s ๐ด โง ๐ด <s ๐) โง ๐ด = ({๐ฅ โฃ โ๐ โ โs ๐ฅ = (๐ด -s ( 1s
/su ๐))} |s
{๐ฅ โฃ โ๐ โ โs
๐ฅ = (๐ด +s ( 1s
/su ๐))})))
โง (๐ต โ No โง (โ๐ โ โs (( -us
โ๐) <s ๐ต โง ๐ต <s ๐) โง ๐ต = ({๐ฆ โฃ โ๐ โ โs ๐ฆ = (๐ต -s ( 1s
/su ๐))} |s
{๐ฆ โฃ โ๐ โ โs
๐ฆ = (๐ต +s ( 1s
/su ๐))}))))) |
196 | | elreno 28163 |
. 2
โข ((๐ด ยทs ๐ต) โ โs
โ ((๐ด
ยทs ๐ต)
โ No โง (โ๐ โ โs (( -us
โ๐) <s (๐ด ยทs ๐ต) โง (๐ด ยทs ๐ต) <s ๐) โง (๐ด ยทs ๐ต) = ({๐ง โฃ โ๐ โ โs ๐ง = ((๐ด ยทs ๐ต) -s ( 1s
/su ๐))} |s
{๐ง โฃ โ๐ โ โs
๐ง = ((๐ด ยทs ๐ต) +s ( 1s
/su ๐))})))) |
197 | 192, 195,
196 | 3imtr4i 292 |
1
โข ((๐ด โ โs
โง ๐ต โ
โs) โ (๐ด ยทs ๐ต) โ
โs) |