Theorem dya2ub

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

	Ref	Expression
Assertion	dya2ub	⊢ ( 𝑅 ∈ ℝ+ → ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) < 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		uzid	⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
3	1 2	ax-mp	⊢ 2 ∈ ( ℤ≥ ‘ 2 )
4		relogbzcl	⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ ℝ+ ) → ( 2 logb 𝑅 ) ∈ ℝ )
5	3 4	mpan	⊢ ( 𝑅 ∈ ℝ+ → ( 2 logb 𝑅 ) ∈ ℝ )
6	5	renegcld	⊢ ( 𝑅 ∈ ℝ+ → - ( 2 logb 𝑅 ) ∈ ℝ )
7		flltp1	⊢ ( - ( 2 logb 𝑅 ) ∈ ℝ → - ( 2 logb 𝑅 ) < ( ( ⌊ ‘ - ( 2 logb 𝑅 ) ) + 1 ) )
8	6 7	syl	⊢ ( 𝑅 ∈ ℝ+ → - ( 2 logb 𝑅 ) < ( ( ⌊ ‘ - ( 2 logb 𝑅 ) ) + 1 ) )
9		1z	⊢ 1 ∈ ℤ
10		fladdz	⊢ ( ( - ( 2 logb 𝑅 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ⌊ ‘ ( - ( 2 logb 𝑅 ) + 1 ) ) = ( ( ⌊ ‘ - ( 2 logb 𝑅 ) ) + 1 ) )
11	6 9 10	sylancl	⊢ ( 𝑅 ∈ ℝ+ → ( ⌊ ‘ ( - ( 2 logb 𝑅 ) + 1 ) ) = ( ( ⌊ ‘ - ( 2 logb 𝑅 ) ) + 1 ) )
12	5	recnd	⊢ ( 𝑅 ∈ ℝ+ → ( 2 logb 𝑅 ) ∈ ℂ )
13		ax-1cn	⊢ 1 ∈ ℂ
14		negsubdi	⊢ ( ( ( 2 logb 𝑅 ) ∈ ℂ ∧ 1 ∈ ℂ ) → - ( ( 2 logb 𝑅 ) − 1 ) = ( - ( 2 logb 𝑅 ) + 1 ) )
15		negsubdi2	⊢ ( ( ( 2 logb 𝑅 ) ∈ ℂ ∧ 1 ∈ ℂ ) → - ( ( 2 logb 𝑅 ) − 1 ) = ( 1 − ( 2 logb 𝑅 ) ) )
16	14 15	eqtr3d	⊢ ( ( ( 2 logb 𝑅 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( - ( 2 logb 𝑅 ) + 1 ) = ( 1 − ( 2 logb 𝑅 ) ) )
17	12 13 16	sylancl	⊢ ( 𝑅 ∈ ℝ+ → ( - ( 2 logb 𝑅 ) + 1 ) = ( 1 − ( 2 logb 𝑅 ) ) )
18	17	fveq2d	⊢ ( 𝑅 ∈ ℝ+ → ( ⌊ ‘ ( - ( 2 logb 𝑅 ) + 1 ) ) = ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) )
19	11 18	eqtr3d	⊢ ( 𝑅 ∈ ℝ+ → ( ( ⌊ ‘ - ( 2 logb 𝑅 ) ) + 1 ) = ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) )
20	8 19	breqtrd	⊢ ( 𝑅 ∈ ℝ+ → - ( 2 logb 𝑅 ) < ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) )
21	3	a1i	⊢ ( 𝑅 ∈ ℝ+ → 2 ∈ ( ℤ≥ ‘ 2 ) )
22		2rp	⊢ 2 ∈ ℝ+
23	22	a1i	⊢ ( 𝑅 ∈ ℝ+ → 2 ∈ ℝ+ )
24		1red	⊢ ( 𝑅 ∈ ℝ+ → 1 ∈ ℝ )
25	24 5	resubcld	⊢ ( 𝑅 ∈ ℝ+ → ( 1 − ( 2 logb 𝑅 ) ) ∈ ℝ )
26	25	flcld	⊢ ( 𝑅 ∈ ℝ+ → ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ∈ ℤ )
27	23 26	rpexpcld	⊢ ( 𝑅 ∈ ℝ+ → ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ∈ ℝ+ )
28	27	rpreccld	⊢ ( 𝑅 ∈ ℝ+ → ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ∈ ℝ+ )
29		id	⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ+ )
30		logblt	⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ∈ ℝ+ ∧ 𝑅 ∈ ℝ+ ) → ( ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) < 𝑅 ↔ ( 2 logb ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ) < ( 2 logb 𝑅 ) ) )
31	21 28 29 30	syl3anc	⊢ ( 𝑅 ∈ ℝ+ → ( ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) < 𝑅 ↔ ( 2 logb ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ) < ( 2 logb 𝑅 ) ) )
32		logbrec	⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ∈ ℝ+ ) → ( 2 logb ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ) = - ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) )
33	21 27 32	syl2anc	⊢ ( 𝑅 ∈ ℝ+ → ( 2 logb ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ) = - ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) )
34	33	breq1d	⊢ ( 𝑅 ∈ ℝ+ → ( ( 2 logb ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ) < ( 2 logb 𝑅 ) ↔ - ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) < ( 2 logb 𝑅 ) ) )
35		relogbzcl	⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ∈ ℝ+ ) → ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ∈ ℝ )
36	21 27 35	syl2anc	⊢ ( 𝑅 ∈ ℝ+ → ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ∈ ℝ )
37		ltnegcon1	⊢ ( ( ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ∈ ℝ ∧ ( 2 logb 𝑅 ) ∈ ℝ ) → ( - ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) < ( 2 logb 𝑅 ) ↔ - ( 2 logb 𝑅 ) < ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ) )
38	36 5 37	syl2anc	⊢ ( 𝑅 ∈ ℝ+ → ( - ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) < ( 2 logb 𝑅 ) ↔ - ( 2 logb 𝑅 ) < ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ) )
39	31 34 38	3bitrd	⊢ ( 𝑅 ∈ ℝ+ → ( ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) < 𝑅 ↔ - ( 2 logb 𝑅 ) < ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ) )
40		nnlogbexp	⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ∈ ℤ ) → ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) = ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) )
41	21 26 40	syl2anc	⊢ ( 𝑅 ∈ ℝ+ → ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) = ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) )
42	41	breq2d	⊢ ( 𝑅 ∈ ℝ+ → ( - ( 2 logb 𝑅 ) < ( 2 logb ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) ↔ - ( 2 logb 𝑅 ) < ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) )
43	39 42	bitrd	⊢ ( 𝑅 ∈ ℝ+ → ( ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) < 𝑅 ↔ - ( 2 logb 𝑅 ) < ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) )
44	20 43	mpbird	⊢ ( 𝑅 ∈ ℝ+ → ( 1 / ( 2 ↑ ( ⌊ ‘ ( 1 − ( 2 logb 𝑅 ) ) ) ) ) < 𝑅 )