dyaddisjlem

		Ref	Expression
	Hypothesis	dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
	Assertion	dyaddisjlem	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \land C \leq D) \to ([.] (A F C) \subseteq [.] (B F D) \lor [.] (B F D) \subseteq [.] (A F C) \lor (.) (A F C) \cap (.) (B F D) = \emptyset)$

Proof

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

Metamath Proof Explorer

Theorem dyaddisjlem

Proof