Theorem dignn0flhalflem2

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

	Ref	Expression
Assertion	dignn0flhalflem2	|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN0 ) -> ( |_ ` ( A / ( 2 ^ ( N + 1 ) ) ) ) = ( |_ ` ( ( |_ ` ( A / 2 ) ) / ( 2 ^ N ) ) ) )

Proof

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