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 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) )