Metamath Proof Explorer

Theorem mulsproplem5

Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 4-Mar-2025)

Ref Expression
Hypotheses 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 mulsproplem5 ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) )

Proof

Step Hyp Ref Expression
1 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 ๐‘’ ) ) ) ) ) )
2 mulsproplem5.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ No )
3 mulsproplem5.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ No )
4 mulsproplem5.3 โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ ( L โ€˜ ๐ด ) )
5 mulsproplem5.4 โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ ( L โ€˜ ๐ต ) )
6 mulsproplem5.5 โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ ( L โ€˜ ๐ด ) )
7 mulsproplem5.6 โŠข ( ๐œ‘ โ†’ ๐‘ˆ โˆˆ ( R โ€˜ ๐ต ) )
8 leftssno โŠข ( L โ€˜ ๐ด ) โŠ† No
9 8 4 sselid โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ No )
10 8 6 sselid โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ No )
11 sltlin โŠข ( ( ๐‘ƒ โˆˆ No โˆง ๐‘‡ โˆˆ No ) โ†’ ( ๐‘ƒ <s ๐‘‡ โˆจ ๐‘ƒ = ๐‘‡ โˆจ ๐‘‡ <s ๐‘ƒ ) )
12 9 10 11 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ <s ๐‘‡ โˆจ ๐‘ƒ = ๐‘‡ โˆจ ๐‘‡ <s ๐‘ƒ ) )
13 leftssold โŠข ( L โ€˜ ๐ด ) โŠ† ( O โ€˜ ( bday โ€˜ ๐ด ) )
14 13 4 sselid โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ ( O โ€˜ ( bday โ€˜ ๐ด ) ) )
15 1 14 3 mulsproplem2 โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ ยทs ๐ต ) โˆˆ No )
16 leftssold โŠข ( L โ€˜ ๐ต ) โŠ† ( O โ€˜ ( bday โ€˜ ๐ต ) )
17 16 5 sselid โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ ( O โ€˜ ( bday โ€˜ ๐ต ) ) )
18 1 2 17 mulsproplem3 โŠข ( ๐œ‘ โ†’ ( ๐ด ยทs ๐‘„ ) โˆˆ No )
19 15 18 addscld โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) โˆˆ No )
20 1 14 17 mulsproplem4 โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ ยทs ๐‘„ ) โˆˆ No )
21 19 20 subscld โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) โˆˆ No )
22 21 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) โˆˆ No )
23 13 6 sselid โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ ( O โ€˜ ( bday โ€˜ ๐ด ) ) )
24 1 23 3 mulsproplem2 โŠข ( ๐œ‘ โ†’ ( ๐‘‡ ยทs ๐ต ) โˆˆ No )
25 24 18 addscld โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) โˆˆ No )
26 1 23 17 mulsproplem4 โŠข ( ๐œ‘ โ†’ ( ๐‘‡ ยทs ๐‘„ ) โˆˆ No )
27 25 26 subscld โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘‡ ยทs ๐‘„ ) ) โˆˆ No )
28 27 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘‡ ยทs ๐‘„ ) ) โˆˆ No )
29 rightssold โŠข ( R โ€˜ ๐ต ) โŠ† ( O โ€˜ ( bday โ€˜ ๐ต ) )
30 29 7 sselid โŠข ( ๐œ‘ โ†’ ๐‘ˆ โˆˆ ( O โ€˜ ( bday โ€˜ ๐ต ) ) )
31 1 2 30 mulsproplem3 โŠข ( ๐œ‘ โ†’ ( ๐ด ยทs ๐‘ˆ ) โˆˆ No )
32 24 31 addscld โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) โˆˆ No )
33 1 23 30 mulsproplem4 โŠข ( ๐œ‘ โ†’ ( ๐‘‡ ยทs ๐‘ˆ ) โˆˆ No )
34 32 33 subscld โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) โˆˆ No )
35 34 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) โˆˆ No )
36 ssltleft โŠข ( ๐ต โˆˆ No โ†’ ( L โ€˜ ๐ต ) <<s { ๐ต } )
37 3 36 syl โŠข ( ๐œ‘ โ†’ ( L โ€˜ ๐ต ) <<s { ๐ต } )
38 snidg โŠข ( ๐ต โˆˆ No โ†’ ๐ต โˆˆ { ๐ต } )
39 3 38 syl โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ { ๐ต } )
40 37 5 39 ssltsepcd โŠข ( ๐œ‘ โ†’ ๐‘„ <s ๐ต )
41 0sno โŠข 0s โˆˆ No
42 41 a1i โŠข ( ๐œ‘ โ†’ 0s โˆˆ No )
43 leftssno โŠข ( L โ€˜ ๐ต ) โŠ† No
44 43 5 sselid โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ No )
45 bday0s โŠข ( bday โ€˜ 0s ) = โˆ…
46 45 45 oveq12i โŠข ( ( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ) ) = ( โˆ… +no โˆ… )
47 0elon โŠข โˆ… โˆˆ On
48 naddrid โŠข ( โˆ… โˆˆ On โ†’ ( โˆ… +no โˆ… ) = โˆ… )
49 47 48 ax-mp โŠข ( โˆ… +no โˆ… ) = โˆ…
50 46 49 eqtri โŠข ( ( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ) ) = โˆ…
51 50 uneq1i โŠข ( ( ( 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 โŠข ( โˆ… โˆช ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) ) ) ) = ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) ) )
53 51 52 eqtri โŠข ( ( ( 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 โŠข ( ๐‘ƒ โˆˆ ( O โ€˜ ( bday โ€˜ ๐ด ) ) โ†’ ( bday โ€˜ ๐‘ƒ ) โˆˆ ( bday โ€˜ ๐ด ) )
55 14 54 syl โŠข ( ๐œ‘ โ†’ ( bday โ€˜ ๐‘ƒ ) โˆˆ ( bday โ€˜ ๐ด ) )
56 oldbdayim โŠข ( ๐‘„ โˆˆ ( O โ€˜ ( bday โ€˜ ๐ต ) ) โ†’ ( bday โ€˜ ๐‘„ ) โˆˆ ( bday โ€˜ ๐ต ) )
57 17 56 syl โŠข ( ๐œ‘ โ†’ ( bday โ€˜ ๐‘„ ) โˆˆ ( bday โ€˜ ๐ต ) )
58 bdayelon โŠข ( bday โ€˜ ๐ด ) โˆˆ On
59 bdayelon โŠข ( bday โ€˜ ๐ต ) โˆˆ On
60 naddel12 โŠข ( ( ( bday โ€˜ ๐ด ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On ) โ†’ ( ( ( bday โ€˜ ๐‘ƒ ) โˆˆ ( bday โ€˜ ๐ด ) โˆง ( bday โ€˜ ๐‘„ ) โˆˆ ( bday โ€˜ ๐ต ) ) โ†’ ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
61 58 59 60 mp2an โŠข ( ( ( bday โ€˜ ๐‘ƒ ) โˆˆ ( bday โ€˜ ๐ด ) โˆง ( bday โ€˜ ๐‘„ ) โˆˆ ( bday โ€˜ ๐ต ) ) โ†’ ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
62 55 57 61 syl2anc โŠข ( ๐œ‘ โ†’ ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
63 oldbdayim โŠข ( ๐‘‡ โˆˆ ( O โ€˜ ( bday โ€˜ ๐ด ) ) โ†’ ( bday โ€˜ ๐‘‡ ) โˆˆ ( bday โ€˜ ๐ด ) )
64 23 63 syl โŠข ( ๐œ‘ โ†’ ( bday โ€˜ ๐‘‡ ) โˆˆ ( bday โ€˜ ๐ด ) )
65 bdayelon โŠข ( bday โ€˜ ๐‘‡ ) โˆˆ On
66 naddel1 โŠข ( ( ( bday โ€˜ ๐‘‡ ) โˆˆ On โˆง ( bday โ€˜ ๐ด ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐‘‡ ) โˆˆ ( bday โ€˜ ๐ด ) โ†” ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
67 65 58 59 66 mp3an โŠข ( ( bday โ€˜ ๐‘‡ ) โˆˆ ( bday โ€˜ ๐ด ) โ†” ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
68 64 67 sylib โŠข ( ๐œ‘ โ†’ ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
69 62 68 jca โŠข ( ๐œ‘ โ†’ ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
70 bdayelon โŠข ( bday โ€˜ ๐‘ƒ ) โˆˆ On
71 naddel1 โŠข ( ( ( bday โ€˜ ๐‘ƒ ) โˆˆ On โˆง ( bday โ€˜ ๐ด ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐‘ƒ ) โˆˆ ( bday โ€˜ ๐ด ) โ†” ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
72 70 58 59 71 mp3an โŠข ( ( bday โ€˜ ๐‘ƒ ) โˆˆ ( bday โ€˜ ๐ด ) โ†” ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
73 55 72 sylib โŠข ( ๐œ‘ โ†’ ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
74 naddel12 โŠข ( ( ( bday โ€˜ ๐ด ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On ) โ†’ ( ( ( bday โ€˜ ๐‘‡ ) โˆˆ ( bday โ€˜ ๐ด ) โˆง ( bday โ€˜ ๐‘„ ) โˆˆ ( bday โ€˜ ๐ต ) ) โ†’ ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
75 58 59 74 mp2an โŠข ( ( ( bday โ€˜ ๐‘‡ ) โˆˆ ( bday โ€˜ ๐ด ) โˆง ( bday โ€˜ ๐‘„ ) โˆˆ ( bday โ€˜ ๐ต ) ) โ†’ ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
76 64 57 75 syl2anc โŠข ( ๐œ‘ โ†’ ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
77 73 76 jca โŠข ( ๐œ‘ โ†’ ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
78 bdayelon โŠข ( bday โ€˜ ๐‘„ ) โˆˆ On
79 naddcl โŠข ( ( ( bday โ€˜ ๐‘ƒ ) โˆˆ On โˆง ( bday โ€˜ ๐‘„ ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ On )
80 70 78 79 mp2an โŠข ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ On
81 naddcl โŠข ( ( ( bday โ€˜ ๐‘‡ ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ On )
82 65 59 81 mp2an โŠข ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ On
83 80 82 onun2i โŠข ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆˆ On
84 naddcl โŠข ( ( ( bday โ€˜ ๐‘ƒ ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ On )
85 70 59 84 mp2an โŠข ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ On
86 naddcl โŠข ( ( ( bday โ€˜ ๐‘‡ ) โˆˆ On โˆง ( bday โ€˜ ๐‘„ ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ On )
87 65 78 86 mp2an โŠข ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ On
88 85 87 onun2i โŠข ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) ) โˆˆ On
89 naddcl โŠข ( ( ( bday โ€˜ ๐ด ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆˆ On )
90 58 59 89 mp2an โŠข ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆˆ On
91 onunel โŠข ( ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
92 83 88 90 91 mp3an โŠข ( ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( 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 โŠข ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
94 80 82 90 93 mp3an โŠข ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
95 onunel โŠข ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
96 85 87 90 95 mp3an โŠข ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
97 94 96 anbi12i โŠข ( ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) โ†” ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) โˆง ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) ) )
98 92 97 bitri โŠข ( ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) โˆง ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) ) )
99 69 77 98 sylanbrc โŠข ( ๐œ‘ โ†’ ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
100 elun1 โŠข ( ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†’ ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐ธ ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐น ) ) ) โˆช ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐น ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐ธ ) ) ) ) ) )
101 99 100 syl โŠข ( ๐œ‘ โ†’ ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐ธ ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐น ) ) ) โˆช ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐น ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐ธ ) ) ) ) ) )
102 53 101 eqeltrid โŠข ( ๐œ‘ โ†’ ( ( ( 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 โ€˜ ๐ธ ) ) ) ) ) )
103 1 42 42 9 10 44 3 102 mulsproplem1 โŠข ( ๐œ‘ โ†’ ( ( 0s ยทs 0s ) โˆˆ No โˆง ( ( ๐‘ƒ <s ๐‘‡ โˆง ๐‘„ <s ๐ต ) โ†’ ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) ) ) )
104 103 simprd โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ <s ๐‘‡ โˆง ๐‘„ <s ๐ต ) โ†’ ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) ) )
105 40 104 mpan2d โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ <s ๐‘‡ โ†’ ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) ) )
106 105 imp โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) )
107 15 20 subscld โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) โˆˆ No )
108 24 26 subscld โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) โˆˆ No )
109 107 108 18 sltadd1d โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) โ†” ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) +s ( ๐ด ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) +s ( ๐ด ยทs ๐‘„ ) ) ) )
110 109 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) โ†” ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) +s ( ๐ด ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) +s ( ๐ด ยทs ๐‘„ ) ) ) )
111 106 110 mpbid โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) +s ( ๐ด ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) +s ( ๐ด ยทs ๐‘„ ) ) )
112 15 18 20 addsubsd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) = ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) +s ( ๐ด ยทs ๐‘„ ) ) )
113 112 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) = ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) +s ( ๐ด ยทs ๐‘„ ) ) )
114 24 18 26 addsubsd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘‡ ยทs ๐‘„ ) ) = ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) +s ( ๐ด ยทs ๐‘„ ) ) )
115 114 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘‡ ยทs ๐‘„ ) ) = ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘„ ) ) +s ( ๐ด ยทs ๐‘„ ) ) )
116 111 113 115 3brtr4d โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘‡ ยทs ๐‘„ ) ) )
117 ssltleft โŠข ( ๐ด โˆˆ No โ†’ ( L โ€˜ ๐ด ) <<s { ๐ด } )
118 2 117 syl โŠข ( ๐œ‘ โ†’ ( L โ€˜ ๐ด ) <<s { ๐ด } )
119 snidg โŠข ( ๐ด โˆˆ No โ†’ ๐ด โˆˆ { ๐ด } )
120 2 119 syl โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ { ๐ด } )
121 118 6 120 ssltsepcd โŠข ( ๐œ‘ โ†’ ๐‘‡ <s ๐ด )
122 lltropt โŠข ( L โ€˜ ๐ต ) <<s ( R โ€˜ ๐ต )
123 122 a1i โŠข ( ๐œ‘ โ†’ ( L โ€˜ ๐ต ) <<s ( R โ€˜ ๐ต ) )
124 123 5 7 ssltsepcd โŠข ( ๐œ‘ โ†’ ๐‘„ <s ๐‘ˆ )
125 rightssno โŠข ( R โ€˜ ๐ต ) โŠ† No
126 125 7 sselid โŠข ( ๐œ‘ โ†’ ๐‘ˆ โˆˆ No )
127 50 uneq1i โŠข ( ( ( 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 โŠข ( โˆ… โˆช ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) ) = ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) )
129 127 128 eqtri โŠข ( ( ( 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 โŠข ( ๐‘ˆ โˆˆ ( O โ€˜ ( bday โ€˜ ๐ต ) ) โ†’ ( bday โ€˜ ๐‘ˆ ) โˆˆ ( bday โ€˜ ๐ต ) )
131 30 130 syl โŠข ( ๐œ‘ โ†’ ( bday โ€˜ ๐‘ˆ ) โˆˆ ( bday โ€˜ ๐ต ) )
132 bdayelon โŠข ( bday โ€˜ ๐‘ˆ ) โˆˆ On
133 naddel2 โŠข ( ( ( bday โ€˜ ๐‘ˆ ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On โˆง ( bday โ€˜ ๐ด ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐‘ˆ ) โˆˆ ( bday โ€˜ ๐ต ) โ†” ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
134 132 59 58 133 mp3an โŠข ( ( bday โ€˜ ๐‘ˆ ) โˆˆ ( bday โ€˜ ๐ต ) โ†” ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
135 131 134 sylib โŠข ( ๐œ‘ โ†’ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
136 76 135 jca โŠข ( ๐œ‘ โ†’ ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
137 naddel12 โŠข ( ( ( bday โ€˜ ๐ด ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On ) โ†’ ( ( ( bday โ€˜ ๐‘‡ ) โˆˆ ( bday โ€˜ ๐ด ) โˆง ( bday โ€˜ ๐‘ˆ ) โˆˆ ( bday โ€˜ ๐ต ) ) โ†’ ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
138 58 59 137 mp2an โŠข ( ( ( bday โ€˜ ๐‘‡ ) โˆˆ ( bday โ€˜ ๐ด ) โˆง ( bday โ€˜ ๐‘ˆ ) โˆˆ ( bday โ€˜ ๐ต ) ) โ†’ ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
139 64 131 138 syl2anc โŠข ( ๐œ‘ โ†’ ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
140 naddel2 โŠข ( ( ( bday โ€˜ ๐‘„ ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On โˆง ( bday โ€˜ ๐ด ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐‘„ ) โˆˆ ( bday โ€˜ ๐ต ) โ†” ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
141 78 59 58 140 mp3an โŠข ( ( bday โ€˜ ๐‘„ ) โˆˆ ( bday โ€˜ ๐ต ) โ†” ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
142 57 141 sylib โŠข ( ๐œ‘ โ†’ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
143 139 142 jca โŠข ( ๐œ‘ โ†’ ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
144 naddcl โŠข ( ( ( bday โ€˜ ๐ด ) โˆˆ On โˆง ( bday โ€˜ ๐‘ˆ ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ On )
145 58 132 144 mp2an โŠข ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ On
146 87 145 onun2i โŠข ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ On
147 naddcl โŠข ( ( ( bday โ€˜ ๐‘‡ ) โˆˆ On โˆง ( bday โ€˜ ๐‘ˆ ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ On )
148 65 132 147 mp2an โŠข ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ On
149 naddcl โŠข ( ( ( bday โ€˜ ๐ด ) โˆˆ On โˆง ( bday โ€˜ ๐‘„ ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ On )
150 58 78 149 mp2an โŠข ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ On
151 148 150 onun2i โŠข ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) โˆˆ On
152 onunel โŠข ( ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
153 146 151 90 152 mp3an โŠข ( ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( 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 โŠข ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
155 87 145 90 154 mp3an โŠข ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
156 onunel โŠข ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
157 148 150 90 156 mp3an โŠข ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
158 155 157 anbi12i โŠข ( ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) โ†” ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) โˆง ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) ) )
159 153 158 bitri โŠข ( ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) โˆง ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) ) )
160 136 143 159 sylanbrc โŠข ( ๐œ‘ โ†’ ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
161 elun1 โŠข ( ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†’ ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐ธ ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐น ) ) ) โˆช ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐น ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐ธ ) ) ) ) ) )
162 160 161 syl โŠข ( ๐œ‘ โ†’ ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐ธ ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐น ) ) ) โˆช ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐น ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐ธ ) ) ) ) ) )
163 129 162 eqeltrid โŠข ( ๐œ‘ โ†’ ( ( ( 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 โ€˜ ๐ธ ) ) ) ) ) )
164 1 42 42 10 2 44 126 163 mulsproplem1 โŠข ( ๐œ‘ โ†’ ( ( 0s ยทs 0s ) โˆˆ No โˆง ( ( ๐‘‡ <s ๐ด โˆง ๐‘„ <s ๐‘ˆ ) โ†’ ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐ด ยทs ๐‘„ ) ) ) ) )
165 164 simprd โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ <s ๐ด โˆง ๐‘„ <s ๐‘ˆ ) โ†’ ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐ด ยทs ๐‘„ ) ) ) )
166 121 124 165 mp2and โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐ด ยทs ๐‘„ ) ) )
167 33 31 26 18 sltsubsub3bd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐ด ยทs ๐‘„ ) ) โ†” ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) )
168 18 26 subscld โŠข ( ๐œ‘ โ†’ ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) โˆˆ No )
169 31 33 subscld โŠข ( ๐œ‘ โ†’ ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) โˆˆ No )
170 168 169 24 sltadd2d โŠข ( ๐œ‘ โ†’ ( ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) โ†” ( ( ๐‘‡ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) ) <s ( ( ๐‘‡ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) ) )
171 167 170 bitrd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐ด ยทs ๐‘„ ) ) โ†” ( ( ๐‘‡ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) ) <s ( ( ๐‘‡ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) ) )
172 166 171 mpbid โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) ) <s ( ( ๐‘‡ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) )
173 24 18 26 addsubsassd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘‡ ยทs ๐‘„ ) ) = ( ( ๐‘‡ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘‡ ยทs ๐‘„ ) ) ) )
174 24 31 33 addsubsassd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) = ( ( ๐‘‡ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) )
175 172 173 174 3brtr4d โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘‡ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) )
176 175 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘‡ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) )
177 22 28 35 116 176 slttrd โŠข ( ( ๐œ‘ โˆง ๐‘ƒ <s ๐‘‡ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) )
178 177 ex โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ <s ๐‘‡ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) )
179 oveq1 โŠข ( ๐‘ƒ = ๐‘‡ โ†’ ( ๐‘ƒ ยทs ๐ต ) = ( ๐‘‡ ยทs ๐ต ) )
180 179 oveq1d โŠข ( ๐‘ƒ = ๐‘‡ โ†’ ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) = ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) )
181 oveq1 โŠข ( ๐‘ƒ = ๐‘‡ โ†’ ( ๐‘ƒ ยทs ๐‘„ ) = ( ๐‘‡ ยทs ๐‘„ ) )
182 180 181 oveq12d โŠข ( ๐‘ƒ = ๐‘‡ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) = ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘‡ ยทs ๐‘„ ) ) )
183 182 breq1d โŠข ( ๐‘ƒ = ๐‘‡ โ†’ ( ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) โ†” ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘‡ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) )
184 175 183 syl5ibrcom โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ = ๐‘‡ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) )
185 21 adantr โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) โˆˆ No )
186 15 31 addscld โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) โˆˆ No )
187 1 14 30 mulsproplem4 โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ ยทs ๐‘ˆ ) โˆˆ No )
188 186 187 subscld โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) โˆˆ No )
189 188 adantr โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) โˆˆ No )
190 34 adantr โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) โˆˆ No )
191 118 4 120 ssltsepcd โŠข ( ๐œ‘ โ†’ ๐‘ƒ <s ๐ด )
192 50 uneq1i โŠข ( ( ( 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 โŠข ( โˆ… โˆช ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) ) = ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) )
194 192 193 eqtri โŠข ( ( ( 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 โ€˜ ๐‘„ ) ) ) )
195 62 135 jca โŠข ( ๐œ‘ โ†’ ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
196 naddel12 โŠข ( ( ( bday โ€˜ ๐ด ) โˆˆ On โˆง ( bday โ€˜ ๐ต ) โˆˆ On ) โ†’ ( ( ( bday โ€˜ ๐‘ƒ ) โˆˆ ( bday โ€˜ ๐ด ) โˆง ( bday โ€˜ ๐‘ˆ ) โˆˆ ( bday โ€˜ ๐ต ) ) โ†’ ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
197 58 59 196 mp2an โŠข ( ( ( bday โ€˜ ๐‘ƒ ) โˆˆ ( bday โ€˜ ๐ด ) โˆง ( bday โ€˜ ๐‘ˆ ) โˆˆ ( bday โ€˜ ๐ต ) ) โ†’ ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
198 55 131 197 syl2anc โŠข ( ๐œ‘ โ†’ ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
199 198 142 jca โŠข ( ๐œ‘ โ†’ ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
200 80 145 onun2i โŠข ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ On
201 naddcl โŠข ( ( ( bday โ€˜ ๐‘ƒ ) โˆˆ On โˆง ( bday โ€˜ ๐‘ˆ ) โˆˆ On ) โ†’ ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ On )
202 70 132 201 mp2an โŠข ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ On
203 202 150 onun2i โŠข ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) โˆˆ On
204 onunel โŠข ( ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
205 200 203 90 204 mp3an โŠข ( ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( 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 โŠข ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
207 80 145 90 206 mp3an โŠข ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
208 onunel โŠข ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
209 202 150 90 208 mp3an โŠข ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
210 207 209 anbi12i โŠข ( ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) โ†” ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) โˆง ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) ) )
211 205 210 bitri โŠข ( ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) โˆง ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) ) )
212 195 199 211 sylanbrc โŠข ( ๐œ‘ โ†’ ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
213 elun1 โŠข ( ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†’ ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐ธ ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐น ) ) ) โˆช ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐น ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐ธ ) ) ) ) ) )
214 212 213 syl โŠข ( ๐œ‘ โ†’ ( ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘„ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐‘„ ) ) ) ) โˆˆ ( ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐ธ ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐น ) ) ) โˆช ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐น ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐ธ ) ) ) ) ) )
215 194 214 eqeltrid โŠข ( ๐œ‘ โ†’ ( ( ( 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 โ€˜ ๐ธ ) ) ) ) ) )
216 1 42 42 9 2 44 126 215 mulsproplem1 โŠข ( ๐œ‘ โ†’ ( ( 0s ยทs 0s ) โˆˆ No โˆง ( ( ๐‘ƒ <s ๐ด โˆง ๐‘„ <s ๐‘ˆ ) โ†’ ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐ด ยทs ๐‘„ ) ) ) ) )
217 216 simprd โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ <s ๐ด โˆง ๐‘„ <s ๐‘ˆ ) โ†’ ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐ด ยทs ๐‘„ ) ) ) )
218 191 124 217 mp2and โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐ด ยทs ๐‘„ ) ) )
219 187 31 20 18 sltsubsub3bd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐ด ยทs ๐‘„ ) ) โ†” ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) ) )
220 18 20 subscld โŠข ( ๐œ‘ โ†’ ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) โˆˆ No )
221 31 187 subscld โŠข ( ๐œ‘ โ†’ ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) โˆˆ No )
222 220 221 15 sltadd2d โŠข ( ๐œ‘ โ†’ ( ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) โ†” ( ( ๐‘ƒ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) ) <s ( ( ๐‘ƒ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) ) ) )
223 219 222 bitrd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐ด ยทs ๐‘„ ) ) โ†” ( ( ๐‘ƒ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) ) <s ( ( ๐‘ƒ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) ) ) )
224 218 223 mpbid โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) ) <s ( ( ๐‘ƒ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) ) )
225 15 18 20 addsubsassd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) = ( ( ๐‘ƒ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘„ ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) ) )
226 15 31 187 addsubsassd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) = ( ( ๐‘ƒ ยทs ๐ต ) +s ( ( ๐ด ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) ) )
227 224 225 226 3brtr4d โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) )
228 227 adantr โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) )
229 ssltright โŠข ( ๐ต โˆˆ No โ†’ { ๐ต } <<s ( R โ€˜ ๐ต ) )
230 3 229 syl โŠข ( ๐œ‘ โ†’ { ๐ต } <<s ( R โ€˜ ๐ต ) )
231 230 39 7 ssltsepcd โŠข ( ๐œ‘ โ†’ ๐ต <s ๐‘ˆ )
232 50 uneq1i โŠข ( ( ( 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 โŠข ( โˆ… โˆช ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) ) ) ) = ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) ) )
234 232 233 eqtri โŠข ( ( ( 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 โŠข ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
236 82 202 90 235 mp3an โŠข ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
237 68 198 236 sylanbrc โŠข ( ๐œ‘ โ†’ ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
238 139 73 jca โŠข ( ๐œ‘ โ†’ ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
239 82 202 onun2i โŠข ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ On
240 148 85 onun2i โŠข ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) ) โˆˆ On
241 onunel โŠข ( ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
242 239 240 90 241 mp3an โŠข ( ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( 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 โŠข ( ( ( ( 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 โ€˜ ๐ต ) ) ) ) )
244 148 85 90 243 mp3an โŠข ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) )
245 244 anbi2i โŠข ( ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) โ†” ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) ) )
246 242 245 bitri โŠข ( ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†” ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆง ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) ) ) )
247 237 238 246 sylanbrc โŠข ( ๐œ‘ โ†’ ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) )
248 elun1 โŠข ( ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) ) ) โˆˆ ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โ†’ ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) ) ) โˆˆ ( ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐ธ ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐น ) ) ) โˆช ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐น ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐ธ ) ) ) ) ) )
249 247 248 syl โŠข ( ๐œ‘ โ†’ ( ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐‘ˆ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘‡ ) +no ( bday โ€˜ ๐‘ˆ ) ) โˆช ( ( bday โ€˜ ๐‘ƒ ) +no ( bday โ€˜ ๐ต ) ) ) ) โˆˆ ( ( ( bday โ€˜ ๐ด ) +no ( bday โ€˜ ๐ต ) ) โˆช ( ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐ธ ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐น ) ) ) โˆช ( ( ( bday โ€˜ ๐ถ ) +no ( bday โ€˜ ๐น ) ) โˆช ( ( bday โ€˜ ๐ท ) +no ( bday โ€˜ ๐ธ ) ) ) ) ) )
250 234 249 eqeltrid โŠข ( ๐œ‘ โ†’ ( ( ( 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 โ€˜ ๐ธ ) ) ) ) ) )
251 1 42 42 10 9 3 126 250 mulsproplem1 โŠข ( ๐œ‘ โ†’ ( ( 0s ยทs 0s ) โˆˆ No โˆง ( ( ๐‘‡ <s ๐‘ƒ โˆง ๐ต <s ๐‘ˆ ) โ†’ ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐ต ) ) <s ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐ต ) ) ) ) )
252 251 simprd โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ <s ๐‘ƒ โˆง ๐ต <s ๐‘ˆ ) โ†’ ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐ต ) ) <s ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐ต ) ) ) )
253 231 252 mpan2d โŠข ( ๐œ‘ โ†’ ( ๐‘‡ <s ๐‘ƒ โ†’ ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐ต ) ) <s ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐ต ) ) ) )
254 253 imp โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐ต ) ) <s ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐ต ) ) )
255 33 24 187 15 sltsubsub2bd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐ต ) ) <s ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐ต ) ) โ†” ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) <s ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) )
256 15 187 subscld โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) โˆˆ No )
257 24 33 subscld โŠข ( ๐œ‘ โ†’ ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) โˆˆ No )
258 256 257 31 sltadd1d โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) <s ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) โ†” ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) ) )
259 255 258 bitrd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐ต ) ) <s ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐ต ) ) โ†” ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) ) )
260 259 adantr โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘‡ ยทs ๐‘ˆ ) -s ( ๐‘‡ ยทs ๐ต ) ) <s ( ( ๐‘ƒ ยทs ๐‘ˆ ) -s ( ๐‘ƒ ยทs ๐ต ) ) โ†” ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) ) )
261 254 260 mpbid โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) )
262 15 31 187 addsubsd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) = ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) )
263 262 adantr โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) = ( ( ( ๐‘ƒ ยทs ๐ต ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) )
264 24 31 33 addsubsd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) = ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) )
265 264 adantr โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) = ( ( ( ๐‘‡ ยทs ๐ต ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) +s ( ๐ด ยทs ๐‘ˆ ) ) )
266 261 263 265 3brtr4d โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘ƒ ยทs ๐‘ˆ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) )
267 185 189 190 228 266 slttrd โŠข ( ( ๐œ‘ โˆง ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) )
268 267 ex โŠข ( ๐œ‘ โ†’ ( ๐‘‡ <s ๐‘ƒ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) )
269 178 184 268 3jaod โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ <s ๐‘‡ โˆจ ๐‘ƒ = ๐‘‡ โˆจ ๐‘‡ <s ๐‘ƒ ) โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) ) )
270 12 269 mpd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ƒ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘„ ) ) -s ( ๐‘ƒ ยทs ๐‘„ ) ) <s ( ( ( ๐‘‡ ยทs ๐ต ) +s ( ๐ด ยทs ๐‘ˆ ) ) -s ( ๐‘‡ ยทs ๐‘ˆ ) ) )