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 ⊒ ( πœ‘ β†’ ( ( 𝐡 Β· 𝑋 ) 𝐷 ( 𝐢 Β· π‘Œ ) ) < 𝑅 )