Metamath Proof Explorer

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 sseldi ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
86 85 rexrd ⊢ ( 𝜑 → 𝑃 ∈ ℝ* )
87 84 7 sseldi ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
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 sseldi ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
134 133 rexrd ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
135 84 9 sseldi ⊢ ( 𝜑 → 𝑍 ∈ ℝ )
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 ) ) ) )