Step | Hyp | Ref
| Expression |
1 | | mulsproplem.1 |
. . . 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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
2 | 1 | adantr 481 |
. . 3
โข ((๐ โง ((
bday โ๐ธ)
โ ( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ))) โ โ๐ โ 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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
3 | | mulsproplem.2 |
. . . 4
โข (๐ โ ๐ถ โ No
) |
4 | 3 | adantr 481 |
. . 3
โข ((๐ โง ((
bday โ๐ธ)
โ ( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ))) โ ๐ถ โ No
) |
5 | | mulsproplem.3 |
. . . 4
โข (๐ โ ๐ท โ No
) |
6 | 5 | adantr 481 |
. . 3
โข ((๐ โง ((
bday โ๐ธ)
โ ( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ))) โ ๐ท โ No
) |
7 | | mulsproplem.4 |
. . . 4
โข (๐ โ ๐ธ โ No
) |
8 | 7 | adantr 481 |
. . 3
โข ((๐ โง ((
bday โ๐ธ)
โ ( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ))) โ ๐ธ โ No
) |
9 | | mulsproplem.5 |
. . . 4
โข (๐ โ ๐น โ No
) |
10 | 9 | adantr 481 |
. . 3
โข ((๐ โง ((
bday โ๐ธ)
โ ( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ))) โ ๐น โ No
) |
11 | | mulsproplem.6 |
. . . 4
โข (๐ โ ๐ถ <s ๐ท) |
12 | 11 | adantr 481 |
. . 3
โข ((๐ โง ((
bday โ๐ธ)
โ ( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ))) โ ๐ถ <s ๐ท) |
13 | | mulsproplem.7 |
. . . 4
โข (๐ โ ๐ธ <s ๐น) |
14 | 13 | adantr 481 |
. . 3
โข ((๐ โง ((
bday โ๐ธ)
โ ( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ))) โ ๐ธ <s ๐น) |
15 | | simpr 485 |
. . 3
โข ((๐ โง ((
bday โ๐ธ)
โ ( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ))) โ (( bday
โ๐ธ) โ
( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ))) |
16 | 2, 4, 6, 8, 10, 12, 14, 15 | mulsproplem13 27497 |
. 2
โข ((๐ โง ((
bday โ๐ธ)
โ ( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ))) โ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ))) |
17 | 7 | adantr 481 |
. . . 4
โข ((๐ โง (
bday โ๐ธ) =
( bday โ๐น)) โ ๐ธ โ No
) |
18 | 9 | adantr 481 |
. . . 4
โข ((๐ โง (
bday โ๐ธ) =
( bday โ๐น)) โ ๐น โ No
) |
19 | | simpr 485 |
. . . 4
โข ((๐ โง (
bday โ๐ธ) =
( bday โ๐น)) โ ( bday
โ๐ธ) = ( bday โ๐น)) |
20 | 13 | adantr 481 |
. . . 4
โข ((๐ โง (
bday โ๐ธ) =
( bday โ๐น)) โ ๐ธ <s ๐น) |
21 | | nodense 27122 |
. . . 4
โข (((๐ธ โ
No โง ๐น โ
No ) โง (( bday
โ๐ธ) = ( bday โ๐น) โง ๐ธ <s ๐น)) โ โ๐ฅ โ No
(( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)) |
22 | 17, 18, 19, 20, 21 | syl22anc 837 |
. . 3
โข ((๐ โง (
bday โ๐ธ) =
( bday โ๐น)) โ โ๐ฅ โ No
(( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)) |
23 | | unidm 4148 |
. . . . . . . . . . . . . . . . 17
โข (((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s )))) = ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) |
24 | | unidm 4148 |
. . . . . . . . . . . . . . . . 17
โข ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) = (( bday โ 0s ) +no ( bday โ 0s )) |
25 | | bday0s 27255 |
. . . . . . . . . . . . . . . . . . 19
โข ( bday โ 0s ) = โ
|
26 | 25, 25 | oveq12i 7405 |
. . . . . . . . . . . . . . . . . 18
โข (( bday โ 0s ) +no ( bday โ 0s )) = (โ
+no
โ
) |
27 | | 0elon 6407 |
. . . . . . . . . . . . . . . . . . 19
โข โ
โ On |
28 | | naddrid 8665 |
. . . . . . . . . . . . . . . . . . 19
โข (โ
โ On โ (โ
+no โ
) = โ
) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
โข (โ
+no โ
) = โ
|
30 | 26, 29 | eqtri 2759 |
. . . . . . . . . . . . . . . . 17
โข (( bday โ 0s ) +no ( bday โ 0s )) =
โ
|
31 | 23, 24, 30 | 3eqtri 2763 |
. . . . . . . . . . . . . . . 16
โข (((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s )))) =
โ
|
32 | 31 | uneq2i 4156 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ท) +no ( bday
โ๐ธ)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) = ((( bday โ๐ท) +no ( bday
โ๐ธ)) โช
โ
) |
33 | | un0 4386 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ท) +no ( bday
โ๐ธ)) โช
โ
) = (( bday โ๐ท) +no ( bday
โ๐ธ)) |
34 | 32, 33 | eqtri 2759 |
. . . . . . . . . . . . . 14
โข ((( bday โ๐ท) +no ( bday
โ๐ธ)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) = (( bday โ๐ท) +no ( bday
โ๐ธ)) |
35 | | ssun2 4169 |
. . . . . . . . . . . . . . . 16
โข (( bday โ๐ท) +no ( bday
โ๐ธ)) โ
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))) |
36 | | ssun2 4169 |
. . . . . . . . . . . . . . . 16
โข ((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) |
37 | 35, 36 | sstri 3987 |
. . . . . . . . . . . . . . 15
โข (( bday โ๐ท) +no ( bday
โ๐ธ)) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) |
38 | | ssun2 4169 |
. . . . . . . . . . . . . . 15
โข (((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
39 | 37, 38 | sstri 3987 |
. . . . . . . . . . . . . 14
โข (( bday โ๐ท) +no ( bday
โ๐ธ)) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
40 | 34, 39 | eqsstri 4012 |
. . . . . . . . . . . . 13
โข ((( bday โ๐ท) +no ( bday
โ๐ธ)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) โ ((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
41 | 40 | sseli 3974 |
. . . . . . . . . . . 12
โข (((( 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 ))))) โ ((( bday โ๐) +no ( bday
โ๐)) โช
(((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))))) |
42 | 41 | imim1i 63 |
. . . . . . . . . . 11
โข
((((( bday โ๐) +no ( bday
โ๐)) โช
(((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ (((( 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 ๐)))))) |
43 | 42 | 6ralimi 3126 |
. . . . . . . . . 10
โข
(โ๐ โ
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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ โ๐ โ 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 ๐)))))) |
44 | 1, 43 | syl 17 |
. . . . . . . . 9
โข (๐ โ โ๐ โ 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 ๐)))))) |
45 | 44, 5, 7 | mulsproplem11 27495 |
. . . . . . . 8
โข (๐ โ (๐ท ยทs ๐ธ) โ No
) |
46 | 31 | uneq2i 4156 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) = ((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
โ
) |
47 | | un0 4386 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
โ
) = (( bday โ๐ถ) +no ( bday
โ๐ธ)) |
48 | 46, 47 | eqtri 2759 |
. . . . . . . . . . . . . 14
โข ((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) = (( bday โ๐ถ) +no ( bday
โ๐ธ)) |
49 | | ssun1 4168 |
. . . . . . . . . . . . . . . 16
โข (( bday โ๐ถ) +no ( bday
โ๐ธ)) โ
((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) |
50 | | ssun1 4168 |
. . . . . . . . . . . . . . . 16
โข ((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) |
51 | 49, 50 | sstri 3987 |
. . . . . . . . . . . . . . 15
โข (( bday โ๐ถ) +no ( bday
โ๐ธ)) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) |
52 | 51, 38 | sstri 3987 |
. . . . . . . . . . . . . 14
โข (( bday โ๐ถ) +no ( bday
โ๐ธ)) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
53 | 48, 52 | eqsstri 4012 |
. . . . . . . . . . . . 13
โข ((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) โ ((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
54 | 53 | sseli 3974 |
. . . . . . . . . . . 12
โข (((( 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 ))))) โ ((( bday โ๐) +no ( bday
โ๐)) โช
(((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))))) |
55 | 54 | imim1i 63 |
. . . . . . . . . . 11
โข
((((( bday โ๐) +no ( bday
โ๐)) โช
(((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ (((( 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 ๐)))))) |
56 | 55 | 6ralimi 3126 |
. . . . . . . . . 10
โข
(โ๐ โ
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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ โ๐ โ 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 ๐)))))) |
57 | 1, 56 | syl 17 |
. . . . . . . . 9
โข (๐ โ โ๐ โ 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 ๐)))))) |
58 | 57, 3, 7 | mulsproplem11 27495 |
. . . . . . . 8
โข (๐ โ (๐ถ ยทs ๐ธ) โ No
) |
59 | 45, 58 | subscld 27449 |
. . . . . . 7
โข (๐ โ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) โ No
) |
60 | 59 | adantr 481 |
. . . . . 6
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) โ No
) |
61 | 44 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ โ๐ โ 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 ๐)))))) |
62 | 5 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ๐ท โ No
) |
63 | | simprr1 1221 |
. . . . . . . . . 10
โข ((( bday โ๐ธ) = ( bday
โ๐น) โง
(๐ฅ โ No โง (( bday
โ๐ฅ) โ
( bday โ๐ธ) โง ๐ธ <s ๐ฅ โง ๐ฅ <s ๐น))) โ ( bday
โ๐ฅ) โ
( bday โ๐ธ)) |
64 | 63 | adantl 482 |
. . . . . . . . 9
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ( bday
โ๐ฅ) โ
( bday โ๐ธ)) |
65 | | bdayelon 27204 |
. . . . . . . . . 10
โข ( bday โ๐ธ) โ On |
66 | | simprrl 779 |
. . . . . . . . . 10
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ๐ฅ โ No
) |
67 | | oldbday 27318 |
. . . . . . . . . 10
โข ((( bday โ๐ธ) โ On โง ๐ฅ โ No )
โ (๐ฅ โ ( O
โ( bday โ๐ธ)) โ ( bday
โ๐ฅ) โ
( bday โ๐ธ))) |
68 | 65, 66, 67 | sylancr 587 |
. . . . . . . . 9
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (๐ฅ โ ( O โ(
bday โ๐ธ))
โ ( bday โ๐ฅ) โ ( bday
โ๐ธ))) |
69 | 64, 68 | mpbird 256 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ๐ฅ โ ( O โ(
bday โ๐ธ))) |
70 | 61, 62, 69 | mulsproplem3 27487 |
. . . . . . 7
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (๐ท ยทs ๐ฅ) โ No
) |
71 | 57 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ โ๐ โ 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 ๐)))))) |
72 | 3 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ๐ถ โ No
) |
73 | 71, 72, 69 | mulsproplem3 27487 |
. . . . . . 7
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (๐ถ ยทs ๐ฅ) โ No
) |
74 | 70, 73 | subscld 27449 |
. . . . . 6
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((๐ท ยทs ๐ฅ) -s (๐ถ ยทs ๐ฅ)) โ No
) |
75 | 31 | uneq2i 4156 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ท) +no ( bday
โ๐น)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) = ((( bday โ๐ท) +no ( bday
โ๐น)) โช
โ
) |
76 | | un0 4386 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ท) +no ( bday
โ๐น)) โช
โ
) = (( bday โ๐ท) +no ( bday
โ๐น)) |
77 | 75, 76 | eqtri 2759 |
. . . . . . . . . . . . . 14
โข ((( bday โ๐ท) +no ( bday
โ๐น)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) = (( bday โ๐ท) +no ( bday
โ๐น)) |
78 | | ssun2 4169 |
. . . . . . . . . . . . . . . 16
โข (( bday โ๐ท) +no ( bday
โ๐น)) โ
((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) |
79 | 78, 50 | sstri 3987 |
. . . . . . . . . . . . . . 15
โข (( bday โ๐ท) +no ( bday
โ๐น)) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) |
80 | 79, 38 | sstri 3987 |
. . . . . . . . . . . . . 14
โข (( bday โ๐ท) +no ( bday
โ๐น)) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
81 | 77, 80 | eqsstri 4012 |
. . . . . . . . . . . . 13
โข ((( bday โ๐ท) +no ( bday
โ๐น)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) โ ((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
82 | 81 | sseli 3974 |
. . . . . . . . . . . 12
โข (((( 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 ))))) โ ((( bday โ๐) +no ( bday
โ๐)) โช
(((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))))) |
83 | 82 | imim1i 63 |
. . . . . . . . . . 11
โข
((((( bday โ๐) +no ( bday
โ๐)) โช
(((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ (((( 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 ๐)))))) |
84 | 83 | 6ralimi 3126 |
. . . . . . . . . 10
โข
(โ๐ โ
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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ โ๐ โ 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 ๐)))))) |
85 | 1, 84 | syl 17 |
. . . . . . . . 9
โข (๐ โ โ๐ โ 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 ๐)))))) |
86 | 85, 5, 9 | mulsproplem11 27495 |
. . . . . . . 8
โข (๐ โ (๐ท ยทs ๐น) โ No
) |
87 | 31 | uneq2i 4156 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) = ((( bday โ๐ถ) +no ( bday
โ๐น)) โช
โ
) |
88 | | un0 4386 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ถ) +no ( bday
โ๐น)) โช
โ
) = (( bday โ๐ถ) +no ( bday
โ๐น)) |
89 | 87, 88 | eqtri 2759 |
. . . . . . . . . . . . . 14
โข ((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) = (( bday โ๐ถ) +no ( bday
โ๐น)) |
90 | | ssun1 4168 |
. . . . . . . . . . . . . . . 16
โข (( bday โ๐ถ) +no ( bday
โ๐น)) โ
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))) |
91 | 90, 36 | sstri 3987 |
. . . . . . . . . . . . . . 15
โข (( bday โ๐ถ) +no ( bday
โ๐น)) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) |
92 | 91, 38 | sstri 3987 |
. . . . . . . . . . . . . 14
โข (( bday โ๐ถ) +no ( bday
โ๐น)) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
93 | 89, 92 | eqsstri 4012 |
. . . . . . . . . . . . 13
โข ((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))) โช ((( bday โ 0s ) +no ( bday โ 0s )) โช (( bday โ 0s ) +no ( bday โ 0s ))))) โ ((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
94 | 93 | sseli 3974 |
. . . . . . . . . . . 12
โข (((( 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 ))))) โ ((( bday โ๐) +no ( bday
โ๐)) โช
(((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))))) |
95 | 94 | imim1i 63 |
. . . . . . . . . . 11
โข
((((( bday โ๐) +no ( bday
โ๐)) โช
(((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ (((( 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 ๐)))))) |
96 | 95 | 6ralimi 3126 |
. . . . . . . . . 10
โข
(โ๐ โ
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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ โ๐ โ 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 ๐)))))) |
97 | 1, 96 | syl 17 |
. . . . . . . . 9
โข (๐ โ โ๐ โ 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 ๐)))))) |
98 | 97, 3, 9 | mulsproplem11 27495 |
. . . . . . . 8
โข (๐ โ (๐ถ ยทs ๐น) โ No
) |
99 | 86, 98 | subscld 27449 |
. . . . . . 7
โข (๐ โ ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ No
) |
100 | 99 | adantr 481 |
. . . . . 6
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ No
) |
101 | 1 | mulsproplemcbv 27484 |
. . . . . . . . . 10
โข (๐ โ โ๐ โ 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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
โ) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
102 | 101 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ โ๐ โ 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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
โ) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
103 | | onelss 6395 |
. . . . . . . . . . . . . . . . . 18
โข (( bday โ๐ธ) โ On โ ((
bday โ๐ฅ)
โ ( bday โ๐ธ) โ ( bday
โ๐ฅ) โ
( bday โ๐ธ))) |
104 | 65, 64, 103 | mpsyl 68 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ( bday
โ๐ฅ) โ
( bday โ๐ธ)) |
105 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ( bday
โ๐ธ) = ( bday โ๐น)) |
106 | 104, 105 | sseqtrd 4018 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ( bday
โ๐ฅ) โ
( bday โ๐น)) |
107 | | bdayelon 27204 |
. . . . . . . . . . . . . . . . 17
โข ( bday โ๐ฅ) โ On |
108 | | bdayelon 27204 |
. . . . . . . . . . . . . . . . 17
โข ( bday โ๐น) โ On |
109 | | bdayelon 27204 |
. . . . . . . . . . . . . . . . 17
โข ( bday โ๐ท) โ On |
110 | | naddss2 8672 |
. . . . . . . . . . . . . . . . 17
โข ((( bday โ๐ฅ) โ On โง (
bday โ๐น)
โ On โง ( bday โ๐ท) โ On) โ ((
bday โ๐ฅ)
โ ( bday โ๐น) โ (( bday
โ๐ท) +no ( bday โ๐ฅ)) โ (( bday
โ๐ท) +no ( bday โ๐น)))) |
111 | 107, 108,
109, 110 | mp3an 1461 |
. . . . . . . . . . . . . . . 16
โข (( bday โ๐ฅ) โ ( bday
โ๐น) โ
(( bday โ๐ท) +no ( bday
โ๐ฅ)) โ
(( bday โ๐ท) +no ( bday
โ๐น))) |
112 | 106, 111 | sylib 217 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (( bday
โ๐ท) +no ( bday โ๐ฅ)) โ (( bday
โ๐ท) +no ( bday โ๐น))) |
113 | | unss2 4177 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ท) +no ( bday
โ๐ฅ)) โ
(( bday โ๐ท) +no ( bday
โ๐น)) โ
((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))) โ
((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น)))) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐ฅ))) โ ((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐น)))) |
115 | | bdayelon 27204 |
. . . . . . . . . . . . . . . . 17
โข ( bday โ๐ถ) โ On |
116 | | naddss2 8672 |
. . . . . . . . . . . . . . . . 17
โข ((( bday โ๐ฅ) โ On โง (
bday โ๐น)
โ On โง ( bday โ๐ถ) โ On) โ ((
bday โ๐ฅ)
โ ( bday โ๐น) โ (( bday
โ๐ถ) +no ( bday โ๐ฅ)) โ (( bday
โ๐ถ) +no ( bday โ๐น)))) |
117 | 107, 108,
115, 116 | mp3an 1461 |
. . . . . . . . . . . . . . . 16
โข (( bday โ๐ฅ) โ ( bday
โ๐น) โ
(( bday โ๐ถ) +no ( bday
โ๐ฅ)) โ
(( bday โ๐ถ) +no ( bday
โ๐น))) |
118 | 106, 117 | sylib 217 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (( bday
โ๐ถ) +no ( bday โ๐ฅ)) โ (( bday
โ๐ถ) +no ( bday โ๐น))) |
119 | | unss1 4175 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โ
(( bday โ๐ถ) +no ( bday
โ๐น)) โ
((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))) โ
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((( bday
โ๐ถ) +no ( bday โ๐ฅ)) โช (( bday
โ๐ท) +no ( bday โ๐ธ))) โ ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ธ)))) |
121 | | unss12 4178 |
. . . . . . . . . . . . . 14
โข
((((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))) โ
((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โง
((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))) โ
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))) โช
((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
122 | 114, 120,
121 | syl2anc 584 |
. . . . . . . . . . . . 13
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐ฅ))) โช ((( bday
โ๐ถ) +no ( bday โ๐ฅ)) โช (( bday
โ๐ท) +no ( bday โ๐ธ)))) โ (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ธ))))) |
123 | | unss2 4177 |
. . . . . . . . . . . . 13
โข
((((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))) โช
((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))) โช
((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))))
โ ((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))))) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐ฅ))) โช ((( bday
โ๐ถ) +no ( bday โ๐ฅ)) โช (( bday
โ๐ท) +no ( bday โ๐ธ))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ธ)))))) |
125 | 124 | sseld 3977 |
. . . . . . . . . . 11
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (((( bday
โ๐) +no ( bday โโ)) โช (((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))) โช ((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐ฅ))) โช ((( bday
โ๐ถ) +no ( bday โ๐ฅ)) โช (( bday
โ๐ท) +no ( bday โ๐ธ))))) โ ((( bday
โ๐) +no ( bday โโ)) โช (((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))) โช ((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ธ))))))) |
126 | 125 | imim1d 82 |
. . . . . . . . . 10
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((((( bday
โ๐) +no ( bday โโ)) โช (((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))) โช ((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ธ))))) โ ((๐ ยทs โ) โ No
โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ (((( bday
โ๐) +no ( bday โโ)) โช (((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))) โช ((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐ฅ))) โช ((( bday
โ๐ถ) +no ( bday โ๐ฅ)) โช (( bday
โ๐ท) +no ( bday โ๐ธ))))) โ ((๐ ยทs โ) โ No
โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))))) |
127 | 126 | ralimd6v 3207 |
. . . . . . . . 9
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (โ๐ โ 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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
โ) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ โ๐ โ 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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))) โช
((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
โ) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))))) |
128 | 102, 127 | mpd 15 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ โ๐ โ 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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))) โช
((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
โ) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
129 | 7 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ๐ธ โ No
) |
130 | 11 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ๐ถ <s ๐ท) |
131 | | simprr2 1222 |
. . . . . . . . 9
โข ((( bday โ๐ธ) = ( bday
โ๐น) โง
(๐ฅ โ No โง (( bday
โ๐ฅ) โ
( bday โ๐ธ) โง ๐ธ <s ๐ฅ โง ๐ฅ <s ๐น))) โ ๐ธ <s ๐ฅ) |
132 | 131 | adantl 482 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ๐ธ <s ๐ฅ) |
133 | 64 | olcd 872 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (( bday
โ๐ธ) โ
( bday โ๐ฅ) โจ ( bday
โ๐ฅ) โ
( bday โ๐ธ))) |
134 | 128, 72, 62, 129, 66, 130, 132, 133 | mulsproplem13 27497 |
. . . . . . 7
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((๐ถ ยทs ๐ฅ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐ฅ) -s (๐ท ยทs ๐ธ))) |
135 | 45 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (๐ท ยทs ๐ธ) โ No
) |
136 | 58 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (๐ถ ยทs ๐ธ) โ No
) |
137 | 135, 70, 136, 73 | sltsubsub3bd 27466 |
. . . . . . 7
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐ฅ) -s (๐ถ ยทs ๐ฅ)) โ ((๐ถ ยทs ๐ฅ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐ฅ) -s (๐ท ยทs ๐ธ)))) |
138 | 134, 137 | mpbird 256 |
. . . . . 6
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐ฅ) -s (๐ถ ยทs ๐ฅ))) |
139 | | naddss2 8672 |
. . . . . . . . . . . . . . . . 17
โข ((( bday โ๐ฅ) โ On โง (
bday โ๐ธ)
โ On โง ( bday โ๐ถ) โ On) โ ((
bday โ๐ฅ)
โ ( bday โ๐ธ) โ (( bday
โ๐ถ) +no ( bday โ๐ฅ)) โ (( bday
โ๐ถ) +no ( bday โ๐ธ)))) |
140 | 107, 65, 115, 139 | mp3an 1461 |
. . . . . . . . . . . . . . . 16
โข (( bday โ๐ฅ) โ ( bday
โ๐ธ) โ
(( bday โ๐ถ) +no ( bday
โ๐ฅ)) โ
(( bday โ๐ถ) +no ( bday
โ๐ธ))) |
141 | 104, 140 | sylib 217 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (( bday
โ๐ถ) +no ( bday โ๐ฅ)) โ (( bday
โ๐ถ) +no ( bday โ๐ธ))) |
142 | | unss1 4175 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โ
(( bday โ๐ถ) +no ( bday
โ๐ธ)) โ
((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โ
((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น)))) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((( bday
โ๐ถ) +no ( bday โ๐ฅ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โ ((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐น)))) |
144 | | naddss2 8672 |
. . . . . . . . . . . . . . . . 17
โข ((( bday โ๐ฅ) โ On โง (
bday โ๐ธ)
โ On โง ( bday โ๐ท) โ On) โ ((
bday โ๐ฅ)
โ ( bday โ๐ธ) โ (( bday
โ๐ท) +no ( bday โ๐ฅ)) โ (( bday
โ๐ท) +no ( bday โ๐ธ)))) |
145 | 107, 65, 109, 144 | mp3an 1461 |
. . . . . . . . . . . . . . . 16
โข (( bday โ๐ฅ) โ ( bday
โ๐ธ) โ
(( bday โ๐ท) +no ( bday
โ๐ฅ)) โ
(( bday โ๐ท) +no ( bday
โ๐ธ))) |
146 | 104, 145 | sylib 217 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (( bday
โ๐ท) +no ( bday โ๐ฅ)) โ (( bday
โ๐ท) +no ( bday โ๐ธ))) |
147 | | unss2 4177 |
. . . . . . . . . . . . . . 15
โข ((( bday โ๐ท) +no ( bday
โ๐ฅ)) โ
(( bday โ๐ท) +no ( bday
โ๐ธ)) โ
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))) โ
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ฅ))) โ ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ธ)))) |
149 | | unss12 4178 |
. . . . . . . . . . . . . 14
โข
((((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โ
((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โง
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))) โ
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) โ
(((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ)))) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) |
150 | 143, 148,
149 | syl2anc 584 |
. . . . . . . . . . . . 13
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (((( bday
โ๐ถ) +no ( bday โ๐ฅ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ฅ)))) โ (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ธ))))) |
151 | | unss2 4177 |
. . . . . . . . . . . . 13
โข
((((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ)))) โ
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ)))))
โ ((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ)))))) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ฅ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ฅ))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ธ)))))) |
153 | 152 | sseld 3977 |
. . . . . . . . . . 11
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (((( bday
โ๐) +no ( bday โโ)) โช (((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))) โช ((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ฅ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ฅ))))) โ ((( bday
โ๐) +no ( bday โโ)) โช (((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))) โช ((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ธ))))))) |
154 | 153 | imim1d 82 |
. . . . . . . . . 10
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((((( bday
โ๐) +no ( bday โโ)) โช (((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))) โช ((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ธ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ธ))))) โ ((๐ ยทs โ) โ No
โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ (((( bday
โ๐) +no ( bday โโ)) โช (((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))) โช ((( bday
โ๐) +no ( bday โ๐)) โช (( bday
โ๐) +no ( bday โ๐))))) โ ((( bday
โ๐ด) +no ( bday โ๐ต)) โช (((( bday
โ๐ถ) +no ( bday โ๐ฅ)) โช (( bday
โ๐ท) +no ( bday โ๐น))) โช ((( bday
โ๐ถ) +no ( bday โ๐น)) โช (( bday
โ๐ท) +no ( bday โ๐ฅ))))) โ ((๐ ยทs โ) โ No
โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))))) |
155 | 154 | ralimd6v 3207 |
. . . . . . . . 9
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (โ๐ โ 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 โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
โ) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))) โ โ๐ โ 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 โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))))) โ
((๐ ยทs
โ) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐))))))) |
156 | 102, 155 | mpd 15 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ โ๐ โ 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 โ๐ถ) +no ( bday
โ๐ฅ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ฅ))))) โ
((๐ ยทs
โ) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
157 | 9 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ๐น โ No
) |
158 | | simprr3 1223 |
. . . . . . . . 9
โข ((( bday โ๐ธ) = ( bday
โ๐น) โง
(๐ฅ โ No โง (( bday
โ๐ฅ) โ
( bday โ๐ธ) โง ๐ธ <s ๐ฅ โง ๐ฅ <s ๐น))) โ ๐ฅ <s ๐น) |
159 | 158 | adantl 482 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ๐ฅ <s ๐น) |
160 | 64, 105 | eleqtrd 2834 |
. . . . . . . . 9
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ( bday
โ๐ฅ) โ
( bday โ๐น)) |
161 | 160 | orcd 871 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (( bday
โ๐ฅ) โ
( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ฅ))) |
162 | 156, 72, 62, 66, 157, 130, 159, 161 | mulsproplem13 27497 |
. . . . . . 7
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ฅ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ฅ))) |
163 | 86 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (๐ท ยทs ๐น) โ No
) |
164 | 98 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (๐ถ ยทs ๐น) โ No
) |
165 | 70, 163, 73, 164 | sltsubsub3bd 27466 |
. . . . . . 7
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (((๐ท ยทs ๐ฅ) -s (๐ถ ยทs ๐ฅ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ฅ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ฅ)))) |
166 | 162, 165 | mpbird 256 |
. . . . . 6
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((๐ท ยทs ๐ฅ) -s (๐ถ ยทs ๐ฅ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น))) |
167 | 60, 74, 100, 138, 166 | slttrd 27189 |
. . . . 5
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น))) |
168 | 45, 86, 58, 98 | sltsubsub3bd 27466 |
. . . . . 6
โข (๐ โ (((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))) |
169 | 168 | adantr 481 |
. . . . 5
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ (((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))) |
170 | 167, 169 | mpbid 231 |
. . . 4
โข ((๐ โง ((
bday โ๐ธ) =
( bday โ๐น) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น)))) โ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ))) |
171 | 170 | anassrs 468 |
. . 3
โข (((๐ โง (
bday โ๐ธ) =
( bday โ๐น)) โง (๐ฅ โ No
โง (( bday โ๐ฅ) โ ( bday
โ๐ธ) โง
๐ธ <s ๐ฅ โง ๐ฅ <s ๐น))) โ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ))) |
172 | 22, 171 | rexlimddv 3160 |
. 2
โข ((๐ โง (
bday โ๐ธ) =
( bday โ๐น)) โ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ))) |
173 | 65 | onordi 6464 |
. . . . 5
โข Ord
( bday โ๐ธ) |
174 | 108 | onordi 6464 |
. . . . 5
โข Ord
( bday โ๐น) |
175 | | ordtri3or 6385 |
. . . . 5
โข ((Ord
( bday โ๐ธ) โง Ord ( bday
โ๐น)) โ
(( bday โ๐ธ) โ ( bday
โ๐น) โจ
( bday โ๐ธ) = ( bday
โ๐น) โจ
( bday โ๐น) โ ( bday
โ๐ธ))) |
176 | 173, 174,
175 | mp2an 690 |
. . . 4
โข (( bday โ๐ธ) โ ( bday
โ๐น) โจ
( bday โ๐ธ) = ( bday
โ๐น) โจ
( bday โ๐น) โ ( bday
โ๐ธ)) |
177 | | df-3or 1088 |
. . . . 5
โข ((( bday โ๐ธ) โ ( bday
โ๐น) โจ
( bday โ๐ธ) = ( bday
โ๐น) โจ
( bday โ๐น) โ ( bday
โ๐ธ)) โ
((( bday โ๐ธ) โ ( bday
โ๐น) โจ
( bday โ๐ธ) = ( bday
โ๐น)) โจ
( bday โ๐น) โ ( bday
โ๐ธ))) |
178 | | or32 924 |
. . . . 5
โข (((( bday โ๐ธ) โ ( bday
โ๐น) โจ
( bday โ๐ธ) = ( bday
โ๐น)) โจ
( bday โ๐น) โ ( bday
โ๐ธ)) โ
((( bday โ๐ธ) โ ( bday
โ๐น) โจ
( bday โ๐น) โ ( bday
โ๐ธ)) โจ
( bday โ๐ธ) = ( bday
โ๐น))) |
179 | 177, 178 | bitri 274 |
. . . 4
โข ((( bday โ๐ธ) โ ( bday
โ๐น) โจ
( bday โ๐ธ) = ( bday
โ๐น) โจ
( bday โ๐น) โ ( bday
โ๐ธ)) โ
((( bday โ๐ธ) โ ( bday
โ๐น) โจ
( bday โ๐น) โ ( bday
โ๐ธ)) โจ
( bday โ๐ธ) = ( bday
โ๐น))) |
180 | 176, 179 | mpbi 229 |
. . 3
โข ((( bday โ๐ธ) โ ( bday
โ๐น) โจ
( bday โ๐น) โ ( bday
โ๐ธ)) โจ
( bday โ๐ธ) = ( bday
โ๐น)) |
181 | 180 | a1i 11 |
. 2
โข (๐ โ (((
bday โ๐ธ)
โ ( bday โ๐น) โจ ( bday
โ๐น) โ
( bday โ๐ธ)) โจ ( bday
โ๐ธ) = ( bday โ๐น))) |
182 | 16, 172, 181 | mpjaodan 957 |
1
โข (๐ โ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ))) |