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

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

Proof of Theorem mulsproplem5
StepHypRef Expression
1 leftssno 27781 . . . 4 ( L โ€˜๐ด) โІ No
2 mulsproplem5.3 . . . 4 (๐œ‘ โ†’ ๐‘ƒ โˆˆ ( L โ€˜๐ด))
31, 2sselid 3976 . . 3 (๐œ‘ โ†’ ๐‘ƒ โˆˆ No )
4 mulsproplem5.5 . . . 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 โ€˜๐ด))
109, 2sselid 3976 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ƒ โˆˆ ( O โ€˜( bday โ€˜๐ด)))
11 mulsproplem5.2 . . . . . . . . 9 (๐œ‘ โ†’ ๐ต โˆˆ No )
128, 10, 11mulsproplem2 27991 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒ ยทs ๐ต) โˆˆ No )
13 mulsproplem5.1 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โˆˆ No )
14 leftssold 27779 . . . . . . . . . 10 ( L โ€˜๐ต) โІ ( O โ€˜( bday โ€˜๐ต))
15 mulsproplem5.4 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘„ โˆˆ ( L โ€˜๐ต))
1614, 15sselid 3976 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘„ โˆˆ ( O โ€˜( bday โ€˜๐ต)))
178, 13, 16mulsproplem3 27992 . . . . . . . 8 (๐œ‘ โ†’ (๐ด ยทs ๐‘„) โˆˆ No )
1812, 17addscld 27871 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) โˆˆ No )
198, 10, 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 )
229, 4sselid 3976 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‡ โˆˆ ( O โ€˜( bday โ€˜๐ด)))
238, 22, 11mulsproplem2 27991 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‡ ยทs ๐ต) โˆˆ No )
2423, 17addscld 27871 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) โˆˆ No )
258, 22, 16mulsproplem4 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 mulsproplem5.6 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ˆ โˆˆ ( R โ€˜๐ต))
3028, 29sselid 3976 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ˆ โˆˆ ( O โ€˜( bday โ€˜๐ต)))
318, 13, 30mulsproplem3 27992 . . . . . . . 8 (๐œ‘ โ†’ (๐ด ยทs ๐‘ˆ) โˆˆ No )
3223, 31addscld 27871 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) โˆˆ No )
338, 22, 30mulsproplem4 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 {๐ต})
3711, 36syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ( L โ€˜๐ต) <<s {๐ต})
38 snidg 4658 . . . . . . . . . . 11 (๐ต โˆˆ No โ†’ ๐ต โˆˆ {๐ต})
3911, 38syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ต โˆˆ {๐ต})
4037, 15, 39ssltsepcd 27701 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘„ <s ๐ต)
41 0sno 27733 . . . . . . . . . . . 12 0s โˆˆ No
4241a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 0s โˆˆ No )
43 leftssno 27781 . . . . . . . . . . . 12 ( L โ€˜๐ต) โІ No
4443, 15sselid 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 โ€˜๐ด))
5510, 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 naddel1 8699 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘‡) โˆˆ On โˆง ( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ (( bday โ€˜๐‘‡) โˆˆ ( bday โ€˜๐ด) โ†” (( bday โ€˜๐‘‡) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
6765, 58, 59, 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 bdayelon 27683 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐‘ƒ) โˆˆ On
71 naddel1 8699 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ƒ) โˆˆ On โˆง ( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ (( bday โ€˜๐‘ƒ) โˆˆ ( bday โ€˜๐ด) โ†” (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
7270, 58, 59, 71mp3an 1458 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ƒ) โˆˆ ( bday โ€˜๐ด) โ†” (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
7355, 72sylib 217 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
74 naddel12 8712 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ ((( bday โ€˜๐‘‡) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
7558, 59, 74mp2an 691 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘‡) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
7664, 57, 75syl2anc 583 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
7773, 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)
8070, 78, 79mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆˆ On
81 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐‘‡) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ (( bday โ€˜๐‘‡) +no ( bday โ€˜๐ต)) โˆˆ On)
8265, 59, 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)
8570, 59, 84mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ On
86 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐‘‡) โˆˆ On โˆง ( bday โ€˜๐‘„) โˆˆ On) โ†’ (( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘„)) โˆˆ On)
8765, 78, 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, 3, 5, 44, 11, 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, 104mpan2d 693 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒ <s ๐‘‡ โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘„))))
106105imp 406 . . . . . . 7 ((๐œ‘ โˆง ๐‘ƒ <s ๐‘‡) โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘„)))
10712, 19subscld 27947 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) โˆˆ No )
10823, 25subscld 27947 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘„)) โˆˆ No )
109107, 108, 17sltadd1d 27889 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘„)) โ†” (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)) <s (((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„))))
110109adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘ƒ <s ๐‘‡) โ†’ (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘„)) โ†” (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)) <s (((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„))))
111106, 110mpbid 231 . . . . . 6 ((๐œ‘ โˆง ๐‘ƒ <s ๐‘‡) โ†’ (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)) <s (((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)))
11212, 17, 19addsubsd 27964 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) = (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)))
113112adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘ƒ <s ๐‘‡) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) = (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘„)) +s (๐ด ยทs ๐‘„)))
11423, 17, 25addsubsd 27964 . . . . . . 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 ๐‘„)))
116111, 113, 1153brtr4d 5174 . . . . 5 ((๐œ‘ โˆง ๐‘ƒ <s ๐‘‡) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘‡ ยทs ๐‘„)))
117 ssltleft 27771 . . . . . . . . . . 11 (๐ด โˆˆ No โ†’ ( L โ€˜๐ด) <<s {๐ด})
11813, 117syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ( L โ€˜๐ด) <<s {๐ด})
119 snidg 4658 . . . . . . . . . . 11 (๐ด โˆˆ No โ†’ ๐ด โˆˆ {๐ด})
12013, 119syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ด โˆˆ {๐ด})
121118, 4, 120ssltsepcd 27701 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‡ <s ๐ด)
122 lltropt 27773 . . . . . . . . . . 11 ( L โ€˜๐ต) <<s ( R โ€˜๐ต)
123122a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ ( L โ€˜๐ต) <<s ( R โ€˜๐ต))
124123, 15, 29ssltsepcd 27701 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘„ <s ๐‘ˆ)
125 rightssno 27782 . . . . . . . . . . . 12 ( R โ€˜๐ต) โІ No
126125, 29sselid 3976 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ˆ โˆˆ No )
12750uneq1i 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 โ€˜๐‘„)))))
128 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 โ€˜๐‘„))))
129127, 128eqtri 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 โ€˜๐‘„))))
130 oldbdayim 27789 . . . . . . . . . . . . . . . . 17 (๐‘ˆ โˆˆ ( O โ€˜( bday โ€˜๐ต)) โ†’ ( bday โ€˜๐‘ˆ) โˆˆ ( bday โ€˜๐ต))
13130, 130syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ( bday โ€˜๐‘ˆ) โˆˆ ( bday โ€˜๐ต))
132 bdayelon 27683 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐‘ˆ) โˆˆ On
133 naddel2 8700 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ˆ) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On โˆง ( bday โ€˜๐ด) โˆˆ On) โ†’ (( bday โ€˜๐‘ˆ) โˆˆ ( bday โ€˜๐ต) โ†” (( bday โ€˜๐ด) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
134132, 59, 58, 133mp3an 1458 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ˆ) โˆˆ ( bday โ€˜๐ต) โ†” (( bday โ€˜๐ด) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
135131, 134sylib 217 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐ด) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
13676, 135jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
137 naddel12 8712 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On) โ†’ ((( bday โ€˜๐‘‡) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘ˆ) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
13858, 59, 137mp2an 691 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘‡) โˆˆ ( bday โ€˜๐ด) โˆง ( bday โ€˜๐‘ˆ) โˆˆ ( bday โ€˜๐ต)) โ†’ (( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
13964, 131, 138syl2anc 583 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
140 naddel2 8700 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘„) โˆˆ On โˆง ( bday โ€˜๐ต) โˆˆ On โˆง ( bday โ€˜๐ด) โˆˆ On) โ†’ (( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต) โ†” (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
14178, 59, 58, 140mp3an 1458 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘„) โˆˆ ( bday โ€˜๐ต) โ†” (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
14257, 141sylib 217 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
143139, 142jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
144 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐‘ˆ) โˆˆ On) โ†’ (( bday โ€˜๐ด) +no ( bday โ€˜๐‘ˆ)) โˆˆ On)
14558, 132, 144mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐ด) +no ( bday โ€˜๐‘ˆ)) โˆˆ On
14687, 145onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘ˆ))) โˆˆ On
147 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐‘‡) โˆˆ On โˆง ( bday โ€˜๐‘ˆ) โˆˆ On) โ†’ (( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆˆ On)
14865, 132, 147mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆˆ On
149 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐ด) โˆˆ On โˆง ( bday โ€˜๐‘„) โˆˆ On) โ†’ (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ On)
15058, 78, 149mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ On
151148, 150onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„))) โˆˆ On
152 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 โ€˜๐ต)))))
153146, 151, 90, 152mp3an 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 โ€˜๐ต))))
154 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 โ€˜๐ต)))))
15587, 145, 90, 154mp3an 1458 . . . . . . . . . . . . . . . 16 (((( 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 โ€˜๐ต)))))
157148, 150, 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 โ€˜๐ต))))
158155, 157anbi12i 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 โ€˜๐ต)))))
159153, 158bitri 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 โ€˜๐ต)))))
160136, 143, 159sylanbrc 582 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘ˆ))) โˆช ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
161 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 โ€˜๐ธ))))))
162160, 161syl 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 โ€˜๐ธ))))))
163129, 162eqeltrid 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 โ€˜๐ธ))))))
1648, 42, 42, 5, 13, 44, 126, 163mulsproplem1 27990 . . . . . . . . . 10 (๐œ‘ โ†’ (( 0s ยทs 0s ) โˆˆ No โˆง ((๐‘‡ <s ๐ด โˆง ๐‘„ <s ๐‘ˆ) โ†’ ((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐ด ยทs ๐‘„)))))
165164simprd 495 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‡ <s ๐ด โˆง ๐‘„ <s ๐‘ˆ) โ†’ ((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐ด ยทs ๐‘„))))
166121, 124, 165mp2and 698 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐ด ยทs ๐‘„)))
16733, 31, 25, 17sltsubsub3bd 27967 . . . . . . . . 9 (๐œ‘ โ†’ (((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐ด ยทs ๐‘„)) โ†” ((๐ด ยทs ๐‘„) -s (๐‘‡ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘ˆ))))
16817, 25subscld 27947 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยทs ๐‘„) -s (๐‘‡ ยทs ๐‘„)) โˆˆ No )
16931, 33subscld 27947 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘ˆ)) โˆˆ No )
170168, 169, 23sltadd2d 27888 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด ยทs ๐‘„) -s (๐‘‡ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘ˆ)) โ†” ((๐‘‡ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘‡ ยทs ๐‘„))) <s ((๐‘‡ ยทs ๐ต) +s ((๐ด ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘ˆ)))))
171167, 170bitrd 279 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐ด ยทs ๐‘„)) โ†” ((๐‘‡ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘‡ ยทs ๐‘„))) <s ((๐‘‡ ยทs ๐ต) +s ((๐ด ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘ˆ)))))
172166, 171mpbid 231 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‡ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘‡ ยทs ๐‘„))) <s ((๐‘‡ ยทs ๐ต) +s ((๐ด ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐‘ˆ))))
17323, 17, 25addsubsassd 27963 . . . . . . 7 (๐œ‘ โ†’ (((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘‡ ยทs ๐‘„)) = ((๐‘‡ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘‡ ยทs ๐‘„))))
17423, 31, 33addsubsassd 27963 . . . . . . 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, 116, 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 oveq1 7421 . . . . . . 7 (๐‘ƒ = ๐‘‡ โ†’ (๐‘ƒ ยทs ๐ต) = (๐‘‡ ยทs ๐ต))
180179oveq1d 7429 . . . . . 6 (๐‘ƒ = ๐‘‡ โ†’ ((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) = ((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘„)))
181 oveq1 7421 . . . . . 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 )
18612, 31addscld 27871 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) โˆˆ No )
1878, 10, 30mulsproplem4 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 )
191118, 2, 120ssltsepcd 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, 135jca 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 โ€˜๐ต)))
19855, 131, 197syl2anc 583 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
199198, 142jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐ด) +no ( bday โ€˜๐‘„)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
20080, 145onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘„)) โˆช (( bday โ€˜๐ด) +no ( bday โ€˜๐‘ˆ))) โˆˆ On
201 naddcl 8689 . . . . . . . . . . . . . . . . . 18 ((( bday โ€˜๐‘ƒ) โˆˆ On โˆง ( bday โ€˜๐‘ˆ) โˆˆ On) โ†’ (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘ˆ)) โˆˆ On)
20270, 132, 201mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘ˆ)) โˆˆ On
203202, 150onun2i 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, 145, 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 โ€˜๐ต)))))
209202, 150, 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, 3, 13, 44, 126, 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 ๐‘„))))
218191, 124, 217mp2and 698 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐ด ยทs ๐‘„)))
219187, 31, 19, 17sltsubsub3bd 27967 . . . . . . . . 9 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐ด ยทs ๐‘„)) โ†” ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐‘ˆ))))
22017, 19subscld 27947 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„)) โˆˆ No )
22131, 187subscld 27947 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐‘ˆ)) โˆˆ No )
222220, 221, 12sltadd2d 27888 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐‘ˆ)) โ†” ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„))) <s ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐‘ˆ)))))
223219, 222bitrd 279 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐‘„)) <s ((๐ด ยทs ๐‘ˆ) -s (๐ด ยทs ๐‘„)) โ†” ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„))) <s ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐‘ˆ)))))
224218, 223mpbid 231 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„))) <s ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐‘ˆ))))
22512, 17, 19addsubsassd 27963 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) = ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘„) -s (๐‘ƒ ยทs ๐‘„))))
22612, 31, 187addsubsassd 27963 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) -s (๐‘ƒ ยทs ๐‘ˆ)) = ((๐‘ƒ ยทs ๐ต) +s ((๐ด ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐‘ˆ))))
227224, 225, 2263brtr4d 5174 . . . . . 6 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) -s (๐‘ƒ ยทs ๐‘ˆ)))
228227adantr 480 . . . . 5 ((๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) -s (๐‘ƒ ยทs ๐‘ˆ)))
229 ssltright 27772 . . . . . . . . . . 11 (๐ต โˆˆ No โ†’ {๐ต} <<s ( R โ€˜๐ต))
23011, 229syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ {๐ต} <<s ( R โ€˜๐ต))
231230, 39, 29ssltsepcd 27701 . . . . . . . . 9 (๐œ‘ โ†’ ๐ต <s ๐‘ˆ)
23250uneq1i 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 โ€˜๐ต)))))
233 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 โ€˜๐ต))))
234232, 233eqtri 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 โ€˜๐ต))))
235 onunel 6468 . . . . . . . . . . . . . . . 16 (((( 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 โ€˜๐ต)))))
23682, 202, 90, 235mp3an 1458 . . . . . . . . . . . . . . 15 (((( bday โ€˜๐‘‡) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘ˆ))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
23768, 198, 236sylanbrc 582 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘ˆ))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
238139, 73jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
23982, 202onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘ˆ))) โˆˆ On
240148, 85onun2i 6485 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆช (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต))) โˆˆ On
241 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 โ€˜๐ต)))))
242239, 240, 90, 241mp3an 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 โ€˜๐ต))))
243 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 โ€˜๐ต)))))
244148, 85, 90, 243mp3an 1458 . . . . . . . . . . . . . . . 16 (((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆช (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โ†” ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆง (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต))))
245244anbi2i 622 . . . . . . . . . . . . . . 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 โ€˜๐ต)))))
246242, 245bitri 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 โ€˜๐ต)))))
247237, 238, 246sylanbrc 582 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((( bday โ€˜๐‘‡) +no ( bday โ€˜๐ต)) โˆช (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐‘ˆ))) โˆช ((( bday โ€˜๐‘‡) +no ( bday โ€˜๐‘ˆ)) โˆช (( bday โ€˜๐‘ƒ) +no ( bday โ€˜๐ต)))) โˆˆ (( bday โ€˜๐ด) +no ( bday โ€˜๐ต)))
248 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 โ€˜๐ธ))))))
249247, 248syl 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 โ€˜๐ธ))))))
250234, 249eqeltrid 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 โ€˜๐ธ))))))
2518, 42, 42, 5, 3, 11, 126, 250mulsproplem1 27990 . . . . . . . . . 10 (๐œ‘ โ†’ (( 0s ยทs 0s ) โˆˆ No โˆง ((๐‘‡ <s ๐‘ƒ โˆง ๐ต <s ๐‘ˆ) โ†’ ((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐ต)) <s ((๐‘ƒ ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐ต)))))
252251simprd 495 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‡ <s ๐‘ƒ โˆง ๐ต <s ๐‘ˆ) โ†’ ((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐ต)) <s ((๐‘ƒ ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐ต))))
253231, 252mpan2d 693 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‡ <s ๐‘ƒ โ†’ ((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐ต)) <s ((๐‘ƒ ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐ต))))
254253imp 406 . . . . . . 7 ((๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ) โ†’ ((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐ต)) <s ((๐‘ƒ ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐ต)))
25533, 23, 187, 12sltsubsub2bd 27966 . . . . . . . . 9 (๐œ‘ โ†’ (((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐ต)) <s ((๐‘ƒ ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐ต)) โ†” ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘ˆ)) <s ((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘ˆ))))
25612, 187subscld 27947 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘ˆ)) โˆˆ No )
25723, 33subscld 27947 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘ˆ)) โˆˆ No )
258256, 257, 31sltadd1d 27889 . . . . . . . . 9 (๐œ‘ โ†’ (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘ˆ)) <s ((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘ˆ)) โ†” (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘ˆ)) +s (๐ด ยทs ๐‘ˆ)) <s (((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘ˆ)) +s (๐ด ยทs ๐‘ˆ))))
259255, 258bitrd 279 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐ต)) <s ((๐‘ƒ ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐ต)) โ†” (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘ˆ)) +s (๐ด ยทs ๐‘ˆ)) <s (((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘ˆ)) +s (๐ด ยทs ๐‘ˆ))))
260259adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ) โ†’ (((๐‘‡ ยทs ๐‘ˆ) -s (๐‘‡ ยทs ๐ต)) <s ((๐‘ƒ ยทs ๐‘ˆ) -s (๐‘ƒ ยทs ๐ต)) โ†” (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘ˆ)) +s (๐ด ยทs ๐‘ˆ)) <s (((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘ˆ)) +s (๐ด ยทs ๐‘ˆ))))
261254, 260mpbid 231 . . . . . 6 ((๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ) โ†’ (((๐‘ƒ ยทs ๐ต) -s (๐‘ƒ ยทs ๐‘ˆ)) +s (๐ด ยทs ๐‘ˆ)) <s (((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘ˆ)) +s (๐ด ยทs ๐‘ˆ)))
26212, 31, 187addsubsd 27964 . . . . . . 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 ๐‘ˆ)))
26423, 31, 33addsubsd 27964 . . . . . . 7 (๐œ‘ โ†’ (((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) -s (๐‘‡ ยทs ๐‘ˆ)) = (((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘ˆ)) +s (๐ด ยทs ๐‘ˆ)))
265264adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ) โ†’ (((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) -s (๐‘‡ ยทs ๐‘ˆ)) = (((๐‘‡ ยทs ๐ต) -s (๐‘‡ ยทs ๐‘ˆ)) +s (๐ด ยทs ๐‘ˆ)))
266261, 263, 2653brtr4d 5174 . . . . 5 ((๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) -s (๐‘ƒ ยทs ๐‘ˆ)) <s (((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) -s (๐‘‡ ยทs ๐‘ˆ)))
267185, 189, 190, 228, 266slttrd 27666 . . . 4 ((๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) -s (๐‘‡ ยทs ๐‘ˆ)))
268267ex 412 . . 3 (๐œ‘ โ†’ (๐‘‡ <s ๐‘ƒ โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) -s (๐‘‡ ยทs ๐‘ˆ))))
269178, 184, 2683jaod 1426 . 2 (๐œ‘ โ†’ ((๐‘ƒ <s ๐‘‡ โˆจ ๐‘ƒ = ๐‘‡ โˆจ ๐‘‡ <s ๐‘ƒ) โ†’ (((๐‘ƒ ยทs ๐ต) +s (๐ด ยทs ๐‘„)) -s (๐‘ƒ ยทs ๐‘„)) <s (((๐‘‡ ยทs ๐ต) +s (๐ด ยทs ๐‘ˆ)) -s (๐‘‡ ยทs ๐‘ˆ))))
2707, 269mpd 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