dyadmaxlem

	Ref	Expression
Hypotheses	dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
	dyadmax.2	$⊢ φ \to A \in ℤ$
	dyadmax.3	$⊢ φ \to B \in ℤ$
	dyadmax.4	$⊢ φ \to C \in ℕ_{0}$
	dyadmax.5	$⊢ φ \to D \in ℕ_{0}$
	dyadmax.6	$⊢ φ \to \neg D < C$
	dyadmax.7	$⊢ φ \to [.] (A F C) \subseteq [.] (B F D)$
Assertion	dyadmaxlem	$⊢ φ \to (A = B \land C = D)$

Proof

Step	Hyp	Ref	Expression
1		dyadmbl.1	$⊢ F = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
2		dyadmax.2	$⊢ φ \to A \in ℤ$
3		dyadmax.3	$⊢ φ \to B \in ℤ$
4		dyadmax.4	$⊢ φ \to C \in ℕ_{0}$
5		dyadmax.5	$⊢ φ \to D \in ℕ_{0}$
6		dyadmax.6	$⊢ φ \to \neg D < C$
7		dyadmax.7	$⊢ φ \to [.] (A F C) \subseteq [.] (B F D)$
8	1	dyadval	$⊢ (A \in ℤ \land C \in ℕ_{0}) \to A F C = ⟨\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}⟩$
9	2 4 8	syl2anc	$⊢ φ \to A F C = ⟨\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}⟩$
10	9	fveq2d	$⊢ φ \to [.] (A F C) = [.] (⟨\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}⟩)$
11		df-ov	$⊢ [\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}] = [.] (⟨\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}⟩)$
12	10 11	eqtr4di	$⊢ φ \to [.] (A F C) = [\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}]$
13	1	dyadss	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℕ_{0} \land D \in ℕ_{0})) \to ([.] (A F C) \subseteq [.] (B F D) \to D \leq C)$
14	2 3 4 5 13	syl22anc	$⊢ φ \to ([.] (A F C) \subseteq [.] (B F D) \to D \leq C)$
15	7 14	mpd	$⊢ φ \to D \leq C$
16	5	nn0red	$⊢ φ \to D \in ℝ$
17	4	nn0red	$⊢ φ \to C \in ℝ$
18	16 17	eqleltd	$⊢ φ \to (D = C \leftrightarrow (D \leq C \land \neg D < C))$
19	15 6 18	mpbir2and	$⊢ φ \to D = C$
20	19	oveq2d	$⊢ φ \to B F D = B F C$
21	1	dyadval	$⊢ (B \in ℤ \land C \in ℕ_{0}) \to B F C = ⟨\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}⟩$
22	3 4 21	syl2anc	$⊢ φ \to B F C = ⟨\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}⟩$
23	20 22	eqtrd	$⊢ φ \to B F D = ⟨\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}⟩$
24	23	fveq2d	$⊢ φ \to [.] (B F D) = [.] (⟨\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}⟩)$
25		df-ov	$⊢ [\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}] = [.] (⟨\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}⟩)$
26	24 25	eqtr4di	$⊢ φ \to [.] (B F D) = [\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}]$
27	7 12 26	3sstr3d	$⊢ φ \to [\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}] \subseteq [\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}]$
28	2	zred	$⊢ φ \to A \in ℝ$
29		2nn	$⊢ 2 \in ℕ$
30		nnexpcl	$⊢ (2 \in ℕ \land C \in ℕ_{0}) \to 2^{C} \in ℕ$
31	29 4 30	sylancr	$⊢ φ \to 2^{C} \in ℕ$
32	28 31	nndivred	$⊢ φ \to \frac{A}{2^{C}} \in ℝ$
33	32	rexrd	$⊢ φ \to \frac{A}{2^{C}} \in ℝ^{*}$
34		peano2re	$⊢ A \in ℝ \to A + 1 \in ℝ$
35	28 34	syl	$⊢ φ \to A + 1 \in ℝ$
36	35 31	nndivred	$⊢ φ \to \frac{A + 1}{2^{C}} \in ℝ$
37	36	rexrd	$⊢ φ \to \frac{A + 1}{2^{C}} \in ℝ^{*}$
38	28	lep1d	$⊢ φ \to A \leq A + 1$
39	31	nnred	$⊢ φ \to 2^{C} \in ℝ$
40	31	nngt0d	$⊢ φ \to 0 < 2^{C}$
41		lediv1	$⊢ (A \in ℝ \land A + 1 \in ℝ \land (2^{C} \in ℝ \land 0 < 2^{C})) \to (A \leq A + 1 \leftrightarrow \frac{A}{2^{C}} \leq \frac{A + 1}{2^{C}})$
42	28 35 39 40 41	syl112anc	$⊢ φ \to (A \leq A + 1 \leftrightarrow \frac{A}{2^{C}} \leq \frac{A + 1}{2^{C}})$
43	38 42	mpbid	$⊢ φ \to \frac{A}{2^{C}} \leq \frac{A + 1}{2^{C}}$
44		ubicc2	$⊢ (\frac{A}{2^{C}} \in ℝ^{} \land \frac{A + 1}{2^{C}} \in ℝ^{} \land \frac{A}{2^{C}} \leq \frac{A + 1}{2^{C}}) \to \frac{A + 1}{2^{C}} \in [\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}]$
45	33 37 43 44	syl3anc	$⊢ φ \to \frac{A + 1}{2^{C}} \in [\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}]$
46	27 45	sseldd	$⊢ φ \to \frac{A + 1}{2^{C}} \in [\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}]$
47	3	zred	$⊢ φ \to B \in ℝ$
48	47 31	nndivred	$⊢ φ \to \frac{B}{2^{C}} \in ℝ$
49		peano2re	$⊢ B \in ℝ \to B + 1 \in ℝ$
50	47 49	syl	$⊢ φ \to B + 1 \in ℝ$
51	50 31	nndivred	$⊢ φ \to \frac{B + 1}{2^{C}} \in ℝ$
52		elicc2	$⊢ (\frac{B}{2^{C}} \in ℝ \land \frac{B + 1}{2^{C}} \in ℝ) \to (\frac{A + 1}{2^{C}} \in [\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}] \leftrightarrow (\frac{A + 1}{2^{C}} \in ℝ \land \frac{B}{2^{C}} \leq \frac{A + 1}{2^{C}} \land \frac{A + 1}{2^{C}} \leq \frac{B + 1}{2^{C}}))$
53	48 51 52	syl2anc	$⊢ φ \to (\frac{A + 1}{2^{C}} \in [\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}] \leftrightarrow (\frac{A + 1}{2^{C}} \in ℝ \land \frac{B}{2^{C}} \leq \frac{A + 1}{2^{C}} \land \frac{A + 1}{2^{C}} \leq \frac{B + 1}{2^{C}}))$
54	46 53	mpbid	$⊢ φ \to (\frac{A + 1}{2^{C}} \in ℝ \land \frac{B}{2^{C}} \leq \frac{A + 1}{2^{C}} \land \frac{A + 1}{2^{C}} \leq \frac{B + 1}{2^{C}})$
55	54	simp3d	$⊢ φ \to \frac{A + 1}{2^{C}} \leq \frac{B + 1}{2^{C}}$
56		lediv1	$⊢ (A + 1 \in ℝ \land B + 1 \in ℝ \land (2^{C} \in ℝ \land 0 < 2^{C})) \to (A + 1 \leq B + 1 \leftrightarrow \frac{A + 1}{2^{C}} \leq \frac{B + 1}{2^{C}})$
57	35 50 39 40 56	syl112anc	$⊢ φ \to (A + 1 \leq B + 1 \leftrightarrow \frac{A + 1}{2^{C}} \leq \frac{B + 1}{2^{C}})$
58	55 57	mpbird	$⊢ φ \to A + 1 \leq B + 1$
59		1red	$⊢ φ \to 1 \in ℝ$
60	28 47 59	leadd1d	$⊢ φ \to (A \leq B \leftrightarrow A + 1 \leq B + 1)$
61	58 60	mpbird	$⊢ φ \to A \leq B$
62		lbicc2	$⊢ (\frac{A}{2^{C}} \in ℝ^{} \land \frac{A + 1}{2^{C}} \in ℝ^{} \land \frac{A}{2^{C}} \leq \frac{A + 1}{2^{C}}) \to \frac{A}{2^{C}} \in [\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}]$
63	33 37 43 62	syl3anc	$⊢ φ \to \frac{A}{2^{C}} \in [\frac{A}{2^{C}}, \frac{A + 1}{2^{C}}]$
64	27 63	sseldd	$⊢ φ \to \frac{A}{2^{C}} \in [\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}]$
65		elicc2	$⊢ (\frac{B}{2^{C}} \in ℝ \land \frac{B + 1}{2^{C}} \in ℝ) \to (\frac{A}{2^{C}} \in [\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}] \leftrightarrow (\frac{A}{2^{C}} \in ℝ \land \frac{B}{2^{C}} \leq \frac{A}{2^{C}} \land \frac{A}{2^{C}} \leq \frac{B + 1}{2^{C}}))$
66	48 51 65	syl2anc	$⊢ φ \to (\frac{A}{2^{C}} \in [\frac{B}{2^{C}}, \frac{B + 1}{2^{C}}] \leftrightarrow (\frac{A}{2^{C}} \in ℝ \land \frac{B}{2^{C}} \leq \frac{A}{2^{C}} \land \frac{A}{2^{C}} \leq \frac{B + 1}{2^{C}}))$
67	64 66	mpbid	$⊢ φ \to (\frac{A}{2^{C}} \in ℝ \land \frac{B}{2^{C}} \leq \frac{A}{2^{C}} \land \frac{A}{2^{C}} \leq \frac{B + 1}{2^{C}})$
68	67	simp2d	$⊢ φ \to \frac{B}{2^{C}} \leq \frac{A}{2^{C}}$
69		lediv1	$⊢ (B \in ℝ \land A \in ℝ \land (2^{C} \in ℝ \land 0 < 2^{C})) \to (B \leq A \leftrightarrow \frac{B}{2^{C}} \leq \frac{A}{2^{C}})$
70	47 28 39 40 69	syl112anc	$⊢ φ \to (B \leq A \leftrightarrow \frac{B}{2^{C}} \leq \frac{A}{2^{C}})$
71	68 70	mpbird	$⊢ φ \to B \leq A$
72	28 47	letri3d	$⊢ φ \to (A = B \leftrightarrow (A \leq B \land B \leq A))$
73	61 71 72	mpbir2and	$⊢ φ \to A = B$
74	19	eqcomd	$⊢ φ \to C = D$
75	73 74	jca	$⊢ φ \to (A = B \land C = D)$

Metamath Proof Explorer

Theorem dyadmaxlem

Proof