# Metamath Proof Explorer

## Theorem bposlem7

Description: Lemma for bpos . The function F is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Hypotheses bposlem7.1 ${⊢}{F}=\left({n}\in ℕ⟼\sqrt{2}{G}\left(\sqrt{{n}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{n}}}\right)\right)$
bposlem7.2 ${⊢}{G}=\left({x}\in {ℝ}^{+}⟼\frac{\mathrm{log}{x}}{{x}}\right)$
bposlem7.3 ${⊢}{\phi }\to {A}\in ℕ$
bposlem7.4 ${⊢}{\phi }\to {B}\in ℕ$
bposlem7.5 ${⊢}{\phi }\to {\mathrm{e}}^{2}\le {A}$
bposlem7.6 ${⊢}{\phi }\to {\mathrm{e}}^{2}\le {B}$
Assertion bposlem7 ${⊢}{\phi }\to \left({A}<{B}\to {F}\left({B}\right)<{F}\left({A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 bposlem7.1 ${⊢}{F}=\left({n}\in ℕ⟼\sqrt{2}{G}\left(\sqrt{{n}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{n}}}\right)\right)$
2 bposlem7.2 ${⊢}{G}=\left({x}\in {ℝ}^{+}⟼\frac{\mathrm{log}{x}}{{x}}\right)$
3 bposlem7.3 ${⊢}{\phi }\to {A}\in ℕ$
4 bposlem7.4 ${⊢}{\phi }\to {B}\in ℕ$
5 bposlem7.5 ${⊢}{\phi }\to {\mathrm{e}}^{2}\le {A}$
6 bposlem7.6 ${⊢}{\phi }\to {\mathrm{e}}^{2}\le {B}$
7 4 nnrpd ${⊢}{\phi }\to {B}\in {ℝ}^{+}$
8 7 rpsqrtcld ${⊢}{\phi }\to \sqrt{{B}}\in {ℝ}^{+}$
9 fveq2 ${⊢}{x}=\sqrt{{B}}\to \mathrm{log}{x}=\mathrm{log}\sqrt{{B}}$
10 id ${⊢}{x}=\sqrt{{B}}\to {x}=\sqrt{{B}}$
11 9 10 oveq12d ${⊢}{x}=\sqrt{{B}}\to \frac{\mathrm{log}{x}}{{x}}=\frac{\mathrm{log}\sqrt{{B}}}{\sqrt{{B}}}$
12 ovex ${⊢}\frac{\mathrm{log}\sqrt{{B}}}{\sqrt{{B}}}\in \mathrm{V}$
13 11 2 12 fvmpt ${⊢}\sqrt{{B}}\in {ℝ}^{+}\to {G}\left(\sqrt{{B}}\right)=\frac{\mathrm{log}\sqrt{{B}}}{\sqrt{{B}}}$
14 8 13 syl ${⊢}{\phi }\to {G}\left(\sqrt{{B}}\right)=\frac{\mathrm{log}\sqrt{{B}}}{\sqrt{{B}}}$
15 3 nnrpd ${⊢}{\phi }\to {A}\in {ℝ}^{+}$
16 15 rpsqrtcld ${⊢}{\phi }\to \sqrt{{A}}\in {ℝ}^{+}$
17 fveq2 ${⊢}{x}=\sqrt{{A}}\to \mathrm{log}{x}=\mathrm{log}\sqrt{{A}}$
18 id ${⊢}{x}=\sqrt{{A}}\to {x}=\sqrt{{A}}$
19 17 18 oveq12d ${⊢}{x}=\sqrt{{A}}\to \frac{\mathrm{log}{x}}{{x}}=\frac{\mathrm{log}\sqrt{{A}}}{\sqrt{{A}}}$
20 ovex ${⊢}\frac{\mathrm{log}\sqrt{{A}}}{\sqrt{{A}}}\in \mathrm{V}$
21 19 2 20 fvmpt ${⊢}\sqrt{{A}}\in {ℝ}^{+}\to {G}\left(\sqrt{{A}}\right)=\frac{\mathrm{log}\sqrt{{A}}}{\sqrt{{A}}}$
22 16 21 syl ${⊢}{\phi }\to {G}\left(\sqrt{{A}}\right)=\frac{\mathrm{log}\sqrt{{A}}}{\sqrt{{A}}}$
23 14 22 breq12d ${⊢}{\phi }\to \left({G}\left(\sqrt{{B}}\right)<{G}\left(\sqrt{{A}}\right)↔\frac{\mathrm{log}\sqrt{{B}}}{\sqrt{{B}}}<\frac{\mathrm{log}\sqrt{{A}}}{\sqrt{{A}}}\right)$
24 16 rpred ${⊢}{\phi }\to \sqrt{{A}}\in ℝ$
25 15 rprege0d ${⊢}{\phi }\to \left({A}\in ℝ\wedge 0\le {A}\right)$
26 resqrtth ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to {\sqrt{{A}}}^{2}={A}$
27 25 26 syl ${⊢}{\phi }\to {\sqrt{{A}}}^{2}={A}$
28 5 27 breqtrrd ${⊢}{\phi }\to {\mathrm{e}}^{2}\le {\sqrt{{A}}}^{2}$
29 16 rpge0d ${⊢}{\phi }\to 0\le \sqrt{{A}}$
30 ere ${⊢}\mathrm{e}\in ℝ$
31 0re ${⊢}0\in ℝ$
32 epos ${⊢}0<\mathrm{e}$
33 31 30 32 ltleii ${⊢}0\le \mathrm{e}$
34 le2sq ${⊢}\left(\left(\mathrm{e}\in ℝ\wedge 0\le \mathrm{e}\right)\wedge \left(\sqrt{{A}}\in ℝ\wedge 0\le \sqrt{{A}}\right)\right)\to \left(\mathrm{e}\le \sqrt{{A}}↔{\mathrm{e}}^{2}\le {\sqrt{{A}}}^{2}\right)$
35 30 33 34 mpanl12 ${⊢}\left(\sqrt{{A}}\in ℝ\wedge 0\le \sqrt{{A}}\right)\to \left(\mathrm{e}\le \sqrt{{A}}↔{\mathrm{e}}^{2}\le {\sqrt{{A}}}^{2}\right)$
36 24 29 35 syl2anc ${⊢}{\phi }\to \left(\mathrm{e}\le \sqrt{{A}}↔{\mathrm{e}}^{2}\le {\sqrt{{A}}}^{2}\right)$
37 28 36 mpbird ${⊢}{\phi }\to \mathrm{e}\le \sqrt{{A}}$
38 8 rpred ${⊢}{\phi }\to \sqrt{{B}}\in ℝ$
39 7 rprege0d ${⊢}{\phi }\to \left({B}\in ℝ\wedge 0\le {B}\right)$
40 resqrtth ${⊢}\left({B}\in ℝ\wedge 0\le {B}\right)\to {\sqrt{{B}}}^{2}={B}$
41 39 40 syl ${⊢}{\phi }\to {\sqrt{{B}}}^{2}={B}$
42 6 41 breqtrrd ${⊢}{\phi }\to {\mathrm{e}}^{2}\le {\sqrt{{B}}}^{2}$
43 8 rpge0d ${⊢}{\phi }\to 0\le \sqrt{{B}}$
44 le2sq ${⊢}\left(\left(\mathrm{e}\in ℝ\wedge 0\le \mathrm{e}\right)\wedge \left(\sqrt{{B}}\in ℝ\wedge 0\le \sqrt{{B}}\right)\right)\to \left(\mathrm{e}\le \sqrt{{B}}↔{\mathrm{e}}^{2}\le {\sqrt{{B}}}^{2}\right)$
45 30 33 44 mpanl12 ${⊢}\left(\sqrt{{B}}\in ℝ\wedge 0\le \sqrt{{B}}\right)\to \left(\mathrm{e}\le \sqrt{{B}}↔{\mathrm{e}}^{2}\le {\sqrt{{B}}}^{2}\right)$
46 38 43 45 syl2anc ${⊢}{\phi }\to \left(\mathrm{e}\le \sqrt{{B}}↔{\mathrm{e}}^{2}\le {\sqrt{{B}}}^{2}\right)$
47 42 46 mpbird ${⊢}{\phi }\to \mathrm{e}\le \sqrt{{B}}$
48 logdivlt ${⊢}\left(\left(\sqrt{{A}}\in ℝ\wedge \mathrm{e}\le \sqrt{{A}}\right)\wedge \left(\sqrt{{B}}\in ℝ\wedge \mathrm{e}\le \sqrt{{B}}\right)\right)\to \left(\sqrt{{A}}<\sqrt{{B}}↔\frac{\mathrm{log}\sqrt{{B}}}{\sqrt{{B}}}<\frac{\mathrm{log}\sqrt{{A}}}{\sqrt{{A}}}\right)$
49 24 37 38 47 48 syl22anc ${⊢}{\phi }\to \left(\sqrt{{A}}<\sqrt{{B}}↔\frac{\mathrm{log}\sqrt{{B}}}{\sqrt{{B}}}<\frac{\mathrm{log}\sqrt{{A}}}{\sqrt{{A}}}\right)$
50 24 38 29 43 lt2sqd ${⊢}{\phi }\to \left(\sqrt{{A}}<\sqrt{{B}}↔{\sqrt{{A}}}^{2}<{\sqrt{{B}}}^{2}\right)$
51 23 49 50 3bitr2rd ${⊢}{\phi }\to \left({\sqrt{{A}}}^{2}<{\sqrt{{B}}}^{2}↔{G}\left(\sqrt{{B}}\right)<{G}\left(\sqrt{{A}}\right)\right)$
52 27 41 breq12d ${⊢}{\phi }\to \left({\sqrt{{A}}}^{2}<{\sqrt{{B}}}^{2}↔{A}<{B}\right)$
53 relogcl ${⊢}{x}\in {ℝ}^{+}\to \mathrm{log}{x}\in ℝ$
54 rerpdivcl ${⊢}\left(\mathrm{log}{x}\in ℝ\wedge {x}\in {ℝ}^{+}\right)\to \frac{\mathrm{log}{x}}{{x}}\in ℝ$
55 53 54 mpancom ${⊢}{x}\in {ℝ}^{+}\to \frac{\mathrm{log}{x}}{{x}}\in ℝ$
56 2 55 fmpti ${⊢}{G}:{ℝ}^{+}⟶ℝ$
57 56 ffvelrni ${⊢}\sqrt{{B}}\in {ℝ}^{+}\to {G}\left(\sqrt{{B}}\right)\in ℝ$
58 8 57 syl ${⊢}{\phi }\to {G}\left(\sqrt{{B}}\right)\in ℝ$
59 56 ffvelrni ${⊢}\sqrt{{A}}\in {ℝ}^{+}\to {G}\left(\sqrt{{A}}\right)\in ℝ$
60 16 59 syl ${⊢}{\phi }\to {G}\left(\sqrt{{A}}\right)\in ℝ$
61 2rp ${⊢}2\in {ℝ}^{+}$
62 rpsqrtcl ${⊢}2\in {ℝ}^{+}\to \sqrt{2}\in {ℝ}^{+}$
63 61 62 mp1i ${⊢}{\phi }\to \sqrt{2}\in {ℝ}^{+}$
64 58 60 63 ltmul2d ${⊢}{\phi }\to \left({G}\left(\sqrt{{B}}\right)<{G}\left(\sqrt{{A}}\right)↔\sqrt{2}{G}\left(\sqrt{{B}}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)\right)$
65 51 52 64 3bitr3d ${⊢}{\phi }\to \left({A}<{B}↔\sqrt{2}{G}\left(\sqrt{{B}}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)\right)$
66 65 biimpd ${⊢}{\phi }\to \left({A}<{B}\to \sqrt{2}{G}\left(\sqrt{{B}}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)\right)$
67 3 nnred ${⊢}{\phi }\to {A}\in ℝ$
68 4 nnred ${⊢}{\phi }\to {B}\in ℝ$
69 2re ${⊢}2\in ℝ$
70 2pos ${⊢}0<2$
71 69 70 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
72 71 a1i ${⊢}{\phi }\to \left(2\in ℝ\wedge 0<2\right)$
73 ltdiv1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left({A}<{B}↔\frac{{A}}{2}<\frac{{B}}{2}\right)$
74 67 68 72 73 syl3anc ${⊢}{\phi }\to \left({A}<{B}↔\frac{{A}}{2}<\frac{{B}}{2}\right)$
75 15 rphalfcld ${⊢}{\phi }\to \frac{{A}}{2}\in {ℝ}^{+}$
76 75 rpred ${⊢}{\phi }\to \frac{{A}}{2}\in ℝ$
77 30 69 remulcli ${⊢}\mathrm{e}\cdot 2\in ℝ$
78 77 a1i ${⊢}{\phi }\to \mathrm{e}\cdot 2\in ℝ$
79 30 resqcli ${⊢}{\mathrm{e}}^{2}\in ℝ$
80 79 a1i ${⊢}{\phi }\to {\mathrm{e}}^{2}\in ℝ$
81 egt2lt3 ${⊢}\left(2<\mathrm{e}\wedge \mathrm{e}<3\right)$
82 81 simpli ${⊢}2<\mathrm{e}$
83 69 30 82 ltleii ${⊢}2\le \mathrm{e}$
84 69 30 30 lemul2i ${⊢}0<\mathrm{e}\to \left(2\le \mathrm{e}↔\mathrm{e}\cdot 2\le \mathrm{e}\mathrm{e}\right)$
85 32 84 ax-mp ${⊢}2\le \mathrm{e}↔\mathrm{e}\cdot 2\le \mathrm{e}\mathrm{e}$
86 83 85 mpbi ${⊢}\mathrm{e}\cdot 2\le \mathrm{e}\mathrm{e}$
87 30 recni ${⊢}\mathrm{e}\in ℂ$
88 87 sqvali ${⊢}{\mathrm{e}}^{2}=\mathrm{e}\mathrm{e}$
89 86 88 breqtrri ${⊢}\mathrm{e}\cdot 2\le {\mathrm{e}}^{2}$
90 89 a1i ${⊢}{\phi }\to \mathrm{e}\cdot 2\le {\mathrm{e}}^{2}$
91 78 80 67 90 5 letrd ${⊢}{\phi }\to \mathrm{e}\cdot 2\le {A}$
92 lemuldiv ${⊢}\left(\mathrm{e}\in ℝ\wedge {A}\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\mathrm{e}\cdot 2\le {A}↔\mathrm{e}\le \frac{{A}}{2}\right)$
93 30 71 92 mp3an13 ${⊢}{A}\in ℝ\to \left(\mathrm{e}\cdot 2\le {A}↔\mathrm{e}\le \frac{{A}}{2}\right)$
94 67 93 syl ${⊢}{\phi }\to \left(\mathrm{e}\cdot 2\le {A}↔\mathrm{e}\le \frac{{A}}{2}\right)$
95 91 94 mpbid ${⊢}{\phi }\to \mathrm{e}\le \frac{{A}}{2}$
96 7 rphalfcld ${⊢}{\phi }\to \frac{{B}}{2}\in {ℝ}^{+}$
97 96 rpred ${⊢}{\phi }\to \frac{{B}}{2}\in ℝ$
98 78 80 68 90 6 letrd ${⊢}{\phi }\to \mathrm{e}\cdot 2\le {B}$
99 lemuldiv ${⊢}\left(\mathrm{e}\in ℝ\wedge {B}\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\mathrm{e}\cdot 2\le {B}↔\mathrm{e}\le \frac{{B}}{2}\right)$
100 30 71 99 mp3an13 ${⊢}{B}\in ℝ\to \left(\mathrm{e}\cdot 2\le {B}↔\mathrm{e}\le \frac{{B}}{2}\right)$
101 68 100 syl ${⊢}{\phi }\to \left(\mathrm{e}\cdot 2\le {B}↔\mathrm{e}\le \frac{{B}}{2}\right)$
102 98 101 mpbid ${⊢}{\phi }\to \mathrm{e}\le \frac{{B}}{2}$
103 logdivlt ${⊢}\left(\left(\frac{{A}}{2}\in ℝ\wedge \mathrm{e}\le \frac{{A}}{2}\right)\wedge \left(\frac{{B}}{2}\in ℝ\wedge \mathrm{e}\le \frac{{B}}{2}\right)\right)\to \left(\frac{{A}}{2}<\frac{{B}}{2}↔\frac{\mathrm{log}\left(\frac{{B}}{2}\right)}{\frac{{B}}{2}}<\frac{\mathrm{log}\left(\frac{{A}}{2}\right)}{\frac{{A}}{2}}\right)$
104 76 95 97 102 103 syl22anc ${⊢}{\phi }\to \left(\frac{{A}}{2}<\frac{{B}}{2}↔\frac{\mathrm{log}\left(\frac{{B}}{2}\right)}{\frac{{B}}{2}}<\frac{\mathrm{log}\left(\frac{{A}}{2}\right)}{\frac{{A}}{2}}\right)$
105 74 104 bitrd ${⊢}{\phi }\to \left({A}<{B}↔\frac{\mathrm{log}\left(\frac{{B}}{2}\right)}{\frac{{B}}{2}}<\frac{\mathrm{log}\left(\frac{{A}}{2}\right)}{\frac{{A}}{2}}\right)$
106 fveq2 ${⊢}{x}=\frac{{B}}{2}\to \mathrm{log}{x}=\mathrm{log}\left(\frac{{B}}{2}\right)$
107 id ${⊢}{x}=\frac{{B}}{2}\to {x}=\frac{{B}}{2}$
108 106 107 oveq12d ${⊢}{x}=\frac{{B}}{2}\to \frac{\mathrm{log}{x}}{{x}}=\frac{\mathrm{log}\left(\frac{{B}}{2}\right)}{\frac{{B}}{2}}$
109 ovex ${⊢}\frac{\mathrm{log}\left(\frac{{B}}{2}\right)}{\frac{{B}}{2}}\in \mathrm{V}$
110 108 2 109 fvmpt ${⊢}\frac{{B}}{2}\in {ℝ}^{+}\to {G}\left(\frac{{B}}{2}\right)=\frac{\mathrm{log}\left(\frac{{B}}{2}\right)}{\frac{{B}}{2}}$
111 96 110 syl ${⊢}{\phi }\to {G}\left(\frac{{B}}{2}\right)=\frac{\mathrm{log}\left(\frac{{B}}{2}\right)}{\frac{{B}}{2}}$
112 fveq2 ${⊢}{x}=\frac{{A}}{2}\to \mathrm{log}{x}=\mathrm{log}\left(\frac{{A}}{2}\right)$
113 id ${⊢}{x}=\frac{{A}}{2}\to {x}=\frac{{A}}{2}$
114 112 113 oveq12d ${⊢}{x}=\frac{{A}}{2}\to \frac{\mathrm{log}{x}}{{x}}=\frac{\mathrm{log}\left(\frac{{A}}{2}\right)}{\frac{{A}}{2}}$
115 ovex ${⊢}\frac{\mathrm{log}\left(\frac{{A}}{2}\right)}{\frac{{A}}{2}}\in \mathrm{V}$
116 114 2 115 fvmpt ${⊢}\frac{{A}}{2}\in {ℝ}^{+}\to {G}\left(\frac{{A}}{2}\right)=\frac{\mathrm{log}\left(\frac{{A}}{2}\right)}{\frac{{A}}{2}}$
117 75 116 syl ${⊢}{\phi }\to {G}\left(\frac{{A}}{2}\right)=\frac{\mathrm{log}\left(\frac{{A}}{2}\right)}{\frac{{A}}{2}}$
118 111 117 breq12d ${⊢}{\phi }\to \left({G}\left(\frac{{B}}{2}\right)<{G}\left(\frac{{A}}{2}\right)↔\frac{\mathrm{log}\left(\frac{{B}}{2}\right)}{\frac{{B}}{2}}<\frac{\mathrm{log}\left(\frac{{A}}{2}\right)}{\frac{{A}}{2}}\right)$
119 56 ffvelrni ${⊢}\frac{{B}}{2}\in {ℝ}^{+}\to {G}\left(\frac{{B}}{2}\right)\in ℝ$
120 96 119 syl ${⊢}{\phi }\to {G}\left(\frac{{B}}{2}\right)\in ℝ$
121 56 ffvelrni ${⊢}\frac{{A}}{2}\in {ℝ}^{+}\to {G}\left(\frac{{A}}{2}\right)\in ℝ$
122 75 121 syl ${⊢}{\phi }\to {G}\left(\frac{{A}}{2}\right)\in ℝ$
123 9nn ${⊢}9\in ℕ$
124 4nn ${⊢}4\in ℕ$
125 nnrp ${⊢}9\in ℕ\to 9\in {ℝ}^{+}$
126 nnrp ${⊢}4\in ℕ\to 4\in {ℝ}^{+}$
127 rpdivcl ${⊢}\left(9\in {ℝ}^{+}\wedge 4\in {ℝ}^{+}\right)\to \frac{9}{4}\in {ℝ}^{+}$
128 125 126 127 syl2an ${⊢}\left(9\in ℕ\wedge 4\in ℕ\right)\to \frac{9}{4}\in {ℝ}^{+}$
129 123 124 128 mp2an ${⊢}\frac{9}{4}\in {ℝ}^{+}$
130 129 a1i ${⊢}{\phi }\to \frac{9}{4}\in {ℝ}^{+}$
131 120 122 130 ltmul2d ${⊢}{\phi }\to \left({G}\left(\frac{{B}}{2}\right)<{G}\left(\frac{{A}}{2}\right)↔\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\right)$
132 105 118 131 3bitr2d ${⊢}{\phi }\to \left({A}<{B}↔\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\right)$
133 132 biimpd ${⊢}{\phi }\to \left({A}<{B}\to \left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\right)$
134 66 133 jcad ${⊢}{\phi }\to \left({A}<{B}\to \left(\sqrt{2}{G}\left(\sqrt{{B}}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)\wedge \left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\right)\right)$
135 sqrt2re ${⊢}\sqrt{2}\in ℝ$
136 remulcl ${⊢}\left(\sqrt{2}\in ℝ\wedge {G}\left(\sqrt{{B}}\right)\in ℝ\right)\to \sqrt{2}{G}\left(\sqrt{{B}}\right)\in ℝ$
137 135 58 136 sylancr ${⊢}{\phi }\to \sqrt{2}{G}\left(\sqrt{{B}}\right)\in ℝ$
138 9re ${⊢}9\in ℝ$
139 4re ${⊢}4\in ℝ$
140 4ne0 ${⊢}4\ne 0$
141 138 139 140 redivcli ${⊢}\frac{9}{4}\in ℝ$
142 remulcl ${⊢}\left(\frac{9}{4}\in ℝ\wedge {G}\left(\frac{{B}}{2}\right)\in ℝ\right)\to \left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)\in ℝ$
143 141 120 142 sylancr ${⊢}{\phi }\to \left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)\in ℝ$
144 remulcl ${⊢}\left(\sqrt{2}\in ℝ\wedge {G}\left(\sqrt{{A}}\right)\in ℝ\right)\to \sqrt{2}{G}\left(\sqrt{{A}}\right)\in ℝ$
145 135 60 144 sylancr ${⊢}{\phi }\to \sqrt{2}{G}\left(\sqrt{{A}}\right)\in ℝ$
146 remulcl ${⊢}\left(\frac{9}{4}\in ℝ\wedge {G}\left(\frac{{A}}{2}\right)\in ℝ\right)\to \left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\in ℝ$
147 141 122 146 sylancr ${⊢}{\phi }\to \left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\in ℝ$
148 lt2add ${⊢}\left(\left(\sqrt{2}{G}\left(\sqrt{{B}}\right)\in ℝ\wedge \left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)\in ℝ\right)\wedge \left(\sqrt{2}{G}\left(\sqrt{{A}}\right)\in ℝ\wedge \left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\in ℝ\right)\right)\to \left(\left(\sqrt{2}{G}\left(\sqrt{{B}}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)\wedge \left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\right)\to \sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\right)$
149 137 143 145 147 148 syl22anc ${⊢}{\phi }\to \left(\left(\sqrt{2}{G}\left(\sqrt{{B}}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)\wedge \left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\right)\to \sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\right)$
150 134 149 syld ${⊢}{\phi }\to \left({A}<{B}\to \sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\right)$
151 ltmul2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left({A}<{B}↔2{A}<2{B}\right)$
152 67 68 72 151 syl3anc ${⊢}{\phi }\to \left({A}<{B}↔2{A}<2{B}\right)$
153 rpmulcl ${⊢}\left(2\in {ℝ}^{+}\wedge {A}\in {ℝ}^{+}\right)\to 2{A}\in {ℝ}^{+}$
154 61 15 153 sylancr ${⊢}{\phi }\to 2{A}\in {ℝ}^{+}$
155 154 rpsqrtcld ${⊢}{\phi }\to \sqrt{2{A}}\in {ℝ}^{+}$
156 rpmulcl ${⊢}\left(2\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to 2{B}\in {ℝ}^{+}$
157 61 7 156 sylancr ${⊢}{\phi }\to 2{B}\in {ℝ}^{+}$
158 157 rpsqrtcld ${⊢}{\phi }\to \sqrt{2{B}}\in {ℝ}^{+}$
159 rprege0 ${⊢}\sqrt{2{A}}\in {ℝ}^{+}\to \left(\sqrt{2{A}}\in ℝ\wedge 0\le \sqrt{2{A}}\right)$
160 rprege0 ${⊢}\sqrt{2{B}}\in {ℝ}^{+}\to \left(\sqrt{2{B}}\in ℝ\wedge 0\le \sqrt{2{B}}\right)$
161 lt2sq ${⊢}\left(\left(\sqrt{2{A}}\in ℝ\wedge 0\le \sqrt{2{A}}\right)\wedge \left(\sqrt{2{B}}\in ℝ\wedge 0\le \sqrt{2{B}}\right)\right)\to \left(\sqrt{2{A}}<\sqrt{2{B}}↔{\sqrt{2{A}}}^{2}<{\sqrt{2{B}}}^{2}\right)$
162 159 160 161 syl2an ${⊢}\left(\sqrt{2{A}}\in {ℝ}^{+}\wedge \sqrt{2{B}}\in {ℝ}^{+}\right)\to \left(\sqrt{2{A}}<\sqrt{2{B}}↔{\sqrt{2{A}}}^{2}<{\sqrt{2{B}}}^{2}\right)$
163 155 158 162 syl2anc ${⊢}{\phi }\to \left(\sqrt{2{A}}<\sqrt{2{B}}↔{\sqrt{2{A}}}^{2}<{\sqrt{2{B}}}^{2}\right)$
164 154 rprege0d ${⊢}{\phi }\to \left(2{A}\in ℝ\wedge 0\le 2{A}\right)$
165 resqrtth ${⊢}\left(2{A}\in ℝ\wedge 0\le 2{A}\right)\to {\sqrt{2{A}}}^{2}=2{A}$
166 164 165 syl ${⊢}{\phi }\to {\sqrt{2{A}}}^{2}=2{A}$
167 157 rprege0d ${⊢}{\phi }\to \left(2{B}\in ℝ\wedge 0\le 2{B}\right)$
168 resqrtth ${⊢}\left(2{B}\in ℝ\wedge 0\le 2{B}\right)\to {\sqrt{2{B}}}^{2}=2{B}$
169 167 168 syl ${⊢}{\phi }\to {\sqrt{2{B}}}^{2}=2{B}$
170 166 169 breq12d ${⊢}{\phi }\to \left({\sqrt{2{A}}}^{2}<{\sqrt{2{B}}}^{2}↔2{A}<2{B}\right)$
171 163 170 bitr2d ${⊢}{\phi }\to \left(2{A}<2{B}↔\sqrt{2{A}}<\sqrt{2{B}}\right)$
172 1lt2 ${⊢}1<2$
173 rplogcl ${⊢}\left(2\in ℝ\wedge 1<2\right)\to \mathrm{log}2\in {ℝ}^{+}$
174 69 172 173 mp2an ${⊢}\mathrm{log}2\in {ℝ}^{+}$
175 174 a1i ${⊢}{\phi }\to \mathrm{log}2\in {ℝ}^{+}$
176 155 158 175 ltdiv2d ${⊢}{\phi }\to \left(\sqrt{2{A}}<\sqrt{2{B}}↔\frac{\mathrm{log}2}{\sqrt{2{B}}}<\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)$
177 152 171 176 3bitrd ${⊢}{\phi }\to \left({A}<{B}↔\frac{\mathrm{log}2}{\sqrt{2{B}}}<\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)$
178 177 biimpd ${⊢}{\phi }\to \left({A}<{B}\to \frac{\mathrm{log}2}{\sqrt{2{B}}}<\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)$
179 150 178 jcad ${⊢}{\phi }\to \left({A}<{B}\to \left(\sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\wedge \frac{\mathrm{log}2}{\sqrt{2{B}}}<\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)\right)$
180 137 143 readdcld ${⊢}{\phi }\to \sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)\in ℝ$
181 rpre ${⊢}\mathrm{log}2\in {ℝ}^{+}\to \mathrm{log}2\in ℝ$
182 174 181 ax-mp ${⊢}\mathrm{log}2\in ℝ$
183 rerpdivcl ${⊢}\left(\mathrm{log}2\in ℝ\wedge \sqrt{2{B}}\in {ℝ}^{+}\right)\to \frac{\mathrm{log}2}{\sqrt{2{B}}}\in ℝ$
184 182 158 183 sylancr ${⊢}{\phi }\to \frac{\mathrm{log}2}{\sqrt{2{B}}}\in ℝ$
185 145 147 readdcld ${⊢}{\phi }\to \sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\in ℝ$
186 rerpdivcl ${⊢}\left(\mathrm{log}2\in ℝ\wedge \sqrt{2{A}}\in {ℝ}^{+}\right)\to \frac{\mathrm{log}2}{\sqrt{2{A}}}\in ℝ$
187 182 155 186 sylancr ${⊢}{\phi }\to \frac{\mathrm{log}2}{\sqrt{2{A}}}\in ℝ$
188 lt2add ${⊢}\left(\left(\sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)\in ℝ\wedge \frac{\mathrm{log}2}{\sqrt{2{B}}}\in ℝ\right)\wedge \left(\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\in ℝ\wedge \frac{\mathrm{log}2}{\sqrt{2{A}}}\in ℝ\right)\right)\to \left(\left(\sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\wedge \frac{\mathrm{log}2}{\sqrt{2{B}}}<\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)\to \sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{B}}}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)\right)$
189 180 184 185 187 188 syl22anc ${⊢}{\phi }\to \left(\left(\sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)\wedge \frac{\mathrm{log}2}{\sqrt{2{B}}}<\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)\to \sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{B}}}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)\right)$
190 179 189 syld ${⊢}{\phi }\to \left({A}<{B}\to \sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{B}}}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)\right)$
191 2fveq3 ${⊢}{n}={B}\to {G}\left(\sqrt{{n}}\right)={G}\left(\sqrt{{B}}\right)$
192 191 oveq2d ${⊢}{n}={B}\to \sqrt{2}{G}\left(\sqrt{{n}}\right)=\sqrt{2}{G}\left(\sqrt{{B}}\right)$
193 fvoveq1 ${⊢}{n}={B}\to {G}\left(\frac{{n}}{2}\right)={G}\left(\frac{{B}}{2}\right)$
194 193 oveq2d ${⊢}{n}={B}\to \left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)=\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)$
195 192 194 oveq12d ${⊢}{n}={B}\to \sqrt{2}{G}\left(\sqrt{{n}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)=\sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)$
196 oveq2 ${⊢}{n}={B}\to 2{n}=2{B}$
197 196 fveq2d ${⊢}{n}={B}\to \sqrt{2{n}}=\sqrt{2{B}}$
198 197 oveq2d ${⊢}{n}={B}\to \frac{\mathrm{log}2}{\sqrt{2{n}}}=\frac{\mathrm{log}2}{\sqrt{2{B}}}$
199 195 198 oveq12d ${⊢}{n}={B}\to \sqrt{2}{G}\left(\sqrt{{n}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{n}}}\right)=\sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{B}}}\right)$
200 ovex ${⊢}\sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{B}}}\right)\in \mathrm{V}$
201 199 1 200 fvmpt ${⊢}{B}\in ℕ\to {F}\left({B}\right)=\sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{B}}}\right)$
202 4 201 syl ${⊢}{\phi }\to {F}\left({B}\right)=\sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{B}}}\right)$
203 2fveq3 ${⊢}{n}={A}\to {G}\left(\sqrt{{n}}\right)={G}\left(\sqrt{{A}}\right)$
204 203 oveq2d ${⊢}{n}={A}\to \sqrt{2}{G}\left(\sqrt{{n}}\right)=\sqrt{2}{G}\left(\sqrt{{A}}\right)$
205 fvoveq1 ${⊢}{n}={A}\to {G}\left(\frac{{n}}{2}\right)={G}\left(\frac{{A}}{2}\right)$
206 205 oveq2d ${⊢}{n}={A}\to \left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)=\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)$
207 204 206 oveq12d ${⊢}{n}={A}\to \sqrt{2}{G}\left(\sqrt{{n}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)=\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)$
208 oveq2 ${⊢}{n}={A}\to 2{n}=2{A}$
209 208 fveq2d ${⊢}{n}={A}\to \sqrt{2{n}}=\sqrt{2{A}}$
210 209 oveq2d ${⊢}{n}={A}\to \frac{\mathrm{log}2}{\sqrt{2{n}}}=\frac{\mathrm{log}2}{\sqrt{2{A}}}$
211 207 210 oveq12d ${⊢}{n}={A}\to \sqrt{2}{G}\left(\sqrt{{n}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{n}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{n}}}\right)=\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)$
212 ovex ${⊢}\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)\in \mathrm{V}$
213 211 1 212 fvmpt ${⊢}{A}\in ℕ\to {F}\left({A}\right)=\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)$
214 3 213 syl ${⊢}{\phi }\to {F}\left({A}\right)=\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)$
215 202 214 breq12d ${⊢}{\phi }\to \left({F}\left({B}\right)<{F}\left({A}\right)↔\sqrt{2}{G}\left(\sqrt{{B}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{B}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{B}}}\right)<\sqrt{2}{G}\left(\sqrt{{A}}\right)+\left(\frac{9}{4}\right){G}\left(\frac{{A}}{2}\right)+\left(\frac{\mathrm{log}2}{\sqrt{2{A}}}\right)\right)$
216 190 215 sylibrd ${⊢}{\phi }\to \left({A}<{B}\to {F}\left({B}\right)<{F}\left({A}\right)\right)$