Metamath Proof Explorer

Theorem dyadss

Description: Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015) (Proof shortened by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypothesis dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
Assertion dyadss ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) → ( ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) → 𝐷 ≤ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2 simpr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) )
3 simpllr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → 𝐵 ∈ ℤ )
4 simplrr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → 𝐷 ∈ ℕ0 )
5 1 dyadval ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℕ0 ) → ( 𝐵 𝐹 𝐷 ) = ⟨ ( 𝐵 / ( 2 ↑ 𝐷 ) ) , ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐷 ) ) ⟩ )
6 3 4 5 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( 𝐵 𝐹 𝐷 ) = ⟨ ( 𝐵 / ( 2 ↑ 𝐷 ) ) , ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐷 ) ) ⟩ )
7 6 fveq2d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) = ( [,] ‘ ⟨ ( 𝐵 / ( 2 ↑ 𝐷 ) ) , ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐷 ) ) ⟩ ) )
8 df-ov ⊢ ( ( 𝐵 / ( 2 ↑ 𝐷 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐷 ) ) ) = ( [,] ‘ ⟨ ( 𝐵 / ( 2 ↑ 𝐷 ) ) , ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐷 ) ) ⟩ )
9 7 8 eqtr4di ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) = ( ( 𝐵 / ( 2 ↑ 𝐷 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐷 ) ) ) )
10 3 zred ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → 𝐵 ∈ ℝ )
11 2nn ⊢ 2 ∈ ℕ
12 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐷 ∈ ℕ0 ) → ( 2 ↑ 𝐷 ) ∈ ℕ )
13 11 4 12 sylancr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( 2 ↑ 𝐷 ) ∈ ℕ )
14 10 13 nndivred ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( 𝐵 / ( 2 ↑ 𝐷 ) ) ∈ ℝ )
15 peano2re ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 1 ) ∈ ℝ )
16 10 15 syl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( 𝐵 + 1 ) ∈ ℝ )
17 16 13 nndivred ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐷 ) ) ∈ ℝ )
18 iccssre ⊢ ( ( ( 𝐵 / ( 2 ↑ 𝐷 ) ) ∈ ℝ ∧ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐷 ) ) ∈ ℝ ) → ( ( 𝐵 / ( 2 ↑ 𝐷 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐷 ) ) ) ⊆ ℝ )
19 14 17 18 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( ( 𝐵 / ( 2 ↑ 𝐷 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐷 ) ) ) ⊆ ℝ )
20 9 19 eqsstrd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ⊆ ℝ )
21 ovolss ⊢ ( ( ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ∧ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ⊆ ℝ ) → ( vol* ‘ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ) ≤ ( vol* ‘ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) )
22 2 20 21 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( vol* ‘ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ) ≤ ( vol* ‘ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) )
23 simplll ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → 𝐴 ∈ ℤ )
24 simplrl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → 𝐶 ∈ ℕ0 )
25 1 dyadovol ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( vol* ‘ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ) = ( 1 / ( 2 ↑ 𝐶 ) ) )
26 23 24 25 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( vol* ‘ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ) = ( 1 / ( 2 ↑ 𝐶 ) ) )
27 1 dyadovol ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℕ0 ) → ( vol* ‘ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) = ( 1 / ( 2 ↑ 𝐷 ) ) )
28 3 4 27 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( vol* ‘ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) = ( 1 / ( 2 ↑ 𝐷 ) ) )
29 22 26 28 3brtr3d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( 1 / ( 2 ↑ 𝐶 ) ) ≤ ( 1 / ( 2 ↑ 𝐷 ) ) )
30 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) → ( 2 ↑ 𝐶 ) ∈ ℕ )
31 11 24 30 sylancr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( 2 ↑ 𝐶 ) ∈ ℕ )
32 nnre ⊢ ( ( 2 ↑ 𝐷 ) ∈ ℕ → ( 2 ↑ 𝐷 ) ∈ ℝ )
33 nngt0 ⊢ ( ( 2 ↑ 𝐷 ) ∈ ℕ → 0 < ( 2 ↑ 𝐷 ) )
34 32 33 jca ⊢ ( ( 2 ↑ 𝐷 ) ∈ ℕ → ( ( 2 ↑ 𝐷 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐷 ) ) )
35 nnre ⊢ ( ( 2 ↑ 𝐶 ) ∈ ℕ → ( 2 ↑ 𝐶 ) ∈ ℝ )
36 nngt0 ⊢ ( ( 2 ↑ 𝐶 ) ∈ ℕ → 0 < ( 2 ↑ 𝐶 ) )
37 35 36 jca ⊢ ( ( 2 ↑ 𝐶 ) ∈ ℕ → ( ( 2 ↑ 𝐶 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐶 ) ) )
38 lerec ⊢ ( ( ( ( 2 ↑ 𝐷 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐷 ) ) ∧ ( ( 2 ↑ 𝐶 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐶 ) ) ) → ( ( 2 ↑ 𝐷 ) ≤ ( 2 ↑ 𝐶 ) ↔ ( 1 / ( 2 ↑ 𝐶 ) ) ≤ ( 1 / ( 2 ↑ 𝐷 ) ) ) )
39 34 37 38 syl2an ⊢ ( ( ( 2 ↑ 𝐷 ) ∈ ℕ ∧ ( 2 ↑ 𝐶 ) ∈ ℕ ) → ( ( 2 ↑ 𝐷 ) ≤ ( 2 ↑ 𝐶 ) ↔ ( 1 / ( 2 ↑ 𝐶 ) ) ≤ ( 1 / ( 2 ↑ 𝐷 ) ) ) )
40 13 31 39 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( ( 2 ↑ 𝐷 ) ≤ ( 2 ↑ 𝐶 ) ↔ ( 1 / ( 2 ↑ 𝐶 ) ) ≤ ( 1 / ( 2 ↑ 𝐷 ) ) ) )
41 29 40 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( 2 ↑ 𝐷 ) ≤ ( 2 ↑ 𝐶 ) )
42 2re ⊢ 2 ∈ ℝ
43 42 a1i ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → 2 ∈ ℝ )
44 4 nn0zd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → 𝐷 ∈ ℤ )
45 24 nn0zd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → 𝐶 ∈ ℤ )
46 1lt2 ⊢ 1 < 2
47 46 a1i ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → 1 < 2 )
48 43 44 45 47 leexp2d ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → ( 𝐷 ≤ 𝐶 ↔ ( 2 ↑ 𝐷 ) ≤ ( 2 ↑ 𝐶 ) ) )
49 41 48 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) ∧ ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) ) → 𝐷 ≤ 𝐶 )
50 49 ex ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) → ( ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) → 𝐷 ≤ 𝐶 ) )