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

Proof

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