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

Theorem mulsproplem14 27945
Description: Lemma for surreal multiplication. Finally, we remove the restriction on ๐ธ and ๐น from mulsproplem12 27943 and mulsproplem13 27944. This completes the induction on surreal multiplication. mulsprop 27946 brings all this together technically. (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 ๐‘’))))))
mulsproplem.2 (๐œ‘ โ†’ ๐ถ โˆˆ No )
mulsproplem.3 (๐œ‘ โ†’ ๐ท โˆˆ No )
mulsproplem.4 (๐œ‘ โ†’ ๐ธ โˆˆ No )
mulsproplem.5 (๐œ‘ โ†’ ๐น โˆˆ No )
mulsproplem.6 (๐œ‘ โ†’ ๐ถ <s ๐ท)
mulsproplem.7 (๐œ‘ โ†’ ๐ธ <s ๐น)
Assertion
Ref Expression
mulsproplem14 (๐œ‘ โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
Distinct variable groups:   ๐ด,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ต,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ถ,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ท,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ธ,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐น,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“
Allowed substitution hints:   ๐œ‘(๐‘’,๐‘“,๐‘Ž,๐‘,๐‘,๐‘‘)

Proof of Theorem mulsproplem14
Dummy variables ๐‘” โ„Ž ๐‘– ๐‘— ๐‘˜ ๐‘™ ๐‘ฅ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulsproplem.1 . . . 4 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
21adantr 480 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
3 mulsproplem.2 . . . 4 (๐œ‘ โ†’ ๐ถ โˆˆ No )
43adantr 480 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐ถ โˆˆ No )
5 mulsproplem.3 . . . 4 (๐œ‘ โ†’ ๐ท โˆˆ No )
65adantr 480 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐ท โˆˆ No )
7 mulsproplem.4 . . . 4 (๐œ‘ โ†’ ๐ธ โˆˆ No )
87adantr 480 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐ธ โˆˆ No )
9 mulsproplem.5 . . . 4 (๐œ‘ โ†’ ๐น โˆˆ No )
109adantr 480 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐น โˆˆ No )
11 mulsproplem.6 . . . 4 (๐œ‘ โ†’ ๐ถ <s ๐ท)
1211adantr 480 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐ถ <s ๐ท)
13 mulsproplem.7 . . . 4 (๐œ‘ โ†’ ๐ธ <s ๐น)
1413adantr 480 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐ธ <s ๐น)
15 simpr 484 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)))
162, 4, 6, 8, 10, 12, 14, 15mulsproplem13 27944 . 2 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
177adantr 480 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ ๐ธ โˆˆ No )
189adantr 480 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ ๐น โˆˆ No )
19 simpr 484 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ ( bday โ€˜๐ธ) = ( bday โ€˜๐น))
2013adantr 480 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ ๐ธ <s ๐น)
21 nodense 27541 . . . 4 (((๐ธ โˆˆ No โˆง ๐น โˆˆ No ) โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง ๐ธ <s ๐น)) โ†’ โˆƒ๐‘ฅ โˆˆ No (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))
2217, 18, 19, 20, 21syl22anc 836 . . 3 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ โˆƒ๐‘ฅ โˆˆ No (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))
23 unidm 4144 . . . . . . . . . . . . . . . . 17 (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )))) = ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )))
24 unidm 4144 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) = (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))
25 bday0s 27677 . . . . . . . . . . . . . . . . . . 19 ( bday โ€˜ 0s ) = โˆ…
2625, 25oveq12i 7413 . . . . . . . . . . . . . . . . . 18 (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) = (โˆ… +no โˆ…)
27 0elon 6408 . . . . . . . . . . . . . . . . . . 19 โˆ… โˆˆ On
28 naddrid 8678 . . . . . . . . . . . . . . . . . . 19 (โˆ… โˆˆ On โ†’ (โˆ… +no โˆ…) = โˆ…)
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . 18 (โˆ… +no โˆ…) = โˆ…
3026, 29eqtri 2752 . . . . . . . . . . . . . . . . 17 (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) = โˆ…
3123, 24, 303eqtri 2756 . . . . . . . . . . . . . . . 16 (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )))) = โˆ…
3231uneq2i 4152 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช โˆ…)
33 un0 4382 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช โˆ…) = (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))
3432, 33eqtri 2752 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))
35 ssun2 4165 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
36 ssun2 4165 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
3735, 36sstri 3983 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
38 ssun2 4165 . . . . . . . . . . . . . . 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 โ€˜๐ธ)))))
3937, 38sstri 3983 . . . . . . . . . . . . . 14 (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
4034, 39eqsstri 4008 . . . . . . . . . . . . 13 ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
4140sseli 3970 . . . . . . . . . . . 12 (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
4241imim1i 63 . . . . . . . . . . 11 ((((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
43426ralimi 3119 . . . . . . . . . 10 (โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
441, 43syl 17 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
4544, 5, 7mulsproplem11 27942 . . . . . . . 8 (๐œ‘ โ†’ (๐ท ยทs ๐ธ) โˆˆ No )
4631uneq2i 4152 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช โˆ…)
47 un0 4382 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช โˆ…) = (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ))
4846, 47eqtri 2752 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ))
49 ssun1 4164 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
50 ssun1 4164 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
5149, 50sstri 3983 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
5251, 38sstri 3983 . . . . . . . . . . . . . 14 (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
5348, 52eqsstri 4008 . . . . . . . . . . . . 13 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
5453sseli 3970 . . . . . . . . . . . 12 (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
5554imim1i 63 . . . . . . . . . . 11 ((((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
56556ralimi 3119 . . . . . . . . . 10 (โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
571, 56syl 17 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
5857, 3, 7mulsproplem11 27942 . . . . . . . 8 (๐œ‘ โ†’ (๐ถ ยทs ๐ธ) โˆˆ No )
5945, 58subscld 27889 . . . . . . 7 (๐œ‘ โ†’ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) โˆˆ No )
6059adantr 480 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) โˆˆ No )
6144adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
625adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐ท โˆˆ No )
63 simprr1 1218 . . . . . . . . . 10 ((( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))) โ†’ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ))
6463adantl 481 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ))
65 bdayelon 27625 . . . . . . . . . 10 ( bday โ€˜๐ธ) โˆˆ On
66 simprrl 778 . . . . . . . . . 10 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐‘ฅ โˆˆ No )
67 oldbday 27743 . . . . . . . . . 10 ((( bday โ€˜๐ธ) โˆˆ On โˆง ๐‘ฅ โˆˆ No ) โ†’ (๐‘ฅ โˆˆ ( O โ€˜( bday โ€˜๐ธ)) โ†” ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ)))
6865, 66, 67sylancr 586 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐‘ฅ โˆˆ ( O โ€˜( bday โ€˜๐ธ)) โ†” ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ)))
6964, 68mpbird 257 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐‘ฅ โˆˆ ( O โ€˜( bday โ€˜๐ธ)))
7061, 62, 69mulsproplem3 27934 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ท ยทs ๐‘ฅ) โˆˆ No )
7157adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
723adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐ถ โˆˆ No )
7371, 72, 69mulsproplem3 27934 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ถ ยทs ๐‘ฅ) โˆˆ No )
7470, 73subscld 27889 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐‘ฅ) -s (๐ถ ยทs ๐‘ฅ)) โˆˆ No )
7531uneq2i 4152 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช โˆ…)
76 un0 4382 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช โˆ…) = (( bday โ€˜๐ท) +no ( bday โ€˜๐น))
7775, 76eqtri 2752 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = (( bday โ€˜๐ท) +no ( bday โ€˜๐น))
78 ssun2 4165 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
7978, 50sstri 3983 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
8079, 38sstri 3983 . . . . . . . . . . . . . 14 (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
8177, 80eqsstri 4008 . . . . . . . . . . . . 13 ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
8281sseli 3970 . . . . . . . . . . . 12 (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
8382imim1i 63 . . . . . . . . . . 11 ((((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
84836ralimi 3119 . . . . . . . . . 10 (โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
851, 84syl 17 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
8685, 5, 9mulsproplem11 27942 . . . . . . . 8 (๐œ‘ โ†’ (๐ท ยทs ๐น) โˆˆ No )
8731uneq2i 4152 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช โˆ…)
88 un0 4382 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช โˆ…) = (( bday โ€˜๐ถ) +no ( bday โ€˜๐น))
8987, 88eqtri 2752 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = (( bday โ€˜๐ถ) +no ( bday โ€˜๐น))
90 ssun1 4164 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
9190, 36sstri 3983 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
9291, 38sstri 3983 . . . . . . . . . . . . . 14 (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
9389, 92eqsstri 4008 . . . . . . . . . . . . 13 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
9493sseli 3970 . . . . . . . . . . . 12 (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
9594imim1i 63 . . . . . . . . . . 11 ((((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
96956ralimi 3119 . . . . . . . . . 10 (โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
971, 96syl 17 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
9897, 3, 9mulsproplem11 27942 . . . . . . . 8 (๐œ‘ โ†’ (๐ถ ยทs ๐น) โˆˆ No )
9986, 98subscld 27889 . . . . . . 7 (๐œ‘ โ†’ ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โˆˆ No )
10099adantr 480 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โˆˆ No )
1011mulsproplemcbv 27931 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))))
102101adantr 480 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))))
103 onelss 6396 . . . . . . . . . . . . . . . . . 18 (( bday โ€˜๐ธ) โˆˆ On โ†’ (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โ†’ ( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐ธ)))
10465, 64, 103mpsyl 68 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐ธ))
105 simprl 768 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ( bday โ€˜๐ธ) = ( bday โ€˜๐น))
106104, 105sseqtrd 4014 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐น))
107 bdayelon 27625 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐‘ฅ) โˆˆ On
108 bdayelon 27625 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐น) โˆˆ On
109 bdayelon 27625 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐ท) โˆˆ On
110 naddss2 8685 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐น) โˆˆ On โˆง ( bday โ€˜๐ท) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐น) โ†” (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
111107, 108, 109, 110mp3an 1457 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐น) โ†” (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
112106, 111sylib 217 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
113 unss2 4173 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
114112, 113syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
115 bdayelon 27625 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐ถ) โˆˆ On
116 naddss2 8685 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐น) โˆˆ On โˆง ( bday โ€˜๐ถ) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐น) โ†” (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ถ) +no ( bday โ€˜๐น))))
117107, 108, 115, 116mp3an 1457 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐น) โ†” (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)))
118106, 117sylib 217 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)))
119 unss1 4171 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
120118, 119syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
121 unss12 4174 . . . . . . . . . . . . . 14 ((((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆง ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โ†’ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
122114, 120, 121syl2anc 583 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
123 unss2 4173 . . . . . . . . . . . . 13 ((((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โ†’ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
124122, 123syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
125124sseld 3973 . . . . . . . . . . 11 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))))
126125imim1d 82 . . . . . . . . . 10 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))) โ†’ (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜)))))))
127126ralimd6v 3200 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))) โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜)))))))
128102, 127mpd 15 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))))
1297adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐ธ โˆˆ No )
13011adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐ถ <s ๐ท)
131 simprr2 1219 . . . . . . . . 9 ((( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))) โ†’ ๐ธ <s ๐‘ฅ)
132131adantl 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐ธ <s ๐‘ฅ)
13364olcd 871 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐‘ฅ) โˆจ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ)))
134128, 72, 62, 129, 66, 130, 132, 133mulsproplem13 27944 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ถ ยทs ๐‘ฅ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐‘ฅ) -s (๐ท ยทs ๐ธ)))
13545adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ท ยทs ๐ธ) โˆˆ No )
13658adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ถ ยทs ๐ธ) โˆˆ No )
137135, 70, 136, 73sltsubsub3bd 27909 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐‘ฅ) -s (๐ถ ยทs ๐‘ฅ)) โ†” ((๐ถ ยทs ๐‘ฅ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐‘ฅ) -s (๐ท ยทs ๐ธ))))
138134, 137mpbird 257 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐‘ฅ) -s (๐ถ ยทs ๐‘ฅ)))
139 naddss2 8685 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐ธ) โˆˆ On โˆง ( bday โ€˜๐ถ) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐ธ) โ†” (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ))))
140107, 65, 115, 139mp3an 1457 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐ธ) โ†” (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)))
141104, 140sylib 217 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)))
142 unss1 4171 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
143141, 142syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
144 naddss2 8685 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐ธ) โˆˆ On โˆง ( bday โ€˜๐ท) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐ธ) โ†” (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
145107, 65, 109, 144mp3an 1457 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ฅ) โІ ( bday โ€˜๐ธ) โ†” (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
146104, 145sylib 217 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
147 unss2 4173 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โІ (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
148146, 147syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
149 unss12 4174 . . . . . . . . . . . . . 14 ((((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆง ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โІ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โ†’ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)))) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
150143, 148, 149syl2anc 583 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)))) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
151 unss2 4173 . . . . . . . . . . . . 13 ((((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)))) โІ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โ†’ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
152150, 151syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โІ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
153152sseld 3973 . . . . . . . . . . 11 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โ†’ ((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))))
154153imim1d 82 . . . . . . . . . 10 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))) โ†’ (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜)))))))
155154ralimd6v 3200 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))) โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜)))))))
156102, 155mpd 15 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))))
1579adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐น โˆˆ No )
158 simprr3 1220 . . . . . . . . 9 ((( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))) โ†’ ๐‘ฅ <s ๐น)
159158adantl 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐‘ฅ <s ๐น)
16064, 105eleqtrd 2827 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐น))
161160orcd 870 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐‘ฅ)))
162156, 72, 62, 66, 157, 130, 159, 161mulsproplem13 27944 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐‘ฅ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐‘ฅ)))
16386adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ท ยทs ๐น) โˆˆ No )
16498adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ถ ยทs ๐น) โˆˆ No )
16570, 163, 73, 164sltsubsub3bd 27909 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((๐ท ยทs ๐‘ฅ) -s (๐ถ ยทs ๐‘ฅ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ†” ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐‘ฅ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐‘ฅ))))
166162, 165mpbird 257 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐‘ฅ) -s (๐ถ ยทs ๐‘ฅ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)))
16760, 74, 100, 138, 166slttrd 27608 . . . . 5 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)))
16845, 86, 58, 98sltsubsub3bd 27909 . . . . . 6 (๐œ‘ โ†’ (((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ†” ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ))))
169168adantr 480 . . . . 5 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ†” ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ))))
170167, 169mpbid 231 . . . 4 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
171170anassrs 467 . . 3 (((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
17222, 171rexlimddv 3153 . 2 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
17365onordi 6465 . . . . 5 Ord ( bday โ€˜๐ธ)
174108onordi 6465 . . . . 5 Ord ( bday โ€˜๐น)
175 ordtri3or 6386 . . . . 5 ((Ord ( bday โ€˜๐ธ) โˆง Ord ( bday โ€˜๐น)) โ†’ (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)))
176173, 174, 175mp2an 689 . . . 4 (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))
177 df-3or 1085 . . . . 5 ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โ†” ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)))
178 or32 922 . . . . 5 (((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โ†” ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น)))
179177, 178bitri 275 . . . 4 ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โ†” ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น)))
180176, 179mpbi 229 . . 3 ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น))
181180a1i 11 . 2 (๐œ‘ โ†’ ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น)))
18216, 172, 181mpjaodan 955 1 (๐œ‘ โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆจ w3o 1083   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  โˆ€wral 3053  โˆƒwrex 3062   โˆช cun 3938   โІ wss 3940  โˆ…c0 4314   class class class wbr 5138  Ord word 6353  Oncon0 6354  โ€˜cfv 6533  (class class class)co 7401   +no cnadd 8660   No csur 27489   <s cslt 27490   bday cbday 27491   0s c0s 27671   O cold 27686   -s csubs 27849   ยทs cmuls 27922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-ot 4629  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-1o 8461  df-2o 8462  df-nadd 8661  df-no 27492  df-slt 27493  df-bday 27494  df-sle 27594  df-sslt 27630  df-scut 27632  df-0s 27673  df-made 27690  df-old 27691  df-left 27693  df-right 27694  df-norec 27771  df-norec2 27782  df-adds 27793  df-negs 27850  df-subs 27851  df-muls 27923
This theorem is referenced by:  mulsprop  27946
  Copyright terms: Public domain W3C validator