smfmullem1

Description: The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfmullem1.a	$⊢ φ \to A \in ℝ$
	smfmullem1.u	$⊢ φ \to U \in ℝ$
	smfmullem1.v	$⊢ φ \to V \in ℝ$
	smfmullem1.l	$⊢ φ \to U V < A$
	smfmullem1.x	$⊢ X = \frac{A - U V}{1 + \|U\| + \|V\|}$
	smfmullem1.y	$⊢ Y = if (1 \leq X, 1, X)$
	smfmullem1.p	$⊢ φ \to P \in (U - Y, U)$
	smfmullem1.r	$⊢ φ \to R \in (U, U + Y)$
	smfmullem1.s	$⊢ φ \to S \in (V - Y, V)$
	smfmullem1.z	$⊢ φ \to Z \in (V, V + Y)$
	smfmullem1.h	$⊢ φ \to H \in (P, R)$
	smfmullem1.i	$⊢ φ \to I \in (S, Z)$
Assertion	smfmullem1	$⊢ φ \to H \cdot I < A$

Proof

Step	Hyp	Ref	Expression
1		smfmullem1.a	$⊢ φ \to A \in ℝ$
2		smfmullem1.u	$⊢ φ \to U \in ℝ$
3		smfmullem1.v	$⊢ φ \to V \in ℝ$
4		smfmullem1.l	$⊢ φ \to U V < A$
5		smfmullem1.x	$⊢ X = \frac{A - U V}{1 + \|U\| + \|V\|}$
6		smfmullem1.y	$⊢ Y = if (1 \leq X, 1, X)$
7		smfmullem1.p	$⊢ φ \to P \in (U - Y, U)$
8		smfmullem1.r	$⊢ φ \to R \in (U, U + Y)$
9		smfmullem1.s	$⊢ φ \to S \in (V - Y, V)$
10		smfmullem1.z	$⊢ φ \to Z \in (V, V + Y)$
11		smfmullem1.h	$⊢ φ \to H \in (P, R)$
12		smfmullem1.i	$⊢ φ \to I \in (S, Z)$
13	11	elioored	$⊢ φ \to H \in ℝ$
14	13	recnd	$⊢ φ \to H \in ℂ$
15	2	recnd	$⊢ φ \to U \in ℂ$
16	12	elioored	$⊢ φ \to I \in ℝ$
17	16	recnd	$⊢ φ \to I \in ℂ$
18	3	recnd	$⊢ φ \to V \in ℂ$
19	14 15 17 18	mulsubd	$⊢ φ \to (H - U) (I - V) = H \cdot I + V U - (H V + I U)$
20	14 15 18	subdird	$⊢ φ \to (H - U) V = H V - U V$
21	15 17 18	subdid	$⊢ φ \to U (I - V) = U \cdot I - U V$
22	20 21	oveq12d	$⊢ φ \to (H - U) V + U (I - V) = (H V - U V) + U \cdot I - U V$
23	14 18	mulcld	$⊢ φ \to H V \in ℂ$
24	15 17	mulcld	$⊢ φ \to U \cdot I \in ℂ$
25	15 18	mulcld	$⊢ φ \to U V \in ℂ$
26	23 24 25 25	addsub4d	$⊢ φ \to H V + U \cdot I - (U V + U V) = (H V - U V) + U \cdot I - U V$
27	26	eqcomd	$⊢ φ \to (H V - U V) + U \cdot I - U V = H V + U \cdot I - (U V + U V)$
28	15 17	mulcomd	$⊢ φ \to U \cdot I = I U$
29	28	oveq2d	$⊢ φ \to H V + U \cdot I = H V + I U$
30	29	oveq1d	$⊢ φ \to H V + U \cdot I - (U V + U V) = H V + I U - (U V + U V)$
31	22 27 30	3eqtrd	$⊢ φ \to (H - U) V + U (I - V) = H V + I U - (U V + U V)$
32	19 31	oveq12d	$⊢ φ \to (H - U) (I - V) + (H - U) V + U (I - V) = (H \cdot I + V U - (H V + I U)) + (H V + I U) - (U V + U V)$
33	14 17	mulcld	$⊢ φ \to H \cdot I \in ℂ$
34	18 15	mulcld	$⊢ φ \to V U \in ℂ$
35	33 34	addcld	$⊢ φ \to H \cdot I + V U \in ℂ$
36	17 15	mulcld	$⊢ φ \to I U \in ℂ$
37	23 36	addcld	$⊢ φ \to H V + I U \in ℂ$
38	35 37	npcand	$⊢ φ \to (H \cdot I + V U - (H V + I U)) + H V + I U = H \cdot I + V U$
39	18 15	mulcomd	$⊢ φ \to V U = U V$
40	39	oveq2d	$⊢ φ \to H \cdot I + V U = H \cdot I + U V$
41	38 40	eqtrd	$⊢ φ \to (H \cdot I + V U - (H V + I U)) + H V + I U = H \cdot I + U V$
42	41	eqcomd	$⊢ φ \to H \cdot I + U V = (H \cdot I + V U - (H V + I U)) + H V + I U$
43	42	oveq1d	$⊢ φ \to H \cdot I + U V - (U V + U V) = (H \cdot I + V U - (H V + I U)) + (H V + I U) - (U V + U V)$
44	35 37	subcld	$⊢ φ \to H \cdot I + V U - (H V + I U) \in ℂ$
45	25 25	addcld	$⊢ φ \to U V + U V \in ℂ$
46	44 37 45	addsubassd	$⊢ φ \to (H \cdot I + V U - (H V + I U)) + (H V + I U) - (U V + U V) = (H \cdot I + V U - (H V + I U)) + (H V + I U) - (U V + U V)$
47	43 46	eqtr2d	$⊢ φ \to (H \cdot I + V U - (H V + I U)) + (H V + I U) - (U V + U V) = H \cdot I + U V - (U V + U V)$
48	33 25 25	pnpcan2d	$⊢ φ \to H \cdot I + U V - (U V + U V) = H \cdot I - U V$
49	32 47 48	3eqtrrd	$⊢ φ \to H \cdot I - U V = (H - U) (I - V) + (H - U) V + U (I - V)$
50	13 2	jca	$⊢ φ \to (H \in ℝ \land U \in ℝ)$
51		resubcl	$⊢ (H \in ℝ \land U \in ℝ) \to H - U \in ℝ$
52	50 51	syl	$⊢ φ \to H - U \in ℝ$
53	16 3	jca	$⊢ φ \to (I \in ℝ \land V \in ℝ)$
54		resubcl	$⊢ (I \in ℝ \land V \in ℝ) \to I - V \in ℝ$
55	53 54	syl	$⊢ φ \to I - V \in ℝ$
56	52 55	jca	$⊢ φ \to (H - U \in ℝ \land I - V \in ℝ)$
57		remulcl	$⊢ (H - U \in ℝ \land I - V \in ℝ) \to (H - U) (I - V) \in ℝ$
58	56 57	syl	$⊢ φ \to (H - U) (I - V) \in ℝ$
59	52 3	jca	$⊢ φ \to (H - U \in ℝ \land V \in ℝ)$
60		remulcl	$⊢ (H - U \in ℝ \land V \in ℝ) \to (H - U) V \in ℝ$
61	59 60	syl	$⊢ φ \to (H - U) V \in ℝ$
62	2 55	jca	$⊢ φ \to (U \in ℝ \land I - V \in ℝ)$
63		remulcl	$⊢ (U \in ℝ \land I - V \in ℝ) \to U (I - V) \in ℝ$
64	62 63	syl	$⊢ φ \to U (I - V) \in ℝ$
65	61 64	jca	$⊢ φ \to ((H - U) V \in ℝ \land U (I - V) \in ℝ)$
66		readdcl	$⊢ ((H - U) V \in ℝ \land U (I - V) \in ℝ) \to (H - U) V + U (I - V) \in ℝ$
67	65 66	syl	$⊢ φ \to (H - U) V + U (I - V) \in ℝ$
68	58 67	jca	$⊢ φ \to ((H - U) (I - V) \in ℝ \land (H - U) V + U (I - V) \in ℝ)$
69		readdcl	$⊢ ((H - U) (I - V) \in ℝ \land (H - U) V + U (I - V) \in ℝ) \to (H - U) (I - V) + (H - U) V + U (I - V) \in ℝ$
70	68 69	syl	$⊢ φ \to (H - U) (I - V) + (H - U) V + U (I - V) \in ℝ$
71	6	a1i	$⊢ φ \to Y = if (1 \leq X, 1, X)$
72		1rp	$⊢ 1 \in ℝ^{+}$
73	72	a1i	$⊢ φ \to 1 \in ℝ^{+}$
74	5	a1i	$⊢ φ \to X = \frac{A - U V}{1 + \|U\| + \|V\|}$
75	2 3	remulcld	$⊢ φ \to U V \in ℝ$
76		difrp	$⊢ (U V \in ℝ \land A \in ℝ) \to (U V < A \leftrightarrow A - U V \in ℝ^{+})$
77	75 1 76	syl2anc	$⊢ φ \to (U V < A \leftrightarrow A - U V \in ℝ^{+})$
78	4 77	mpbid	$⊢ φ \to A - U V \in ℝ^{+}$
79		1red	$⊢ φ \to 1 \in ℝ$
80	15	abscld	$⊢ φ \to \|U\| \in ℝ$
81	18	abscld	$⊢ φ \to \|V\| \in ℝ$
82	80 81	readdcld	$⊢ φ \to \|U\| + \|V\| \in ℝ$
83	79 82	readdcld	$⊢ φ \to 1 + \|U\| + \|V\| \in ℝ$
84		0re	$⊢ 0 \in ℝ$
85	84	a1i	$⊢ φ \to 0 \in ℝ$
86	73	rpgt0d	$⊢ φ \to 0 < 1$
87	15	absge0d	$⊢ φ \to 0 \leq \|U\|$
88	18	absge0d	$⊢ φ \to 0 \leq \|V\|$
89	80 81	addge01d	$⊢ φ \to (0 \leq \|V\| \leftrightarrow \|U\| \leq \|U\| + \|V\|)$
90	88 89	mpbid	$⊢ φ \to \|U\| \leq \|U\| + \|V\|$
91	85 80 82 87 90	letrd	$⊢ φ \to 0 \leq \|U\| + \|V\|$
92	79 82	addge01d	$⊢ φ \to (0 \leq \|U\| + \|V\| \leftrightarrow 1 \leq 1 + \|U\| + \|V\|)$
93	91 92	mpbid	$⊢ φ \to 1 \leq 1 + \|U\| + \|V\|$
94	85 79 83 86 93	ltletrd	$⊢ φ \to 0 < 1 + \|U\| + \|V\|$
95	83 94	elrpd	$⊢ φ \to 1 + \|U\| + \|V\| \in ℝ^{+}$
96	78 95	rpdivcld	$⊢ φ \to \frac{A - U V}{1 + \|U\| + \|V\|} \in ℝ^{+}$
97	74 96	eqeltrd	$⊢ φ \to X \in ℝ^{+}$
98	73 97	ifcld	$⊢ φ \to if (1 \leq X, 1, X) \in ℝ^{+}$
99	71 98	eqeltrd	$⊢ φ \to Y \in ℝ^{+}$
100	99	rpred	$⊢ φ \to Y \in ℝ$
101		resqcl	$⊢ Y \in ℝ \to Y^{2} \in ℝ$
102	100 101	syl	$⊢ φ \to Y^{2} \in ℝ$
103	100 81	remulcld	$⊢ φ \to Y \|V\| \in ℝ$
104	100 80	remulcld	$⊢ φ \to Y \|U\| \in ℝ$
105	103 104	jca	$⊢ φ \to (Y \|V\| \in ℝ \land Y \|U\| \in ℝ)$
106		readdcl	$⊢ (Y \|V\| \in ℝ \land Y \|U\| \in ℝ) \to Y \|V\| + Y \|U\| \in ℝ$
107	105 106	syl	$⊢ φ \to Y \|V\| + Y \|U\| \in ℝ$
108	102 107	jca	$⊢ φ \to (Y^{2} \in ℝ \land Y \|V\| + Y \|U\| \in ℝ)$
109		readdcl	$⊢ (Y^{2} \in ℝ \land Y \|V\| + Y \|U\| \in ℝ) \to Y^{2} + Y \|V\| + Y \|U\| \in ℝ$
110	108 109	syl	$⊢ φ \to Y^{2} + Y \|V\| + Y \|U\| \in ℝ$
111	1 75	resubcld	$⊢ φ \to A - U V \in ℝ$
112	100	resqcld	$⊢ φ \to Y^{2} \in ℝ$
113	103 104	readdcld	$⊢ φ \to Y \|V\| + Y \|U\| \in ℝ$
114	19 44	eqeltrd	$⊢ φ \to (H - U) (I - V) \in ℂ$
115	114	abscld	$⊢ φ \to \|(H - U) (I - V)\| \in ℝ$
116	100 100	remulcld	$⊢ φ \to Y Y \in ℝ$
117	58	leabsd	$⊢ φ \to (H - U) (I - V) \leq \|(H - U) (I - V)\|$
118	52	recnd	$⊢ φ \to H - U \in ℂ$
119	55	recnd	$⊢ φ \to I - V \in ℂ$
120	118 119	absmuld	$⊢ φ \to \|(H - U) (I - V)\| = \|H - U\| \|I - V\|$
121	118	abscld	$⊢ φ \to \|H - U\| \in ℝ$
122	119	abscld	$⊢ φ \to \|I - V\| \in ℝ$
123	118	absge0d	$⊢ φ \to 0 \leq \|H - U\|$
124	2 100	resubcld	$⊢ φ \to U - Y \in ℝ$
125	7	elioored	$⊢ φ \to P \in ℝ$
126	124	rexrd	$⊢ φ \to U - Y \in ℝ^{*}$
127	2	rexrd	$⊢ φ \to U \in ℝ^{*}$
128		ioogtlb	$⊢ (U - Y \in ℝ^{} \land U \in ℝ^{} \land P \in (U - Y, U)) \to U - Y < P$
129	126 127 7 128	syl3anc	$⊢ φ \to U - Y < P$
130	125	rexrd	$⊢ φ \to P \in ℝ^{*}$
131	8	elioored	$⊢ φ \to R \in ℝ$
132	131	rexrd	$⊢ φ \to R \in ℝ^{*}$
133		ioogtlb	$⊢ (P \in ℝ^{} \land R \in ℝ^{} \land H \in (P, R)) \to P < H$
134	130 132 11 133	syl3anc	$⊢ φ \to P < H$
135	124 125 13 129 134	lttrd	$⊢ φ \to U - Y < H$
136	2 100	readdcld	$⊢ φ \to U + Y \in ℝ$
137		iooltub	$⊢ (P \in ℝ^{} \land R \in ℝ^{} \land H \in (P, R)) \to H < R$
138	130 132 11 137	syl3anc	$⊢ φ \to H < R$
139	136	rexrd	$⊢ φ \to U + Y \in ℝ^{*}$
140		iooltub	$⊢ (U \in ℝ^{} \land U + Y \in ℝ^{} \land R \in (U, U + Y)) \to R < U + Y$
141	127 139 8 140	syl3anc	$⊢ φ \to R < U + Y$
142	13 131 136 138 141	lttrd	$⊢ φ \to H < U + Y$
143	135 142	jca	$⊢ φ \to (U - Y < H \land H < U + Y)$
144	13 2 100	absdifltd	$⊢ φ \to (\|H - U\| < Y \leftrightarrow (U - Y < H \land H < U + Y))$
145	143 144	mpbird	$⊢ φ \to \|H - U\| < Y$
146	119	absge0d	$⊢ φ \to 0 \leq \|I - V\|$
147	3 100	resubcld	$⊢ φ \to V - Y \in ℝ$
148	9	elioored	$⊢ φ \to S \in ℝ$
149	147	rexrd	$⊢ φ \to V - Y \in ℝ^{*}$
150	3	rexrd	$⊢ φ \to V \in ℝ^{*}$
151	149 150 9	ioogtlbd	$⊢ φ \to V - Y < S$
152	148	rexrd	$⊢ φ \to S \in ℝ^{*}$
153	10	elioored	$⊢ φ \to Z \in ℝ$
154	153	rexrd	$⊢ φ \to Z \in ℝ^{*}$
155	152 154 12	ioogtlbd	$⊢ φ \to S < I$
156	147 148 16 151 155	lttrd	$⊢ φ \to V - Y < I$
157	3 100	readdcld	$⊢ φ \to V + Y \in ℝ$
158	152 154 12	iooltubd	$⊢ φ \to I < Z$
159	157	rexrd	$⊢ φ \to V + Y \in ℝ^{*}$
160	150 159 10	iooltubd	$⊢ φ \to Z < V + Y$
161	16 153 157 158 160	lttrd	$⊢ φ \to I < V + Y$
162	156 161	jca	$⊢ φ \to (V - Y < I \land I < V + Y)$
163	16 3 100	absdifltd	$⊢ φ \to (\|I - V\| < Y \leftrightarrow (V - Y < I \land I < V + Y))$
164	162 163	mpbird	$⊢ φ \to \|I - V\| < Y$
165	121 100 122 100 123 145 146 164	ltmul12ad	$⊢ φ \to \|H - U\| \|I - V\| < Y Y$
166	120 165	eqbrtrd	$⊢ φ \to \|(H - U) (I - V)\| < Y Y$
167	58 115 116 117 166	lelttrd	$⊢ φ \to (H - U) (I - V) < Y Y$
168	100	recnd	$⊢ φ \to Y \in ℂ$
169	168	sqvald	$⊢ φ \to Y^{2} = Y Y$
170	169	eqcomd	$⊢ φ \to Y Y = Y^{2}$
171	167 170	breqtrd	$⊢ φ \to (H - U) (I - V) < Y^{2}$
172	61	recnd	$⊢ φ \to (H - U) V \in ℂ$
173	172	abscld	$⊢ φ \to \|(H - U) V\| \in ℝ$
174	61	leabsd	$⊢ φ \to (H - U) V \leq \|(H - U) V\|$
175	118 18	absmuld	$⊢ φ \to \|(H - U) V\| = \|H - U\| \|V\|$
176	121 100 145	ltled	$⊢ φ \to \|H - U\| \leq Y$
177	121 100 81 88 176	lemul1ad	$⊢ φ \to \|H - U\| \|V\| \leq Y \|V\|$
178	175 177	eqbrtrd	$⊢ φ \to \|(H - U) V\| \leq Y \|V\|$
179	61 173 103 174 178	letrd	$⊢ φ \to (H - U) V \leq Y \|V\|$
180	64	recnd	$⊢ φ \to U (I - V) \in ℂ$
181	180	abscld	$⊢ φ \to \|U (I - V)\| \in ℝ$
182	64	leabsd	$⊢ φ \to U (I - V) \leq \|U (I - V)\|$
183	15 119	absmuld	$⊢ φ \to \|U (I - V)\| = \|U\| \|I - V\|$
184	80	recnd	$⊢ φ \to \|U\| \in ℂ$
185	122	recnd	$⊢ φ \to \|I - V\| \in ℂ$
186	184 185	mulcomd	$⊢ φ \to \|U\| \|I - V\| = \|I - V\| \|U\|$
187	183 186	eqtrd	$⊢ φ \to \|U (I - V)\| = \|I - V\| \|U\|$
188	122 100 164	ltled	$⊢ φ \to \|I - V\| \leq Y$
189	122 100 80 87 188	lemul1ad	$⊢ φ \to \|I - V\| \|U\| \leq Y \|U\|$
190	187 189	eqbrtrd	$⊢ φ \to \|U (I - V)\| \leq Y \|U\|$
191	64 181 104 182 190	letrd	$⊢ φ \to U (I - V) \leq Y \|U\|$
192	61 64 103 104 179 191	leadd12dd	$⊢ φ \to (H - U) V + U (I - V) \leq Y \|V\| + Y \|U\|$
193	58 67 112 113 171 192	ltleaddd	$⊢ φ \to (H - U) (I - V) + (H - U) V + U (I - V) < Y^{2} + Y \|V\| + Y \|U\|$
194	100 107	readdcld	$⊢ φ \to Y + Y \|V\| + Y \|U\| \in ℝ$
195	85 121 100 123 176	letrd	$⊢ φ \to 0 \leq Y$
196	97	rpred	$⊢ φ \to X \in ℝ$
197		min1	$⊢ (1 \in ℝ \land X \in ℝ) \to if (1 \leq X, 1, X) \leq 1$
198	79 196 197	syl2anc	$⊢ φ \to if (1 \leq X, 1, X) \leq 1$
199	6 198	eqbrtrid	$⊢ φ \to Y \leq 1$
200	85 79 100 195 199	eliccd	$⊢ φ \to Y \in [0, 1]$
201	100	sqrlearg	$⊢ φ \to (Y^{2} \leq Y \leftrightarrow Y \in [0, 1])$
202	200 201	mpbird	$⊢ φ \to Y^{2} \leq Y$
203	102 100 107 202	leadd1dd	$⊢ φ \to Y^{2} + Y \|V\| + Y \|U\| \leq Y + Y \|V\| + Y \|U\|$
204		1cnd	$⊢ φ \to 1 \in ℂ$
205	81	recnd	$⊢ φ \to \|V\| \in ℂ$
206	205 184	addcld	$⊢ φ \to \|V\| + \|U\| \in ℂ$
207	168 204 206	adddid	$⊢ φ \to Y (1 + \|V\| + \|U\|) = Y \cdot 1 + Y (\|V\| + \|U\|)$
208	168	mulid1d	$⊢ φ \to Y \cdot 1 = Y$
209	168 205 184	adddid	$⊢ φ \to Y (\|V\| + \|U\|) = Y \|V\| + Y \|U\|$
210	208 209	oveq12d	$⊢ φ \to Y \cdot 1 + Y (\|V\| + \|U\|) = Y + Y \|V\| + Y \|U\|$
211	207 210	eqtr2d	$⊢ φ \to Y + Y \|V\| + Y \|U\| = Y (1 + \|V\| + \|U\|)$
212	81 80	readdcld	$⊢ φ \to \|V\| + \|U\| \in ℝ$
213	79 212	readdcld	$⊢ φ \to 1 + \|V\| + \|U\| \in ℝ$
214	81 80	addge01d	$⊢ φ \to (0 \leq \|U\| \leftrightarrow \|V\| \leq \|V\| + \|U\|)$
215	87 214	mpbid	$⊢ φ \to \|V\| \leq \|V\| + \|U\|$
216	85 81 212 88 215	letrd	$⊢ φ \to 0 \leq \|V\| + \|U\|$
217	79 212	addge01d	$⊢ φ \to (0 \leq \|V\| + \|U\| \leftrightarrow 1 \leq 1 + \|V\| + \|U\|)$
218	216 217	mpbid	$⊢ φ \to 1 \leq 1 + \|V\| + \|U\|$
219	85 79 213 86 218	ltletrd	$⊢ φ \to 0 < 1 + \|V\| + \|U\|$
220	85 213 219	ltled	$⊢ φ \to 0 \leq 1 + \|V\| + \|U\|$
221		min2	$⊢ (1 \in ℝ \land X \in ℝ) \to if (1 \leq X, 1, X) \leq X$
222	79 196 221	syl2anc	$⊢ φ \to if (1 \leq X, 1, X) \leq X$
223	71 222	eqbrtrd	$⊢ φ \to Y \leq X$
224	100 196 213 220 223	lemul1ad	$⊢ φ \to Y (1 + \|V\| + \|U\|) \leq X (1 + \|V\| + \|U\|)$
225	74	oveq1d	$⊢ φ \to X (1 + \|V\| + \|U\|) = (\frac{A - U V}{1 + \|U\| + \|V\|}) (1 + \|V\| + \|U\|)$
226	184 205	addcomd	$⊢ φ \to \|U\| + \|V\| = \|V\| + \|U\|$
227	226	oveq2d	$⊢ φ \to 1 + \|U\| + \|V\| = 1 + \|V\| + \|U\|$
228	227	oveq2d	$⊢ φ \to \frac{A - U V}{1 + \|U\| + \|V\|} = \frac{A - U V}{1 + \|V\| + \|U\|}$
229	228	oveq1d	$⊢ φ \to (\frac{A - U V}{1 + \|U\| + \|V\|}) (1 + \|V\| + \|U\|) = (\frac{A - U V}{1 + \|V\| + \|U\|}) (1 + \|V\| + \|U\|)$
230	111	recnd	$⊢ φ \to A - U V \in ℂ$
231	204 206	addcld	$⊢ φ \to 1 + \|V\| + \|U\| \in ℂ$
232	85 219	gtned	$⊢ φ \to 1 + \|V\| + \|U\| \neq 0$
233	230 231 232	divcan1d	$⊢ φ \to (\frac{A - U V}{1 + \|V\| + \|U\|}) (1 + \|V\| + \|U\|) = A - U V$
234	225 229 233	3eqtrd	$⊢ φ \to X (1 + \|V\| + \|U\|) = A - U V$
235	224 234	breqtrd	$⊢ φ \to Y (1 + \|V\| + \|U\|) \leq A - U V$
236	211 235	eqbrtrd	$⊢ φ \to Y + Y \|V\| + Y \|U\| \leq A - U V$
237	110 194 111 203 236	letrd	$⊢ φ \to Y^{2} + Y \|V\| + Y \|U\| \leq A - U V$
238	70 110 111 193 237	ltletrd	$⊢ φ \to (H - U) (I - V) + (H - U) V + U (I - V) < A - U V$
239	49 238	eqbrtrd	$⊢ φ \to H \cdot I - U V < A - U V$
240	13 16	remulcld	$⊢ φ \to H \cdot I \in ℝ$
241	240 1 75	ltsub1d	$⊢ φ \to (H \cdot I < A \leftrightarrow H \cdot I - U V < A - U V)$
242	239 241	mpbird	$⊢ φ \to H \cdot I < A$

Metamath Proof Explorer

Theorem smfmullem1

Proof