Step | Hyp | Ref
| Expression |
1 | | mulscutlem.1 |
. 2
โข (๐ โ ๐ด โ No
) |
2 | | mulscutlem.2 |
. 2
โข (๐ โ ๐ต โ No
) |
3 | | mulsprop 27499 |
. . . . . . . . 9
โข (((๐ โ
No โง ๐ โ
No ) โง (๐ โ No
โง โ โ No ) โง (๐ โ No
โง ๐ โ No )) โ ((๐ ยทs ๐) โ No
โง ((๐ <s โ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((โ ยทs ๐) -s (โ ยทs ๐))))) |
4 | 3 | a1d 25 |
. . . . . . . 8
โข (((๐ โ
No โง ๐ โ
No ) โง (๐ โ No
โง โ โ No ) โง (๐ โ No
โง ๐ โ No )) โ (((( bday
โ๐) +no ( bday โ๐)) โช (((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โโ) +no ( bday โ๐))) โช ((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โโ) +no ( bday โ๐))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ 0s ) +no ( bday โ
0s )) โช (( bday โ
0s ) +no ( bday โ 0s
))) โช ((( bday โ 0s ) +no
( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) โ ((๐ ยทs ๐) โ
No โง ((๐ <s
โ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((โ ยทs ๐) -s (โ ยทs ๐)))))) |
5 | 4 | 3expa 1118 |
. . . . . . 7
โข ((((๐ โ
No โง ๐ โ
No ) โง (๐ โ No
โง โ โ No )) โง (๐ โ No
โง ๐ โ No )) โ (((( bday
โ๐) +no ( bday โ๐)) โช (((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โโ) +no ( bday โ๐))) โช ((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โโ) +no ( bday โ๐))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ 0s ) +no ( bday โ
0s )) โช (( bday โ
0s ) +no ( bday โ 0s
))) โช ((( bday โ 0s ) +no
( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) โ ((๐ ยทs ๐) โ
No โง ((๐ <s
โ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((โ ยทs ๐) -s (โ ยทs ๐)))))) |
6 | 5 | ralrimivva 3199 |
. . . . . 6
โข (((๐ โ
No โง ๐ โ
No ) โง (๐ โ No
โง โ โ No )) โ โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โโ) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โโ) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) โ ((๐ ยทs ๐) โ
No โง ((๐ <s
โ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((โ ยทs ๐) -s (โ ยทs ๐)))))) |
7 | 6 | ralrimivva 3199 |
. . . . 5
โข ((๐ โ
No โง ๐ โ
No ) โ โ๐ โ No
โโ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โโ) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โโ) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) โ ((๐ ยทs ๐) โ
No โง ((๐ <s
โ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((โ ยทs ๐) -s (โ ยทs ๐)))))) |
8 | 7 | rgen2 3196 |
. . . 4
โข
โ๐ โ
No โ๐ โ No
โ๐ โ No โโ โ No
โ๐ โ No โ๐ โ No
(((( bday โ๐) +no ( bday
โ๐)) โช
(((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โโ) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โโ) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) โ ((๐ ยทs ๐) โ
No โง ((๐ <s
โ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((โ ยทs ๐) -s (โ ยทs ๐))))) |
9 | 8 | a1i 11 |
. . 3
โข ((๐ด โ
No โง ๐ต โ
No ) โ โ๐ โ No
โ๐ โ No โ๐ โ No
โโ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โโ) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โโ) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) โ ((๐ ยทs ๐) โ
No โง ((๐ <s
โ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((โ ยทs ๐) -s (โ ยทs ๐)))))) |
10 | | simpl 483 |
. . 3
โข ((๐ด โ
No โง ๐ต โ
No ) โ ๐ด โ No
) |
11 | | simpr 485 |
. . 3
โข ((๐ด โ
No โง ๐ต โ
No ) โ ๐ต โ No
) |
12 | 9, 10, 11 | mulsproplem10 27494 |
. 2
โข ((๐ด โ
No โง ๐ต โ
No ) โ ((๐ด ยทs ๐ต) โ No
โง ({๐ โฃ
โ๐ โ ( L
โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) <<s {(๐ด ยทs ๐ต)} โง {(๐ด ยทs ๐ต)} <<s ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}))) |
13 | 1, 2, 12 | syl2anc 584 |
1
โข (๐ โ ((๐ด ยทs ๐ต) โ No
โง ({๐ โฃ
โ๐ โ ( L
โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) <<s {(๐ด ยทs ๐ต)} โง {(๐ด ยทs ๐ต)} <<s ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}))) |