This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( √ ‘ 2 ) · ( 𝐺 ‘ ( √ ‘ 𝑛 ) ) ) + ( ( 9 / 4 ) · ( 𝐺 ‘ ( 𝑛 / 2 ) ) ) ) + ( ( log ‘ 2 ) / ( √ ‘ ( 2 · 𝑛 ) ) ) ) )
bposlem7.2 ⊢ 𝐺 = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) / 𝑥 ) )
bposlem7.3 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
bposlem7.4 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
bposlem7.5 ⊢ ( 𝜑 → ( e ↑ 2 ) ≤ 𝐴 )
bposlem7.6 ⊢ ( 𝜑 → ( e ↑ 2 ) ≤ 𝐵 )
Assertion bposlem7 ( 𝜑 → ( 𝐴 < 𝐵 → ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ) )

Proof

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