dignn0flhalflem2 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dignn0flhalflem2		Structured version Visualization version GIF version

Theorem dignn0flhalflem2 49822

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

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

**Proof of Theorem dignn0flhalflem2**
Step	Hyp	Ref	Expression
1		zre 12701	. . . . . . . . 9 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
2	1	rehalfcld 12597	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ → (𝐴 / 2) ∈ ℝ)
3	2	flcld 13942	. . . . . . 7 ⊢ (𝐴 ∈ ℤ → (⌊‘(𝐴 / 2)) ∈ ℤ)
4	3	zred 12807	. . . . . 6 ⊢ (𝐴 ∈ ℤ → (⌊‘(𝐴 / 2)) ∈ ℝ)
5	4	3ad2ant1 1151	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘(𝐴 / 2)) ∈ ℝ)
6		2re 12421	. . . . . . . 8 ⊢ 2 ∈ ℝ
7	6	a1i 11	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 2 ∈ ℝ)
8		id 23	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℕ₀)
9	7, 8	reexpcld 14310	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (2↑𝑁) ∈ ℝ)
10	9	3ad2ant3 1153	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2↑𝑁) ∈ ℝ)
11		2cnd 12425	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → 2 ∈ ℂ)
12		2ne0 12453	. . . . . . 7 ⊢ 2 ≠ 0
13	12	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → 2 ≠ 0)
14		nn0z 12721	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
15	14	3ad2ant3 1153	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℤ)
16	11, 13, 15	expne0d 14299	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2↑𝑁) ≠ 0)
17	5, 10, 16	redivcld 12149	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((⌊‘(𝐴 / 2)) / (2↑𝑁)) ∈ ℝ)
18	17	flcld 13942	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∈ ℤ)
19	1	3ad2ant1 1151	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → 𝐴 ∈ ℝ)
20	6	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → 2 ∈ ℝ)
21		simp3 1156	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℕ₀)
22		1nn0 12626	. . . . . . . 8 ⊢ 1 ∈ ℕ₀
23	22	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → 1 ∈ ℕ₀)
24	21, 23	nn0addcld 12675	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (𝑁 + 1) ∈ ℕ₀)
25	20, 24	reexpcld 14310	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2↑(𝑁 + 1)) ∈ ℝ)
26	15	peano2zd 12810	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (𝑁 + 1) ∈ ℤ)
27	11, 13, 26	expne0d 14299	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2↑(𝑁 + 1)) ≠ 0)
28	19, 25, 27	redivcld 12149	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (𝐴 / (2↑(𝑁 + 1))) ∈ ℝ)
29	28	flcld 13942	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) ∈ ℤ)
30		nn0p1nn 12649	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
31		dignn0flhalflem1 49821	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ (𝑁 + 1) ∈ ℕ) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) < (⌊‘((𝐴 − 1) / (2↑(𝑁 + 1)))))
32	30, 31	syl3an3 1183	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) < (⌊‘((𝐴 − 1) / (2↑(𝑁 + 1)))))
33		1zzd 12731	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → 1 ∈ ℤ)
34		flsubz 49728	. . . . . 6 ⊢ (((𝐴 / (2↑(𝑁 + 1))) ∈ ℝ ∧ 1 ∈ ℤ) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) = ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1))
35	28, 33, 34	syl2anc 596	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)) = ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1))
36	35	eqcomd 2766	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) = (⌊‘((𝐴 / (2↑(𝑁 + 1))) − 1)))
37		nnz 12718	. . . . . . . . . 10 ⊢ (((𝐴 − 1) / 2) ∈ ℕ → ((𝐴 − 1) / 2) ∈ ℤ)
38		zob 16535	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℤ → (((𝐴 + 1) / 2) ∈ ℤ ↔ ((𝐴 − 1) / 2) ∈ ℤ))
39	37, 38	imbitrrid 249	. . . . . . . . 9 ⊢ (𝐴 ∈ ℤ → (((𝐴 − 1) / 2) ∈ ℕ → ((𝐴 + 1) / 2) ∈ ℤ))
40	39	imp 412	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ) → ((𝐴 + 1) / 2) ∈ ℤ)
41		zofldiv2 49737	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 + 1) / 2) ∈ ℤ) → (⌊‘(𝐴 / 2)) = ((𝐴 − 1) / 2))
42	40, 41	syldan 603	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ) → (⌊‘(𝐴 / 2)) = ((𝐴 − 1) / 2))
43	42	3adant3 1150	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘(𝐴 / 2)) = ((𝐴 − 1) / 2))
44	43	fvoveq1d 7443	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(((𝐴 − 1) / 2) / (2↑𝑁))))
45		zcn 12702	. . . . . . . . 9 ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
46		1cnd 11306	. . . . . . . . 9 ⊢ (𝐴 ∈ ℤ → 1 ∈ ℂ)
47	45, 46	subcld 11673	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℂ)
48		2rp 13129	. . . . . . . . . 10 ⊢ 2 ∈ ℝ⁺
49	48	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 − 1) / 2) ∈ ℕ → 2 ∈ ℝ⁺)
50	49	rpcnne0d 13177	. . . . . . . 8 ⊢ (((𝐴 − 1) / 2) ∈ ℕ → (2 ∈ ℂ ∧ 2 ≠ 0))
51	48	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → 2 ∈ ℝ⁺)
52	51, 14	rpexpcld 14395	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (2↑𝑁) ∈ ℝ⁺)
53	52	rpcnne0d 13177	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0))
54		divdiv1 12032	. . . . . . . 8 ⊢ (((𝐴 − 1) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0)) → (((𝐴 − 1) / 2) / (2↑𝑁)) = ((𝐴 − 1) / (2 · (2↑𝑁))))
55	47, 50, 53, 54	syl3an 1178	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (((𝐴 − 1) / 2) / (2↑𝑁)) = ((𝐴 − 1) / (2 · (2↑𝑁))))
56	10	recnd 11341	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2↑𝑁) ∈ ℂ)
57	11, 56	mulcomd 11334	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2 · (2↑𝑁)) = ((2↑𝑁) · 2))
58	11, 21	expp1d 14294	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2))
59	57, 58	eqtr4d 2798	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2 · (2↑𝑁)) = (2↑(𝑁 + 1)))
60	59	oveq2d 7437	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((𝐴 − 1) / (2 · (2↑𝑁))) = ((𝐴 − 1) / (2↑(𝑁 + 1))))
61	55, 60	eqtrd 2795	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (((𝐴 − 1) / 2) / (2↑𝑁)) = ((𝐴 − 1) / (2↑(𝑁 + 1))))
62	61	fveq2d 6890	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘(((𝐴 − 1) / 2) / (2↑𝑁))) = (⌊‘((𝐴 − 1) / (2↑(𝑁 + 1)))))
63	44, 62	eqtrd 2795	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘((𝐴 − 1) / (2↑(𝑁 + 1)))))
64	32, 36, 63	3brtr4d 5136	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) < (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))))
65	19	rehalfcld 12597	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (𝐴 / 2) ∈ ℝ)
66	65, 10, 16	redivcld 12149	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((𝐴 / 2) / (2↑𝑁)) ∈ ℝ)
67		reflcl 13940	. . . . . . 7 ⊢ ((𝐴 / 2) ∈ ℝ → (⌊‘(𝐴 / 2)) ∈ ℝ)
68	65, 67	syl 18	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘(𝐴 / 2)) ∈ ℝ)
69	48	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → 2 ∈ ℝ⁺)
70	69, 15	rpexpcld 14395	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2↑𝑁) ∈ ℝ⁺)
71		flle 13943	. . . . . . 7 ⊢ ((𝐴 / 2) ∈ ℝ → (⌊‘(𝐴 / 2)) ≤ (𝐴 / 2))
72	65, 71	syl 18	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘(𝐴 / 2)) ≤ (𝐴 / 2))
73	68, 65, 70, 72	lediv1dd 13226	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((⌊‘(𝐴 / 2)) / (2↑𝑁)) ≤ ((𝐴 / 2) / (2↑𝑁)))
74		flwordi 13956	. . . . 5 ⊢ ((((⌊‘(𝐴 / 2)) / (2↑𝑁)) ∈ ℝ ∧ ((𝐴 / 2) / (2↑𝑁)) ∈ ℝ ∧ ((⌊‘(𝐴 / 2)) / (2↑𝑁)) ≤ ((𝐴 / 2) / (2↑𝑁))) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘((𝐴 / 2) / (2↑𝑁))))
75	17, 66, 73, 74	syl3anc 1398	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘((𝐴 / 2) / (2↑𝑁))))
76		divdiv1 12032	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((2↑𝑁) ∈ ℂ ∧ (2↑𝑁) ≠ 0)) → ((𝐴 / 2) / (2↑𝑁)) = (𝐴 / (2 · (2↑𝑁))))
77	45, 50, 53, 76	syl3an 1178	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((𝐴 / 2) / (2↑𝑁)) = (𝐴 / (2 · (2↑𝑁))))
78	52	rpcnd 13170	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (2↑𝑁) ∈ ℂ)
79	78	3ad2ant3 1153	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2↑𝑁) ∈ ℂ)
80	11, 79	mulcomd 11334	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2 · (2↑𝑁)) = ((2↑𝑁) · 2))
81	11, 13, 15	expp1zd 14302	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2))
82	80, 81	eqtr4d 2798	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (2 · (2↑𝑁)) = (2↑(𝑁 + 1)))
83	82	oveq2d 7437	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (𝐴 / (2 · (2↑𝑁))) = (𝐴 / (2↑(𝑁 + 1))))
84	77, 83	eqtrd 2795	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → ((𝐴 / 2) / (2↑𝑁)) = (𝐴 / (2↑(𝑁 + 1))))
85	84	eqcomd 2766	. . . . 5 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (𝐴 / (2↑(𝑁 + 1))) = ((𝐴 / 2) / (2↑𝑁)))
86	85	fveq2d 6890	. . . 4 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) = (⌊‘((𝐴 / 2) / (2↑𝑁))))
87	75, 86	breqtrrd 5132	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘(𝐴 / (2↑(𝑁 + 1)))))
88		zgtp1leeq 49727	. . . 4 ⊢ (((⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∈ ℤ ∧ (⌊‘(𝐴 / (2↑(𝑁 + 1)))) ∈ ℤ) → ((((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) < (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∧ (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘(𝐴 / (2↑(𝑁 + 1))))) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(𝐴 / (2↑(𝑁 + 1))))))
89	88	imp 412	. . 3 ⊢ ((((⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∈ ℤ ∧ (⌊‘(𝐴 / (2↑(𝑁 + 1)))) ∈ ℤ) ∧ (((⌊‘(𝐴 / (2↑(𝑁 + 1)))) − 1) < (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ∧ (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) ≤ (⌊‘(𝐴 / (2↑(𝑁 + 1)))))) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(𝐴 / (2↑(𝑁 + 1)))))
90	18, 29, 64, 87, 89	syl22anc 852	. 2 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))) = (⌊‘(𝐴 / (2↑(𝑁 + 1)))))
91	90	eqcomd 2766	1 ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) = (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 class class class wbr 5102 ‘cfv 6539 (class class class)co 7421 ℂcc 11202 ℝcr 11203 0cc0 11204 1c1 11205 + caddc 11207 · cmul 11209 < clt 11347 ≤ cle 11348 − cmin 11545 / cdiv 11977 ℕcn 12339 2c2 12401 ℕ₀cn0 12610 ℤcz 12697 ℝ⁺crp 13124 ⌊cfl 13934 ↑cexp 14208

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-er 8721 df-en 8978 df-dom 8979 df-sdom 8980 df-sup 9438 df-inf 9439 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-n0 12611 df-z 12698 df-uz 12970 df-rp 13125 df-fz 13644 df-fzo 13793 df-fl 13936 df-mod 14014 df-seq 14149 df-exp 14209

This theorem is used by: dignn0flhalf 49824

W3C validator