smfmullem3

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	smfmullem3.r	$⊢ φ \to R \in ℝ$
	smfmullem3.k	$⊢ K = \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R\}$
	smfmullem3.u	$⊢ φ \to U \in ℝ$
	smfmullem3.v	$⊢ φ \to V \in ℝ$
	smfmullem3.l	$⊢ φ \to U V < R$
	smfmullem3.x	$⊢ X = \frac{R - U V}{1 + \|U\| + \|V\|}$
	smfmullem3.y	$⊢ Y = if (1 \leq X, 1, X)$
Assertion	smfmullem3	$⊢ φ \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3)))$

Proof

Step	Hyp	Ref	Expression
1		smfmullem3.r	$⊢ φ \to R \in ℝ$
2		smfmullem3.k	$⊢ K = \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < R\}$
3		smfmullem3.u	$⊢ φ \to U \in ℝ$
4		smfmullem3.v	$⊢ φ \to V \in ℝ$
5		smfmullem3.l	$⊢ φ \to U V < R$
6		smfmullem3.x	$⊢ X = \frac{R - U V}{1 + \|U\| + \|V\|}$
7		smfmullem3.y	$⊢ Y = if (1 \leq X, 1, X)$
8	7	a1i	$⊢ φ \to Y = if (1 \leq X, 1, X)$
9		1rp	$⊢ 1 \in ℝ^{+}$
10	9	a1i	$⊢ φ \to 1 \in ℝ^{+}$
11	6	a1i	$⊢ φ \to X = \frac{R - U V}{1 + \|U\| + \|V\|}$
12	3 4	remulcld	$⊢ φ \to U V \in ℝ$
13		difrp	$⊢ (U V \in ℝ \land R \in ℝ) \to (U V < R \leftrightarrow R - U V \in ℝ^{+})$
14	12 1 13	syl2anc	$⊢ φ \to (U V < R \leftrightarrow R - U V \in ℝ^{+})$
15	5 14	mpbid	$⊢ φ \to R - U V \in ℝ^{+}$
16		1re	$⊢ 1 \in ℝ$
17	16	a1i	$⊢ φ \to 1 \in ℝ$
18	3	recnd	$⊢ φ \to U \in ℂ$
19	18	abscld	$⊢ φ \to \|U\| \in ℝ$
20	4	recnd	$⊢ φ \to V \in ℂ$
21	20	abscld	$⊢ φ \to \|V\| \in ℝ$
22	19 21	readdcld	$⊢ φ \to \|U\| + \|V\| \in ℝ$
23	17 22	readdcld	$⊢ φ \to 1 + \|U\| + \|V\| \in ℝ$
24		0re	$⊢ 0 \in ℝ$
25	24	a1i	$⊢ φ \to 0 \in ℝ$
26	10	rpgt0d	$⊢ φ \to 0 < 1$
27		0red	$⊢ φ \to 0 \in ℝ$
28	18	absge0d	$⊢ φ \to 0 \leq \|U\|$
29	20	absge0d	$⊢ φ \to 0 \leq \|V\|$
30	19 21	addge01d	$⊢ φ \to (0 \leq \|V\| \leftrightarrow \|U\| \leq \|U\| + \|V\|)$
31	29 30	mpbid	$⊢ φ \to \|U\| \leq \|U\| + \|V\|$
32	27 19 22 28 31	letrd	$⊢ φ \to 0 \leq \|U\| + \|V\|$
33	17 22	addge01d	$⊢ φ \to (0 \leq \|U\| + \|V\| \leftrightarrow 1 \leq 1 + \|U\| + \|V\|)$
34	32 33	mpbid	$⊢ φ \to 1 \leq 1 + \|U\| + \|V\|$
35	25 17 23 26 34	ltletrd	$⊢ φ \to 0 < 1 + \|U\| + \|V\|$
36	23 35	elrpd	$⊢ φ \to 1 + \|U\| + \|V\| \in ℝ^{+}$
37	15 36	rpdivcld	$⊢ φ \to \frac{R - U V}{1 + \|U\| + \|V\|} \in ℝ^{+}$
38	11 37	eqeltrd	$⊢ φ \to X \in ℝ^{+}$
39	10 38	ifcld	$⊢ φ \to if (1 \leq X, 1, X) \in ℝ^{+}$
40	8 39	eqeltrd	$⊢ φ \to Y \in ℝ^{+}$
41	40	rpred	$⊢ φ \to Y \in ℝ$
42	3 41	resubcld	$⊢ φ \to U - Y \in ℝ$
43	42	rexrd	$⊢ φ \to U - Y \in ℝ^{*}$
44	3	rexrd	$⊢ φ \to U \in ℝ^{*}$
45	3 40	ltsubrpd	$⊢ φ \to U - Y < U$
46	43 44 45	qelioo	$⊢ φ \to \exists p \in ℚ p \in (U - Y, U)$
47	3 41	readdcld	$⊢ φ \to U + Y \in ℝ$
48	47	rexrd	$⊢ φ \to U + Y \in ℝ^{*}$
49	3 40	ltaddrpd	$⊢ φ \to U < U + Y$
50	44 48 49	qelioo	$⊢ φ \to \exists r \in ℚ r \in (U, U + Y)$
51	50	ad2antrr	$⊢ ((φ \land p \in ℚ) \land p \in (U - Y, U)) \to \exists r \in ℚ r \in (U, U + Y)$
52		simp-4l	$⊢ ((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \to φ$
53	4 41	resubcld	$⊢ φ \to V - Y \in ℝ$
54	53	rexrd	$⊢ φ \to V - Y \in ℝ^{*}$
55	4	rexrd	$⊢ φ \to V \in ℝ^{*}$
56	4 40	ltsubrpd	$⊢ φ \to V - Y < V$
57	54 55 56	qelioo	$⊢ φ \to \exists s \in ℚ s \in (V - Y, V)$
58	52 57	syl	$⊢ ((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \to \exists s \in ℚ s \in (V - Y, V)$
59	52	ad2antrr	$⊢ ((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \to φ$
60	4 41	readdcld	$⊢ φ \to V + Y \in ℝ$
61	60	rexrd	$⊢ φ \to V + Y \in ℝ^{*}$
62	4 40	ltaddrpd	$⊢ φ \to V < V + Y$
63	55 61 62	qelioo	$⊢ φ \to \exists z \in ℚ z \in (V, V + Y)$
64	59 63	syl	$⊢ ((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \to \exists z \in ℚ z \in (V, V + Y)$
65	1	ad8antr	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to R \in ℝ$
66	3	ad8antr	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to U \in ℝ$
67	4	ad8antr	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to V \in ℝ$
68	5	ad8antr	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to U V < R$
69		simp-8r	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to p \in ℚ$
70		simp-6r	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to r \in ℚ$
71		simp-4r	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to s \in ℚ$
72		simplr	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to z \in ℚ$
73		simp-7r	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to p \in (U - Y, U)$
74		simp-5r	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to r \in (U, U + Y)$
75		simpllr	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to s \in (V - Y, V)$
76		simpr	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to z \in (V, V + Y)$
77	65 2 66 67 68 69 70 71 72 73 74 75 76 6 7	smfmullem2	$⊢ ((((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \land z \in ℚ) \land z \in (V, V + Y)) \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3)))$
78	77	rexlimdva2	$⊢ ((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \to (\exists z \in ℚ z \in (V, V + Y) \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3))))$
79	64 78	mpd	$⊢ ((((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \land s \in ℚ) \land s \in (V - Y, V)) \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3)))$
80	79	rexlimdva2	$⊢ ((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \to (\exists s \in ℚ s \in (V - Y, V) \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3))))$
81	58 80	mpd	$⊢ ((((φ \land p \in ℚ) \land p \in (U - Y, U)) \land r \in ℚ) \land r \in (U, U + Y)) \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3)))$
82	81	rexlimdva2	$⊢ ((φ \land p \in ℚ) \land p \in (U - Y, U)) \to (\exists r \in ℚ r \in (U, U + Y) \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3))))$
83	51 82	mpd	$⊢ ((φ \land p \in ℚ) \land p \in (U - Y, U)) \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3)))$
84	83	rexlimdva2	$⊢ φ \to (\exists p \in ℚ p \in (U - Y, U) \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3))))$
85	46 84	mpd	$⊢ φ \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3)))$

Metamath Proof Explorer

Theorem smfmullem3

Proof