bposlem7

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

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

Proof

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

Metamath Proof Explorer

Theorem bposlem7

Proof