Metamath Proof Explorer


Theorem mulsproplem14

Description: Lemma for surreal multiplication. Finally, we remove the restriction on E and F from mulsproplem12 and mulsproplem13 . This completes the induction on surreal multiplication. mulsprop brings all this together technically. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypotheses mulsproplem.1 φaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdse
mulsproplem.2 φCNo
mulsproplem.3 φDNo
mulsproplem.4 φENo
mulsproplem.5 φFNo
mulsproplem.6 φC<sD
mulsproplem.7 φE<sF
Assertion mulsproplem14 φCsF-sCsE<sDsF-sDsE

Proof

Step Hyp Ref Expression
1 mulsproplem.1 φaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdse
2 mulsproplem.2 φCNo
3 mulsproplem.3 φDNo
4 mulsproplem.4 φENo
5 mulsproplem.5 φFNo
6 mulsproplem.6 φC<sD
7 mulsproplem.7 φE<sF
8 1 adantr φbdayEbdayFbdayFbdayEaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdse
9 2 adantr φbdayEbdayFbdayFbdayECNo
10 3 adantr φbdayEbdayFbdayFbdayEDNo
11 4 adantr φbdayEbdayFbdayFbdayEENo
12 5 adantr φbdayEbdayFbdayFbdayEFNo
13 6 adantr φbdayEbdayFbdayFbdayEC<sD
14 7 adantr φbdayEbdayFbdayFbdayEE<sF
15 simpr φbdayEbdayFbdayFbdayEbdayEbdayFbdayFbdayE
16 8 9 10 11 12 13 14 15 mulsproplem13 φbdayEbdayFbdayFbdayECsF-sCsE<sDsF-sDsE
17 4 adantr φbdayE=bdayFENo
18 5 adantr φbdayE=bdayFFNo
19 simpr φbdayE=bdayFbdayE=bdayF
20 7 adantr φbdayE=bdayFE<sF
21 nodense ENoFNobdayE=bdayFE<sFxNobdayxbdayEE<sxx<sF
22 17 18 19 20 21 syl22anc φbdayE=bdayFxNobdayxbdayEE<sxx<sF
23 unidm bday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0s=bday0s+bday0sbday0s+bday0s
24 unidm bday0s+bday0sbday0s+bday0s=bday0s+bday0s
25 bday0s bday0s=
26 25 25 oveq12i bday0s+bday0s=+
27 0elon On
28 naddrid On+=
29 27 28 ax-mp +=
30 26 29 eqtri bday0s+bday0s=
31 23 24 30 3eqtri bday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0s=
32 31 uneq2i bdayD+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0s=bdayD+bdayE
33 un0 bdayD+bdayE=bdayD+bdayE
34 32 33 eqtri bdayD+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0s=bdayD+bdayE
35 ssun2 bdayD+bdayEbdayC+bdayFbdayD+bdayE
36 ssun2 bdayC+bdayFbdayD+bdayEbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
37 35 36 sstri bdayD+bdayEbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
38 ssun2 bdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
39 37 38 sstri bdayD+bdayEbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
40 34 39 eqsstri bdayD+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
41 40 sseli bdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayD+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sbdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
42 41 imim1i bdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdsebdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayD+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
43 42 6ralimi aNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdseaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayD+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
44 1 43 syl φaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayD+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
45 44 3 4 mulsproplem11 φDsENo
46 31 uneq2i bdayC+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0s=bdayC+bdayE
47 un0 bdayC+bdayE=bdayC+bdayE
48 46 47 eqtri bdayC+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0s=bdayC+bdayE
49 ssun1 bdayC+bdayEbdayC+bdayEbdayD+bdayF
50 ssun1 bdayC+bdayEbdayD+bdayFbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
51 49 50 sstri bdayC+bdayEbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
52 51 38 sstri bdayC+bdayEbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
53 48 52 eqsstri bdayC+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
54 53 sseli bdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayC+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sbdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
55 54 imim1i bdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdsebdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayC+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
56 55 6ralimi aNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdseaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayC+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
57 1 56 syl φaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayC+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
58 57 2 4 mulsproplem11 φCsENo
59 45 58 subscld φDsE-sCsENo
60 59 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsE-sCsENo
61 44 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayD+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
62 3 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFDNo
63 simprr1 bdayE=bdayFxNobdayxbdayEE<sxx<sFbdayxbdayE
64 63 adantl φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayxbdayE
65 bdayelon bdayEOn
66 simprrl φbdayE=bdayFxNobdayxbdayEE<sxx<sFxNo
67 oldbday bdayEOnxNoxOldbdayEbdayxbdayE
68 65 66 67 sylancr φbdayE=bdayFxNobdayxbdayEE<sxx<sFxOldbdayEbdayxbdayE
69 64 68 mpbird φbdayE=bdayFxNobdayxbdayEE<sxx<sFxOldbdayE
70 61 62 69 mulsproplem3 φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsxNo
71 57 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayC+bdayEbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
72 2 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFCNo
73 71 72 69 mulsproplem3 φbdayE=bdayFxNobdayxbdayEE<sxx<sFCsxNo
74 70 73 subscld φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsx-sCsxNo
75 31 uneq2i bdayD+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0s=bdayD+bdayF
76 un0 bdayD+bdayF=bdayD+bdayF
77 75 76 eqtri bdayD+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0s=bdayD+bdayF
78 ssun2 bdayD+bdayFbdayC+bdayEbdayD+bdayF
79 78 50 sstri bdayD+bdayFbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
80 79 38 sstri bdayD+bdayFbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
81 77 80 eqsstri bdayD+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
82 81 sseli bdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayD+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sbdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
83 82 imim1i bdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdsebdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayD+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
84 83 6ralimi aNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdseaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayD+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
85 1 84 syl φaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayD+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
86 85 3 5 mulsproplem11 φDsFNo
87 31 uneq2i bdayC+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0s=bdayC+bdayF
88 un0 bdayC+bdayF=bdayC+bdayF
89 87 88 eqtri bdayC+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0s=bdayC+bdayF
90 ssun1 bdayC+bdayFbdayC+bdayFbdayD+bdayE
91 90 36 sstri bdayC+bdayFbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
92 91 38 sstri bdayC+bdayFbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
93 89 92 eqsstri bdayC+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
94 93 sseli bdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayC+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sbdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
95 94 imim1i bdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdsebdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayC+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
96 95 6ralimi aNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEasbNoc<sde<sfcsf-scse<sdsf-sdseaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayC+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
97 1 96 syl φaNobNocNodNoeNofNobdaya+bdaybbdayc+bdayebdayd+bdayfbdayc+bdayfbdayd+bdayebdayC+bdayFbday0s+bday0sbday0s+bday0sbday0s+bday0sbday0s+bday0sasbNoc<sde<sfcsf-scse<sdsf-sdse
98 97 2 5 mulsproplem11 φCsFNo
99 86 98 subscld φDsF-sCsFNo
100 99 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsF-sCsFNo
101 1 mulsproplemcbv φgNohNoiNojNokNolNobdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEgshNoi<sjk<slisl-sisk<sjsl-sjsk
102 101 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFgNohNoiNojNokNolNobdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEgshNoi<sjk<slisl-sisk<sjsl-sjsk
103 onelss bdayEOnbdayxbdayEbdayxbdayE
104 65 64 103 mpsyl φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayxbdayE
105 simprl φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayE=bdayF
106 104 105 sseqtrd φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayxbdayF
107 bdayelon bdayxOn
108 bdayelon bdayFOn
109 bdayelon bdayDOn
110 naddss2 bdayxOnbdayFOnbdayDOnbdayxbdayFbdayD+bdayxbdayD+bdayF
111 107 108 109 110 mp3an bdayxbdayFbdayD+bdayxbdayD+bdayF
112 106 111 sylib φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayD+bdayxbdayD+bdayF
113 unss2 bdayD+bdayxbdayD+bdayFbdayC+bdayEbdayD+bdayxbdayC+bdayEbdayD+bdayF
114 112 113 syl φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayC+bdayEbdayD+bdayxbdayC+bdayEbdayD+bdayF
115 bdayelon bdayCOn
116 naddss2 bdayxOnbdayFOnbdayCOnbdayxbdayFbdayC+bdayxbdayC+bdayF
117 107 108 115 116 mp3an bdayxbdayFbdayC+bdayxbdayC+bdayF
118 106 117 sylib φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayC+bdayxbdayC+bdayF
119 unss1 bdayC+bdayxbdayC+bdayFbdayC+bdayxbdayD+bdayEbdayC+bdayFbdayD+bdayE
120 118 119 syl φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayC+bdayxbdayD+bdayEbdayC+bdayFbdayD+bdayE
121 unss12 bdayC+bdayEbdayD+bdayxbdayC+bdayEbdayD+bdayFbdayC+bdayxbdayD+bdayEbdayC+bdayFbdayD+bdayEbdayC+bdayEbdayD+bdayxbdayC+bdayxbdayD+bdayEbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
122 114 120 121 syl2anc φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayC+bdayEbdayD+bdayxbdayC+bdayxbdayD+bdayEbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
123 unss2 bdayC+bdayEbdayD+bdayxbdayC+bdayxbdayD+bdayEbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEbdayA+bdayBbdayC+bdayEbdayD+bdayxbdayC+bdayxbdayD+bdayEbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
124 122 123 syl φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayA+bdayBbdayC+bdayEbdayD+bdayxbdayC+bdayxbdayD+bdayEbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
125 124 sseld φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayxbdayC+bdayxbdayD+bdayEbdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
126 125 imim1d φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEgshNoi<sjk<slisl-sisk<sjsl-sjskbdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayxbdayC+bdayxbdayD+bdayEgshNoi<sjk<slisl-sisk<sjsl-sjsk
127 126 ralimd6v φbdayE=bdayFxNobdayxbdayEE<sxx<sFgNohNoiNojNokNolNobdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEgshNoi<sjk<slisl-sisk<sjsl-sjskgNohNoiNojNokNolNobdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayxbdayC+bdayxbdayD+bdayEgshNoi<sjk<slisl-sisk<sjsl-sjsk
128 102 127 mpd φbdayE=bdayFxNobdayxbdayEE<sxx<sFgNohNoiNojNokNolNobdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayxbdayC+bdayxbdayD+bdayEgshNoi<sjk<slisl-sisk<sjsl-sjsk
129 4 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFENo
130 6 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFC<sD
131 simprr2 bdayE=bdayFxNobdayxbdayEE<sxx<sFE<sx
132 131 adantl φbdayE=bdayFxNobdayxbdayEE<sxx<sFE<sx
133 64 olcd φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayEbdayxbdayxbdayE
134 128 72 62 129 66 130 132 133 mulsproplem13 φbdayE=bdayFxNobdayxbdayEE<sxx<sFCsx-sCsE<sDsx-sDsE
135 45 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsENo
136 58 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFCsENo
137 135 70 136 73 sltsubsub3bd φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsE-sCsE<sDsx-sCsxCsx-sCsE<sDsx-sDsE
138 134 137 mpbird φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsE-sCsE<sDsx-sCsx
139 naddss2 bdayxOnbdayEOnbdayCOnbdayxbdayEbdayC+bdayxbdayC+bdayE
140 107 65 115 139 mp3an bdayxbdayEbdayC+bdayxbdayC+bdayE
141 104 140 sylib φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayC+bdayxbdayC+bdayE
142 unss1 bdayC+bdayxbdayC+bdayEbdayC+bdayxbdayD+bdayFbdayC+bdayEbdayD+bdayF
143 141 142 syl φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayC+bdayxbdayD+bdayFbdayC+bdayEbdayD+bdayF
144 naddss2 bdayxOnbdayEOnbdayDOnbdayxbdayEbdayD+bdayxbdayD+bdayE
145 107 65 109 144 mp3an bdayxbdayEbdayD+bdayxbdayD+bdayE
146 104 145 sylib φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayD+bdayxbdayD+bdayE
147 unss2 bdayD+bdayxbdayD+bdayEbdayC+bdayFbdayD+bdayxbdayC+bdayFbdayD+bdayE
148 146 147 syl φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayC+bdayFbdayD+bdayxbdayC+bdayFbdayD+bdayE
149 unss12 bdayC+bdayxbdayD+bdayFbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayxbdayC+bdayFbdayD+bdayEbdayC+bdayxbdayD+bdayFbdayC+bdayFbdayD+bdayxbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
150 143 148 149 syl2anc φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayC+bdayxbdayD+bdayFbdayC+bdayFbdayD+bdayxbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
151 unss2 bdayC+bdayxbdayD+bdayFbdayC+bdayFbdayD+bdayxbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEbdayA+bdayBbdayC+bdayxbdayD+bdayFbdayC+bdayFbdayD+bdayxbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
152 150 151 syl φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayA+bdayBbdayC+bdayxbdayD+bdayFbdayC+bdayFbdayD+bdayxbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
153 152 sseld φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayxbdayD+bdayFbdayC+bdayFbdayD+bdayxbdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayE
154 153 imim1d φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEgshNoi<sjk<slisl-sisk<sjsl-sjskbdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayxbdayD+bdayFbdayC+bdayFbdayD+bdayxgshNoi<sjk<slisl-sisk<sjsl-sjsk
155 154 ralimd6v φbdayE=bdayFxNobdayxbdayEE<sxx<sFgNohNoiNojNokNolNobdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayEbdayD+bdayFbdayC+bdayFbdayD+bdayEgshNoi<sjk<slisl-sisk<sjsl-sjskgNohNoiNojNokNolNobdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayxbdayD+bdayFbdayC+bdayFbdayD+bdayxgshNoi<sjk<slisl-sisk<sjsl-sjsk
156 102 155 mpd φbdayE=bdayFxNobdayxbdayEE<sxx<sFgNohNoiNojNokNolNobdayg+bdayhbdayi+bdaykbdayj+bdaylbdayi+bdaylbdayj+bdaykbdayA+bdayBbdayC+bdayxbdayD+bdayFbdayC+bdayFbdayD+bdayxgshNoi<sjk<slisl-sisk<sjsl-sjsk
157 5 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFFNo
158 simprr3 bdayE=bdayFxNobdayxbdayEE<sxx<sFx<sF
159 158 adantl φbdayE=bdayFxNobdayxbdayEE<sxx<sFx<sF
160 64 105 eleqtrd φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayxbdayF
161 160 orcd φbdayE=bdayFxNobdayxbdayEE<sxx<sFbdayxbdayFbdayFbdayx
162 156 72 62 66 157 130 159 161 mulsproplem13 φbdayE=bdayFxNobdayxbdayEE<sxx<sFCsF-sCsx<sDsF-sDsx
163 86 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsFNo
164 98 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFCsFNo
165 70 163 73 164 sltsubsub3bd φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsx-sCsx<sDsF-sCsFCsF-sCsx<sDsF-sDsx
166 162 165 mpbird φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsx-sCsx<sDsF-sCsF
167 60 74 100 138 166 slttrd φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsE-sCsE<sDsF-sCsF
168 45 86 58 98 sltsubsub3bd φDsE-sCsE<sDsF-sCsFCsF-sCsE<sDsF-sDsE
169 168 adantr φbdayE=bdayFxNobdayxbdayEE<sxx<sFDsE-sCsE<sDsF-sCsFCsF-sCsE<sDsF-sDsE
170 167 169 mpbid φbdayE=bdayFxNobdayxbdayEE<sxx<sFCsF-sCsE<sDsF-sDsE
171 170 anassrs φbdayE=bdayFxNobdayxbdayEE<sxx<sFCsF-sCsE<sDsF-sDsE
172 22 171 rexlimddv φbdayE=bdayFCsF-sCsE<sDsF-sDsE
173 65 onordi OrdbdayE
174 108 onordi OrdbdayF
175 ordtri3or OrdbdayEOrdbdayFbdayEbdayFbdayE=bdayFbdayFbdayE
176 173 174 175 mp2an bdayEbdayFbdayE=bdayFbdayFbdayE
177 df-3or bdayEbdayFbdayE=bdayFbdayFbdayEbdayEbdayFbdayE=bdayFbdayFbdayE
178 or32 bdayEbdayFbdayE=bdayFbdayFbdayEbdayEbdayFbdayFbdayEbdayE=bdayF
179 177 178 bitri bdayEbdayFbdayE=bdayFbdayFbdayEbdayEbdayFbdayFbdayEbdayE=bdayF
180 176 179 mpbi bdayEbdayFbdayFbdayEbdayE=bdayF
181 180 a1i φbdayEbdayFbdayFbdayEbdayE=bdayF
182 16 172 181 mpjaodan φCsF-sCsE<sDsF-sDsE