Metamath Proof Explorer


Theorem supmul

Description: The supremum function distributes over multiplication, in the sense that ( sup A ) x. ( sup B ) = sup ( A x. B ) , where A x. B is shorthand for { a x. b | a e. A , b e. B } and is defined as C below. We made use of this in our definition of multiplication in the Dedekind cut construction of the reals (see df-mp ). (Contributed by Mario Carneiro, 5-Jul-2013) (Revised by Mario Carneiro, 6-Sep-2014)

Ref Expression
Hypotheses supmul.1 C=z|vAbBz=vb
supmul.2 φxA0xxB0xAAxyAyxBBxyByx
Assertion supmul φsupA<supB<=supC<

Proof

Step Hyp Ref Expression
1 supmul.1 C=z|vAbBz=vb
2 supmul.2 φxA0xxB0xAAxyAyxBBxyByx
3 2 simp2bi φAAxyAyx
4 suprcl AAxyAyxsupA<
5 3 4 syl φsupA<
6 2 simp3bi φBBxyByx
7 suprcl BBxyByxsupB<
8 6 7 syl φsupB<
9 recn supA<supA<
10 recn supB<supB<
11 mulcom supA<supB<supA<supB<=supB<supA<
12 9 10 11 syl2an supA<supB<supA<supB<=supB<supA<
13 5 8 12 syl2anc φsupA<supB<=supB<supA<
14 6 simp2d φB
15 n0 BbbB
16 14 15 sylib φbbB
17 0red φbB0
18 6 simp1d φB
19 18 sselda φbBb
20 8 adantr φbBsupB<
21 simp1r xA0xxB0xAAxyAyxBBxyByxxB0x
22 2 21 sylbi φxB0x
23 breq2 x=b0x0b
24 23 rspccv xB0xbB0b
25 22 24 syl φbB0b
26 25 imp φbB0b
27 suprub BBxyByxbBbsupB<
28 6 27 sylan φbBbsupB<
29 17 19 20 26 28 letrd φbB0supB<
30 16 29 exlimddv φ0supB<
31 simp1l xA0xxB0xAAxyAyxBBxyByxxA0x
32 2 31 sylbi φxA0x
33 eqid z|aAz=supB<a=z|aAz=supB<a
34 biid supB<0supB<xA0xAAxyAyxsupB<0supB<xA0xAAxyAyx
35 33 34 supmul1 supB<0supB<xA0xAAxyAyxsupB<supA<=supz|aAz=supB<a<
36 8 30 32 3 35 syl31anc φsupB<supA<=supz|aAz=supB<a<
37 13 36 eqtrd φsupA<supB<=supz|aAz=supB<a<
38 vex wV
39 eqeq1 z=wz=supB<aw=supB<a
40 39 rexbidv z=waAz=supB<aaAw=supB<a
41 38 40 elab wz|aAz=supB<aaAw=supB<a
42 8 adantr φaAsupB<
43 3 simp1d φA
44 43 sselda φaAa
45 recn aa
46 mulcom supB<asupB<a=asupB<
47 10 45 46 syl2an supB<asupB<a=asupB<
48 42 44 47 syl2anc φaAsupB<a=asupB<
49 breq2 x=a0x0a
50 49 rspccv xA0xaA0a
51 32 50 syl φaA0a
52 51 imp φaA0a
53 22 adantr φaAxB0x
54 6 adantr φaABBxyByx
55 eqid z|bBz=ab=z|bBz=ab
56 biid a0axB0xBBxyByxa0axB0xBBxyByx
57 55 56 supmul1 a0axB0xBBxyByxasupB<=supz|bBz=ab<
58 44 52 53 54 57 syl31anc φaAasupB<=supz|bBz=ab<
59 eqeq1 z=wz=abw=ab
60 59 rexbidv z=wbBz=abbBw=ab
61 38 60 elab wz|bBz=abbBw=ab
62 rspe aAbBw=abaAbBw=ab
63 oveq1 v=avb=ab
64 63 eqeq2d v=az=vbz=ab
65 64 rexbidv v=abBz=vbbBz=ab
66 65 cbvrexvw vAbBz=vbaAbBz=ab
67 59 2rexbidv z=waAbBz=abaAbBw=ab
68 66 67 syl5bb z=wvAbBz=vbaAbBw=ab
69 38 68 1 elab2 wCaAbBw=ab
70 62 69 sylibr aAbBw=abwC
71 70 ex aAbBw=abwC
72 1 2 supmullem2 φCCxwCwx
73 suprub CCxwCwxwCwsupC<
74 73 ex CCxwCwxwCwsupC<
75 72 74 syl φwCwsupC<
76 71 75 sylan9r φaAbBw=abwsupC<
77 61 76 syl5bi φaAwz|bBz=abwsupC<
78 77 ralrimiv φaAwz|bBz=abwsupC<
79 44 adantr φaAbBa
80 19 adantlr φaAbBb
81 79 80 remulcld φaAbBab
82 eleq1a abz=abz
83 81 82 syl φaAbBz=abz
84 83 rexlimdva φaAbBz=abz
85 84 abssdv φaAz|bBz=ab
86 ovex abV
87 86 isseti ww=ab
88 87 rgenw bBww=ab
89 r19.2z BbBww=abbBww=ab
90 14 88 89 sylancl φbBww=ab
91 rexcom4 bBww=abwbBw=ab
92 90 91 sylib φwbBw=ab
93 60 cbvexvw zbBz=abwbBw=ab
94 92 93 sylibr φzbBz=ab
95 abn0 z|bBz=abzbBz=ab
96 94 95 sylibr φz|bBz=ab
97 96 adantr φaAz|bBz=ab
98 suprcl CCxwCwxsupC<
99 72 98 syl φsupC<
100 99 adantr φaAsupC<
101 brralrspcev supC<wz|bBz=abwsupC<xwz|bBz=abwx
102 100 78 101 syl2anc φaAxwz|bBz=abwx
103 suprleub z|bBz=abz|bBz=abxwz|bBz=abwxsupC<supz|bBz=ab<supC<wz|bBz=abwsupC<
104 85 97 102 100 103 syl31anc φaAsupz|bBz=ab<supC<wz|bBz=abwsupC<
105 78 104 mpbird φaAsupz|bBz=ab<supC<
106 58 105 eqbrtrd φaAasupB<supC<
107 48 106 eqbrtrd φaAsupB<asupC<
108 breq1 w=supB<awsupC<supB<asupC<
109 107 108 syl5ibrcom φaAw=supB<awsupC<
110 109 rexlimdva φaAw=supB<awsupC<
111 41 110 syl5bi φwz|aAz=supB<awsupC<
112 111 ralrimiv φwz|aAz=supB<awsupC<
113 42 44 remulcld φaAsupB<a
114 eleq1a supB<az=supB<az
115 113 114 syl φaAz=supB<az
116 115 rexlimdva φaAz=supB<az
117 116 abssdv φz|aAz=supB<a
118 3 simp2d φA
119 ovex supB<aV
120 119 isseti zz=supB<a
121 120 rgenw aAzz=supB<a
122 r19.2z AaAzz=supB<aaAzz=supB<a
123 118 121 122 sylancl φaAzz=supB<a
124 rexcom4 aAzz=supB<azaAz=supB<a
125 123 124 sylib φzaAz=supB<a
126 abn0 z|aAz=supB<azaAz=supB<a
127 125 126 sylibr φz|aAz=supB<a
128 brralrspcev supC<wz|aAz=supB<awsupC<xwz|aAz=supB<awx
129 99 112 128 syl2anc φxwz|aAz=supB<awx
130 suprleub z|aAz=supB<az|aAz=supB<axwz|aAz=supB<awxsupC<supz|aAz=supB<a<supC<wz|aAz=supB<awsupC<
131 117 127 129 99 130 syl31anc φsupz|aAz=supB<a<supC<wz|aAz=supB<awsupC<
132 112 131 mpbird φsupz|aAz=supB<a<supC<
133 37 132 eqbrtrd φsupA<supB<supC<
134 1 2 supmullem1 φwCwsupA<supB<
135 5 8 remulcld φsupA<supB<
136 suprleub CCxwCwxsupA<supB<supC<supA<supB<wCwsupA<supB<
137 72 135 136 syl2anc φsupC<supA<supB<wCwsupA<supB<
138 134 137 mpbird φsupC<supA<supB<
139 135 99 letri3d φsupA<supB<=supC<supA<supB<supC<supC<supA<supB<
140 133 138 139 mpbir2and φsupA<supB<=supC<