dya2ub

Description: An upper bound for a dyadic number. (Contributed by Thierry Arnoux, 19-Sep-2017)

		Ref	Expression
	Assertion	dya2ub	$⊢ R \in ℝ^{+} \to \frac{1}{2^{⌊1 - \log_{2} R⌋}} < R$

Proof

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
3	1 2	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
4		relogbzcl	$⊢ (2 \in ℤ_{\geq 2} \land R \in ℝ^{+}) \to \log_{2} R \in ℝ$
5	3 4	mpan	$⊢ R \in ℝ^{+} \to \log_{2} R \in ℝ$
6	5	renegcld	$⊢ R \in ℝ^{+} \to - \log_{2} R \in ℝ$
7		flltp1	$⊢ - \log_{2} R \in ℝ \to - \log_{2} R < ⌊- \log_{2} R⌋ + 1$
8	6 7	syl	$⊢ R \in ℝ^{+} \to - \log_{2} R < ⌊- \log_{2} R⌋ + 1$
9		1z	$⊢ 1 \in ℤ$
10		fladdz	$⊢ (- \log_{2} R \in ℝ \land 1 \in ℤ) \to ⌊- \log_{2} R + 1⌋ = ⌊- \log_{2} R⌋ + 1$
11	6 9 10	sylancl	$⊢ R \in ℝ^{+} \to ⌊- \log_{2} R + 1⌋ = ⌊- \log_{2} R⌋ + 1$
12	5	recnd	$⊢ R \in ℝ^{+} \to \log_{2} R \in ℂ$
13		ax-1cn	$⊢ 1 \in ℂ$
14		negsubdi	$⊢ (\log_{2} R \in ℂ \land 1 \in ℂ) \to - (\log_{2} R - 1) = - \log_{2} R + 1$
15		negsubdi2	$⊢ (\log_{2} R \in ℂ \land 1 \in ℂ) \to - (\log_{2} R - 1) = 1 - \log_{2} R$
16	14 15	eqtr3d	$⊢ (\log_{2} R \in ℂ \land 1 \in ℂ) \to - \log_{2} R + 1 = 1 - \log_{2} R$
17	12 13 16	sylancl	$⊢ R \in ℝ^{+} \to - \log_{2} R + 1 = 1 - \log_{2} R$
18	17	fveq2d	$⊢ R \in ℝ^{+} \to ⌊- \log_{2} R + 1⌋ = ⌊1 - \log_{2} R⌋$
19	11 18	eqtr3d	$⊢ R \in ℝ^{+} \to ⌊- \log_{2} R⌋ + 1 = ⌊1 - \log_{2} R⌋$
20	8 19	breqtrd	$⊢ R \in ℝ^{+} \to - \log_{2} R < ⌊1 - \log_{2} R⌋$
21	3	a1i	$⊢ R \in ℝ^{+} \to 2 \in ℤ_{\geq 2}$
22		2rp	$⊢ 2 \in ℝ^{+}$
23	22	a1i	$⊢ R \in ℝ^{+} \to 2 \in ℝ^{+}$
24		1red	$⊢ R \in ℝ^{+} \to 1 \in ℝ$
25	24 5	resubcld	$⊢ R \in ℝ^{+} \to 1 - \log_{2} R \in ℝ$
26	25	flcld	$⊢ R \in ℝ^{+} \to ⌊1 - \log_{2} R⌋ \in ℤ$
27	23 26	rpexpcld	$⊢ R \in ℝ^{+} \to 2^{⌊1 - \log_{2} R⌋} \in ℝ^{+}$
28	27	rpreccld	$⊢ R \in ℝ^{+} \to \frac{1}{2^{⌊1 - \log_{2} R⌋}} \in ℝ^{+}$
29		id	$⊢ R \in ℝ^{+} \to R \in ℝ^{+}$
30		logblt	$⊢ (2 \in ℤ_{\geq 2} \land \frac{1}{2^{⌊1 - \log_{2} R⌋}} \in ℝ^{+} \land R \in ℝ^{+}) \to (\frac{1}{2^{⌊1 - \log_{2} R⌋}} < R \leftrightarrow \log_{2} (\frac{1}{2^{⌊1 - \log_{2} R⌋}}) < \log_{2} R)$
31	21 28 29 30	syl3anc	$⊢ R \in ℝ^{+} \to (\frac{1}{2^{⌊1 - \log_{2} R⌋}} < R \leftrightarrow \log_{2} (\frac{1}{2^{⌊1 - \log_{2} R⌋}}) < \log_{2} R)$
32		logbrec	$⊢ (2 \in ℤ_{\geq 2} \land 2^{⌊1 - \log_{2} R⌋} \in ℝ^{+}) \to \log_{2} (\frac{1}{2^{⌊1 - \log_{2} R⌋}}) = - \log_{2} 2^{⌊1 - \log_{2} R⌋}$
33	21 27 32	syl2anc	$⊢ R \in ℝ^{+} \to \log_{2} (\frac{1}{2^{⌊1 - \log_{2} R⌋}}) = - \log_{2} 2^{⌊1 - \log_{2} R⌋}$
34	33	breq1d	$⊢ R \in ℝ^{+} \to (\log_{2} (\frac{1}{2^{⌊1 - \log_{2} R⌋}}) < \log_{2} R \leftrightarrow - \log_{2} 2^{⌊1 - \log_{2} R⌋} < \log_{2} R)$
35		relogbzcl	$⊢ (2 \in ℤ_{\geq 2} \land 2^{⌊1 - \log_{2} R⌋} \in ℝ^{+}) \to \log_{2} 2^{⌊1 - \log_{2} R⌋} \in ℝ$
36	21 27 35	syl2anc	$⊢ R \in ℝ^{+} \to \log_{2} 2^{⌊1 - \log_{2} R⌋} \in ℝ$
37		ltnegcon1	$⊢ (\log_{2} 2^{⌊1 - \log_{2} R⌋} \in ℝ \land \log_{2} R \in ℝ) \to (- \log_{2} 2^{⌊1 - \log_{2} R⌋} < \log_{2} R \leftrightarrow - \log_{2} R < \log_{2} 2^{⌊1 - \log_{2} R⌋})$
38	36 5 37	syl2anc	$⊢ R \in ℝ^{+} \to (- \log_{2} 2^{⌊1 - \log_{2} R⌋} < \log_{2} R \leftrightarrow - \log_{2} R < \log_{2} 2^{⌊1 - \log_{2} R⌋})$
39	31 34 38	3bitrd	$⊢ R \in ℝ^{+} \to (\frac{1}{2^{⌊1 - \log_{2} R⌋}} < R \leftrightarrow - \log_{2} R < \log_{2} 2^{⌊1 - \log_{2} R⌋})$
40		nnlogbexp	$⊢ (2 \in ℤ_{\geq 2} \land ⌊1 - \log_{2} R⌋ \in ℤ) \to \log_{2} 2^{⌊1 - \log_{2} R⌋} = ⌊1 - \log_{2} R⌋$
41	21 26 40	syl2anc	$⊢ R \in ℝ^{+} \to \log_{2} 2^{⌊1 - \log_{2} R⌋} = ⌊1 - \log_{2} R⌋$
42	41	breq2d	$⊢ R \in ℝ^{+} \to (- \log_{2} R < \log_{2} 2^{⌊1 - \log_{2} R⌋} \leftrightarrow - \log_{2} R < ⌊1 - \log_{2} R⌋)$
43	39 42	bitrd	$⊢ R \in ℝ^{+} \to (\frac{1}{2^{⌊1 - \log_{2} R⌋}} < R \leftrightarrow - \log_{2} R < ⌊1 - \log_{2} R⌋)$
44	20 43	mpbird	$⊢ R \in ℝ^{+} \to \frac{1}{2^{⌊1 - \log_{2} R⌋}} < R$

Metamath Proof Explorer

Theorem dya2ub

Proof