Metamath Proof Explorer


Theorem dyadf

Description: The function F returns the endpoints of a dyadic rational covering of the real line. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis dyadmbl.1 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
Assertion dyadf 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2 zre ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
3 2 adantr ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → 𝑥 ∈ ℝ )
4 3 lep1d ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → 𝑥 ≤ ( 𝑥 + 1 ) )
5 peano2re ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
6 3 5 syl ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 + 1 ) ∈ ℝ )
7 2nn 2 ∈ ℕ
8 nnexpcl ( ( 2 ∈ ℕ ∧ 𝑦 ∈ ℕ0 ) → ( 2 ↑ 𝑦 ) ∈ ℕ )
9 7 8 mpan ( 𝑦 ∈ ℕ0 → ( 2 ↑ 𝑦 ) ∈ ℕ )
10 9 adantl ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( 2 ↑ 𝑦 ) ∈ ℕ )
11 10 nnred ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( 2 ↑ 𝑦 ) ∈ ℝ )
12 10 nngt0d ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → 0 < ( 2 ↑ 𝑦 ) )
13 lediv1 ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 + 1 ) ∈ ℝ ∧ ( ( 2 ↑ 𝑦 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑦 ) ) ) → ( 𝑥 ≤ ( 𝑥 + 1 ) ↔ ( 𝑥 / ( 2 ↑ 𝑦 ) ) ≤ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ) )
14 3 6 11 12 13 syl112anc ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 ≤ ( 𝑥 + 1 ) ↔ ( 𝑥 / ( 2 ↑ 𝑦 ) ) ≤ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ) )
15 4 14 mpbid ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 / ( 2 ↑ 𝑦 ) ) ≤ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) )
16 df-br ( ( 𝑥 / ( 2 ↑ 𝑦 ) ) ≤ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ↔ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ≤ )
17 15 16 sylib ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ≤ )
18 nndivre ( ( 𝑥 ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ∈ ℕ ) → ( 𝑥 / ( 2 ↑ 𝑦 ) ) ∈ ℝ )
19 2 9 18 syl2an ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 / ( 2 ↑ 𝑦 ) ) ∈ ℝ )
20 2 5 syl ( 𝑥 ∈ ℤ → ( 𝑥 + 1 ) ∈ ℝ )
21 nndivre ( ( ( 𝑥 + 1 ) ∈ ℝ ∧ ( 2 ↑ 𝑦 ) ∈ ℕ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ∈ ℝ )
22 20 9 21 syl2an ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ∈ ℝ )
23 19 22 opelxpd ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ℝ × ℝ ) )
24 17 23 elind ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ0 ) → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
25 24 rgen2 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℕ0 ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) )
26 1 fmpo ( ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℕ0 ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ↔ 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
27 25 26 mpbi 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) )