Metamath Proof Explorer

Theorem nmoleub2lem3

Description: Lemma for nmoleub2a and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015) (Proof shortened by AV, 29-Sep-2021)

Ref Expression
Hypotheses nmoleub2.n ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
nmoleub2.v ⊢ 𝑉 = ( Base ‘ 𝑆 )
nmoleub2.l ⊢ 𝐿 = ( norm ‘ 𝑆 )
nmoleub2.m ⊢ 𝑀 = ( norm ‘ 𝑇 )
nmoleub2.g ⊢ 𝐺 = ( Scalar ‘ 𝑆 )
nmoleub2.w ⊢ 𝐾 = ( Base ‘ 𝐺 )
nmoleub2.s ⊢ ( 𝜑 → 𝑆 ∈ ( NrmMod ∩ ℂMod ) )
nmoleub2.t ⊢ ( 𝜑 → 𝑇 ∈ ( NrmMod ∩ ℂMod ) )
nmoleub2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
nmoleub2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
nmoleub2.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
nmoleub2a.5 ⊢ ( 𝜑 → ℚ ⊆ 𝐾 )
nmoleub2lem3.p ⊢ · = ( ·𝑠 ‘ 𝑆 )
nmoleub2lem3.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
nmoleub2lem3.2 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
nmoleub2lem3.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
nmoleub2lem3.4 ⊢ ( 𝜑 → 𝐵 ≠ ( 0g ‘ 𝑆 ) )
nmoleub2lem3.5 ⊢ ( 𝜑 → ( ( 𝑟 · 𝐵 ) ∈ 𝑉 → ( ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
nmoleub2lem3.6 ⊢ ( 𝜑 → ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) )
Assertion nmoleub2lem3 ¬ 𝜑

Proof

Step Hyp Ref Expression
1 nmoleub2.n ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmoleub2.v ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmoleub2.l ⊢ 𝐿 = ( norm ‘ 𝑆 )
4 nmoleub2.m ⊢ 𝑀 = ( norm ‘ 𝑇 )
5 nmoleub2.g ⊢ 𝐺 = ( Scalar ‘ 𝑆 )
6 nmoleub2.w ⊢ 𝐾 = ( Base ‘ 𝐺 )
7 nmoleub2.s ⊢ ( 𝜑 → 𝑆 ∈ ( NrmMod ∩ ℂMod ) )
8 nmoleub2.t ⊢ ( 𝜑 → 𝑇 ∈ ( NrmMod ∩ ℂMod ) )
9 nmoleub2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
10 nmoleub2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
11 nmoleub2.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
12 nmoleub2a.5 ⊢ ( 𝜑 → ℚ ⊆ 𝐾 )
13 nmoleub2lem3.p ⊢ · = ( ·𝑠 ‘ 𝑆 )
14 nmoleub2lem3.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
15 nmoleub2lem3.2 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
16 nmoleub2lem3.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
17 nmoleub2lem3.4 ⊢ ( 𝜑 → 𝐵 ≠ ( 0g ‘ 𝑆 ) )
18 nmoleub2lem3.5 ⊢ ( 𝜑 → ( ( 𝑟 · 𝐵 ) ∈ 𝑉 → ( ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
19 nmoleub2lem3.6 ⊢ ( 𝜑 → ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) )
20 simprl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 )
21 qre ⊢ ( 𝑟 ∈ ℚ → 𝑟 ∈ ℝ )
22 21 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝑟 ∈ ℝ )
23 11 rpred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
24 14 23 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝑅 ) ∈ ℝ )
25 8 elin1d ⊢ ( 𝜑 → 𝑇 ∈ NrmMod )
26 nlmngp ⊢ ( 𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp )
27 25 26 syl ⊢ ( 𝜑 → 𝑇 ∈ NrmGrp )
28 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
29 2 28 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
30 9 29 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
31 30 16 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ 𝑇 ) )
32 28 4 nmcl ⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ )
33 27 31 32 syl2anc ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ )
34 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
35 7 elin1d ⊢ ( 𝜑 → 𝑆 ∈ NrmMod )
36 nlmngp ⊢ ( 𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp )
37 35 36 syl ⊢ ( 𝜑 → 𝑆 ∈ NrmGrp )
38 2 3 nmcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ) → ( 𝐿 ‘ 𝐵 ) ∈ ℝ )
39 37 16 38 syl2anc ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐵 ) ∈ ℝ )
40 14 39 remulcld ⊢ ( 𝜑 → ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) ∈ ℝ )
41 2 3 nmge0 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ) → 0 ≤ ( 𝐿 ‘ 𝐵 ) )
42 37 16 41 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 𝐿 ‘ 𝐵 ) )
43 14 39 15 42 mulge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) )
44 40 33 ltnled ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) < ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ↔ ¬ ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) ) )
45 19 44 mpbird ⊢ ( 𝜑 → ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) < ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) )
46 34 40 33 43 45 lelttrd ⊢ ( 𝜑 → 0 < ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) )
47 33 46 elrpd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ+ )
48 24 47 rerpdivcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ∈ ℝ )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ∈ ℝ )
50 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
51 12 sselda ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) → 𝑟 ∈ 𝐾 )
52 51 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝑟 ∈ 𝐾 )
53 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝐵 ∈ 𝑉 )
54 eqid ⊢ ( ·𝑠 ‘ 𝑇 ) = ( ·𝑠 ‘ 𝑇 )
55 5 6 2 13 54 lmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝑟 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝐵 ) ) )
56 50 52 53 55 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝐵 ) ) )
57 56 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) = ( 𝑀 ‘ ( 𝑟 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝐵 ) ) ) )
58 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝑇 ∈ NrmMod )
59 eqid ⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
60 5 59 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Scalar ‘ 𝑇 ) = 𝐺 )
61 50 60 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( Scalar ‘ 𝑇 ) = 𝐺 )
62 61 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ 𝐺 ) )
63 62 6 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( Base ‘ ( Scalar ‘ 𝑇 ) ) = 𝐾 )
64 52 63 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
65 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ 𝑇 ) )
66 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) )
67 eqid ⊢ ( norm ‘ ( Scalar ‘ 𝑇 ) ) = ( norm ‘ ( Scalar ‘ 𝑇 ) )
68 28 4 54 59 66 67 nmvs ⊢ ( ( 𝑇 ∈ NrmMod ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝑟 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝐵 ) ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ 𝑟 ) · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
69 58 64 65 68 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝑀 ‘ ( 𝑟 ( ·𝑠 ‘ 𝑇 ) ( 𝐹 ‘ 𝐵 ) ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ 𝑟 ) · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
70 61 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( norm ‘ ( Scalar ‘ 𝑇 ) ) = ( norm ‘ 𝐺 ) )
71 70 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ 𝑟 ) = ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) )
72 7 elin2d ⊢ ( 𝜑 → 𝑆 ∈ ℂMod )
73 72 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝑆 ∈ ℂMod )
74 5 6 clmabs ⊢ ( ( 𝑆 ∈ ℂMod ∧ 𝑟 ∈ 𝐾 ) → ( abs ‘ 𝑟 ) = ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) )
75 73 52 74 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( abs ‘ 𝑟 ) = ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) )
76 0red ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 0 ∈ ℝ )
77 11 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝑅 )
78 14 23 15 77 mulge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐴 · 𝑅 ) )
79 divge0 ⊢ ( ( ( ( 𝐴 · 𝑅 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · 𝑅 ) ) ∧ ( ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ 0 < ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) → 0 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
80 24 78 33 46 79 syl22anc ⊢ ( 𝜑 → 0 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
81 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 0 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
82 76 49 22 81 20 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 0 < 𝑟 )
83 76 22 82 ltled ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 0 ≤ 𝑟 )
84 22 83 absidd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( abs ‘ 𝑟 ) = 𝑟 )
85 75 84 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) = 𝑟 )
86 71 85 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ 𝑟 ) = 𝑟 )
87 86 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( ( norm ‘ ( Scalar ‘ 𝑇 ) ) ‘ 𝑟 ) · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) = ( 𝑟 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
88 57 69 87 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) = ( 𝑟 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
89 88 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) / 𝑅 ) = ( ( 𝑟 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) / 𝑅 ) )
90 2 5 13 6 clmvscl ⊢ ( ( 𝑆 ∈ ℂMod ∧ 𝑟 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑟 · 𝐵 ) ∈ 𝑉 )
91 73 52 53 90 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝑟 · 𝐵 ) ∈ 𝑉 )
92 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝑆 ∈ NrmMod )
93 eqid ⊢ ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
94 2 3 13 5 6 93 nmvs ⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑟 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) = ( ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) · ( 𝐿 ‘ 𝐵 ) ) )
95 92 52 53 94 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) = ( ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) · ( 𝐿 ‘ 𝐵 ) ) )
96 85 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( ( norm ‘ 𝐺 ) ‘ 𝑟 ) · ( 𝐿 ‘ 𝐵 ) ) = ( 𝑟 · ( 𝐿 ‘ 𝐵 ) ) )
97 95 96 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) = ( 𝑟 · ( 𝐿 ‘ 𝐵 ) ) )
98 simprr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) )
99 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝑅 ∈ ℝ )
100 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
101 2 3 100 nmrpcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝐵 ∈ 𝑉 ∧ 𝐵 ≠ ( 0g ‘ 𝑆 ) ) → ( 𝐿 ‘ 𝐵 ) ∈ ℝ+ )
102 37 16 17 101 syl3anc ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐵 ) ∈ ℝ+ )
103 102 rpregt0d ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐿 ‘ 𝐵 ) ) )
104 103 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( 𝐿 ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐿 ‘ 𝐵 ) ) )
105 ltmuldiv ⊢ ( ( 𝑟 ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ( ( 𝐿 ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐿 ‘ 𝐵 ) ) ) → ( ( 𝑟 · ( 𝐿 ‘ 𝐵 ) ) < 𝑅 ↔ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) )
106 22 99 104 105 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( 𝑟 · ( 𝐿 ‘ 𝐵 ) ) < 𝑅 ↔ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) )
107 98 106 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝑟 · ( 𝐿 ‘ 𝐵 ) ) < 𝑅 )
108 97 107 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) < 𝑅 )
109 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( 𝑟 · 𝐵 ) ∈ 𝑉 → ( ( 𝐿 ‘ ( 𝑟 · 𝐵 ) ) < 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 ) ) )
110 91 108 109 mp2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ ( 𝑟 · 𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 )
111 89 110 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( 𝑟 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 )
112 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ )
113 22 112 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝑟 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ∈ ℝ )
114 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝐴 ∈ ℝ )
115 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝑅 ∈ ℝ+ )
116 113 114 115 ledivmul2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( ( 𝑟 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) / 𝑅 ) ≤ 𝐴 ↔ ( 𝑟 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ≤ ( 𝐴 · 𝑅 ) ) )
117 111 116 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝑟 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ≤ ( 𝐴 · 𝑅 ) )
118 114 99 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝐴 · 𝑅 ) ∈ ℝ )
119 33 46 jca ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ 0 < ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
120 119 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ 0 < ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
121 lemuldiv ⊢ ( ( 𝑟 ∈ ℝ ∧ ( 𝐴 · 𝑅 ) ∈ ℝ ∧ ( ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ 0 < ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) → ( ( 𝑟 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ≤ ( 𝐴 · 𝑅 ) ↔ 𝑟 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) )
122 22 118 120 121 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( ( 𝑟 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ≤ ( 𝐴 · 𝑅 ) ↔ 𝑟 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) )
123 117 122 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → 𝑟 ≤ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
124 22 49 123 lensymd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ¬ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 )
125 20 124 pm2.21dd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℚ ) ∧ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) )
126 23 102 rerpdivcld ⊢ ( 𝜑 → ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ∈ ℝ )
127 14 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
128 23 recnd ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
129 39 recnd ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐵 ) ∈ ℂ )
130 mulass ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( 𝐿 ‘ 𝐵 ) ∈ ℂ ) → ( ( 𝐴 · 𝑅 ) · ( 𝐿 ‘ 𝐵 ) ) = ( 𝐴 · ( 𝑅 · ( 𝐿 ‘ 𝐵 ) ) ) )
131 mul12 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( 𝐿 ‘ 𝐵 ) ∈ ℂ ) → ( 𝐴 · ( 𝑅 · ( 𝐿 ‘ 𝐵 ) ) ) = ( 𝑅 · ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) ) )
132 130 131 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ∧ ( 𝐿 ‘ 𝐵 ) ∈ ℂ ) → ( ( 𝐴 · 𝑅 ) · ( 𝐿 ‘ 𝐵 ) ) = ( 𝑅 · ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) ) )
133 127 128 129 132 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 · 𝑅 ) · ( 𝐿 ‘ 𝐵 ) ) = ( 𝑅 · ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) ) )
134 40 33 11 45 ltmul2dd ⊢ ( 𝜑 → ( 𝑅 · ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) ) < ( 𝑅 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
135 133 134 eqbrtrd ⊢ ( 𝜑 → ( ( 𝐴 · 𝑅 ) · ( 𝐿 ‘ 𝐵 ) ) < ( 𝑅 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
136 lt2mul2div ⊢ ( ( ( ( 𝐴 · 𝑅 ) ∈ ℝ ∧ ( ( 𝐿 ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐿 ‘ 𝐵 ) ) ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ ∧ 0 < ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( ( 𝐴 · 𝑅 ) · ( 𝐿 ‘ 𝐵 ) ) < ( 𝑅 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ↔ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) )
137 24 103 23 119 136 syl22anc ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑅 ) · ( 𝐿 ‘ 𝐵 ) ) < ( 𝑅 · ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ↔ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) )
138 135 137 mpbid ⊢ ( 𝜑 → ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) )
139 qbtwnre ⊢ ( ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ∈ ℝ ∧ ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ∈ ℝ ∧ ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) → ∃ 𝑟 ∈ ℚ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) )
140 48 126 138 139 syl3anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℚ ( ( ( 𝐴 · 𝑅 ) / ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ) < 𝑟 ∧ 𝑟 < ( 𝑅 / ( 𝐿 ‘ 𝐵 ) ) ) )
141 125 140 r19.29a ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝐵 ) ) )
142 141 19 pm2.65i ⊢ ¬ 𝜑