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	⊢ ( 𝜑 → ( 𝐴 < 𝐵 → ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ) )