smfmullem2

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	smfmullem2.a	$⊢ φ \to A \in ℝ$
	smfmullem2.k	$⊢ K = \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < A\}$
	smfmullem2.u	$⊢ φ \to U \in ℝ$
	smfmullem2.v	$⊢ φ \to V \in ℝ$
	smfmullem2.l	$⊢ φ \to U V < A$
	smfmullem2.p	$⊢ φ \to P \in ℚ$
	smfmullem2.r	$⊢ φ \to R \in ℚ$
	smfmullem2.s	$⊢ φ \to S \in ℚ$
	smfmullem2.z	$⊢ φ \to Z \in ℚ$
	smfmullem2.p2	$⊢ φ \to P \in (U - Y, U)$
	smfmullem2.42	$⊢ φ \to R \in (U, U + Y)$
	smfmullem2.w2	$⊢ φ \to S \in (V - Y, V)$
	smfmullem2.z2	$⊢ φ \to Z \in (V, V + Y)$
	smfmullem2.x	$⊢ X = \frac{A - U V}{1 + \|U\| + \|V\|}$
	smfmullem2.y	$⊢ Y = if (1 \leq X, 1, X)$
Assertion	smfmullem2	$⊢ φ \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3)))$

Proof

Step	Hyp	Ref	Expression
1		smfmullem2.a	$⊢ φ \to A \in ℝ$
2		smfmullem2.k	$⊢ K = \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < A\}$
3		smfmullem2.u	$⊢ φ \to U \in ℝ$
4		smfmullem2.v	$⊢ φ \to V \in ℝ$
5		smfmullem2.l	$⊢ φ \to U V < A$
6		smfmullem2.p	$⊢ φ \to P \in ℚ$
7		smfmullem2.r	$⊢ φ \to R \in ℚ$
8		smfmullem2.s	$⊢ φ \to S \in ℚ$
9		smfmullem2.z	$⊢ φ \to Z \in ℚ$
10		smfmullem2.p2	$⊢ φ \to P \in (U - Y, U)$
11		smfmullem2.42	$⊢ φ \to R \in (U, U + Y)$
12		smfmullem2.w2	$⊢ φ \to S \in (V - Y, V)$
13		smfmullem2.z2	$⊢ φ \to Z \in (V, V + Y)$
14		smfmullem2.x	$⊢ X = \frac{A - U V}{1 + \|U\| + \|V\|}$
15		smfmullem2.y	$⊢ Y = if (1 \leq X, 1, X)$
16	6 7 8 9	s4cld	$⊢ φ \to ⟨“ P R S Z ”⟩ \in Word ℚ$
17		s4len	$⊢ \|⟨“ P R S Z ”⟩\| = 4$
18	17	a1i	$⊢ φ \to \|⟨“ P R S Z ”⟩\| = 4$
19	16 18	jca	$⊢ φ \to (⟨“ P R S Z ”⟩ \in Word ℚ \land \|⟨“ P R S Z ”⟩\| = 4)$
20		qex	$⊢ ℚ \in V$
21	20	a1i	$⊢ φ \to ℚ \in V$
22		4nn0	$⊢ 4 \in ℕ_{0}$
23	22	a1i	$⊢ φ \to 4 \in ℕ_{0}$
24		wrdmap	$⊢ (ℚ \in V \land 4 \in ℕ_{0}) \to ((⟨“ P R S Z ”⟩ \in Word ℚ \land \|⟨“ P R S Z ”⟩\| = 4) \leftrightarrow ⟨“ P R S Z ”⟩ \in (ℚ^{(0 ..^4)}))$
25	21 23 24	syl2anc	$⊢ φ \to ((⟨“ P R S Z ”⟩ \in Word ℚ \land \|⟨“ P R S Z ”⟩\| = 4) \leftrightarrow ⟨“ P R S Z ”⟩ \in (ℚ^{(0 ..^4)}))$
26	19 25	mpbid	$⊢ φ \to ⟨“ P R S Z ”⟩ \in (ℚ^{(0 ..^4)})$
27		3z	$⊢ 3 \in ℤ$
28		fzval3	$⊢ 3 \in ℤ \to (0 \dots 3) = (0 ..^3 + 1)$
29	27 28	ax-mp	$⊢ (0 \dots 3) = (0 ..^3 + 1)$
30		3p1e4	$⊢ 3 + 1 = 4$
31	30	oveq2i	$⊢ (0 ..^3 + 1) = (0 ..^4)$
32	29 31	eqtri	$⊢ (0 \dots 3) = (0 ..^4)$
33	32	eqcomi	$⊢ (0 ..^4) = (0 \dots 3)$
34	33	a1i	$⊢ φ \to (0 ..^4) = (0 \dots 3)$
35	34	oveq2d	$⊢ φ \to ℚ^{(0 ..^4)} = ℚ^{(0 \dots 3)}$
36	26 35	eleqtrd	$⊢ φ \to ⟨“ P R S Z ”⟩ \in (ℚ^{(0 \dots 3)})$
37		simpr	$⊢ (φ \land u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1))) \to u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1))$
38		s4fv0	$⊢ P \in ℚ \to ⟨“ P R S Z ”⟩ (0) = P$
39	6 38	syl	$⊢ φ \to ⟨“ P R S Z ”⟩ (0) = P$
40		s4fv1	$⊢ R \in ℚ \to ⟨“ P R S Z ”⟩ (1) = R$
41	7 40	syl	$⊢ φ \to ⟨“ P R S Z ”⟩ (1) = R$
42	39 41	oveq12d	$⊢ φ \to (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) = (P, R)$
43	42	adantr	$⊢ (φ \land u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1))) \to (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) = (P, R)$
44	37 43	eleqtrd	$⊢ (φ \land u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1))) \to u \in (P, R)$
45		simpr	$⊢ (φ \land v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))) \to v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))$
46		s4fv2	$⊢ S \in ℚ \to ⟨“ P R S Z ”⟩ (2) = S$
47	8 46	syl	$⊢ φ \to ⟨“ P R S Z ”⟩ (2) = S$
48		s4fv3	$⊢ Z \in ℚ \to ⟨“ P R S Z ”⟩ (3) = Z$
49	9 48	syl	$⊢ φ \to ⟨“ P R S Z ”⟩ (3) = Z$
50	47 49	oveq12d	$⊢ φ \to (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)) = (S, Z)$
51	50	adantr	$⊢ (φ \land v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))) \to (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)) = (S, Z)$
52	45 51	eleqtrd	$⊢ (φ \land v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))) \to v \in (S, Z)$
53		simpr	$⊢ (φ \land v \in (S, Z)) \to v \in (S, Z)$
54	52 53	syldan	$⊢ (φ \land v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))) \to v \in (S, Z)$
55	54	adantlr	$⊢ ((φ \land u \in (P, R)) \land v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))) \to v \in (S, Z)$
56	1	ad2antrr	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to A \in ℝ$
57	3	ad2antrr	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to U \in ℝ$
58	4	ad2antrr	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to V \in ℝ$
59	5	ad2antrr	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to U V < A$
60	10	ad2antrr	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to P \in (U - Y, U)$
61	11	ad2antrr	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to R \in (U, U + Y)$
62	12	ad2antrr	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to S \in (V - Y, V)$
63	13	ad2antrr	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to Z \in (V, V + Y)$
64		simplr	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to u \in (P, R)$
65		simpr	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to v \in (S, Z)$
66	56 57 58 59 14 15 60 61 62 63 64 65	smfmullem1	$⊢ ((φ \land u \in (P, R)) \land v \in (S, Z)) \to u v < A$
67	55 66	syldan	$⊢ ((φ \land u \in (P, R)) \land v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))) \to u v < A$
68	67	ralrimiva	$⊢ (φ \land u \in (P, R)) \to \forall v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)) u v < A$
69	44 68	syldan	$⊢ (φ \land u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1))) \to \forall v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)) u v < A$
70	69	ralrimiva	$⊢ φ \to \forall u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \forall v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)) u v < A$
71	36 70	jca	$⊢ φ \to (⟨“ P R S Z ”⟩ \in (ℚ^{(0 \dots 3)}) \land \forall u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \forall v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)) u v < A)$
72		fveq1	$⊢ q = ⟨“ P R S Z ”⟩ \to q (0) = ⟨“ P R S Z ”⟩ (0)$
73		fveq1	$⊢ q = ⟨“ P R S Z ”⟩ \to q (1) = ⟨“ P R S Z ”⟩ (1)$
74	72 73	oveq12d	$⊢ q = ⟨“ P R S Z ”⟩ \to (q (0), q (1)) = (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1))$
75	74	raleqdv	$⊢ q = ⟨“ P R S Z ”⟩ \to (\forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < A \leftrightarrow \forall u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \forall v \in (q (2), q (3)) u v < A)$
76		fveq1	$⊢ q = ⟨“ P R S Z ”⟩ \to q (2) = ⟨“ P R S Z ”⟩ (2)$
77		fveq1	$⊢ q = ⟨“ P R S Z ”⟩ \to q (3) = ⟨“ P R S Z ”⟩ (3)$
78	76 77	oveq12d	$⊢ q = ⟨“ P R S Z ”⟩ \to (q (2), q (3)) = (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))$
79	78	raleqdv	$⊢ q = ⟨“ P R S Z ”⟩ \to (\forall v \in (q (2), q (3)) u v < A \leftrightarrow \forall v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)) u v < A)$
80	79	ralbidv	$⊢ q = ⟨“ P R S Z ”⟩ \to (\forall u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \forall v \in (q (2), q (3)) u v < A \leftrightarrow \forall u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \forall v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)) u v < A)$
81	75 80	bitrd	$⊢ q = ⟨“ P R S Z ”⟩ \to (\forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < A \leftrightarrow \forall u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \forall v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)) u v < A)$
82	81 2	elrab2	$⊢ ⟨“ P R S Z ”⟩ \in K \leftrightarrow (⟨“ P R S Z ”⟩ \in (ℚ^{(0 \dots 3)}) \land \forall u \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \forall v \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)) u v < A)$
83	71 82	sylibr	$⊢ φ \to ⟨“ P R S Z ”⟩ \in K$
84		qssre	$⊢ ℚ \subseteq ℝ$
85	84 6	sseldi	$⊢ φ \to P \in ℝ$
86	85	rexrd	$⊢ φ \to P \in ℝ^{*}$
87	84 7	sseldi	$⊢ φ \to R \in ℝ$
88	87	rexrd	$⊢ φ \to R \in ℝ^{*}$
89	15	a1i	$⊢ φ \to Y = if (1 \leq X, 1, X)$
90		1rp	$⊢ 1 \in ℝ^{+}$
91	90	a1i	$⊢ φ \to 1 \in ℝ^{+}$
92	14	a1i	$⊢ φ \to X = \frac{A - U V}{1 + \|U\| + \|V\|}$
93	3 4	remulcld	$⊢ φ \to U V \in ℝ$
94		difrp	$⊢ (U V \in ℝ \land A \in ℝ) \to (U V < A \leftrightarrow A - U V \in ℝ^{+})$
95	93 1 94	syl2anc	$⊢ φ \to (U V < A \leftrightarrow A - U V \in ℝ^{+})$
96	5 95	mpbid	$⊢ φ \to A - U V \in ℝ^{+}$
97		1red	$⊢ φ \to 1 \in ℝ$
98	3	recnd	$⊢ φ \to U \in ℂ$
99	98	abscld	$⊢ φ \to \|U\| \in ℝ$
100	4	recnd	$⊢ φ \to V \in ℂ$
101	100	abscld	$⊢ φ \to \|V\| \in ℝ$
102	99 101	readdcld	$⊢ φ \to \|U\| + \|V\| \in ℝ$
103	97 102	readdcld	$⊢ φ \to 1 + \|U\| + \|V\| \in ℝ$
104		0re	$⊢ 0 \in ℝ$
105	104	a1i	$⊢ φ \to 0 \in ℝ$
106	91	rpgt0d	$⊢ φ \to 0 < 1$
107	98	absge0d	$⊢ φ \to 0 \leq \|U\|$
108	100	absge0d	$⊢ φ \to 0 \leq \|V\|$
109	99 101	addge01d	$⊢ φ \to (0 \leq \|V\| \leftrightarrow \|U\| \leq \|U\| + \|V\|)$
110	108 109	mpbid	$⊢ φ \to \|U\| \leq \|U\| + \|V\|$
111	105 99 102 107 110	letrd	$⊢ φ \to 0 \leq \|U\| + \|V\|$
112	97 102	addge01d	$⊢ φ \to (0 \leq \|U\| + \|V\| \leftrightarrow 1 \leq 1 + \|U\| + \|V\|)$
113	111 112	mpbid	$⊢ φ \to 1 \leq 1 + \|U\| + \|V\|$
114	105 97 103 106 113	ltletrd	$⊢ φ \to 0 < 1 + \|U\| + \|V\|$
115	103 114	elrpd	$⊢ φ \to 1 + \|U\| + \|V\| \in ℝ^{+}$
116	96 115	rpdivcld	$⊢ φ \to \frac{A - U V}{1 + \|U\| + \|V\|} \in ℝ^{+}$
117	92 116	eqeltrd	$⊢ φ \to X \in ℝ^{+}$
118	91 117	ifcld	$⊢ φ \to if (1 \leq X, 1, X) \in ℝ^{+}$
119	89 118	eqeltrd	$⊢ φ \to Y \in ℝ^{+}$
120	119	rpred	$⊢ φ \to Y \in ℝ$
121	3 120	resubcld	$⊢ φ \to U - Y \in ℝ$
122	121	rexrd	$⊢ φ \to U - Y \in ℝ^{*}$
123	3	rexrd	$⊢ φ \to U \in ℝ^{*}$
124		iooltub	$⊢ (U - Y \in ℝ^{} \land U \in ℝ^{} \land P \in (U - Y, U)) \to P < U$
125	122 123 10 124	syl3anc	$⊢ φ \to P < U$
126	3 120	readdcld	$⊢ φ \to U + Y \in ℝ$
127	126	rexrd	$⊢ φ \to U + Y \in ℝ^{*}$
128		ioogtlb	$⊢ (U \in ℝ^{} \land U + Y \in ℝ^{} \land R \in (U, U + Y)) \to U < R$
129	123 127 11 128	syl3anc	$⊢ φ \to U < R$
130	86 88 3 125 129	eliood	$⊢ φ \to U \in (P, R)$
131	42	eqcomd	$⊢ φ \to (P, R) = (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1))$
132	130 131	eleqtrd	$⊢ φ \to U \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1))$
133	84 8	sseldi	$⊢ φ \to S \in ℝ$
134	133	rexrd	$⊢ φ \to S \in ℝ^{*}$
135	84 9	sseldi	$⊢ φ \to Z \in ℝ$
136	135	rexrd	$⊢ φ \to Z \in ℝ^{*}$
137	4 120	resubcld	$⊢ φ \to V - Y \in ℝ$
138	137	rexrd	$⊢ φ \to V - Y \in ℝ^{*}$
139	4	rexrd	$⊢ φ \to V \in ℝ^{*}$
140		iooltub	$⊢ (V - Y \in ℝ^{} \land V \in ℝ^{} \land S \in (V - Y, V)) \to S < V$
141	138 139 12 140	syl3anc	$⊢ φ \to S < V$
142	4 120	readdcld	$⊢ φ \to V + Y \in ℝ$
143	142	rexrd	$⊢ φ \to V + Y \in ℝ^{*}$
144		ioogtlb	$⊢ (V \in ℝ^{} \land V + Y \in ℝ^{} \land Z \in (V, V + Y)) \to V < Z$
145	139 143 13 144	syl3anc	$⊢ φ \to V < Z$
146	134 136 4 141 145	eliood	$⊢ φ \to V \in (S, Z)$
147	50	eqcomd	$⊢ φ \to (S, Z) = (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))$
148	146 147	eleqtrd	$⊢ φ \to V \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))$
149	132 148	jca	$⊢ φ \to (U \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \land V \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)))$
150		nfv	$⊢ Ⅎ q (U \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \land V \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)))$
151		nfcv	$⊢ \underline{Ⅎ} q ⟨“ P R S Z ”⟩$
152		nfrab1	$⊢ \underline{Ⅎ} q \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < A\}$
153	2 152	nfcxfr	$⊢ \underline{Ⅎ} q K$
154	74	eleq2d	$⊢ q = ⟨“ P R S Z ”⟩ \to (U \in (q (0), q (1)) \leftrightarrow U \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)))$
155	78	eleq2d	$⊢ q = ⟨“ P R S Z ”⟩ \to (V \in (q (2), q (3)) \leftrightarrow V \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)))$
156	154 155	anbi12d	$⊢ q = ⟨“ P R S Z ”⟩ \to ((U \in (q (0), q (1)) \land V \in (q (2), q (3))) \leftrightarrow (U \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \land V \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3))))$
157	150 151 153 156	rspcef	$⊢ (⟨“ P R S Z ”⟩ \in K \land (U \in (⟨“ P R S Z ”⟩ (0), ⟨“ P R S Z ”⟩ (1)) \land V \in (⟨“ P R S Z ”⟩ (2), ⟨“ P R S Z ”⟩ (3)))) \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3)))$
158	83 149 157	syl2anc	$⊢ φ \to \exists q \in K (U \in (q (0), q (1)) \land V \in (q (2), q (3)))$

Metamath Proof Explorer

Theorem smfmullem2

Proof