# 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> ( ( A x. R ) / ( M ` ( F ` B ) ) ) e. RR )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> r e. K )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ph /\ r e. QQ ) /\ ( ( ( A x. R ) / ( M ` ( F ` B ) ) ) < r /\ r < ( R / ( L ` B ) ) ) ) -> A e. RR )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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`