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