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

Metamath Proof Explorer

Theorem rpnnen1lem1

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 13-Aug-2021) (Proof modification is discouraged.)

Ref Expression
Hypotheses rpnnen1lem.1 ⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
rpnnen1lem.2 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
rpnnen1lem.n ⊢ ℕ ∈ V
rpnnen1lem.q ⊢ ℚ ∈ V
Assertion rpnnen1lem1 ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) )

Proof

Step Hyp Ref Expression
1 rpnnen1lem.1 ⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
2 rpnnen1lem.2 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
3 rpnnen1lem.n ⊢ ℕ ∈ V
4 rpnnen1lem.q ⊢ ℚ ∈ V
5 3 mptex ⊢ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ∈ V
6 2 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ∈ V ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
7 5 6 mpan2 ⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
8 ssrab2 ⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ⊆ ℤ
9 1 8 eqsstri ⊢ 𝑇 ⊆ ℤ
10 9 a1i ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ⊆ ℤ )
11 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
12 remulcl ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
13 12 ancoms ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
14 11 13 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
15 btwnz ⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ( ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑘 · 𝑥 ) < 𝑛 ) )
16 15 simpld ⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
17 14 16 syl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
18 zre ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℝ )
19 18 adantl ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℝ )
20 simpll ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℝ )
21 nngt0 ⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
22 11 21 jca ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
23 22 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
24 ltdivmul ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
25 19 20 23 24 syl3anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
26 25 rexbidva ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 ↔ ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ) )
27 17 26 mpbird ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
28 rabn0 ⊢ ( { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
29 27 28 sylibr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
30 1 neeq1i ⊢ ( 𝑇 ≠ ∅ ↔ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
31 29 30 sylibr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ≠ ∅ )
32 1 reqabi ⊢ ( 𝑛 ∈ 𝑇 ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) )
33 11 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑘 ∈ ℝ )
34 33 20 12 syl2anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
35 ltle ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑘 · 𝑥 ) ∈ ℝ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
36 19 34 35 syl2anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
37 25 36 sylbid ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
38 37 impr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
39 32 38 sylan2b ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑇 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
40 39 ralrimiva ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) )
41 breq2 ⊢ ( 𝑦 = ( 𝑘 · 𝑥 ) → ( 𝑛 ≤ 𝑦 ↔ 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
42 41 ralbidv ⊢ ( 𝑦 = ( 𝑘 · 𝑥 ) → ( ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
43 42 rspcev ⊢ ( ( ( 𝑘 · 𝑥 ) ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
44 14 40 43 syl2anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
45 suprzcl ⊢ ( ( 𝑇 ⊆ ℤ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
46 10 31 44 45 syl3anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
47 9 46 sselid ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℤ )
48 znq ⊢ ( ( sup ( 𝑇 , ℝ , < ) ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ∈ ℚ )
49 47 48 sylancom ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ∈ ℚ )
50 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
51 49 50 fmptd ⊢ ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) : ℕ ⟶ ℚ )
52 4 3 elmap ⊢ ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ∈ ( ℚ ↑m ℕ ) ↔ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) : ℕ ⟶ ℚ )
53 51 52 sylibr ⊢ ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ∈ ( ℚ ↑m ℕ ) )
54 7 53 eqeltrd ⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) )