This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nlmvscnlem2

Description: Lemma for nlmvscn . Compare this proof with the similar elementary proof mulcn2 for continuity of multiplication on CC . (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses nlmvscn.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
nlmvscn.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
nlmvscn.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
nlmvscn.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
nlmvscn.e ⊢ 𝐸 = ( dist ‘ 𝐹 )
nlmvscn.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
nlmvscn.a ⊢ 𝐴 = ( norm ‘ 𝐹 )
nlmvscn.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
nlmvscn.t ⊢ 𝑇 = ( ( 𝑅 / 2 ) / ( ( 𝐴 ‘ 𝐵 ) + 1 ) )
nlmvscn.u ⊢ 𝑈 = ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) )
nlmvscn.w ⊢ ( 𝜑 → 𝑊 ∈ NrmMod )
nlmvscn.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
nlmvscn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
nlmvscn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
nlmvscn.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
nlmvscn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
nlmvscn.1 ⊢ ( 𝜑 → ( 𝐵 𝐸 𝐶 ) < 𝑈 )
nlmvscn.2 ⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) < 𝑇 )
Assertion nlmvscnlem2 ( 𝜑 → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐶 · 𝑌 ) ) < 𝑅 )

Proof

Step Hyp Ref Expression
1 nlmvscn.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 nlmvscn.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 nlmvscn.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
4 nlmvscn.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
5 nlmvscn.e ⊢ 𝐸 = ( dist ‘ 𝐹 )
6 nlmvscn.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
7 nlmvscn.a ⊢ 𝐴 = ( norm ‘ 𝐹 )
8 nlmvscn.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
9 nlmvscn.t ⊢ 𝑇 = ( ( 𝑅 / 2 ) / ( ( 𝐴 ‘ 𝐵 ) + 1 ) )
10 nlmvscn.u ⊢ 𝑈 = ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) )
11 nlmvscn.w ⊢ ( 𝜑 → 𝑊 ∈ NrmMod )
12 nlmvscn.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
13 nlmvscn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
14 nlmvscn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
15 nlmvscn.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
16 nlmvscn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
17 nlmvscn.1 ⊢ ( 𝜑 → ( 𝐵 𝐸 𝐶 ) < 𝑈 )
18 nlmvscn.2 ⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) < 𝑇 )
19 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
20 11 19 syl ⊢ ( 𝜑 → 𝑊 ∈ NrmGrp )
21 ngpms ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp )
22 20 21 syl ⊢ ( 𝜑 → 𝑊 ∈ MetSp )
23 nlmlmod ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ LMod )
24 11 23 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
25 2 1 8 3 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐵 · 𝑋 ) ∈ 𝑉 )
26 24 13 14 25 syl3anc ⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ 𝑉 )
27 2 1 8 3 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐶 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐶 · 𝑌 ) ∈ 𝑉 )
28 24 15 16 27 syl3anc ⊢ ( 𝜑 → ( 𝐶 · 𝑌 ) ∈ 𝑉 )
29 2 4 mscl ⊢ ( ( 𝑊 ∈ MetSp ∧ ( 𝐵 · 𝑋 ) ∈ 𝑉 ∧ ( 𝐶 · 𝑌 ) ∈ 𝑉 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐶 · 𝑌 ) ) ∈ ℝ )
30 22 26 28 29 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐶 · 𝑌 ) ) ∈ ℝ )
31 2 1 8 3 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐵 · 𝑌 ) ∈ 𝑉 )
32 24 13 16 31 syl3anc ⊢ ( 𝜑 → ( 𝐵 · 𝑌 ) ∈ 𝑉 )
33 2 4 mscl ⊢ ( ( 𝑊 ∈ MetSp ∧ ( 𝐵 · 𝑋 ) ∈ 𝑉 ∧ ( 𝐵 · 𝑌 ) ∈ 𝑉 ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐵 · 𝑌 ) ) ∈ ℝ )
34 22 26 32 33 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐵 · 𝑌 ) ) ∈ ℝ )
35 2 4 mscl ⊢ ( ( 𝑊 ∈ MetSp ∧ ( 𝐵 · 𝑌 ) ∈ 𝑉 ∧ ( 𝐶 · 𝑌 ) ∈ 𝑉 ) → ( ( 𝐵 · 𝑌 ) 𝐷 ( 𝐶 · 𝑌 ) ) ∈ ℝ )
36 22 32 28 35 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 · 𝑌 ) 𝐷 ( 𝐶 · 𝑌 ) ) ∈ ℝ )
37 34 36 readdcld ⊢ ( 𝜑 → ( ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐵 · 𝑌 ) ) + ( ( 𝐵 · 𝑌 ) 𝐷 ( 𝐶 · 𝑌 ) ) ) ∈ ℝ )
38 12 rpred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
39 2 4 mstri ⊢ ( ( 𝑊 ∈ MetSp ∧ ( ( 𝐵 · 𝑋 ) ∈ 𝑉 ∧ ( 𝐶 · 𝑌 ) ∈ 𝑉 ∧ ( 𝐵 · 𝑌 ) ∈ 𝑉 ) ) → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐶 · 𝑌 ) ) ≤ ( ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐵 · 𝑌 ) ) + ( ( 𝐵 · 𝑌 ) 𝐷 ( 𝐶 · 𝑌 ) ) ) )
40 22 26 28 32 39 syl13anc ⊢ ( 𝜑 → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐶 · 𝑌 ) ) ≤ ( ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐵 · 𝑌 ) ) + ( ( 𝐵 · 𝑌 ) 𝐷 ( 𝐶 · 𝑌 ) ) ) )
41 1 nlmngp2 ⊢ ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp )
42 11 41 syl ⊢ ( 𝜑 → 𝐹 ∈ NrmGrp )
43 3 7 nmcl ⊢ ( ( 𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 ‘ 𝐵 ) ∈ ℝ )
44 42 13 43 syl2anc ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐵 ) ∈ ℝ )
45 3 7 nmge0 ⊢ ( ( 𝐹 ∈ NrmGrp ∧ 𝐵 ∈ 𝐾 ) → 0 ≤ ( 𝐴 ‘ 𝐵 ) )
46 42 13 45 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝐴 ‘ 𝐵 ) )
47 44 46 ge0p1rpd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐵 ) + 1 ) ∈ ℝ+ )
48 47 rpred ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐵 ) + 1 ) ∈ ℝ )
49 2 4 mscl ⊢ ( ( 𝑊 ∈ MetSp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 𝐷 𝑌 ) ∈ ℝ )
50 22 14 16 49 syl3anc ⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) ∈ ℝ )
51 48 50 remulcld ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 𝐵 ) + 1 ) · ( 𝑋 𝐷 𝑌 ) ) ∈ ℝ )
52 38 rehalfcld ⊢ ( 𝜑 → ( 𝑅 / 2 ) ∈ ℝ )
53 2 8 1 3 4 7 nlmdsdi ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐴 ‘ 𝐵 ) · ( 𝑋 𝐷 𝑌 ) ) = ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐵 · 𝑌 ) ) )
54 11 13 14 16 53 syl13anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐵 ) · ( 𝑋 𝐷 𝑌 ) ) = ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐵 · 𝑌 ) ) )
55 msxms ⊢ ( 𝑊 ∈ MetSp → 𝑊 ∈ ∞MetSp )
56 22 55 syl ⊢ ( 𝜑 → 𝑊 ∈ ∞MetSp )
57 2 4 xmsge0 ⊢ ( ( 𝑊 ∈ ∞MetSp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 0 ≤ ( 𝑋 𝐷 𝑌 ) )
58 56 14 16 57 syl3anc ⊢ ( 𝜑 → 0 ≤ ( 𝑋 𝐷 𝑌 ) )
59 44 lep1d ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐵 ) ≤ ( ( 𝐴 ‘ 𝐵 ) + 1 ) )
60 44 48 50 58 59 lemul1ad ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐵 ) · ( 𝑋 𝐷 𝑌 ) ) ≤ ( ( ( 𝐴 ‘ 𝐵 ) + 1 ) · ( 𝑋 𝐷 𝑌 ) ) )
61 54 60 eqbrtrrd ⊢ ( 𝜑 → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐵 · 𝑌 ) ) ≤ ( ( ( 𝐴 ‘ 𝐵 ) + 1 ) · ( 𝑋 𝐷 𝑌 ) ) )
62 18 9 breqtrdi ⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) < ( ( 𝑅 / 2 ) / ( ( 𝐴 ‘ 𝐵 ) + 1 ) ) )
63 50 52 47 ltmuldiv2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ‘ 𝐵 ) + 1 ) · ( 𝑋 𝐷 𝑌 ) ) < ( 𝑅 / 2 ) ↔ ( 𝑋 𝐷 𝑌 ) < ( ( 𝑅 / 2 ) / ( ( 𝐴 ‘ 𝐵 ) + 1 ) ) ) )
64 62 63 mpbird ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 𝐵 ) + 1 ) · ( 𝑋 𝐷 𝑌 ) ) < ( 𝑅 / 2 ) )
65 34 51 52 61 64 lelttrd ⊢ ( 𝜑 → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐵 · 𝑌 ) ) < ( 𝑅 / 2 ) )
66 ngpms ⊢ ( 𝐹 ∈ NrmGrp → 𝐹 ∈ MetSp )
67 42 66 syl ⊢ ( 𝜑 → 𝐹 ∈ MetSp )
68 3 5 mscl ⊢ ( ( 𝐹 ∈ MetSp ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝐾 ) → ( 𝐵 𝐸 𝐶 ) ∈ ℝ )
69 67 13 15 68 syl3anc ⊢ ( 𝜑 → ( 𝐵 𝐸 𝐶 ) ∈ ℝ )
70 2 6 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) ∈ ℝ )
71 20 14 70 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ ℝ )
72 12 rphalfcld ⊢ ( 𝜑 → ( 𝑅 / 2 ) ∈ ℝ+ )
73 72 47 rpdivcld ⊢ ( 𝜑 → ( ( 𝑅 / 2 ) / ( ( 𝐴 ‘ 𝐵 ) + 1 ) ) ∈ ℝ+ )
74 9 73 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
75 74 rpred ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
76 71 75 readdcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ∈ ℝ )
77 69 76 remulcld ⊢ ( 𝜑 → ( ( 𝐵 𝐸 𝐶 ) · ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) ∈ ℝ )
78 2 8 1 3 4 6 5 nlmdsdir ⊢ ( ( 𝑊 ∈ NrmMod ∧ ( 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐵 𝐸 𝐶 ) · ( 𝑁 ‘ 𝑌 ) ) = ( ( 𝐵 · 𝑌 ) 𝐷 ( 𝐶 · 𝑌 ) ) )
79 11 13 15 16 78 syl13anc ⊢ ( 𝜑 → ( ( 𝐵 𝐸 𝐶 ) · ( 𝑁 ‘ 𝑌 ) ) = ( ( 𝐵 · 𝑌 ) 𝐷 ( 𝐶 · 𝑌 ) ) )
80 2 6 nmcl ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ 𝑌 ) ∈ ℝ )
81 20 16 80 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑌 ) ∈ ℝ )
82 msxms ⊢ ( 𝐹 ∈ MetSp → 𝐹 ∈ ∞MetSp )
83 67 82 syl ⊢ ( 𝜑 → 𝐹 ∈ ∞MetSp )
84 3 5 xmsge0 ⊢ ( ( 𝐹 ∈ ∞MetSp ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝐾 ) → 0 ≤ ( 𝐵 𝐸 𝐶 ) )
85 83 13 15 84 syl3anc ⊢ ( 𝜑 → 0 ≤ ( 𝐵 𝐸 𝐶 ) )
86 81 71 resubcld ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝑋 ) ) ∈ ℝ )
87 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
88 2 6 87 nm2dif ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝑋 ) ) ≤ ( 𝑁 ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝑋 ) ) )
89 20 16 14 88 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝑋 ) ) ≤ ( 𝑁 ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝑋 ) ) )
90 6 2 87 4 ngpdsr ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 𝐷 𝑌 ) = ( 𝑁 ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝑋 ) ) )
91 20 14 16 90 syl3anc ⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) = ( 𝑁 ‘ ( 𝑌 ( -g ‘ 𝑊 ) 𝑋 ) ) )
92 89 91 breqtrrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝑋 ) ) ≤ ( 𝑋 𝐷 𝑌 ) )
93 50 75 18 ltled ⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) ≤ 𝑇 )
94 86 50 75 92 93 letrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝑋 ) ) ≤ 𝑇 )
95 81 71 75 lesubadd2d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ 𝑌 ) − ( 𝑁 ‘ 𝑋 ) ) ≤ 𝑇 ↔ ( 𝑁 ‘ 𝑌 ) ≤ ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) )
96 94 95 mpbid ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑌 ) ≤ ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) )
97 81 76 69 85 96 lemul2ad ⊢ ( 𝜑 → ( ( 𝐵 𝐸 𝐶 ) · ( 𝑁 ‘ 𝑌 ) ) ≤ ( ( 𝐵 𝐸 𝐶 ) · ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) )
98 79 97 eqbrtrrd ⊢ ( 𝜑 → ( ( 𝐵 · 𝑌 ) 𝐷 ( 𝐶 · 𝑌 ) ) ≤ ( ( 𝐵 𝐸 𝐶 ) · ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) )
99 17 10 breqtrdi ⊢ ( 𝜑 → ( 𝐵 𝐸 𝐶 ) < ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) )
100 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
101 2 6 nmge0 ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ) → 0 ≤ ( 𝑁 ‘ 𝑋 ) )
102 20 14 101 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝑁 ‘ 𝑋 ) )
103 71 74 ltaddrpd ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) < ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) )
104 100 71 76 102 103 lelttrd ⊢ ( 𝜑 → 0 < ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) )
105 ltmuldiv ⊢ ( ( ( 𝐵 𝐸 𝐶 ) ∈ ℝ ∧ ( 𝑅 / 2 ) ∈ ℝ ∧ ( ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ∈ ℝ ∧ 0 < ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) ) → ( ( ( 𝐵 𝐸 𝐶 ) · ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) < ( 𝑅 / 2 ) ↔ ( 𝐵 𝐸 𝐶 ) < ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) ) )
106 69 52 76 104 105 syl112anc ⊢ ( 𝜑 → ( ( ( 𝐵 𝐸 𝐶 ) · ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) < ( 𝑅 / 2 ) ↔ ( 𝐵 𝐸 𝐶 ) < ( ( 𝑅 / 2 ) / ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) ) )
107 99 106 mpbird ⊢ ( 𝜑 → ( ( 𝐵 𝐸 𝐶 ) · ( ( 𝑁 ‘ 𝑋 ) + 𝑇 ) ) < ( 𝑅 / 2 ) )
108 36 77 52 98 107 lelttrd ⊢ ( 𝜑 → ( ( 𝐵 · 𝑌 ) 𝐷 ( 𝐶 · 𝑌 ) ) < ( 𝑅 / 2 ) )
109 34 36 38 65 108 lt2halvesd ⊢ ( 𝜑 → ( ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐵 · 𝑌 ) ) + ( ( 𝐵 · 𝑌 ) 𝐷 ( 𝐶 · 𝑌 ) ) ) < 𝑅 )
110 30 37 38 40 109 lelttrd ⊢ ( 𝜑 → ( ( 𝐵 · 𝑋 ) 𝐷 ( 𝐶 · 𝑌 ) ) < 𝑅 )