dyaddisjlem

		Ref	Expression
	Hypothesis	dyadmbl.1	\|- F = ( x e. ZZ , y e. NN0 \|-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
	Assertion	dyaddisjlem	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	\|- F = ( x e. ZZ , y e. NN0 \|-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2		simplll	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> A e. ZZ )
3		simplrl	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> C e. NN0 )
4	1	dyadval	\|- ( ( A e. ZZ /\ C e. NN0 ) -> ( A F C ) = <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
5	2 3 4	syl2anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A F C ) = <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
6	5	fveq2d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( A F C ) ) = ( (,) ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. ) )
7		df-ov	\|- ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) = ( (,) ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
8	6 7	eqtr4di	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( A F C ) ) = ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) )
9		simpllr	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> B e. ZZ )
10		simplrr	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> D e. NN0 )
11	1	dyadval	\|- ( ( B e. ZZ /\ D e. NN0 ) -> ( B F D ) = <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
12	9 10 11	syl2anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B F D ) = <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
13	12	fveq2d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( B F D ) ) = ( (,) ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. ) )
14		df-ov	\|- ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) = ( (,) ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
15	13 14	eqtr4di	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( B F D ) ) = ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) )
16	8 15	ineq12d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) )
17		incom	\|- ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) )
18	16 17	eqtrdi	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) )
19	18	adantr	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) )
20	2	zred	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> A e. RR )
21	20	recnd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> A e. CC )
22		2nn	\|- 2 e. NN
23		nnexpcl	\|- ( ( 2 e. NN /\ C e. NN0 ) -> ( 2 ^ C ) e. NN )
24	22 3 23	sylancr	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ C ) e. NN )
25	24	nncnd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ C ) e. CC )
26		nnexpcl	\|- ( ( 2 e. NN /\ D e. NN0 ) -> ( 2 ^ D ) e. NN )
27	22 10 26	sylancr	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ D ) e. NN )
28	27	nncnd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ D ) e. CC )
29	24	nnne0d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ C ) =/= 0 )
30	21 25 28 29	div13d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) = ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. A ) )
31		2cnd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> 2 e. CC )
32		2ne0	\|- 2 =/= 0
33	32	a1i	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> 2 =/= 0 )
34	3	nn0zd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> C e. ZZ )
35	10	nn0zd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> D e. ZZ )
36	31 33 34 35	expsubd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ ( D - C ) ) = ( ( 2 ^ D ) / ( 2 ^ C ) ) )
37		2z	\|- 2 e. ZZ
38		simpr	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> C <_ D )
39		znn0sub	\|- ( ( C e. ZZ /\ D e. ZZ ) -> ( C <_ D <-> ( D - C ) e. NN0 ) )
40	34 35 39	syl2anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( C <_ D <-> ( D - C ) e. NN0 ) )
41	38 40	mpbid	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( D - C ) e. NN0 )
42		zexpcl	\|- ( ( 2 e. ZZ /\ ( D - C ) e. NN0 ) -> ( 2 ^ ( D - C ) ) e. ZZ )
43	37 41 42	sylancr	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ ( D - C ) ) e. ZZ )
44	36 43	eqeltrrd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( 2 ^ D ) / ( 2 ^ C ) ) e. ZZ )
45	44 2	zmulcld	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. A ) e. ZZ )
46	30 45	eqeltrd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ )
47		zltp1le	\|- ( ( B e. ZZ /\ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ ) -> ( B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
48	9 46 47	syl2anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
49	9	zred	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> B e. RR )
50	20 24	nndivred	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A / ( 2 ^ C ) ) e. RR )
51	27	nnred	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ D ) e. RR )
52	27	nngt0d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> 0 < ( 2 ^ D ) )
53		ltdivmul2	\|- ( ( B e. RR /\ ( A / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) <-> B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
54	49 50 51 52 53	syl112anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) <-> B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
55		peano2re	\|- ( B e. RR -> ( B + 1 ) e. RR )
56	49 55	syl	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B + 1 ) e. RR )
57		ledivmul2	\|- ( ( ( B + 1 ) e. RR /\ ( A / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
58	56 50 51 52 57	syl112anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
59	48 54 58	3bitr4d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) <-> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) ) )
60	49 27	nndivred	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B / ( 2 ^ D ) ) e. RR )
61	60	rexrd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B / ( 2 ^ D ) ) e. RR* )
62	56 27	nndivred	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B + 1 ) / ( 2 ^ D ) ) e. RR )
63	62	rexrd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* )
64	50	rexrd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A / ( 2 ^ C ) ) e. RR* )
65		peano2re	\|- ( A e. RR -> ( A + 1 ) e. RR )
66	20 65	syl	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A + 1 ) e. RR )
67	66 24	nndivred	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR )
68	67	rexrd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* )
69		ioodisj	\|- ( ( ( ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) /\ ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) ) /\ ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) )
70	69	ex	\|- ( ( ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) /\ ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) ) )
71	61 63 64 68 70	syl22anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) ) )
72	59 71	sylbid	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) ) )
73	72	imp	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) )
74	19 73	eqtrd	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) )
75	74	3mix3d	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
76	50	adantr	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( A / ( 2 ^ C ) ) e. RR )
77	67	adantr	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR )
78		simprl	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) )
79	66	recnd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A + 1 ) e. CC )
80	79 25 28 29	div13d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) = ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. ( A + 1 ) ) )
81	2	peano2zd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A + 1 ) e. ZZ )
82	44 81	zmulcld	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. ( A + 1 ) ) e. ZZ )
83	80 82	eqeltrd	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ )
84		zltp1le	\|- ( ( B e. ZZ /\ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ ) -> ( B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
85	9 83 84	syl2anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
86		ltdivmul2	\|- ( ( B e. RR /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) <-> B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
87	49 67 51 52 86	syl112anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) <-> B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
88		ledivmul2	\|- ( ( ( B + 1 ) e. RR /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
89	56 67 51 52 88	syl112anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
90	85 87 89	3bitr4d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) <-> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) ) )
91	90	biimpa	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) -> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) )
92	91	adantrl	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) )
93		iccss	\|- ( ( ( ( A / ( 2 ^ C ) ) e. RR /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) C_ ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
94	76 77 78 92 93	syl22anc	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) C_ ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
95	12	fveq2d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( B F D ) ) = ( [,] ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. ) )
96		df-ov	\|- ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) = ( [,] ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
97	95 96	eqtr4di	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( B F D ) ) = ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) )
98	97	adantr	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( [,] ` ( B F D ) ) = ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) )
99	5	fveq2d	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( A F C ) ) = ( [,] ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. ) )
100		df-ov	\|- ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) = ( [,] ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
101	99 100	eqtr4di	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( A F C ) ) = ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
102	101	adantr	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( [,] ` ( A F C ) ) = ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
103	94 98 102	3sstr4d	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) )
104	103	3mix2d	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
105	104	anassrs	\|- ( ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
106	16	adantr	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) )
107		ioodisj	\|- ( ( ( ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) /\ ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) )
108	107	ex	\|- ( ( ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) /\ ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) ) )
109	64 68 61 63 108	syl22anc	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) ) )
110	109	imp	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) )
111	106 110	eqtrd	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) )
112	111	3mix3d	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
113	112	adantlr	\|- ( ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
114	60	adantr	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( B / ( 2 ^ D ) ) e. RR )
115	67	adantr	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR )
116	105 113 114 115	ltlecasei	\|- ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
117	75 116 60 50	ltlecasei	\|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )

Metamath Proof Explorer

Theorem dyaddisjlem

Proof