Theorem dignn0flhalflem2

Description: Lemma 2 for dignn0flhalf . (Contributed by AV, 7-Jun-2012)

	Ref	Expression
Assertion	dignn0flhalflem2	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) = ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2	1	rehalfcld	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 / 2 ) ∈ ℝ )
3	2	flcld	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ ( 𝐴 / 2 ) ) ∈ ℤ )
4	3	zred	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
5	4	3ad2ant1	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
6		2re	⊢ 2 ∈ ℝ
7	6	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
8		id	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
9	7 8	reexpcld	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℝ )
10	9	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℝ )
11		2cnd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℂ )
12		2ne0	⊢ 2 ≠ 0
13	12	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 2 ≠ 0 )
14		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
15	14	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
16	11 13 15	expne0d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ≠ 0 )
17	5 10 16	redivcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
18	17	flcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ )
19	1	3ad2ant1	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
20	6	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℝ )
21		simp3	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
22		1nn0	⊢ 1 ∈ ℕ0
23	22	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℕ0 )
24	21 23	nn0addcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℕ0 )
25	20 24	reexpcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℝ )
26	15	peano2zd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℤ )
27	11 13 26	expne0d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ≠ 0 )
28	19 25 27	redivcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ∈ ℝ )
29	28	flcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ∈ ℤ )
30		nn0p1nn	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
31		dignn0flhalflem1	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑁 + 1 ) ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) < ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
32	30 31	syl3an3	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) < ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
33		1zzd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℤ )
34		flsubz	⊢ ( ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) = ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) )
35	28 33 34	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) = ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) )
36	35	eqcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) = ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) )
37		nnz	⊢ ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ )
38		zob	⊢ ( 𝐴 ∈ ℤ → ( ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ ) )
39	37 38	imbitrrid	⊢ ( 𝐴 ∈ ℤ → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
40	39	imp	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ) → ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ )
41		zofldiv2	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) = ( ( 𝐴 − 1 ) / 2 ) )
42	40 41	syldan	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) = ( ( 𝐴 − 1 ) / 2 ) )
43	42	3adant3	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) = ( ( 𝐴 − 1 ) / 2 ) )
44	43	fvoveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( ( ( 𝐴 − 1 ) / 2 ) / ( 2 ↑ 𝑁 ) ) ) )
45		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
46		1cnd	⊢ ( 𝐴 ∈ ℤ → 1 ∈ ℂ )
47	45 46	subcld	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 − 1 ) ∈ ℂ )
48		2rp	⊢ 2 ∈ ℝ+
49	48	a1i	⊢ ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → 2 ∈ ℝ+ )
50	49	rpcnne0d	⊢ ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
51	48	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ+ )
52	51 14	rpexpcld	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
53	52	rpcnne0d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) )
54		divdiv1	⊢ ( ( ( 𝐴 − 1 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) ) → ( ( ( 𝐴 − 1 ) / 2 ) / ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − 1 ) / ( 2 · ( 2 ↑ 𝑁 ) ) ) )
55	47 50 53 54	syl3an	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 − 1 ) / 2 ) / ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − 1 ) / ( 2 · ( 2 ↑ 𝑁 ) ) ) )
56	10	recnd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
57	11 56	mulcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑁 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
58	11 21	expp1d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
59	57 58	eqtr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑁 ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
60	59	oveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 − 1 ) / ( 2 · ( 2 ↑ 𝑁 ) ) ) = ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) )
61	55 60	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 − 1 ) / 2 ) / ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) )
62	61	fveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ( 𝐴 − 1 ) / 2 ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
63	44 62	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
64	32 36 63	3brtr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) < ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) )
65	19	rehalfcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / 2 ) ∈ ℝ )
66	65 10 16	redivcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
67		reflcl	⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
68	65 67	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
69	48	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℝ+ )
70	69 15	rpexpcld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
71		flle	⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 2 ) ) ≤ ( 𝐴 / 2 ) )
72	65 71	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) ≤ ( 𝐴 / 2 ) )
73	68 65 70 72	lediv1dd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ≤ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) )
74		flwordi	⊢ ( ( ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ ∧ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ≤ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ≤ ( ⌊ ‘ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ) )
75	17 66 73 74	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ≤ ( ⌊ ‘ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ) )
76		divdiv1	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) ) → ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) = ( 𝐴 / ( 2 · ( 2 ↑ 𝑁 ) ) ) )
77	45 50 53 76	syl3an	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) = ( 𝐴 / ( 2 · ( 2 ↑ 𝑁 ) ) ) )
78	52	rpcnd	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℂ )
79	78	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
80	11 79	mulcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑁 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
81	11 13 15	expp1zd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
82	80 81	eqtr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑁 ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
83	82	oveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / ( 2 · ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) )
84	77 83	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) = ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) )
85	84	eqcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) )
86	85	fveq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) = ( ⌊ ‘ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ) )
87	75 86	breqtrrd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
88		zgtp1leeq	⊢ ( ( ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ∈ ℤ ) → ( ( ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) < ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ∧ ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ) )
89	88	imp	⊢ ( ( ( ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ∈ ℤ ) ∧ ( ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) < ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ∧ ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ) ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
90	18 29 64 87 89	syl22anc	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
91	90	eqcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) = ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) )