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
|- N = ( S normOp T )
nmoleub2.v
|- V = ( Base ` S )
nmoleub2.l
|- L = ( norm ` S )
nmoleub2.m
|- M = ( norm ` T )
nmoleub2.g
|- G = ( Scalar ` S )
nmoleub2.w
|- K = ( Base ` G )
nmoleub2.s
|- ( ph -> S e. ( NrmMod i^i CMod ) )
nmoleub2.t
|- ( ph -> T e. ( NrmMod i^i CMod ) )
nmoleub2.f
|- ( ph -> F e. ( S LMHom T ) )
nmoleub2.a
|- ( ph -> A e. RR* )
nmoleub2.r
|- ( ph -> R e. RR+ )
nmoleub2a.5
|- ( ph -> QQ C_ K )
nmoleub2lem3.p
|- .x. = ( .s ` S )
nmoleub2lem3.1
|- ( ph -> A e. RR )
nmoleub2lem3.2
|- ( ph -> 0 <_ A )
nmoleub2lem3.3
|- ( ph -> B e. V )
nmoleub2lem3.4
|- ( ph -> B =/= ( 0g ` S ) )
nmoleub2lem3.5
|- ( ph -> ( ( r .x. B ) e. V -> ( ( L ` ( r .x. B ) ) < R -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) <_ A ) ) )
nmoleub2lem3.6
|- ( ph -> -. ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) )
Assertion nmoleub2lem3
|- -. ph

Proof

Step Hyp Ref Expression
1 nmoleub2.n
 |-  N = ( S normOp T )
2 nmoleub2.v
 |-  V = ( Base ` S )
3 nmoleub2.l
 |-  L = ( norm ` S )
4 nmoleub2.m
 |-  M = ( norm ` T )
5 nmoleub2.g
 |-  G = ( Scalar ` S )
6 nmoleub2.w
 |-  K = ( Base ` G )
7 nmoleub2.s
 |-  ( ph -> S e. ( NrmMod i^i CMod ) )
8 nmoleub2.t
 |-  ( ph -> T e. ( NrmMod i^i CMod ) )
9 nmoleub2.f
 |-  ( ph -> F e. ( S LMHom T ) )
10 nmoleub2.a
 |-  ( ph -> A e. RR* )
11 nmoleub2.r
 |-  ( ph -> R e. RR+ )
12 nmoleub2a.5
 |-  ( ph -> QQ C_ K )
13 nmoleub2lem3.p
 |-  .x. = ( .s ` S )
14 nmoleub2lem3.1
 |-  ( ph -> A e. RR )
15 nmoleub2lem3.2
 |-  ( ph -> 0 <_ A )
16 nmoleub2lem3.3
 |-  ( ph -> B e. V )
17 nmoleub2lem3.4
 |-  ( ph -> B =/= ( 0g ` S ) )
18 nmoleub2lem3.5
 |-  ( ph -> ( ( r .x. B ) e. V -> ( ( L ` ( r .x. B ) ) < R -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) <_ A ) ) )
19 nmoleub2lem3.6
 |-  ( ph -> -. ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) )
20 simprl
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r )
21 qre
 |-  ( r e. QQ -> r e. RR )
22 21 ad2antlr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r e. RR )
23 11 rpred
 |-  ( ph -> R e. RR )
24 14 23 remulcld
 |-  ( ph -> ( A x. R ) e. RR )
25 8 elin1d
 |-  ( ph -> T e. NrmMod )
26 nlmngp
 |-  ( T e. NrmMod -> T e. NrmGrp )
27 25 26 syl
 |-  ( ph -> T e. NrmGrp )
28 eqid
 |-  ( Base ` T ) = ( Base ` T )
29 2 28 lmhmf
 |-  ( F e. ( S LMHom T ) -> F : V --> ( Base ` T ) )
30 9 29 syl
 |-  ( ph -> F : V --> ( Base ` T ) )
31 30 16 ffvelrnd
 |-  ( ph -> ( F ` B ) e. ( Base ` T ) )
32 28 4 nmcl
 |-  ( ( T e. NrmGrp /\ ( F ` B ) e. ( Base ` T ) ) -> ( M ` ( F ` B ) ) e. RR )
33 27 31 32 syl2anc
 |-  ( ph -> ( M ` ( F ` B ) ) e. RR )
34 0red
 |-  ( ph -> 0 e. RR )
35 7 elin1d
 |-  ( ph -> S e. NrmMod )
36 nlmngp
 |-  ( S e. NrmMod -> S e. NrmGrp )
37 35 36 syl
 |-  ( ph -> S e. NrmGrp )
38 2 3 nmcl
 |-  ( ( S e. NrmGrp /\ B e. V ) -> ( L ` B ) e. RR )
39 37 16 38 syl2anc
 |-  ( ph -> ( L ` B ) e. RR )
40 14 39 remulcld
 |-  ( ph -> ( A x. ( L ` B ) ) e. RR )
41 2 3 nmge0
 |-  ( ( S e. NrmGrp /\ B e. V ) -> 0 <_ ( L ` B ) )
42 37 16 41 syl2anc
 |-  ( ph -> 0 <_ ( L ` B ) )
43 14 39 15 42 mulge0d
 |-  ( ph -> 0 <_ ( A x. ( L ` B ) ) )
44 40 33 ltnled
 |-  ( ph -> ( ( A x. ( L ` B ) ) < ( M ` ( F ` B ) ) <-> -. ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) ) )
45 19 44 mpbird
 |-  ( ph -> ( A x. ( L ` B ) ) < ( M ` ( F ` B ) ) )
46 34 40 33 43 45 lelttrd
 |-  ( ph -> 0 < ( M ` ( F ` B ) ) )
47 33 46 elrpd
 |-  ( ph -> ( M ` ( F ` B ) ) e. RR+ )
48 24 47 rerpdivcld
 |-  ( ph -> ( ( A x. R ) / ( M ` ( F ` B ) ) ) e. RR )
49 48 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( A x. R ) / ( M ` ( F ` B ) ) ) e. RR )
50 9 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> F e. ( S LMHom T ) )
51 12 sselda
 |-  ( ( ph /\ r e. QQ ) -> r e. K )
52 51 adantr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r e. K )
53 16 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> B e. V )
54 eqid
 |-  ( .s ` T ) = ( .s ` T )
55 5 6 2 13 54 lmhmlin
 |-  ( ( F e. ( S LMHom T ) /\ r e. K /\ B e. V ) -> ( F ` ( r .x. B ) ) = ( r ( .s ` T ) ( F ` B ) ) )
56 50 52 53 55 syl3anc
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( F ` ( r .x. B ) ) = ( r ( .s ` T ) ( F ` B ) ) )
57 56 fveq2d
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( M ` ( F ` ( r .x. B ) ) ) = ( M ` ( r ( .s ` T ) ( F ` B ) ) ) )
58 25 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> T e. NrmMod )
59 eqid
 |-  ( Scalar ` T ) = ( Scalar ` T )
60 5 59 lmhmsca
 |-  ( F e. ( S LMHom T ) -> ( Scalar ` T ) = G )
61 50 60 syl
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( Scalar ` T ) = G )
62 61 fveq2d
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( Base ` ( Scalar ` T ) ) = ( Base ` G ) )
63 62 6 syl6eqr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( Base ` ( Scalar ` T ) ) = K )
64 52 63 eleqtrrd
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r e. ( Base ` ( Scalar ` T ) ) )
65 31 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( F ` B ) e. ( Base ` T ) )
66 eqid
 |-  ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) )
67 eqid
 |-  ( norm ` ( Scalar ` T ) ) = ( norm ` ( Scalar ` T ) )
68 28 4 54 59 66 67 nmvs
 |-  ( ( T e. NrmMod /\ r e. ( Base ` ( Scalar ` T ) ) /\ ( F ` B ) e. ( Base ` T ) ) -> ( M ` ( r ( .s ` T ) ( F ` B ) ) ) = ( ( ( norm ` ( Scalar ` T ) ) ` r ) x. ( M ` ( F ` B ) ) ) )
69 58 64 65 68 syl3anc
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( M ` ( r ( .s ` T ) ( F ` B ) ) ) = ( ( ( norm ` ( Scalar ` T ) ) ` r ) x. ( M ` ( F ` B ) ) ) )
70 61 fveq2d
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( norm ` ( Scalar ` T ) ) = ( norm ` G ) )
71 70 fveq1d
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( norm ` ( Scalar ` T ) ) ` r ) = ( ( norm ` G ) ` r ) )
72 7 elin2d
 |-  ( ph -> S e. CMod )
73 72 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> S e. CMod )
74 5 6 clmabs
 |-  ( ( S e. CMod /\ r e. K ) -> ( abs ` r ) = ( ( norm ` G ) ` r ) )
75 73 52 74 syl2anc
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( abs ` r ) = ( ( norm ` G ) ` r ) )
76 0red
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> 0 e. RR )
77 11 rpge0d
 |-  ( ph -> 0 <_ R )
78 14 23 15 77 mulge0d
 |-  ( ph -> 0 <_ ( A x. R ) )
79 divge0
 |-  ( ( ( ( A x. R ) e. RR /\ 0 <_ ( A x. R ) ) /\ ( ( M ` ( F ` B ) ) e. RR /\ 0 < ( M ` ( F ` B ) ) ) ) -> 0 <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) )
80 24 78 33 46 79 syl22anc
 |-  ( ph -> 0 <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) )
81 80 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> 0 <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) )
82 76 49 22 81 20 lelttrd
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> 0 < r )
83 76 22 82 ltled
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> 0 <_ r )
84 22 83 absidd
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( abs ` r ) = r )
85 75 84 eqtr3d
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( norm ` G ) ` r ) = r )
86 71 85 eqtrd
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( norm ` ( Scalar ` T ) ) ` r ) = r )
87 86 oveq1d
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( ( norm ` ( Scalar ` T ) ) ` r ) x. ( M ` ( F ` B ) ) ) = ( r x. ( M ` ( F ` B ) ) ) )
88 57 69 87 3eqtrd
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( M ` ( F ` ( r .x. B ) ) ) = ( r x. ( M ` ( F ` B ) ) ) )
89 88 oveq1d
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) = ( ( r x. ( M ` ( F ` B ) ) ) / R ) )
90 2 5 13 6 clmvscl
 |-  ( ( S e. CMod /\ r e. K /\ B e. V ) -> ( r .x. B ) e. V )
91 73 52 53 90 syl3anc
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( r .x. B ) e. V )
92 35 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> S e. NrmMod )
93 eqid
 |-  ( norm ` G ) = ( norm ` G )
94 2 3 13 5 6 93 nmvs
 |-  ( ( S e. NrmMod /\ r e. K /\ B e. V ) -> ( L ` ( r .x. B ) ) = ( ( ( norm ` G ) ` r ) x. ( L ` B ) ) )
95 92 52 53 94 syl3anc
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( L ` ( r .x. B ) ) = ( ( ( norm ` G ) ` r ) x. ( L ` B ) ) )
96 85 oveq1d
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( ( norm ` G ) ` r ) x. ( L ` B ) ) = ( r x. ( L ` B ) ) )
97 95 96 eqtrd
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( L ` ( r .x. B ) ) = ( r x. ( L ` B ) ) )
98 simprr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r < ( R / ( L ` B ) ) )
99 23 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> R e. RR )
100 eqid
 |-  ( 0g ` S ) = ( 0g ` S )
101 2 3 100 nmrpcl
 |-  ( ( S e. NrmGrp /\ B e. V /\ B =/= ( 0g ` S ) ) -> ( L ` B ) e. RR+ )
102 37 16 17 101 syl3anc
 |-  ( ph -> ( L ` B ) e. RR+ )
103 102 rpregt0d
 |-  ( ph -> ( ( L ` B ) e. RR /\ 0 < ( L ` B ) ) )
104 103 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( L ` B ) e. RR /\ 0 < ( L ` B ) ) )
105 ltmuldiv
 |-  ( ( r e. RR /\ R e. RR /\ ( ( L ` B ) e. RR /\ 0 < ( L ` B ) ) ) -> ( ( r x. ( L ` B ) ) < R <-> r < ( R / ( L ` B ) ) ) )
106 22 99 104 105 syl3anc
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( r x. ( L ` B ) ) < R <-> r < ( R / ( L ` B ) ) ) )
107 98 106 mpbird
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( r x. ( L ` B ) ) < R )
108 97 107 eqbrtrd
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( L ` ( r .x. B ) ) < R )
109 18 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( r .x. B ) e. V -> ( ( L ` ( r .x. B ) ) < R -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) <_ A ) ) )
110 91 108 109 mp2d
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) <_ A )
111 89 110 eqbrtrrd
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( r x. ( M ` ( F ` B ) ) ) / R ) <_ A )
112 33 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( M ` ( F ` B ) ) e. RR )
113 22 112 remulcld
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( r x. ( M ` ( F ` B ) ) ) e. RR )
114 14 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> A e. RR )
115 11 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> R e. RR+ )
116 113 114 115 ledivmul2d
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( ( r x. ( M ` ( F ` B ) ) ) / R ) <_ A <-> ( r x. ( M ` ( F ` B ) ) ) <_ ( A x. R ) ) )
117 111 116 mpbid
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( r x. ( M ` ( F ` B ) ) ) <_ ( A x. R ) )
118 114 99 remulcld
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( A x. R ) e. RR )
119 33 46 jca
 |-  ( ph -> ( ( M ` ( F ` B ) ) e. RR /\ 0 < ( M ` ( F ` B ) ) ) )
120 119 ad2antrr
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( M ` ( F ` B ) ) e. RR /\ 0 < ( M ` ( F ` B ) ) ) )
121 lemuldiv
 |-  ( ( r e. RR /\ ( A x. R ) e. RR /\ ( ( M ` ( F ` B ) ) e. RR /\ 0 < ( M ` ( F ` B ) ) ) ) -> ( ( r x. ( M ` ( F ` B ) ) ) <_ ( A x. R ) <-> r <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) ) )
122 22 118 120 121 syl3anc
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( r x. ( M ` ( F ` B ) ) ) <_ ( A x. R ) <-> r <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) ) )
123 117 122 mpbid
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r <_ ( ( A x. R ) / ( M ` ( F ` B ) ) ) )
124 22 49 123 lensymd
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> -. ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r )
125 20 124 pm2.21dd
 |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) )
126 23 102 rerpdivcld
 |-  ( ph -> ( R / ( L ` B ) ) e. RR )
127 14 recnd
 |-  ( ph -> A e. CC )
128 23 recnd
 |-  ( ph -> R e. CC )
129 39 recnd
 |-  ( ph -> ( L ` B ) e. CC )
130 mulass
 |-  ( ( A e. CC /\ R e. CC /\ ( L ` B ) e. CC ) -> ( ( A x. R ) x. ( L ` B ) ) = ( A x. ( R x. ( L ` B ) ) ) )
131 mul12
 |-  ( ( A e. CC /\ R e. CC /\ ( L ` B ) e. CC ) -> ( A x. ( R x. ( L ` B ) ) ) = ( R x. ( A x. ( L ` B ) ) ) )
132 130 131 eqtrd
 |-  ( ( A e. CC /\ R e. CC /\ ( L ` B ) e. CC ) -> ( ( A x. R ) x. ( L ` B ) ) = ( R x. ( A x. ( L ` B ) ) ) )
133 127 128 129 132 syl3anc
 |-  ( ph -> ( ( A x. R ) x. ( L ` B ) ) = ( R x. ( A x. ( L ` B ) ) ) )
134 40 33 11 45 ltmul2dd
 |-  ( ph -> ( R x. ( A x. ( L ` B ) ) ) < ( R x. ( M ` ( F ` B ) ) ) )
135 133 134 eqbrtrd
 |-  ( ph -> ( ( A x. R ) x. ( L ` B ) ) < ( R x. ( M ` ( F ` B ) ) ) )
136 lt2mul2div
 |-  ( ( ( ( A x. R ) e. RR /\ ( ( L ` B ) e. RR /\ 0 < ( L ` B ) ) ) /\ ( R e. RR /\ ( ( M ` ( F ` B ) ) e. RR /\ 0 < ( M ` ( F ` B ) ) ) ) ) -> ( ( ( A x. R ) x. ( L ` B ) ) < ( R x. ( M ` ( F ` B ) ) ) <-> ( ( A x. R ) / ( M ` ( F ` B ) ) ) < ( R / ( L ` B ) ) ) )
137 24 103 23 119 136 syl22anc
 |-  ( ph -> ( ( ( A x. R ) x. ( L ` B ) ) < ( R x. ( M ` ( F ` B ) ) ) <-> ( ( A x. R ) / ( M ` ( F ` B ) ) ) < ( R / ( L ` B ) ) ) )
138 135 137 mpbid
 |-  ( ph -> ( ( A x. R ) / ( M ` ( F ` B ) ) ) < ( R / ( L ` B ) ) )
139 qbtwnre
 |-  ( ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) e. RR /\ ( R / ( L ` B ) ) e. RR /\ ( ( A x. R ) / ( M ` ( F ` B ) ) ) < ( R / ( L ` B ) ) ) -> E. r e. QQ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) )
140 48 126 138 139 syl3anc
 |-  ( ph -> E. r e. QQ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) )
141 125 140 r19.29a
 |-  ( ph -> ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) )
142 141 19 pm2.65i
 |-  -. ph