This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dyaddisjlem

Description: Lemma for dyaddisj . (Contributed by Mario Carneiro, 26-Mar-2015)

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

Proof

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