Theorem 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	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
	smfmullem3.k	⊢ 𝐾 = { 𝑞 ∈ ( ℚ ↑m ( 0 ... 3 ) ) ∣ ∀ 𝑢 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑅 }
	smfmullem3.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
	smfmullem3.v	⊢ ( 𝜑 → 𝑉 ∈ ℝ )
	smfmullem3.l	⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) < 𝑅 )
	smfmullem3.x	⊢ 𝑋 = ( ( 𝑅 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
	smfmullem3.y	⊢ 𝑌 = if ( 1 ≤ 𝑋 , 1 , 𝑋 )
Assertion	smfmullem3	⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐾 ( 𝑈 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝑉 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		smfmullem3.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
2		smfmullem3.k	⊢ 𝐾 = { 𝑞 ∈ ( ℚ ↑m ( 0 ... 3 ) ) ∣ ∀ 𝑢 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∀ 𝑣 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ( 𝑢 · 𝑣 ) < 𝑅 }
3		smfmullem3.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
4		smfmullem3.v	⊢ ( 𝜑 → 𝑉 ∈ ℝ )
5		smfmullem3.l	⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) < 𝑅 )
6		smfmullem3.x	⊢ 𝑋 = ( ( 𝑅 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
7		smfmullem3.y	⊢ 𝑌 = if ( 1 ≤ 𝑋 , 1 , 𝑋 )
8	7	a1i	⊢ ( 𝜑 → 𝑌 = if ( 1 ≤ 𝑋 , 1 , 𝑋 ) )
9		1rp	⊢ 1 ∈ ℝ+
10	9	a1i	⊢ ( 𝜑 → 1 ∈ ℝ+ )
11	6	a1i	⊢ ( 𝜑 → 𝑋 = ( ( 𝑅 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) )
12	3 4	remulcld	⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) ∈ ℝ )
13		difrp	⊢ ( ( ( 𝑈 · 𝑉 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( 𝑈 · 𝑉 ) < 𝑅 ↔ ( 𝑅 − ( 𝑈 · 𝑉 ) ) ∈ ℝ+ ) )
14	12 1 13	syl2anc	⊢ ( 𝜑 → ( ( 𝑈 · 𝑉 ) < 𝑅 ↔ ( 𝑅 − ( 𝑈 · 𝑉 ) ) ∈ ℝ+ ) )
15	5 14	mpbid	⊢ ( 𝜑 → ( 𝑅 − ( 𝑈 · 𝑉 ) ) ∈ ℝ+ )
16		1re	⊢ 1 ∈ ℝ
17	16	a1i	⊢ ( 𝜑 → 1 ∈ ℝ )
18	3	recnd	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
19	18	abscld	⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ∈ ℝ )
20	4	recnd	⊢ ( 𝜑 → 𝑉 ∈ ℂ )
21	20	abscld	⊢ ( 𝜑 → ( abs ‘ 𝑉 ) ∈ ℝ )
22	19 21	readdcld	⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ∈ ℝ )
23	17 22	readdcld	⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ∈ ℝ )
24		0re	⊢ 0 ∈ ℝ
25	24	a1i	⊢ ( 𝜑 → 0 ∈ ℝ )
26	10	rpgt0d	⊢ ( 𝜑 → 0 < 1 )
27		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
28	18	absge0d	⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑈 ) )
29	20	absge0d	⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑉 ) )
30	19 21	addge01d	⊢ ( 𝜑 → ( 0 ≤ ( abs ‘ 𝑉 ) ↔ ( abs ‘ 𝑈 ) ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
31	29 30	mpbid	⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) )
32	27 19 22 28 31	letrd	⊢ ( 𝜑 → 0 ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) )
33	17 22	addge01d	⊢ ( 𝜑 → ( 0 ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ↔ 1 ≤ ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) )
34	32 33	mpbid	⊢ ( 𝜑 → 1 ≤ ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
35	25 17 23 26 34	ltletrd	⊢ ( 𝜑 → 0 < ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
36	23 35	elrpd	⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ∈ ℝ+ )
37	15 36	rpdivcld	⊢ ( 𝜑 → ( ( 𝑅 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) ∈ ℝ+ )
38	11 37	eqeltrd	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
39	10 38	ifcld	⊢ ( 𝜑 → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ∈ ℝ+ )
40	8 39	eqeltrd	⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
41	40	rpred	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
42	3 41	resubcld	⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) ∈ ℝ )
43	42	rexrd	⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) ∈ ℝ* )
44	3	rexrd	⊢ ( 𝜑 → 𝑈 ∈ ℝ* )
45	3 40	ltsubrpd	⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) < 𝑈 )
46	43 44 45	qelioo	⊢ ( 𝜑 → ∃ 𝑝 ∈ ℚ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) )
47	3 41	readdcld	⊢ ( 𝜑 → ( 𝑈 + 𝑌 ) ∈ ℝ )
48	47	rexrd	⊢ ( 𝜑 → ( 𝑈 + 𝑌 ) ∈ ℝ* )
49	3 40	ltaddrpd	⊢ ( 𝜑 → 𝑈 < ( 𝑈 + 𝑌 ) )
50	44 48 49	qelioo	⊢ ( 𝜑 → ∃ 𝑟 ∈ ℚ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) )
51	50	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) → ∃ 𝑟 ∈ ℚ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) )
52		simp-4l	⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) → 𝜑 )
53	4 41	resubcld	⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) ∈ ℝ )
54	53	rexrd	⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) ∈ ℝ* )
55	4	rexrd	⊢ ( 𝜑 → 𝑉 ∈ ℝ* )
56	4 40	ltsubrpd	⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) < 𝑉 )
57	54 55 56	qelioo	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℚ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) )
58	52 57	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) → ∃ 𝑠 ∈ ℚ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) )
59	52	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) → 𝜑 )
60	4 41	readdcld	⊢ ( 𝜑 → ( 𝑉 + 𝑌 ) ∈ ℝ )
61	60	rexrd	⊢ ( 𝜑 → ( 𝑉 + 𝑌 ) ∈ ℝ* )
62	4 40	ltaddrpd	⊢ ( 𝜑 → 𝑉 < ( 𝑉 + 𝑌 ) )
63	55 61 62	qelioo	⊢ ( 𝜑 → ∃ 𝑧 ∈ ℚ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) )
64	59 63	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) → ∃ 𝑧 ∈ ℚ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) )
65	1	ad8antr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑅 ∈ ℝ )
66	3	ad8antr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑈 ∈ ℝ )
67	4	ad8antr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑉 ∈ ℝ )
68	5	ad8antr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → ( 𝑈 · 𝑉 ) < 𝑅 )
69		simp-8r	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑝 ∈ ℚ )
70		simp-6r	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑟 ∈ ℚ )
71		simp-4r	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑠 ∈ ℚ )
72		simplr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑧 ∈ ℚ )
73		simp-7r	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) )
74		simp-5r	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) )
75		simpllr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) )
76		simpr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) )
77	65 2 66 67 68 69 70 71 72 73 74 75 76 6 7	smfmullem2	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) ∧ 𝑧 ∈ ℚ ) ∧ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) ) → ∃ 𝑞 ∈ 𝐾 ( 𝑈 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝑉 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) )
78	77	rexlimdva2	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) → ( ∃ 𝑧 ∈ ℚ 𝑧 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) → ∃ 𝑞 ∈ 𝐾 ( 𝑈 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝑉 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) ) )
79	64 78	mpd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) ∧ 𝑠 ∈ ℚ ) ∧ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) ) → ∃ 𝑞 ∈ 𝐾 ( 𝑈 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝑉 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) )
80	79	rexlimdva2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) → ( ∃ 𝑠 ∈ ℚ 𝑠 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) → ∃ 𝑞 ∈ 𝐾 ( 𝑈 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝑉 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) ) )
81	58 80	mpd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) ∧ 𝑟 ∈ ℚ ) ∧ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) → ∃ 𝑞 ∈ 𝐾 ( 𝑈 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝑉 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) )
82	81	rexlimdva2	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) → ( ∃ 𝑟 ∈ ℚ 𝑟 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) → ∃ 𝑞 ∈ 𝐾 ( 𝑈 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝑉 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) ) )
83	51 82	mpd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) → ∃ 𝑞 ∈ 𝐾 ( 𝑈 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝑉 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) )
84	83	rexlimdva2	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℚ 𝑝 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) → ∃ 𝑞 ∈ 𝐾 ( 𝑈 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝑉 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) ) )
85	46 84	mpd	⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐾 ( 𝑈 ∈ ( ( 𝑞 ‘ 0 ) (,) ( 𝑞 ‘ 1 ) ) ∧ 𝑉 ∈ ( ( 𝑞 ‘ 2 ) (,) ( 𝑞 ‘ 3 ) ) ) )