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

Metamath Proof Explorer

Theorem rpnnen1lem3

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 rpnnen1lem3 ( 𝑥 ∈ ℝ → ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 )

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 7 fveq1d ⊢ ( 𝑥 ∈ ℝ → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ‘ 𝑘 ) )
9 ovex ⊢ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ∈ V
10 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
11 10 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ ∧ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ∈ V ) → ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ‘ 𝑘 ) = ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
12 9 11 mpan2 ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ‘ 𝑘 ) = ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
13 8 12 sylan9eq ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) = ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
14 1 reqabi ⊢ ( 𝑛 ∈ 𝑇 ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) )
15 zre ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℝ )
16 15 adantl ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℝ )
17 simpll ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℝ )
18 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
19 nngt0 ⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
20 18 19 jca ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
21 20 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
22 ltdivmul ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
23 16 17 21 22 syl3anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
24 18 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑘 ∈ ℝ )
25 remulcl ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
26 24 17 25 syl2anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
27 ltle ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑘 · 𝑥 ) ∈ ℝ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
28 16 26 27 syl2anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
29 23 28 sylbid ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
30 29 impr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
31 14 30 sylan2b ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑇 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
32 31 ralrimiva ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) )
33 ssrab2 ⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ⊆ ℤ
34 1 33 eqsstri ⊢ 𝑇 ⊆ ℤ
35 zssre ⊢ ℤ ⊆ ℝ
36 34 35 sstri ⊢ 𝑇 ⊆ ℝ
37 36 a1i ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ⊆ ℝ )
38 25 ancoms ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
39 18 38 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
40 btwnz ⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ( ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑘 · 𝑥 ) < 𝑛 ) )
41 40 simpld ⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
42 39 41 syl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
43 23 rexbidva ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 ↔ ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ) )
44 42 43 mpbird ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
45 rabn0 ⊢ ( { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
46 44 45 sylibr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
47 1 neeq1i ⊢ ( 𝑇 ≠ ∅ ↔ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
48 46 47 sylibr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ≠ ∅ )
49 breq2 ⊢ ( 𝑦 = ( 𝑘 · 𝑥 ) → ( 𝑛 ≤ 𝑦 ↔ 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
50 49 ralbidv ⊢ ( 𝑦 = ( 𝑘 · 𝑥 ) → ( ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
51 50 rspcev ⊢ ( ( ( 𝑘 · 𝑥 ) ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
52 39 32 51 syl2anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
53 suprleub ⊢ ( ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ) ∧ ( 𝑘 · 𝑥 ) ∈ ℝ ) → ( sup ( 𝑇 , ℝ , < ) ≤ ( 𝑘 · 𝑥 ) ↔ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
54 37 48 52 39 53 syl31anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( sup ( 𝑇 , ℝ , < ) ≤ ( 𝑘 · 𝑥 ) ↔ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
55 32 54 mpbird ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ≤ ( 𝑘 · 𝑥 ) )
56 1 2 rpnnen1lem2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℤ )
57 56 zred ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℝ )
58 simpl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ ℝ )
59 20 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
60 ledivmul ⊢ ( ( sup ( 𝑇 , ℝ , < ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ≤ 𝑥 ↔ sup ( 𝑇 , ℝ , < ) ≤ ( 𝑘 · 𝑥 ) ) )
61 57 58 59 60 syl3anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ≤ 𝑥 ↔ sup ( 𝑇 , ℝ , < ) ≤ ( 𝑘 · 𝑥 ) ) )
62 55 61 mpbird ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ≤ 𝑥 )
63 13 62 eqbrtrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ 𝑥 )
64 63 ralrimiva ⊢ ( 𝑥 ∈ ℝ → ∀ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ 𝑥 )
65 1 2 3 4 rpnnen1lem1 ⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) )
66 4 3 elmap ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) ↔ ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ )
67 65 66 sylib ⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ )
68 ffn ⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ( 𝐹 ‘ 𝑥 ) Fn ℕ )
69 breq1 ⊢ ( 𝑛 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) → ( 𝑛 ≤ 𝑥 ↔ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ 𝑥 ) )
70 69 ralrn ⊢ ( ( 𝐹 ‘ 𝑥 ) Fn ℕ → ( ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ 𝑥 ) )
71 67 68 70 3syl ⊢ ( 𝑥 ∈ ℝ → ( ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ 𝑥 ) )
72 64 71 mpbird ⊢ ( 𝑥 ∈ ℝ → ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 )