# 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 ${⊢}{T}=\left\{{n}\in ℤ|\frac{{n}}{{k}}<{x}\right\}$
rpnnen1lem.2 ${⊢}{F}=\left({x}\in ℝ⟼\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)\right)$
rpnnen1lem.n ${⊢}ℕ\in \mathrm{V}$
rpnnen1lem.q ${⊢}ℚ\in \mathrm{V}$
Assertion rpnnen1lem3 ${⊢}{x}\in ℝ\to \forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {x}$

### Proof

Step Hyp Ref Expression
1 rpnnen1lem.1 ${⊢}{T}=\left\{{n}\in ℤ|\frac{{n}}{{k}}<{x}\right\}$
2 rpnnen1lem.2 ${⊢}{F}=\left({x}\in ℝ⟼\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)\right)$
3 rpnnen1lem.n ${⊢}ℕ\in \mathrm{V}$
4 rpnnen1lem.q ${⊢}ℚ\in \mathrm{V}$
5 3 mptex ${⊢}\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)\in \mathrm{V}$
6 2 fvmpt2 ${⊢}\left({x}\in ℝ\wedge \left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)\in \mathrm{V}\right)\to {F}\left({x}\right)=\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)$
7 5 6 mpan2 ${⊢}{x}\in ℝ\to {F}\left({x}\right)=\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)$
8 7 fveq1d ${⊢}{x}\in ℝ\to {F}\left({x}\right)\left({k}\right)=\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)\left({k}\right)$
9 ovex ${⊢}\frac{sup\left({T},ℝ,<\right)}{{k}}\in \mathrm{V}$
10 eqid ${⊢}\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)=\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)$
11 10 fvmpt2 ${⊢}\left({k}\in ℕ\wedge \frac{sup\left({T},ℝ,<\right)}{{k}}\in \mathrm{V}\right)\to \left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)\left({k}\right)=\frac{sup\left({T},ℝ,<\right)}{{k}}$
12 9 11 mpan2 ${⊢}{k}\in ℕ\to \left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)\left({k}\right)=\frac{sup\left({T},ℝ,<\right)}{{k}}$
13 8 12 sylan9eq ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {F}\left({x}\right)\left({k}\right)=\frac{sup\left({T},ℝ,<\right)}{{k}}$
14 1 rabeq2i ${⊢}{n}\in {T}↔\left({n}\in ℤ\wedge \frac{{n}}{{k}}<{x}\right)$
15 zre ${⊢}{n}\in ℤ\to {n}\in ℝ$
16 15 adantl ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to {n}\in ℝ$
17 simpll ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to {x}\in ℝ$
18 nnre ${⊢}{k}\in ℕ\to {k}\in ℝ$
19 nngt0 ${⊢}{k}\in ℕ\to 0<{k}$
20 18 19 jca ${⊢}{k}\in ℕ\to \left({k}\in ℝ\wedge 0<{k}\right)$
21 20 ad2antlr ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to \left({k}\in ℝ\wedge 0<{k}\right)$
22 ltdivmul ${⊢}\left({n}\in ℝ\wedge {x}\in ℝ\wedge \left({k}\in ℝ\wedge 0<{k}\right)\right)\to \left(\frac{{n}}{{k}}<{x}↔{n}<{k}{x}\right)$
23 16 17 21 22 syl3anc ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to \left(\frac{{n}}{{k}}<{x}↔{n}<{k}{x}\right)$
24 18 ad2antlr ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to {k}\in ℝ$
25 remulcl ${⊢}\left({k}\in ℝ\wedge {x}\in ℝ\right)\to {k}{x}\in ℝ$
26 24 17 25 syl2anc ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to {k}{x}\in ℝ$
27 ltle ${⊢}\left({n}\in ℝ\wedge {k}{x}\in ℝ\right)\to \left({n}<{k}{x}\to {n}\le {k}{x}\right)$
28 16 26 27 syl2anc ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to \left({n}<{k}{x}\to {n}\le {k}{x}\right)$
29 23 28 sylbid ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to \left(\frac{{n}}{{k}}<{x}\to {n}\le {k}{x}\right)$
30 29 impr ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge \left({n}\in ℤ\wedge \frac{{n}}{{k}}<{x}\right)\right)\to {n}\le {k}{x}$
31 14 30 sylan2b ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in {T}\right)\to {n}\le {k}{x}$
32 31 ralrimiva ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \forall {n}\in {T}\phantom{\rule{.4em}{0ex}}{n}\le {k}{x}$
33 ssrab2 ${⊢}\left\{{n}\in ℤ|\frac{{n}}{{k}}<{x}\right\}\subseteq ℤ$
34 1 33 eqsstri ${⊢}{T}\subseteq ℤ$
35 zssre ${⊢}ℤ\subseteq ℝ$
36 34 35 sstri ${⊢}{T}\subseteq ℝ$
37 36 a1i ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {T}\subseteq ℝ$
38 25 ancoms ${⊢}\left({x}\in ℝ\wedge {k}\in ℝ\right)\to {k}{x}\in ℝ$
39 18 38 sylan2 ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {k}{x}\in ℝ$
40 btwnz ${⊢}{k}{x}\in ℝ\to \left(\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{n}<{k}{x}\wedge \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{k}{x}<{n}\right)$
41 40 simpld ${⊢}{k}{x}\in ℝ\to \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{n}<{k}{x}$
42 39 41 syl ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{n}<{k}{x}$
43 23 rexbidva ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left(\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\frac{{n}}{{k}}<{x}↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{n}<{k}{x}\right)$
44 42 43 mpbird ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\frac{{n}}{{k}}<{x}$
45 rabn0 ${⊢}\left\{{n}\in ℤ|\frac{{n}}{{k}}<{x}\right\}\ne \varnothing ↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\frac{{n}}{{k}}<{x}$
46 44 45 sylibr ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left\{{n}\in ℤ|\frac{{n}}{{k}}<{x}\right\}\ne \varnothing$
47 1 neeq1i ${⊢}{T}\ne \varnothing ↔\left\{{n}\in ℤ|\frac{{n}}{{k}}<{x}\right\}\ne \varnothing$
48 46 47 sylibr ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {T}\ne \varnothing$
49 breq2 ${⊢}{y}={k}{x}\to \left({n}\le {y}↔{n}\le {k}{x}\right)$
50 49 ralbidv ${⊢}{y}={k}{x}\to \left(\forall {n}\in {T}\phantom{\rule{.4em}{0ex}}{n}\le {y}↔\forall {n}\in {T}\phantom{\rule{.4em}{0ex}}{n}\le {k}{x}\right)$
51 50 rspcev ${⊢}\left({k}{x}\in ℝ\wedge \forall {n}\in {T}\phantom{\rule{.4em}{0ex}}{n}\le {k}{x}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {T}\phantom{\rule{.4em}{0ex}}{n}\le {y}$
52 39 32 51 syl2anc ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {T}\phantom{\rule{.4em}{0ex}}{n}\le {y}$
53 suprleub ${⊢}\left(\left({T}\subseteq ℝ\wedge {T}\ne \varnothing \wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in {T}\phantom{\rule{.4em}{0ex}}{n}\le {y}\right)\wedge {k}{x}\in ℝ\right)\to \left(sup\left({T},ℝ,<\right)\le {k}{x}↔\forall {n}\in {T}\phantom{\rule{.4em}{0ex}}{n}\le {k}{x}\right)$
54 37 48 52 39 53 syl31anc ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left(sup\left({T},ℝ,<\right)\le {k}{x}↔\forall {n}\in {T}\phantom{\rule{.4em}{0ex}}{n}\le {k}{x}\right)$
55 32 54 mpbird ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to sup\left({T},ℝ,<\right)\le {k}{x}$
56 1 2 rpnnen1lem2 ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to sup\left({T},ℝ,<\right)\in ℤ$
57 56 zred ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to sup\left({T},ℝ,<\right)\in ℝ$
58 simpl ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {x}\in ℝ$
59 20 adantl ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left({k}\in ℝ\wedge 0<{k}\right)$
60 ledivmul ${⊢}\left(sup\left({T},ℝ,<\right)\in ℝ\wedge {x}\in ℝ\wedge \left({k}\in ℝ\wedge 0<{k}\right)\right)\to \left(\frac{sup\left({T},ℝ,<\right)}{{k}}\le {x}↔sup\left({T},ℝ,<\right)\le {k}{x}\right)$
61 57 58 59 60 syl3anc ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left(\frac{sup\left({T},ℝ,<\right)}{{k}}\le {x}↔sup\left({T},ℝ,<\right)\le {k}{x}\right)$
62 55 61 mpbird ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \frac{sup\left({T},ℝ,<\right)}{{k}}\le {x}$
63 13 62 eqbrtrd ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {F}\left({x}\right)\left({k}\right)\le {x}$
64 63 ralrimiva ${⊢}{x}\in ℝ\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\left({k}\right)\le {x}$
65 1 2 3 4 rpnnen1lem1 ${⊢}{x}\in ℝ\to {F}\left({x}\right)\in \left({ℚ}^{ℕ}\right)$
66 4 3 elmap ${⊢}{F}\left({x}\right)\in \left({ℚ}^{ℕ}\right)↔{F}\left({x}\right):ℕ⟶ℚ$
67 65 66 sylib ${⊢}{x}\in ℝ\to {F}\left({x}\right):ℕ⟶ℚ$
68 ffn ${⊢}{F}\left({x}\right):ℕ⟶ℚ\to {F}\left({x}\right)Fnℕ$
69 breq1 ${⊢}{n}={F}\left({x}\right)\left({k}\right)\to \left({n}\le {x}↔{F}\left({x}\right)\left({k}\right)\le {x}\right)$
70 69 ralrn ${⊢}{F}\left({x}\right)Fnℕ\to \left(\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {x}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\left({k}\right)\le {x}\right)$
71 67 68 70 3syl ${⊢}{x}\in ℝ\to \left(\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {x}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\left({k}\right)\le {x}\right)$
72 64 71 mpbird ${⊢}{x}\in ℝ\to \forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {x}$