MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsproplem6 Structured version   Visualization version   GIF version

Theorem mulsproplem6 27995
Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025.)
Hypotheses
Ref Expression
mulsproplem.1 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ 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 ๐‘’))))))
mulsproplem6.1 (๐œ‘ โ†’ ๐ด โˆˆ No )
mulsproplem6.2 (๐œ‘ โ†’ ๐ต โˆˆ No )
mulsproplem6.3 (๐œ‘ โ†’ ๐‘ƒ โˆˆ ( L โ€˜๐ด))
mulsproplem6.4 (๐œ‘ โ†’ ๐‘„ โˆˆ ( L โ€˜๐ต))
mulsproplem6.5 (๐œ‘ โ†’ ๐‘‰ โˆˆ ( R โ€˜๐ด))
mulsproplem6.6 (๐œ‘ โ†’ ๐‘Š โˆˆ ( L โ€˜๐ต))
Assertion
Ref Expression
mulsproplem6 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)))
Distinct variable groups:   ๐ด,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ต,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ถ,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ท,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ธ,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐น,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐‘ƒ,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐‘„,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐‘‰,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐‘Š,๐‘,๐‘,๐‘‘,๐‘’,๐‘“
Allowed substitution hints:   ๐œ‘(๐‘’,๐‘“,๐‘Ž,๐‘,๐‘,๐‘‘)   ๐‘„(๐‘Ž)   ๐‘Š(๐‘Ž)

Proof of Theorem mulsproplem6
StepHypRef Expression
1 leftssno 27781 . . . 4 ( L โ€˜๐ต) โІ No
2 mulsproplem6.4 . . . 4 (๐œ‘ โ†’ ๐‘„ โˆˆ ( L โ€˜๐ต))
31, 2sselid 3976 . . 3 (๐œ‘ โ†’ ๐‘„ โˆˆ No )
4 mulsproplem6.6 . . . 4 (๐œ‘ โ†’ ๐‘Š โˆˆ ( L โ€˜๐ต))
51, 4sselid 3976 . . 3 (๐œ‘ โ†’ ๐‘Š โˆˆ No )
6 sltlin 27656 . . 3 ((๐‘„ โˆˆ No โˆง ๐‘Š โˆˆ No ) โ†’ (๐‘„ <s ๐‘Š โˆจ ๐‘„ = ๐‘Š โˆจ ๐‘Š <s ๐‘„))
73, 5, 6syl2anc 583 . 2 (๐œ‘ โ†’ (๐‘„ <s ๐‘Š โˆจ ๐‘„ = ๐‘Š โˆจ ๐‘Š <s ๐‘„))
8 mulsproplem.1 . . . . . . . . 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 ๐‘’))))))
9 leftssold 27779 . . . . . . . . . 10 ( L โ€˜๐ด) โІ ( O โ€˜( bday โ€˜๐ด))
10 mulsproplem6.3 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ƒ โˆˆ ( L โ€˜๐ด))
119, 10sselid 3976 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ƒ โˆˆ ( O โ€˜( bday โ€˜๐ด)))
12 mulsproplem6.2 . . . . . . . . 9 (๐œ‘ โ†’ ๐ต โˆˆ No )
138, 11, 12mulsproplem2 27991 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒ ยทs ๐ต) โˆˆ No )
14 mulsproplem6.1 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โˆˆ No )
15 leftssold 27779 . . . . . . . . . 10 ( L โ€˜๐ต) โІ ( O โ€˜( bday โ€˜๐ต))
1615, 2sselid 3976 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘„ โˆˆ ( O โ€˜( bday โ€˜๐ต)))
178, 14, 16mulsproplem3 27992 . . . . . . . 8 (๐œ‘ โ†’ (๐ด ยทs ๐‘„) โˆˆ No )
1813, 17addscld 27871 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) โˆˆ No )
198, 11, 16mulsproplem4 27993 . . . . . . 7 (๐œ‘ โ†’ (๐‘ƒ ยทs ๐‘„) โˆˆ No )
2018, 19subscld 27947 . . . . . 6 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) โˆˆ No )
2120adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) โˆˆ No )
2215, 4sselid 3976 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘Š โˆˆ ( O โ€˜( bday โ€˜๐ต)))
238, 14, 22mulsproplem3 27992 . . . . . . . 8 (๐œ‘ โ†’ (๐ด ยทs ๐‘Š) โˆˆ No )
2413, 23addscld 27871 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) โˆˆ No )
258, 11, 22mulsproplem4 27993 . . . . . . 7 (๐œ‘ โ†’ (๐‘ƒ ยทs ๐‘Š) โˆˆ No )
2624, 25subscld 27947 . . . . . 6 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘ƒ ยทs ๐‘Š)) โˆˆ No )
2726adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘ƒ ยทs ๐‘Š)) โˆˆ No )
28 rightssold 27780 . . . . . . . . . 10 ( R โ€˜๐ด) โІ ( O โ€˜( bday โ€˜๐ด))
29 mulsproplem6.5 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘‰ โˆˆ ( R โ€˜๐ด))
3028, 29sselid 3976 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‰ โˆˆ ( O โ€˜( bday โ€˜๐ด)))
318, 30, 12mulsproplem2 27991 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‰ ยทs ๐ต) โˆˆ No )
3231, 23addscld 27871 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) โˆˆ No )
338, 30, 22mulsproplem4 27993 . . . . . . 7 (๐œ‘ โ†’ (๐‘‰ ยทs ๐‘Š) โˆˆ No )
3432, 33subscld 27947 . . . . . 6 (๐œ‘ โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)) โˆˆ No )
3534adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)) โˆˆ No )
36 ssltleft 27771 . . . . . . . . . . 11 (๐ด โˆˆ No โ†’ ( L โ€˜๐ด) <<s {๐ด})
3714, 36syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ( L โ€˜๐ด) <<s {๐ด})
38 snidg 4658 . . . . . . . . . . 11 (๐ด โˆˆ No โ†’ ๐ด โˆˆ {๐ด})
3914, 38syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ด โˆˆ {๐ด})
4037, 10, 39ssltsepcd 27701 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ƒ <s ๐ด)
41 0sno 27733 . . . . . . . . . . . 12 0s โˆˆ No
4241a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 0s โˆˆ No )
43 leftssno 27781 . . . . . . . . . . . 12 ( L โ€˜๐ด) โІ No
4443, 10sselid 3976 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ƒ โˆˆ No )
45 bday0s 27735 . . . . . . . . . . . . . . . 16 ( bday โ€˜ 0s ) = โˆ…
4645, 45oveq12i 7426 . . . . . . . . . . . . . . 15 (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) = (โˆ… +no โˆ…)
47 0elon 6417 . . . . . . . . . . . . . . . 16 โˆ… โˆˆ On
48 naddrid 8695 . . . . . . . . . . . . . . . 16 (โˆ… โˆˆ On โ†’ (โˆ… +no โˆ…) = โˆ…)
4947, 48ax-mp 5 . . . . . . . . . . . . . . 15 (โˆ… +no โˆ…) = โˆ…
5046, 49eqtri 2755 . . . . . . . . . . . . . 14 (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) = โˆ…
5150uneq1i 4155 . . . . . . . . . . . . 13 ((( 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 โ€˜๐‘„)))))
52 0un 4388 . . . . . . . . . . . . 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 โ€˜๐‘„))))
5351, 52eqtri 2755 . . . . . . . . . . . 12 ((( 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 โ€˜๐‘„))))
54 oldbdayim 27789 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โˆˆ ( O โ€˜( bday โ€˜๐ด)) โ†’ ( bday โ€˜๐‘ƒ) โˆˆ ( bday โ€˜๐ด))
5511, 54syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ( bday โ€˜๐‘ƒ) โˆˆ ( bday โ€˜๐ด))
56 oldbdayim 27789 . . . . . . . . . . . . . . . . 17 (๐‘„ โˆˆ ( O โ€˜( bday โ€˜๐ต)) โ†’ ( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต))
5716, 56syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต))
58 bdayelon 27683 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐ด) โˆˆ On
59 bdayelon 27683 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐ต) โˆˆ On
60 naddel12 8712 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ ((( bday โ€˜๐‘ƒ) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
6158, 59, 60mp2an 691 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘ƒ) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
6255, 57, 61syl2anc 583 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
63 oldbdayim 27789 . . . . . . . . . . . . . . . . 17 (๐‘Š โˆˆ ( O โ€˜( bday โ€˜๐ต)) โ†’ ( bday โ€˜๐‘Š) โˆˆ ( bday โ€˜๐ต))
6422, 63syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ( bday โ€˜๐‘Š) โˆˆ ( bday โ€˜๐ต))
65 bdayelon 27683 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐‘Š) โˆˆ On
66 naddel2 8700 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘Š) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On โˆง ( bday โ€˜๐ด) โˆˆ On) โ†’ (( bday โ€˜๐‘Š) โˆˆ ( bday โ€˜๐ต) โ†” (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
6765, 59, 58, 66mp3an 1458 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘Š) โˆˆ ( bday โ€˜๐ต) โ†” (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
6864, 67sylib 217 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
6962, 68jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
70 naddel12 8712 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ ((( bday โ€˜๐‘ƒ) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘Š) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
7158, 59, 70mp2an 691 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘ƒ) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘Š) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
7255, 64, 71syl2anc 583 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
73 bdayelon 27683 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐‘„) โˆˆ On
74 naddel2 8700 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘„) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On โˆง ( bday โ€˜๐ด) โˆˆ On) โ†’ (( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต) โ†” (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
7573, 59, 58, 74mp3an 1458 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต) โ†” (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
7657, 75sylib 217 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
7772, 76jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
78 bdayelon 27683 . . . . . . . . . . . . . . . . . 18 ( bday โ€˜๐‘ƒ) โˆˆ On
79 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐‘ƒ) โˆˆ On โˆง ( bday โ€˜๐‘„) โˆˆ On) โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ On)
8078, 73, 79mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ On
81 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐‘Š) โˆˆ On) โ†’ (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ On)
8258, 65, 81mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ On
8380, 82onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š))) โˆˆ On
84 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐‘ƒ) โˆˆ On โˆง ( bday โ€˜๐‘Š) โˆˆ On) โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ On)
8578, 65, 84mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ On
86 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐‘„) โˆˆ On) โ†’ (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ On)
8758, 73, 86mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ On
8885, 87onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„))) โˆˆ On
89 naddcl 8689 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On)
9058, 59, 89mp2an 691 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On
91 onunel 6468 . . . . . . . . . . . . . . . 16 ((((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š))) โˆˆ On โˆง ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„))) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ ((((( 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 โ€˜๐ต)))))
9283, 88, 90, 91mp3an 1458 . . . . . . . . . . . . . . 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 โ€˜๐‘Š)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
93 onunel 6468 . . . . . . . . . . . . . . . . 17 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
9480, 82, 90, 93mp3an 1458 . . . . . . . . . . . . . . . 16 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
95 onunel 6468 . . . . . . . . . . . . . . . . 17 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
9685, 87, 90, 95mp3an 1458 . . . . . . . . . . . . . . . 16 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
9794, 96anbi12i 626 . . . . . . . . . . . . . . 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 โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))) โˆง ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
9892, 97bitri 275 . . . . . . . . . . . . . 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 โ€˜๐ต)))))
9969, 77, 98sylanbrc 582 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š))) โˆช ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
100 elun1 4172 . . . . . . . . . . . . 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 โ€˜๐ธ))))))
10199, 100syl 17 . . . . . . . . . . . 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 โ€˜๐ธ))))))
10253, 101eqeltrid 2832 . . . . . . . . . . 11 (๐œ‘ โ†’ ((( 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 โ€˜๐ธ))))))
1038, 42, 42, 44, 14, 3, 5, 102mulsproplem1 27990 . . . . . . . . . 10 (๐œ‘ โ†’ (( 0s ยทs 0s ) โˆˆ No โˆง ((๐‘ƒ <s ๐ด โˆง ๐‘„ <s ๐‘Š) โ†’ ((๐‘ƒ ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐ด ยทs ๐‘„)))))
104103simprd 495 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ƒ <s ๐ด โˆง ๐‘„ <s ๐‘Š) โ†’ ((๐‘ƒ ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐ด ยทs ๐‘„))))
10540, 104mpand 694 . . . . . . . 8 (๐œ‘ โ†’ (๐‘„ <s ๐‘Š โ†’ ((๐‘ƒ ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐ด ยทs ๐‘„))))
106105imp 406 . . . . . . 7 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ ((๐‘ƒ ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐ด ยทs ๐‘„)))
10725, 23, 19, 17sltsubsub3bd 27967 . . . . . . . . 9 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐ด ยทs ๐‘„)) โ†” ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘Š))))
10817, 19subscld 27947 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„)) โˆˆ No )
10923, 25subscld 27947 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘Š)) โˆˆ No )
110108, 109, 13sltadd2d 27888 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘Š)) โ†” ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„))) <s ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘Š)))))
111107, 110bitrd 279 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐ด ยทs ๐‘„)) โ†” ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„))) <s ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘Š)))))
112111adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ (((๐‘ƒ ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐ด ยทs ๐‘„)) โ†” ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„))) <s ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘Š)))))
113106, 112mpbid 231 . . . . . 6 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„))) <s ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘Š))))
11413, 17, 19addsubsassd 27963 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) = ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„))))
115114adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) = ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„))))
11613, 23, 25addsubsassd 27963 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘ƒ ยทs ๐‘Š)) = ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘Š))))
117116adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘ƒ ยทs ๐‘Š)) = ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘ƒ ยทs ๐‘Š))))
118113, 115, 1173brtr4d 5174 . . . . 5 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘ƒ ยทs ๐‘Š)))
119 lltropt 27773 . . . . . . . . . . 11 ( L โ€˜๐ด) <<s ( R โ€˜๐ด)
120119a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ ( L โ€˜๐ด) <<s ( R โ€˜๐ด))
121120, 10, 29ssltsepcd 27701 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ƒ <s ๐‘‰)
122 ssltleft 27771 . . . . . . . . . . 11 (๐ต โˆˆ No โ†’ ( L โ€˜๐ต) <<s {๐ต})
12312, 122syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ( L โ€˜๐ต) <<s {๐ต})
124 snidg 4658 . . . . . . . . . . 11 (๐ต โˆˆ No โ†’ ๐ต โˆˆ {๐ต})
12512, 124syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ต โˆˆ {๐ต})
126123, 4, 125ssltsepcd 27701 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘Š <s ๐ต)
127 rightssno 27782 . . . . . . . . . . . 12 ( R โ€˜๐ด) โІ No
128127, 29sselid 3976 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘‰ โˆˆ No )
12950uneq1i 4155 . . . . . . . . . . . . 13 ((( 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 โ€˜๐‘Š)))))
130 0un 4388 . . . . . . . . . . . . 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 โ€˜๐‘Š))))
131129, 130eqtri 2755 . . . . . . . . . . . 12 ((( 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 โ€˜๐‘Š))))
132 oldbdayim 27789 . . . . . . . . . . . . . . . . 17 (๐‘‰ โˆˆ ( O โ€˜( bday โ€˜๐ด)) โ†’ ( bday โ€˜๐‘‰) โˆˆ ( bday โ€˜๐ด))
13330, 132syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ( bday โ€˜๐‘‰) โˆˆ ( bday โ€˜๐ด))
134 bdayelon 27683 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐‘‰) โˆˆ On
135 naddel1 8699 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘‰) โˆˆ On โˆง ( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ (( bday โ€˜๐‘‰) โˆˆ ( bday โ€˜๐ด) โ†” (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
136134, 58, 59, 135mp3an 1458 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘‰) โˆˆ ( bday โ€˜๐ด) โ†” (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
137133, 136sylib 217 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
13872, 137jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
139 naddel1 8699 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ƒ) โˆˆ On โˆง ( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ (( bday โ€˜๐‘ƒ) โˆˆ ( bday โ€˜๐ด) โ†” (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
14078, 58, 59, 139mp3an 1458 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ƒ) โˆˆ ( bday โ€˜๐ด) โ†” (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
14155, 140sylib 217 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
142 naddel12 8712 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ ((( bday โ€˜๐‘‰) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘Š) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
14358, 59, 142mp2an 691 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘‰) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘Š) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
144133, 64, 143syl2anc 583 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
145141, 144jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
146 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐‘‰) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ On)
147134, 59, 146mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ On
14885, 147onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต))) โˆˆ On
149 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐‘ƒ) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ On)
15078, 59, 149mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ On
151 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐‘‰) โˆˆ On โˆง ( bday โ€˜๐‘Š) โˆˆ On) โ†’ (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ On)
152134, 65, 151mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ On
153150, 152onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š))) โˆˆ On
154 onunel 6468 . . . . . . . . . . . . . . . 16 ((((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต))) โˆˆ On โˆง ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š))) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ ((((( 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 โ€˜๐ต)))))
155148, 153, 90, 154mp3an 1458 . . . . . . . . . . . . . . 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 โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
156 onunel 6468 . . . . . . . . . . . . . . . . 17 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ On โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
15785, 147, 90, 156mp3an 1458 . . . . . . . . . . . . . . . 16 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
158 onunel 6468 . . . . . . . . . . . . . . . . 17 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ On โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
159150, 152, 90, 158mp3an 1458 . . . . . . . . . . . . . . . 16 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
160157, 159anbi12i 626 . . . . . . . . . . . . . . 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 โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))) โˆง ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
161155, 160bitri 275 . . . . . . . . . . . . . 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 โ€˜๐ต)))))
162138, 145, 161sylanbrc 582 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต))) โˆช ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
163 elun1 4172 . . . . . . . . . . . . 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 โ€˜๐ธ))))))
164162, 163syl 17 . . . . . . . . . . . 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 โ€˜๐ธ))))))
165131, 164eqeltrid 2832 . . . . . . . . . . 11 (๐œ‘ โ†’ ((( 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 โ€˜๐ธ))))))
1668, 42, 42, 44, 128, 5, 12, 165mulsproplem1 27990 . . . . . . . . . 10 (๐œ‘ โ†’ (( 0s ยทs 0s ) โˆˆ No โˆง ((๐‘ƒ <s ๐‘‰ โˆง ๐‘Š <s ๐ต) โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘Š)))))
167166simprd 495 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ƒ <s ๐‘‰ โˆง ๐‘Š <s ๐ต) โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘Š))))
168121, 126, 167mp2and 698 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘Š)))
16913, 25subscld 27947 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘Š)) โˆˆ No )
17031, 33subscld 27947 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘Š)) โˆˆ No )
171169, 170, 23sltadd1d 27889 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘Š)) โ†” (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘Š)) +s (๐ด ยทs ๐‘Š)) <s (((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘Š)) +s (๐ด ยทs ๐‘Š))))
172168, 171mpbid 231 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘Š)) +s (๐ด ยทs ๐‘Š)) <s (((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘Š)) +s (๐ด ยทs ๐‘Š)))
17313, 23, 25addsubsd 27964 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘ƒ ยทs ๐‘Š)) = (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘Š)) +s (๐ด ยทs ๐‘Š)))
17431, 23, 33addsubsd 27964 . . . . . . 7 (๐œ‘ โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)) = (((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘Š)) +s (๐ด ยทs ๐‘Š)))
175172, 173, 1743brtr4d 5174 . . . . . 6 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘ƒ ยทs ๐‘Š)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)))
176175adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘ƒ ยทs ๐‘Š)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)))
17721, 27, 35, 118, 176slttrd 27666 . . . 4 ((๐œ‘ โˆง ๐‘„ <s ๐‘Š) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)))
178177ex 412 . . 3 (๐œ‘ โ†’ (๐‘„ <s ๐‘Š โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š))))
179 oveq2 7422 . . . . . . 7 (๐‘„ = ๐‘Š โ†’ (๐ด ยทs ๐‘„) = (๐ด ยทs ๐‘Š))
180179oveq2d 7430 . . . . . 6 (๐‘„ = ๐‘Š โ†’ ((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) = ((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)))
181 oveq2 7422 . . . . . 6 (๐‘„ = ๐‘Š โ†’ (๐‘ƒ ยทs ๐‘„) = (๐‘ƒ ยทs ๐‘Š))
182180, 181oveq12d 7432 . . . . 5 (๐‘„ = ๐‘Š โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) = (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘ƒ ยทs ๐‘Š)))
183182breq1d 5152 . . . 4 (๐‘„ = ๐‘Š โ†’ ((((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)) โ†” (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘ƒ ยทs ๐‘Š)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š))))
184175, 183syl5ibrcom 246 . . 3 (๐œ‘ โ†’ (๐‘„ = ๐‘Š โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š))))
18520adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) โˆˆ No )
18631, 17addscld 27871 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) โˆˆ No )
1878, 30, 16mulsproplem4 27993 . . . . . . 7 (๐œ‘ โ†’ (๐‘‰ ยทs ๐‘„) โˆˆ No )
188186, 187subscld 27947 . . . . . 6 (๐œ‘ โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘‰ ยทs ๐‘„)) โˆˆ No )
189188adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘‰ ยทs ๐‘„)) โˆˆ No )
19034adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)) โˆˆ No )
191123, 2, 125ssltsepcd 27701 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘„ <s ๐ต)
19250uneq1i 4155 . . . . . . . . . . . . 13 ((( 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 โ€˜๐‘„)))))
193 0un 4388 . . . . . . . . . . . . 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 โ€˜๐‘„))))
194192, 193eqtri 2755 . . . . . . . . . . . 12 ((( 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 โ€˜๐‘„))))
19562, 137jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
196 naddel12 8712 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ ((( bday โ€˜๐‘‰) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
19758, 59, 196mp2an 691 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘‰) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
198133, 57, 197syl2anc 583 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
199141, 198jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
20080, 147onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต))) โˆˆ On
201 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐‘‰) โˆˆ On โˆง ( bday โ€˜๐‘„) โˆˆ On) โ†’ (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ On)
202134, 73, 201mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ On
203150, 202onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„))) โˆˆ On
204 onunel 6468 . . . . . . . . . . . . . . . 16 ((((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต))) โˆˆ On โˆง ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„))) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ ((((( 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 โ€˜๐ต)))))
205200, 203, 90, 204mp3an 1458 . . . . . . . . . . . . . . 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 โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
206 onunel 6468 . . . . . . . . . . . . . . . . 17 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ On โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
20780, 147, 90, 206mp3an 1458 . . . . . . . . . . . . . . . 16 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
208 onunel 6468 . . . . . . . . . . . . . . . . 17 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ On โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
209150, 202, 90, 208mp3an 1458 . . . . . . . . . . . . . . . 16 (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
210207, 209anbi12i 626 . . . . . . . . . . . . . . 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 โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))) โˆง ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
211205, 210bitri 275 . . . . . . . . . . . . . 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 โ€˜๐ต)))))
212195, 199, 211sylanbrc 582 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐ต))) โˆช ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
213 elun1 4172 . . . . . . . . . . . . 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 โ€˜๐ธ))))))
214212, 213syl 17 . . . . . . . . . . . 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 โ€˜๐ธ))))))
215194, 214eqeltrid 2832 . . . . . . . . . . 11 (๐œ‘ โ†’ ((( 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 โ€˜๐ธ))))))
2168, 42, 42, 44, 128, 3, 12, 215mulsproplem1 27990 . . . . . . . . . 10 (๐œ‘ โ†’ (( 0s ยทs 0s ) โˆˆ No โˆง ((๐‘ƒ <s ๐‘‰ โˆง ๐‘„ <s ๐ต) โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘„)))))
217216simprd 495 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ƒ <s ๐‘‰ โˆง ๐‘„ <s ๐ต) โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘„))))
218121, 191, 217mp2and 698 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘„)))
21913, 19subscld 27947 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) โˆˆ No )
22031, 187subscld 27947 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘„)) โˆˆ No )
221219, 220, 17sltadd1d 27889 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘„)) โ†” (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„))))
222218, 221mpbid 231 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)))
22313, 17, 19addsubsd 27964 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) = (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)))
22431, 17, 187addsubsd 27964 . . . . . . 7 (๐œ‘ โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘‰ ยทs ๐‘„)) = (((๐‘‰ ยทs ๐ต) -s (๐‘‰ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)))
225222, 223, 2243brtr4d 5174 . . . . . 6 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘‰ ยทs ๐‘„)))
226225adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘‰ ยทs ๐‘„)))
227 ssltright 27772 . . . . . . . . . . 11 (๐ด โˆˆ No โ†’ {๐ด} <<s ( R โ€˜๐ด))
22814, 227syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ {๐ด} <<s ( R โ€˜๐ด))
229228, 39, 29ssltsepcd 27701 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด <s ๐‘‰)
23050uneq1i 4155 . . . . . . . . . . . . 13 ((( 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 โ€˜๐‘Š)))))
231 0un 4388 . . . . . . . . . . . . 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 โ€˜๐‘Š))))
232230, 231eqtri 2755 . . . . . . . . . . . 12 ((( 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 โ€˜๐‘Š))))
23368, 198jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
23476, 144jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
23582, 202onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„))) โˆˆ On
23687, 152onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š))) โˆˆ On
237 onunel 6468 . . . . . . . . . . . . . . . 16 ((((( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„))) โˆˆ On โˆง ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š))) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ ((((( 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 โ€˜๐ต)))))
238235, 236, 90, 237mp3an 1458 . . . . . . . . . . . . . . 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 โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
239 onunel 6468 . . . . . . . . . . . . . . . . 17 (((( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ On โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ (((( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
24082, 202, 90, 239mp3an 1458 . . . . . . . . . . . . . . . 16 (((( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
241 onunel 6468 . . . . . . . . . . . . . . . . 17 (((( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ On โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ On โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆˆ On) โ†’ (((( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
24287, 152, 90, 241mp3an 1458 . . . . . . . . . . . . . . . 16 (((( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
243240, 242anbi12i 626 . . . . . . . . . . . . . . 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 โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))) โˆง ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))))
244238, 243bitri 275 . . . . . . . . . . . . . 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 โ€˜๐ต)))))
245233, 234, 244sylanbrc 582 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((( bday โ€˜๐ด) +no ( bday โ€˜๐‘Š)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘„))) โˆช ((( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐‘‰) +no ( bday โ€˜๐‘Š)))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
246 elun1 4172 . . . . . . . . . . . . 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 โ€˜๐ธ))))))
247245, 246syl 17 . . . . . . . . . . . 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 โ€˜๐ธ))))))
248232, 247eqeltrid 2832 . . . . . . . . . . 11 (๐œ‘ โ†’ ((( 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 โ€˜๐ธ))))))
2498, 42, 42, 14, 128, 5, 3, 248mulsproplem1 27990 . . . . . . . . . 10 (๐œ‘ โ†’ (( 0s ยทs 0s ) โˆˆ No โˆง ((๐ด <s ๐‘‰ โˆง ๐‘Š <s ๐‘„) โ†’ ((๐ด ยทs ๐‘„) -s (๐ด ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘Š)))))
250249simprd 495 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ด <s ๐‘‰ โˆง ๐‘Š <s ๐‘„) โ†’ ((๐ด ยทs ๐‘„) -s (๐ด ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘Š))))
251229, 250mpand 694 . . . . . . . 8 (๐œ‘ โ†’ (๐‘Š <s ๐‘„ โ†’ ((๐ด ยทs ๐‘„) -s (๐ด ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘Š))))
252251imp 406 . . . . . . 7 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ ((๐ด ยทs ๐‘„) -s (๐ด ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘Š)))
25317, 187, 23, 33sltsubsubbd 27965 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด ยทs ๐‘„) -s (๐ด ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘Š)) โ†” ((๐ด ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐‘‰ ยทs ๐‘Š))))
25417, 187subscld 27947 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘„)) โˆˆ No )
25523, 33subscld 27947 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยทs ๐‘Š) -s (๐‘‰ ยทs ๐‘Š)) โˆˆ No )
256254, 255, 31sltadd2d 27888 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘Š) -s (๐‘‰ ยทs ๐‘Š)) โ†” ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘„))) <s ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘‰ ยทs ๐‘Š)))))
257253, 256bitrd 279 . . . . . . . 8 (๐œ‘ โ†’ (((๐ด ยทs ๐‘„) -s (๐ด ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘Š)) โ†” ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘„))) <s ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘‰ ยทs ๐‘Š)))))
258257adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ (((๐ด ยทs ๐‘„) -s (๐ด ยทs ๐‘Š)) <s ((๐‘‰ ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘Š)) โ†” ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘„))) <s ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘‰ ยทs ๐‘Š)))))
259252, 258mpbid 231 . . . . . 6 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘„))) <s ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘‰ ยทs ๐‘Š))))
26031, 17, 187addsubsassd 27963 . . . . . . 7 (๐œ‘ โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘‰ ยทs ๐‘„)) = ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘„))))
261260adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘‰ ยทs ๐‘„)) = ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘‰ ยทs ๐‘„))))
26231, 23, 33addsubsassd 27963 . . . . . . 7 (๐œ‘ โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)) = ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘‰ ยทs ๐‘Š))))
263262adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)) = ((๐‘‰ ยทs ๐ต) +s ((๐ด ยทs ๐‘Š) -s (๐‘‰ ยทs ๐‘Š))))
264259, 261, 2633brtr4d 5174 . . . . 5 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘‰ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)))
265185, 189, 190, 226, 264slttrd 27666 . . . 4 ((๐œ‘ โˆง ๐‘Š <s ๐‘„) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)))
266265ex 412 . . 3 (๐œ‘ โ†’ (๐‘Š <s ๐‘„ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š))))
267178, 184, 2663jaod 1426 . 2 (๐œ‘ โ†’ ((๐‘„ <s ๐‘Š โˆจ ๐‘„ = ๐‘Š โˆจ ๐‘Š <s ๐‘„) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š))))
2687, 267mpd 15 1 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‰ ยทs ๐ต) +s (๐ด ยทs ๐‘Š)) -s (๐‘‰ ยทs ๐‘Š)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ w3o 1084   = wceq 1534   โˆˆ wcel 2099  โˆ€wral 3056   โˆช cun 3942  โˆ…c0 4318  {csn 4624   class class class wbr 5142  Oncon0 6363  โ€˜cfv 6542  (class class class)co 7414   +no cnadd 8677   No csur 27547   <s cslt 27548   bday cbday 27549   <<s csslt 27687   0s c0s 27729   O cold 27744   L cleft 27746   R cright 27747   +s cadds 27850   -s csubs 27907   ยทs cmuls 27980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-ot 4633  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7985  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-1o 8478  df-2o 8479  df-nadd 8678  df-no 27550  df-slt 27551  df-bday 27552  df-sle 27652  df-sslt 27688  df-scut 27690  df-0s 27731  df-made 27748  df-old 27749  df-left 27751  df-right 27752  df-norec 27829  df-norec2 27840  df-adds 27851  df-negs 27908  df-subs 27909
This theorem is referenced by:  mulsproplem9  27998
  Copyright terms: Public domain W3C validator