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	syl5ib	\|- ( ( 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		zexpcl	\|- ( ( 2 e. ZZ /\ ( N - 1 ) e. NN0 ) -> ( 2 ^ ( N - 1 ) ) e. ZZ )
51	48 49 50	syl2anc	\|- ( N e. NN -> ( 2 ^ ( N - 1 ) ) e. ZZ )
52	51	adantl	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ ( N - 1 ) ) e. ZZ )
53	52	adantr	\|- ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / ( 2 ^ N ) ) e. ZZ ) -> ( 2 ^ ( N - 1 ) ) e. ZZ )
54		simpr	\|- ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / ( 2 ^ N ) ) e. ZZ ) -> ( A / ( 2 ^ N ) ) e. ZZ )
55	53 54	zmulcld	\|- ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / ( 2 ^ N ) ) e. ZZ ) -> ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) e. ZZ )
56	55	ex	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A / ( 2 ^ N ) ) e. ZZ -> ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) e. ZZ ) )
57	5	adantl	\|- ( ( A e. ZZ /\ N e. NN ) -> N e. ZZ )
58	57	zcnd	\|- ( ( A e. ZZ /\ N e. NN ) -> N e. CC )
59	39	negcld	\|- ( ( A e. ZZ /\ N e. NN ) -> -u 1 e. CC )
60	58 39	negsubd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( N + -u 1 ) = ( N - 1 ) )
61	60	eqcomd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( N - 1 ) = ( N + -u 1 ) )
62	58 59 61	mvrladdd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( N - 1 ) - N ) = -u 1 )
63	62	oveq2d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ ( ( N - 1 ) - N ) ) = ( 2 ^ -u 1 ) )
64		2cnd	\|- ( ( A e. ZZ /\ N e. NN ) -> 2 e. CC )
65		2ne0	\|- 2 =/= 0
66	65	a1i	\|- ( ( A e. ZZ /\ N e. NN ) -> 2 =/= 0 )
67		1zzd	\|- ( N e. NN -> 1 e. ZZ )
68	5 67	zsubcld	\|- ( N e. NN -> ( N - 1 ) e. ZZ )
69	68 5	jca	\|- ( N e. NN -> ( ( N - 1 ) e. ZZ /\ N e. ZZ ) )
70	69	adantl	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( N - 1 ) e. ZZ /\ N e. ZZ ) )
71		expsub	\|- ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( N - 1 ) e. ZZ /\ N e. ZZ ) ) -> ( 2 ^ ( ( N - 1 ) - N ) ) = ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) )
72	64 66 70 71	syl21anc	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ ( ( N - 1 ) - N ) ) = ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) )
73		expn1	\|- ( 2 e. CC -> ( 2 ^ -u 1 ) = ( 1 / 2 ) )
74	64 73	syl	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ -u 1 ) = ( 1 / 2 ) )
75	63 72 74	3eqtr3d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) = ( 1 / 2 ) )
76	75	oveq2d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( A x. ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) ) = ( A x. ( 1 / 2 ) ) )
77		2cnd	\|- ( N e. NN -> 2 e. CC )
78	77 49	expcld	\|- ( N e. NN -> ( 2 ^ ( N - 1 ) ) e. CC )
79	78	adantl	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ ( N - 1 ) ) e. CC )
80	3	a1i	\|- ( ( A e. ZZ /\ N e. NN ) -> 2 e. RR+ )
81	80 57	rpexpcld	\|- ( ( A e. ZZ /\ N e. NN ) -> ( 2 ^ N ) e. RR+ )
82	81	rpcnne0d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( 2 ^ N ) e. CC /\ ( 2 ^ N ) =/= 0 ) )
83		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 ) ) ) )
84	79 38 82 83	syl3anc	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) = ( A x. ( ( 2 ^ ( N - 1 ) ) / ( 2 ^ N ) ) ) )
85	38 64 66	divrecd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( A / 2 ) = ( A x. ( 1 / 2 ) ) )
86	76 84 85	3eqtr4d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) = ( A / 2 ) )
87	86	eleq1d	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( 2 ^ ( N - 1 ) ) x. ( A / ( 2 ^ N ) ) ) e. ZZ <-> ( A / 2 ) e. ZZ ) )
88	56 87	sylibd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A / ( 2 ^ N ) ) e. ZZ -> ( A / 2 ) e. ZZ ) )
89	47 88	sylbid	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) = 0 -> ( A / 2 ) e. ZZ ) )
90		zeo2	\|- ( A e. ZZ -> ( ( A / 2 ) e. ZZ <-> -. ( ( A + 1 ) / 2 ) e. ZZ ) )
91	90	adantr	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A / 2 ) e. ZZ <-> -. ( ( A + 1 ) / 2 ) e. ZZ ) )
92	89 91	sylibd	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) = 0 -> -. ( ( A + 1 ) / 2 ) e. ZZ ) )
93	92	necon2ad	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( A + 1 ) / 2 ) e. ZZ -> ( A mod ( 2 ^ N ) ) =/= 0 ) )
94	30 45 93	3syld	\|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( A - 1 ) / 2 ) e. NN -> ( A mod ( 2 ^ N ) ) =/= 0 ) )
95	94	ex	\|- ( A e. ZZ -> ( N e. NN -> ( ( ( A - 1 ) / 2 ) e. NN -> ( A mod ( 2 ^ N ) ) =/= 0 ) ) )
96	95	com23	\|- ( A e. ZZ -> ( ( ( A - 1 ) / 2 ) e. NN -> ( N e. NN -> ( A mod ( 2 ^ N ) ) =/= 0 ) ) )
97	96	3imp	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( A mod ( 2 ^ N ) ) =/= 0 )
98	97	neneqd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> -. ( A mod ( 2 ^ N ) ) = 0 )
99	98	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 )
100	28 99	eqtrd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( ( A - 1 ) mod ( 2 ^ N ) ) - ( A mod ( 2 ^ N ) ) ) = -u 1 )
101		neg1lt0	\|- -u 1 < 0
102		2re	\|- 2 e. RR
103		1lt2	\|- 1 < 2
104		expgt1	\|- ( ( 2 e. RR /\ N e. NN /\ 1 < 2 ) -> 1 < ( 2 ^ N ) )
105	102 103 104	mp3an13	\|- ( N e. NN -> 1 < ( 2 ^ N ) )
106		1red	\|- ( N e. NN -> 1 e. RR )
107	106 7	posdifd	\|- ( N e. NN -> ( 1 < ( 2 ^ N ) <-> 0 < ( ( 2 ^ N ) - 1 ) ) )
108	105 107	mpbid	\|- ( N e. NN -> 0 < ( ( 2 ^ N ) - 1 ) )
109	106	renegcld	\|- ( N e. NN -> -u 1 e. RR )
110		0red	\|- ( N e. NN -> 0 e. RR )
111	7 106	resubcld	\|- ( N e. NN -> ( ( 2 ^ N ) - 1 ) e. RR )
112		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 ) ) )
113	109 110 111 112	syl3anc	\|- ( N e. NN -> ( ( -u 1 < 0 /\ 0 < ( ( 2 ^ N ) - 1 ) ) -> -u 1 < ( ( 2 ^ N ) - 1 ) ) )
114	108 113	mpan2d	\|- ( N e. NN -> ( -u 1 < 0 -> -u 1 < ( ( 2 ^ N ) - 1 ) ) )
115	101 114	mpi	\|- ( N e. NN -> -u 1 < ( ( 2 ^ N ) - 1 ) )
116	115	3ad2ant3	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> -u 1 < ( ( 2 ^ N ) - 1 ) )
117	100 116	eqbrtrd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( ( A - 1 ) mod ( 2 ^ N ) ) - ( A mod ( 2 ^ N ) ) ) < ( ( 2 ^ N ) - 1 ) )
118	2 10	modcld	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( A mod ( 2 ^ N ) ) e. RR )
119		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 ) ) ) ) )
120	18 8 118 16 119	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 ) ) ) ) )
121	117 120	mpbid	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 1 + ( ( A - 1 ) mod ( 2 ^ N ) ) ) < ( ( 2 ^ N ) + ( A mod ( 2 ^ N ) ) ) )
122		modid0	\|- ( ( 2 ^ N ) e. RR+ -> ( ( 2 ^ N ) mod ( 2 ^ N ) ) = 0 )
123	10 122	syl	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( 2 ^ N ) mod ( 2 ^ N ) ) = 0 )
124	123	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 ) )
125	118	recnd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( A mod ( 2 ^ N ) ) e. CC )
126	125	subid1d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) - 0 ) = ( A mod ( 2 ^ N ) ) )
127	124 126	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 ) ) )
128	127	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 ) ) )
129		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 ) ) )
130	2 8 10 129	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 ) ) )
131		modabs2	\|- ( ( A e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( ( A mod ( 2 ^ N ) ) mod ( 2 ^ N ) ) = ( A mod ( 2 ^ N ) ) )
132	2 10 131	syl2anc	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A mod ( 2 ^ N ) ) mod ( 2 ^ N ) ) = ( A mod ( 2 ^ N ) ) )
133	128 130 132	3eqtr3d	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) = ( A mod ( 2 ^ N ) ) )
134	133	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 ) ) ) )
135	121 134	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 ) ) ) )
136	19 20 2 135	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 ) ) ) ) )
137	31	3ad2ant1	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> A e. CC )
138	8	recnd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 2 ^ N ) e. CC )
139	11	recnd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - ( 2 ^ N ) ) mod ( 2 ^ N ) ) e. CC )
140	137 138 139	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 ) ) ) ) )
141		1cnd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> 1 e. CC )
142	16	recnd	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( ( A - 1 ) mod ( 2 ^ N ) ) e. CC )
143	137 141 142	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 ) ) ) ) )
144	136 140 143	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 ) ) ) )
145	12 17 10 144	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 ) ) )
146	7	recnd	\|- ( N e. NN -> ( 2 ^ N ) e. CC )
147	146	3ad2ant3	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 2 ^ N ) e. CC )
148	65	a1i	\|- ( N e. NN -> 2 =/= 0 )
149	77 148 5	expne0d	\|- ( N e. NN -> ( 2 ^ N ) =/= 0 )
150	149	3ad2ant3	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( 2 ^ N ) =/= 0 )
151		divsub1dir	\|- ( ( A e. CC /\ ( 2 ^ N ) e. CC /\ ( 2 ^ N ) =/= 0 ) -> ( ( A / ( 2 ^ N ) ) - 1 ) = ( ( A - ( 2 ^ N ) ) / ( 2 ^ N ) ) )
152	151	fveq2d	\|- ( ( A e. CC /\ ( 2 ^ N ) e. CC /\ ( 2 ^ N ) =/= 0 ) -> ( \|_ ` ( ( A / ( 2 ^ N ) ) - 1 ) ) = ( \|_ ` ( ( A - ( 2 ^ N ) ) / ( 2 ^ N ) ) ) )
153	137 147 150 152	syl3anc	\|- ( ( A e. ZZ /\ ( ( A - 1 ) / 2 ) e. NN /\ N e. NN ) -> ( \|_ ` ( ( A / ( 2 ^ N ) ) - 1 ) ) = ( \|_ ` ( ( A - ( 2 ^ N ) ) / ( 2 ^ N ) ) ) )
154		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 ) ) )
155	9 10 154	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 ) ) )
156	153 155	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 ) ) )
157		fldivmod	\|- ( ( ( A - 1 ) e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( \|_ ` ( ( A - 1 ) / ( 2 ^ N ) ) ) = ( ( ( A - 1 ) - ( ( A - 1 ) mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) )
158	15 10 157	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 ) ) )
159	145 156 158	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