dignn0flhalflem1

		Ref	Expression
	Assertion	dignn0flhalflem1	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( \|_ ` ( ( A / ( 2 ^ N ) ) - 1 ) ) < ( \|_ ` ( ( A - 1 ) / ( 2 ^ N ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		zre	\|- ( A e. ZZ -> A e. RR )
2	1	3ad2ant1	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> A e. RR )
3		2rp	\|- 2 e. RR+
4	3	a1i	\|- ( N e. NN -> 2 e. RR+ )
5		nnz	\|- ( N e. NN -> N e. ZZ )
6	4 5	rpexpcld	\|- ( N e. NN -> ( 2 ^ N ) e. RR+ )
7	6	rpred	\|- ( N e. NN -> ( 2 ^ N ) e. RR )
8	7	3ad2ant3	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 2 ^ N ) e. RR )
9	2 8	resubcld	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( A - ( 2 ^ N ) ) e. RR )
10	6	3ad2ant3	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 2 ^ N ) e. RR+ )
11	9 10	modcld	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) e. RR )
12	9 11	resubcld	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - ( 2 ^ N ) ) - ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) e. RR )
13		peano2zm	\|- ( A e. ZZ -> ( A - 1 ) e. ZZ )
14	13	zred	\|- ( A e. ZZ -> ( A - 1 ) e. RR )
15	14	3ad2ant1	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( A - 1 ) e. RR )
16	15 10	modcld	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - 1 ) mod ( 2 ^ N ) ) e. RR )
17	15 16	resubcld	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - 1 ) - ( ( A - 1 ) mod ( 2 ^ N ) ) ) e. RR )
18		1red	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> 1 e. RR )
19	18 16	readdcld	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 1 + ( ( A - 1 ) mod ( 2 ^ N ) ) ) e. RR )
20	8 11	readdcld	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( 2 ^ N ) + ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) e. RR )
21		2nn	\|- 2 e. NN
22	21	a1i	\|- ( N e. NN -> 2 e. NN )
23		nnnn0	\|- ( N e. NN -> N e. NN0 )
24	22 23	nnexpcld	\|- ( N e. NN -> ( 2 ^ N ) e. NN )
25	24	anim2i	\|- ( ( A e. ZZ /\ N e. NN ) -> ( A e. ZZ /\ ( 2 ^ N ) e. NN ) )
26	25	3adant2	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( A e. ZZ /\ ( 2 ^ N ) e. NN ) )
27		m1modmmod	\|- ( ( A e. ZZ /\ ( 2 ^ N ) e. NN ) -> ( ( ( A - 1 ) mod ( 2 ^ N ) ) - ( A mod ( 2 ^ N ) ) ) = if ( ( A mod ( 2 ^ N ) ) = 0 , ( ( 2 ^ N ) - 1 ) , -u 1 ) )
28	26 27	syl	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( ( A - 1 ) mod ( 2 ^ N ) ) - ( A mod ( 2 ^ N ) ) ) = if ( ( A mod ( 2 ^ N ) ) = 0 , ( ( 2 ^ N ) - 1 ) , -u 1 ) )
29		nnz	\|- ( ( ( A - 1 ) / 2 ) e. NN -> ( ( A - 1 ) / 2 ) e. ZZ )
30	29	a1i	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( A - 1 ) / 2 ) e. NN -> ( ( A - 1 ) / 2 ) e. ZZ ) )
31		zcn	\|- ( A e. ZZ -> A e. CC )
32		xp1d2m1eqxm1d2	\|- ( A e. CC -> ( ( ( A + 1 ) / 2 ) - 1 ) = ( ( A - 1 ) / 2 ) )
33	32	eqcomd	\|- ( A e. CC -> ( ( A - 1 ) / 2 ) = ( ( ( A + 1 ) / 2 ) - 1 ) )
34	31 33	syl	\|- ( A e. ZZ -> ( ( A - 1 ) / 2 ) = ( ( ( A + 1 ) / 2 ) - 1 ) )
35	34	adantr	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A - 1 ) / 2 ) = ( ( ( A + 1 ) / 2 ) - 1 ) )
36	35	eleq1d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( A - 1 ) / 2 ) e. ZZ <-> ( ( ( A + 1 ) / 2 ) - 1 ) e. ZZ ) )
37		peano2z	\|- ( ( ( ( A + 1 ) / 2 ) - 1 ) e. ZZ -> ( ( ( ( A + 1 ) / 2 ) - 1 ) + 1 ) e. ZZ )
38	31	adantr	\|- ( ( A e. ZZ /\ N e. NN ) -> A e. CC )
39		1cnd	\|- ( ( A e. ZZ /\ N e. NN ) -> 1 e. CC )
40	38 39	addcld	\|- ( ( A e. ZZ /\ N e. NN ) -> ( A + 1 ) e. CC )
41	40	halfcld	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A + 1 ) / 2 ) e. CC )
42	41 39	npcand	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( ( A + 1 ) / 2 ) - 1 ) + 1 ) = ( ( A + 1 ) / 2 ) )
43	42	eleq1d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( ( ( A + 1 ) / 2 ) - 1 ) + 1 ) e. ZZ <-> ( ( A + 1 ) / 2 ) e. ZZ ) )
44	37 43	imbitrid	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( ( A + 1 ) / 2 ) - 1 ) e. ZZ -> ( ( A + 1 ) / 2 ) e. ZZ ) )
45	36 44	sylbid	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( A - 1 ) / 2 ) e. ZZ -> ( ( A + 1 ) / 2 ) e. ZZ ) )
46		mod0	\|- ( ( A e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( ( A mod ( 2 ^ N ) ) = 0 <-> ( A / ( 2 ^ N ) ) e. ZZ ) )
47	1 6 46	syl2an	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) = 0 <-> ( A / ( 2 ^ N ) ) e. ZZ ) )
48	22	nnzd	\|- ( N e. NN -> 2 e. ZZ )
49		nnm1nn0	\|- ( N e. NN -> ( N - 1 ) e. NN0 )
50	48 49	zexpcld	\|- ( N e. NN -> ( 2 ^ ( N - 1 ) ) e. ZZ )
51	50	adantl	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ ( N - 1 ) ) e. ZZ )
52	51	adantr	\|- ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / ( 2 ^ N ) ) e. ZZ ) -> ( 2 ^ ( N - 1 ) ) e. ZZ )
53		simpr	\|- ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / ( 2 ^ N ) ) e. ZZ ) -> ( A / ( 2 ^ N ) ) e. ZZ )
54	52 53	zmulcld	\|- ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / ( 2 ^ N ) ) e. ZZ ) -> ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) e. ZZ )
55	54	ex	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A / ( 2 ^ N ) ) e. ZZ -> ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) e. ZZ ) )
56	5	adantl	\|- ( ( A e. ZZ /\ N e. NN ) -> N e. ZZ )
57	56	zcnd	\|- ( ( A e. ZZ /\ N e. NN ) -> N e. CC )
58	39	negcld	\|- ( ( A e. ZZ /\ N e. NN ) -> -u 1 e. CC )
59	57 39	negsubd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( N + -u 1 ) = ( N - 1 ) )
60	57 58 59	mvlladdcd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( N - 1 ) - N ) = -u 1 )
61	60	oveq2d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ ( ( N - 1 ) - N ) ) = ( 2 ^ -u 1 ) )
62		2cnd	\|- ( ( A e. ZZ /\ N e. NN ) -> 2 e. CC )
63		2ne0	\|- 2 =/= 0
64	63	a1i	\|- ( ( A e. ZZ /\ N e. NN ) -> 2 =/= 0 )
65		1zzd	\|- ( N e. NN -> 1 e. ZZ )
66	5 65	zsubcld	\|- ( N e. NN -> ( N - 1 ) e. ZZ )
67	66 5	jca	\|- ( N e. NN -> ( ( N - 1 ) e. ZZ /\ N e. ZZ ) )
68	67	adantl	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( N - 1 ) e. ZZ /\ N e. ZZ ) )
69		expsub	\|- ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( N - 1 ) e. ZZ /\ N e. ZZ ) ) -> ( 2 ^ ( ( N - 1 ) - N ) ) = ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) )
70	62 64 68 69	syl21anc	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ ( ( N - 1 ) - N ) ) = ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) )
71		expn1	\|- ( 2 e. CC -> ( 2 ^ -u 1 ) = ( 1 / 2 ) )
72	62 71	syl	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ -u 1 ) = ( 1 / 2 ) )
73	61 70 72	3eqtr3d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) = ( 1 / 2 ) )
74	73	oveq2d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( A x. ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) ) = ( A x. ( 1 / 2 ) ) )
75		2cnd	\|- ( N e. NN -> 2 e. CC )
76	75 49	expcld	\|- ( N e. NN -> ( 2 ^ ( N - 1 ) ) e. CC )
77	76	adantl	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ ( N - 1 ) ) e. CC )
78	3	a1i	\|- ( ( A e. ZZ /\ N e. NN ) -> 2 e. RR+ )
79	78 56	rpexpcld	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ N ) e. RR+ )
80	79	rpcnne0d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( 2 ^ N ) e. CC /\ ( 2 ^ N ) =/= 0 ) )
81		div12	\|- ( ( ( 2 ^ ( N - 1 ) ) e. CC /\ A e. CC /\ ( ( 2 ^ N ) e. CC /\ ( 2 ^ N ) =/= 0 ) ) -> ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) = ( A x. ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) ) )
82	77 38 80 81	syl3anc	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) = ( A x. ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) ) )
83	38 62 64	divrecd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( A / 2 ) = ( A x. ( 1 / 2 ) ) )
84	74 82 83	3eqtr4d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) = ( A / 2 ) )
85	84	eleq1d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) e. ZZ <-> ( A / 2 ) e. ZZ ) )
86	55 85	sylibd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A / ( 2 ^ N ) ) e. ZZ -> ( A / 2 ) e. ZZ ) )
87	47 86	sylbid	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) = 0 -> ( A / 2 ) e. ZZ ) )
88		zeo2	\|- ( A e. ZZ -> ( ( A / 2 ) e. ZZ <-> -. ( ( A + 1 ) / 2 ) e. ZZ ) )
89	88	adantr	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A / 2 ) e. ZZ <-> -. ( ( A + 1 ) / 2 ) e. ZZ ) )
90	87 89	sylibd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) = 0 -> -. ( ( A + 1 ) / 2 ) e. ZZ ) )
91	90	necon2ad	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( A + 1 ) / 2 ) e. ZZ -> ( A mod ( 2 ^ N ) ) =/= 0 ) )
92	30 45 91	3syld	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( A - 1 ) / 2 ) e. NN -> ( A mod ( 2 ^ N ) ) =/= 0 ) )
93	92	ex	\|- ( A e. ZZ -> ( N e. NN -> ( ( ( A - 1 ) / 2 ) e. NN -> ( A mod ( 2 ^ N ) ) =/= 0 ) ) )
94	93	com23	\|- ( A e. ZZ -> ( ( ( A - 1 ) / 2 ) e. NN -> ( N e. NN -> ( A mod ( 2 ^ N ) ) =/= 0 ) ) )
95	94	3imp	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( A mod ( 2 ^ N ) ) =/= 0 )
96	95	neneqd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> -. ( A mod ( 2 ^ N ) ) = 0 )
97	96	iffalsed	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> if ( ( A mod ( 2 ^ N ) ) = 0 , ( ( 2 ^ N ) - 1 ) , -u 1 ) = -u 1 )
98	28 97	eqtrd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( ( A - 1 ) mod ( 2 ^ N ) ) - ( A mod ( 2 ^ N ) ) ) = -u 1 )
99		neg1lt0	\|- -u 1 < 0
100		2re	\|- 2 e. RR
101		1lt2	\|- 1 < 2
102		expgt1	\|- ( ( 2 e. RR /\ N e. NN /\ 1 < 2 ) -> 1 < ( 2 ^ N ) )
103	100 101 102	mp3an13	\|- ( N e. NN -> 1 < ( 2 ^ N ) )
104		1red	\|- ( N e. NN -> 1 e. RR )
105	104 7	posdifd	\|- ( N e. NN -> ( 1 < ( 2 ^ N ) <-> 0 < ( ( 2 ^ N ) - 1 ) ) )
106	103 105	mpbid	\|- ( N e. NN -> 0 < ( ( 2 ^ N ) - 1 ) )
107	104	renegcld	\|- ( N e. NN -> -u 1 e. RR )
108		0red	\|- ( N e. NN -> 0 e. RR )
109	7 104	resubcld	\|- ( N e. NN -> ( ( 2 ^ N ) - 1 ) e. RR )
110		lttr	\|- ( ( -u 1 e. RR /\ 0 e. RR /\ ( ( 2 ^ N ) - 1 ) e. RR ) -> ( ( -u 1 < 0 /\ 0 < ( ( 2 ^ N ) - 1 ) ) -> -u 1 < ( ( 2 ^ N ) - 1 ) ) )
111	107 108 109 110	syl3anc	\|- ( N e. NN -> ( ( -u 1 < 0 /\ 0 < ( ( 2 ^ N ) - 1 ) ) -> -u 1 < ( ( 2 ^ N ) - 1 ) ) )
112	106 111	mpan2d	\|- ( N e. NN -> ( -u 1 < 0 -> -u 1 < ( ( 2 ^ N ) - 1 ) ) )
113	99 112	mpi	\|- ( N e. NN -> -u 1 < ( ( 2 ^ N ) - 1 ) )
114	113	3ad2ant3	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> -u 1 < ( ( 2 ^ N ) - 1 ) )
115	98 114	eqbrtrd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( ( A - 1 ) mod ( 2 ^ N ) ) - ( A mod ( 2 ^ N ) ) ) < ( ( 2 ^ N ) - 1 ) )
116	2 10	modcld	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( A mod ( 2 ^ N ) ) e. RR )
117		ltsubadd2b	\|- ( ( ( 1 e. RR /\ ( 2 ^ N ) e. RR ) /\ ( ( A mod ( 2 ^ N ) ) e. RR /\ ( ( A - 1 ) mod ( 2 ^ N ) ) e. RR ) ) -> ( ( ( ( A - 1 ) mod ( 2 ^ N ) ) - ( A mod ( 2 ^ N ) ) ) < ( ( 2 ^ N ) - 1 ) <-> ( 1 + ( ( A - 1 ) mod ( 2 ^ N ) ) ) < ( ( 2 ^ N ) + ( A mod ( 2 ^ N ) ) ) ) )
118	18 8 116 16 117	syl22anc	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( ( ( A - 1 ) mod ( 2 ^ N ) ) - ( A mod ( 2 ^ N ) ) ) < ( ( 2 ^ N ) - 1 ) <-> ( 1 + ( ( A - 1 ) mod ( 2 ^ N ) ) ) < ( ( 2 ^ N ) + ( A mod ( 2 ^ N ) ) ) ) )
119	115 118	mpbid	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 1 + ( ( A - 1 ) mod ( 2 ^ N ) ) ) < ( ( 2 ^ N ) + ( A mod ( 2 ^ N ) ) ) )
120		modid0	\|- ( ( 2 ^ N ) e. RR+ -> ( ( 2 ^ N ) mod ( 2 ^ N ) ) = 0 )
121	10 120	syl	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( 2 ^ N ) mod ( 2 ^ N ) ) = 0 )
122	121	oveq2d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) - ( ( 2 ^ N ) mod ( 2 ^ N ) ) ) = ( ( A mod ( 2 ^ N ) ) - 0 ) )
123	116	recnd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( A mod ( 2 ^ N ) ) e. CC )
124	123	subid1d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) - 0 ) = ( A mod ( 2 ^ N ) ) )
125	122 124	eqtrd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) - ( ( 2 ^ N ) mod ( 2 ^ N ) ) ) = ( A mod ( 2 ^ N ) ) )
126	125	oveq1d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( ( A mod ( 2 ^ N ) ) - ( ( 2 ^ N ) mod ( 2 ^ N ) ) ) mod ( 2 ^ N ) ) = ( ( A mod ( 2 ^ N ) ) mod ( 2 ^ N ) ) )
127		modsubmodmod	\|- ( ( A e. RR /\ ( 2 ^ N ) e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( ( ( A mod ( 2 ^ N ) ) - ( ( 2 ^ N ) mod ( 2 ^ N ) ) ) mod ( 2 ^ N ) ) = ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) )
128	2 8 10 127	syl3anc	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( ( A mod ( 2 ^ N ) ) - ( ( 2 ^ N ) mod ( 2 ^ N ) ) ) mod ( 2 ^ N ) ) = ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) )
129		modabs2	\|- ( ( A e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( ( A mod ( 2 ^ N ) ) mod ( 2 ^ N ) ) = ( A mod ( 2 ^ N ) ) )
130	2 10 129	syl2anc	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) mod ( 2 ^ N ) ) = ( A mod ( 2 ^ N ) ) )
131	126 128 130	3eqtr3d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) = ( A mod ( 2 ^ N ) ) )
132	131	oveq2d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( 2 ^ N ) + ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) = ( ( 2 ^ N ) + ( A mod ( 2 ^ N ) ) ) )
133	119 132	breqtrrd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 1 + ( ( A - 1 ) mod ( 2 ^ N ) ) ) < ( ( 2 ^ N ) + ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) )
134	19 20 2 133	ltsub2dd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( A - ( ( 2 ^ N ) + ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) ) < ( A - ( 1 + ( ( A - 1 ) mod ( 2 ^ N ) ) ) ) )
135	31	3ad2ant1	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> A e. CC )
136	8	recnd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 2 ^ N ) e. CC )
137	11	recnd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) e. CC )
138	135 136 137	subsub4d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - ( 2 ^ N ) ) - ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) = ( A - ( ( 2 ^ N ) + ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) ) )
139		1cnd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> 1 e. CC )
140	16	recnd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - 1 ) mod ( 2 ^ N ) ) e. CC )
141	135 139 140	subsub4d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - 1 ) - ( ( A - 1 ) mod ( 2 ^ N ) ) ) = ( A - ( 1 + ( ( A - 1 ) mod ( 2 ^ N ) ) ) ) )
142	134 138 141	3brtr4d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - ( 2 ^ N ) ) - ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) < ( ( A - 1 ) - ( ( A - 1 ) mod ( 2 ^ N ) ) ) )
143	12 17 10 142	ltdiv1dd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( ( A - ( 2 ^ N ) ) - ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) < ( ( ( A - 1 ) - ( ( A - 1 ) mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
144	7	recnd	\|- ( N e. NN -> ( 2 ^ N ) e. CC )
145	144	3ad2ant3	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 2 ^ N ) e. CC )
146	63	a1i	\|- ( N e. NN -> 2 =/= 0 )
147	75 146 5	expne0d	\|- ( N e. NN -> ( 2 ^ N ) =/= 0 )
148	147	3ad2ant3	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 2 ^ N ) =/= 0 )
149		divsub1dir	\|- ( ( A e. CC /\ ( 2 ^ N ) e. CC /\ ( 2 ^ N ) =/= 0 ) -> ( ( A / ( 2 ^ N ) ) - 1 ) = ( ( A - ( 2 ^ N ) ) / ( 2 ^ N ) ) )
150	149	fveq2d	\|- ( ( A e. CC /\ ( 2 ^ N ) e. CC /\ ( 2 ^ N ) =/= 0 ) -> ( \|_ ` ( ( A / ( 2 ^ N ) ) - 1 ) ) = ( \|_ ` ( ( A - ( 2 ^ N ) ) / ( 2 ^ N ) ) ) )
151	135 145 148 150	syl3anc	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( \|_ ` ( ( A / ( 2 ^ N ) ) - 1 ) ) = ( \|_ ` ( ( A - ( 2 ^ N ) ) / ( 2 ^ N ) ) ) )
152		fldivmod	\|- ( ( ( A - ( 2 ^ N ) ) e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( \|_ ` ( ( A - ( 2 ^ N ) ) / ( 2 ^ N ) ) ) = ( ( ( A - ( 2 ^ N ) ) - ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
153	9 10 152	syl2anc	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( \|_ ` ( ( A - ( 2 ^ N ) ) / ( 2 ^ N ) ) ) = ( ( ( A - ( 2 ^ N ) ) - ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
154	151 153	eqtrd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( \|_ ` ( ( A / ( 2 ^ N ) ) - 1 ) ) = ( ( ( A - ( 2 ^ N ) ) - ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
155		fldivmod	\|- ( ( ( A - 1 ) e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( \|_ ` ( ( A - 1 ) / ( 2 ^ N ) ) ) = ( ( ( A - 1 ) - ( ( A - 1 ) mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
156	15 10 155	syl2anc	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( \|_ ` ( ( A - 1 ) / ( 2 ^ N ) ) ) = ( ( ( A - 1 ) - ( ( A - 1 ) mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
157	143 154 156	3brtr4d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( \|_ ` ( ( A / ( 2 ^ N ) ) - 1 ) ) < ( \|_ ` ( ( A - 1 ) / ( 2 ^ N ) ) ) )

Metamath Proof Explorer

Theorem dignn0flhalflem1

Proof