# Metamath Proof Explorer

## Theorem rpnnen1lem5

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 rpnnen1lem5 ${⊢}{x}\in ℝ\to sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)={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 1 2 3 4 rpnnen1lem3 ${⊢}{x}\in ℝ\to \forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {x}$
6 1 2 3 4 rpnnen1lem1 ${⊢}{x}\in ℝ\to {F}\left({x}\right)\in \left({ℚ}^{ℕ}\right)$
7 4 3 elmap ${⊢}{F}\left({x}\right)\in \left({ℚ}^{ℕ}\right)↔{F}\left({x}\right):ℕ⟶ℚ$
8 6 7 sylib ${⊢}{x}\in ℝ\to {F}\left({x}\right):ℕ⟶ℚ$
9 frn ${⊢}{F}\left({x}\right):ℕ⟶ℚ\to \mathrm{ran}{F}\left({x}\right)\subseteq ℚ$
10 qssre ${⊢}ℚ\subseteq ℝ$
11 9 10 sstrdi ${⊢}{F}\left({x}\right):ℕ⟶ℚ\to \mathrm{ran}{F}\left({x}\right)\subseteq ℝ$
12 8 11 syl ${⊢}{x}\in ℝ\to \mathrm{ran}{F}\left({x}\right)\subseteq ℝ$
13 1nn ${⊢}1\in ℕ$
14 13 ne0ii ${⊢}ℕ\ne \varnothing$
15 fdm ${⊢}{F}\left({x}\right):ℕ⟶ℚ\to \mathrm{dom}{F}\left({x}\right)=ℕ$
16 15 neeq1d ${⊢}{F}\left({x}\right):ℕ⟶ℚ\to \left(\mathrm{dom}{F}\left({x}\right)\ne \varnothing ↔ℕ\ne \varnothing \right)$
17 14 16 mpbiri ${⊢}{F}\left({x}\right):ℕ⟶ℚ\to \mathrm{dom}{F}\left({x}\right)\ne \varnothing$
18 dm0rn0 ${⊢}\mathrm{dom}{F}\left({x}\right)=\varnothing ↔\mathrm{ran}{F}\left({x}\right)=\varnothing$
19 18 necon3bii ${⊢}\mathrm{dom}{F}\left({x}\right)\ne \varnothing ↔\mathrm{ran}{F}\left({x}\right)\ne \varnothing$
20 17 19 sylib ${⊢}{F}\left({x}\right):ℕ⟶ℚ\to \mathrm{ran}{F}\left({x}\right)\ne \varnothing$
21 8 20 syl ${⊢}{x}\in ℝ\to \mathrm{ran}{F}\left({x}\right)\ne \varnothing$
22 breq2 ${⊢}{y}={x}\to \left({n}\le {y}↔{n}\le {x}\right)$
23 22 ralbidv ${⊢}{y}={x}\to \left(\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {y}↔\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {x}\right)$
24 23 rspcev ${⊢}\left({x}\in ℝ\wedge \forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {x}\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {y}$
25 5 24 mpdan ${⊢}{x}\in ℝ\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {y}$
26 id ${⊢}{x}\in ℝ\to {x}\in ℝ$
27 suprleub ${⊢}\left(\left(\mathrm{ran}{F}\left({x}\right)\subseteq ℝ\wedge \mathrm{ran}{F}\left({x}\right)\ne \varnothing \wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {y}\right)\wedge {x}\in ℝ\right)\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\le {x}↔\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {x}\right)$
28 12 21 25 26 27 syl31anc ${⊢}{x}\in ℝ\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\le {x}↔\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {x}\right)$
29 5 28 mpbird ${⊢}{x}\in ℝ\to sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\le {x}$
30 1 2 3 4 rpnnen1lem4 ${⊢}{x}\in ℝ\to sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ$
31 resubcl ${⊢}\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ\right)\to {x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ$
32 30 31 mpdan ${⊢}{x}\in ℝ\to {x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ$
33 32 adantr ${⊢}\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\to {x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ$
34 posdif ${⊢}\left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ\wedge {x}\in ℝ\right)\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}↔0<{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\right)$
35 30 34 mpancom ${⊢}{x}\in ℝ\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}↔0<{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\right)$
36 35 biimpa ${⊢}\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\to 0<{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)$
37 36 gt0ne0d ${⊢}\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\to {x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\ne 0$
38 33 37 rereccld ${⊢}\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\to \frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}\in ℝ$
39 arch ${⊢}\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}\in ℝ\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}$
40 38 39 syl ${⊢}\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}$
41 40 ex ${⊢}{x}\in ℝ\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\right)$
42 1 2 rpnnen1lem2 ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to sup\left({T},ℝ,<\right)\in ℤ$
43 42 zred ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to sup\left({T},ℝ,<\right)\in ℝ$
44 43 3adant3 ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\wedge \frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\right)\to sup\left({T},ℝ,<\right)\in ℝ$
45 44 ltp1d ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\wedge \frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\right)\to sup\left({T},ℝ,<\right)
46 33 36 jca ${⊢}\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\to \left({x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ\wedge 0<{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\right)$
47 nnre ${⊢}{k}\in ℕ\to {k}\in ℝ$
48 nngt0 ${⊢}{k}\in ℕ\to 0<{k}$
49 47 48 jca ${⊢}{k}\in ℕ\to \left({k}\in ℝ\wedge 0<{k}\right)$
50 ltrec1 ${⊢}\left(\left({x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ\wedge 0<{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\right)\wedge \left({k}\in ℝ\wedge 0<{k}\right)\right)\to \left(\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}↔\frac{1}{{k}}<{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\right)$
51 46 49 50 syl2an ${⊢}\left(\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\wedge {k}\in ℕ\right)\to \left(\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}↔\frac{1}{{k}}<{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\right)$
52 30 ad2antrr ${⊢}\left(\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\wedge {k}\in ℕ\right)\to sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ$
53 nnrecre ${⊢}{k}\in ℕ\to \frac{1}{{k}}\in ℝ$
54 53 adantl ${⊢}\left(\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\wedge {k}\in ℕ\right)\to \frac{1}{{k}}\in ℝ$
55 simpll ${⊢}\left(\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\wedge {k}\in ℕ\right)\to {x}\in ℝ$
56 52 54 55 ltaddsub2d ${⊢}\left(\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\wedge {k}\in ℕ\right)\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)<{x}↔\frac{1}{{k}}<{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\right)$
57 12 adantr ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \mathrm{ran}{F}\left({x}\right)\subseteq ℝ$
58 ffn ${⊢}{F}\left({x}\right):ℕ⟶ℚ\to {F}\left({x}\right)Fnℕ$
59 8 58 syl ${⊢}{x}\in ℝ\to {F}\left({x}\right)Fnℕ$
60 fnfvelrn ${⊢}\left({F}\left({x}\right)Fnℕ\wedge {k}\in ℕ\right)\to {F}\left({x}\right)\left({k}\right)\in \mathrm{ran}{F}\left({x}\right)$
61 59 60 sylan ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {F}\left({x}\right)\left({k}\right)\in \mathrm{ran}{F}\left({x}\right)$
62 57 61 sseldd ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {F}\left({x}\right)\left({k}\right)\in ℝ$
63 30 adantr ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ$
64 53 adantl ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \frac{1}{{k}}\in ℝ$
65 12 21 25 3jca ${⊢}{x}\in ℝ\to \left(\mathrm{ran}{F}\left({x}\right)\subseteq ℝ\wedge \mathrm{ran}{F}\left({x}\right)\ne \varnothing \wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {y}\right)$
66 65 adantr ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left(\mathrm{ran}{F}\left({x}\right)\subseteq ℝ\wedge \mathrm{ran}{F}\left({x}\right)\ne \varnothing \wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {y}\right)$
67 suprub ${⊢}\left(\left(\mathrm{ran}{F}\left({x}\right)\subseteq ℝ\wedge \mathrm{ran}{F}\left({x}\right)\ne \varnothing \wedge \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {n}\in \mathrm{ran}{F}\left({x}\right)\phantom{\rule{.4em}{0ex}}{n}\le {y}\right)\wedge {F}\left({x}\right)\left({k}\right)\in \mathrm{ran}{F}\left({x}\right)\right)\to {F}\left({x}\right)\left({k}\right)\le sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)$
68 66 61 67 syl2anc ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {F}\left({x}\right)\left({k}\right)\le sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)$
69 62 63 64 68 leadd1dd ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)\le sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)$
70 62 64 readdcld ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)\in ℝ$
71 readdcl ${⊢}\left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ\wedge \frac{1}{{k}}\in ℝ\right)\to sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)\in ℝ$
72 30 53 71 syl2an ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)\in ℝ$
73 simpl ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {x}\in ℝ$
74 lelttr ${⊢}\left({F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)\in ℝ\wedge {x}\in ℝ\right)\to \left(\left({F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)\le sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)<{x}\right)\to {F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)<{x}\right)$
75 74 expd ${⊢}\left({F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)\in ℝ\wedge {x}\in ℝ\right)\to \left({F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)\le sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)<{x}\to {F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)<{x}\right)\right)$
76 70 72 73 75 syl3anc ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left({F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)\le sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)<{x}\to {F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)<{x}\right)\right)$
77 69 76 mpd ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)<{x}\to {F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)<{x}\right)$
78 77 adantlr ${⊢}\left(\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\wedge {k}\in ℕ\right)\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)+\left(\frac{1}{{k}}\right)<{x}\to {F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)<{x}\right)$
79 56 78 sylbird ${⊢}\left(\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\wedge {k}\in ℕ\right)\to \left(\frac{1}{{k}}<{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\to {F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)<{x}\right)$
80 51 79 sylbid ${⊢}\left(\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\wedge {k}\in ℕ\right)\to \left(\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\to {F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)<{x}\right)$
81 42 peano2zd ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to sup\left({T},ℝ,<\right)+1\in ℤ$
82 oveq1 ${⊢}{n}=sup\left({T},ℝ,<\right)+1\to \frac{{n}}{{k}}=\frac{sup\left({T},ℝ,<\right)+1}{{k}}$
83 82 breq1d ${⊢}{n}=sup\left({T},ℝ,<\right)+1\to \left(\frac{{n}}{{k}}<{x}↔\frac{sup\left({T},ℝ,<\right)+1}{{k}}<{x}\right)$
84 83 1 elrab2 ${⊢}sup\left({T},ℝ,<\right)+1\in {T}↔\left(sup\left({T},ℝ,<\right)+1\in ℤ\wedge \frac{sup\left({T},ℝ,<\right)+1}{{k}}<{x}\right)$
85 84 biimpri ${⊢}\left(sup\left({T},ℝ,<\right)+1\in ℤ\wedge \frac{sup\left({T},ℝ,<\right)+1}{{k}}<{x}\right)\to sup\left({T},ℝ,<\right)+1\in {T}$
86 81 85 sylan ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge \frac{sup\left({T},ℝ,<\right)+1}{{k}}<{x}\right)\to sup\left({T},ℝ,<\right)+1\in {T}$
87 ssrab2 ${⊢}\left\{{n}\in ℤ|\frac{{n}}{{k}}<{x}\right\}\subseteq ℤ$
88 1 87 eqsstri ${⊢}{T}\subseteq ℤ$
89 zssre ${⊢}ℤ\subseteq ℝ$
90 88 89 sstri ${⊢}{T}\subseteq ℝ$
91 90 a1i ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {T}\subseteq ℝ$
92 remulcl ${⊢}\left({k}\in ℝ\wedge {x}\in ℝ\right)\to {k}{x}\in ℝ$
93 92 ancoms ${⊢}\left({x}\in ℝ\wedge {k}\in ℝ\right)\to {k}{x}\in ℝ$
94 47 93 sylan2 ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {k}{x}\in ℝ$
95 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)$
96 95 simpld ${⊢}{k}{x}\in ℝ\to \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{n}<{k}{x}$
97 94 96 syl ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{n}<{k}{x}$
98 zre ${⊢}{n}\in ℤ\to {n}\in ℝ$
99 98 adantl ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to {n}\in ℝ$
100 simpll ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to {x}\in ℝ$
101 49 ad2antlr ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to \left({k}\in ℝ\wedge 0<{k}\right)$
102 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)$
103 99 100 101 102 syl3anc ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to \left(\frac{{n}}{{k}}<{x}↔{n}<{k}{x}\right)$
104 103 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)$
105 97 104 mpbird ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\frac{{n}}{{k}}<{x}$
106 rabn0 ${⊢}\left\{{n}\in ℤ|\frac{{n}}{{k}}<{x}\right\}\ne \varnothing ↔\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}\frac{{n}}{{k}}<{x}$
107 105 106 sylibr ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left\{{n}\in ℤ|\frac{{n}}{{k}}<{x}\right\}\ne \varnothing$
108 1 neeq1i ${⊢}{T}\ne \varnothing ↔\left\{{n}\in ℤ|\frac{{n}}{{k}}<{x}\right\}\ne \varnothing$
109 107 108 sylibr ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {T}\ne \varnothing$
110 1 rabeq2i ${⊢}{n}\in {T}↔\left({n}\in ℤ\wedge \frac{{n}}{{k}}<{x}\right)$
111 47 ad2antlr ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to {k}\in ℝ$
112 111 100 92 syl2anc ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to {k}{x}\in ℝ$
113 ltle ${⊢}\left({n}\in ℝ\wedge {k}{x}\in ℝ\right)\to \left({n}<{k}{x}\to {n}\le {k}{x}\right)$
114 99 112 113 syl2anc ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in ℤ\right)\to \left({n}<{k}{x}\to {n}\le {k}{x}\right)$
115 103 114 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)$
116 115 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}$
117 110 116 sylan2b ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge {n}\in {T}\right)\to {n}\le {k}{x}$
118 117 ralrimiva ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \forall {n}\in {T}\phantom{\rule{.4em}{0ex}}{n}\le {k}{x}$
119 breq2 ${⊢}{y}={k}{x}\to \left({n}\le {y}↔{n}\le {k}{x}\right)$
120 119 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)$
121 120 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}$
122 94 118 121 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}$
123 91 109 122 3jca ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \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)$
124 suprub ${⊢}\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 sup\left({T},ℝ,<\right)+1\in {T}\right)\to sup\left({T},ℝ,<\right)+1\le sup\left({T},ℝ,<\right)$
125 123 124 sylan ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge sup\left({T},ℝ,<\right)+1\in {T}\right)\to sup\left({T},ℝ,<\right)+1\le sup\left({T},ℝ,<\right)$
126 86 125 syldan ${⊢}\left(\left({x}\in ℝ\wedge {k}\in ℕ\right)\wedge \frac{sup\left({T},ℝ,<\right)+1}{{k}}<{x}\right)\to sup\left({T},ℝ,<\right)+1\le sup\left({T},ℝ,<\right)$
127 126 ex ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left(\frac{sup\left({T},ℝ,<\right)+1}{{k}}<{x}\to sup\left({T},ℝ,<\right)+1\le sup\left({T},ℝ,<\right)\right)$
128 42 zcnd ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to sup\left({T},ℝ,<\right)\in ℂ$
129 1cnd ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to 1\in ℂ$
130 nncn ${⊢}{k}\in ℕ\to {k}\in ℂ$
131 nnne0 ${⊢}{k}\in ℕ\to {k}\ne 0$
132 130 131 jca ${⊢}{k}\in ℕ\to \left({k}\in ℂ\wedge {k}\ne 0\right)$
133 132 adantl ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left({k}\in ℂ\wedge {k}\ne 0\right)$
134 divdir ${⊢}\left(sup\left({T},ℝ,<\right)\in ℂ\wedge 1\in ℂ\wedge \left({k}\in ℂ\wedge {k}\ne 0\right)\right)\to \frac{sup\left({T},ℝ,<\right)+1}{{k}}=\left(\frac{sup\left({T},ℝ,<\right)}{{k}}\right)+\left(\frac{1}{{k}}\right)$
135 128 129 133 134 syl3anc ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \frac{sup\left({T},ℝ,<\right)+1}{{k}}=\left(\frac{sup\left({T},ℝ,<\right)}{{k}}\right)+\left(\frac{1}{{k}}\right)$
136 3 mptex ${⊢}\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)\in \mathrm{V}$
137 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)$
138 136 137 mpan2 ${⊢}{x}\in ℝ\to {F}\left({x}\right)=\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)$
139 138 fveq1d ${⊢}{x}\in ℝ\to {F}\left({x}\right)\left({k}\right)=\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)\left({k}\right)$
140 ovex ${⊢}\frac{sup\left({T},ℝ,<\right)}{{k}}\in \mathrm{V}$
141 eqid ${⊢}\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)=\left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)$
142 141 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}}$
143 140 142 mpan2 ${⊢}{k}\in ℕ\to \left({k}\in ℕ⟼\frac{sup\left({T},ℝ,<\right)}{{k}}\right)\left({k}\right)=\frac{sup\left({T},ℝ,<\right)}{{k}}$
144 139 143 sylan9eq ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {F}\left({x}\right)\left({k}\right)=\frac{sup\left({T},ℝ,<\right)}{{k}}$
145 144 oveq1d ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to {F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)=\left(\frac{sup\left({T},ℝ,<\right)}{{k}}\right)+\left(\frac{1}{{k}}\right)$
146 135 145 eqtr4d ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \frac{sup\left({T},ℝ,<\right)+1}{{k}}={F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)$
147 146 breq1d ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left(\frac{sup\left({T},ℝ,<\right)+1}{{k}}<{x}↔{F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)<{x}\right)$
148 81 zred ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to sup\left({T},ℝ,<\right)+1\in ℝ$
149 148 43 lenltd ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left(sup\left({T},ℝ,<\right)+1\le sup\left({T},ℝ,<\right)↔¬sup\left({T},ℝ,<\right)
150 127 147 149 3imtr3d ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\right)\to \left({F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)<{x}\to ¬sup\left({T},ℝ,<\right)
151 150 adantlr ${⊢}\left(\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\wedge {k}\in ℕ\right)\to \left({F}\left({x}\right)\left({k}\right)+\left(\frac{1}{{k}}\right)<{x}\to ¬sup\left({T},ℝ,<\right)
152 80 151 syld ${⊢}\left(\left({x}\in ℝ\wedge sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\wedge {k}\in ℕ\right)\to \left(\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\to ¬sup\left({T},ℝ,<\right)
153 152 exp31 ${⊢}{x}\in ℝ\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\to \left({k}\in ℕ\to \left(\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\to ¬sup\left({T},ℝ,<\right)
154 153 com4l ${⊢}sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\to \left({k}\in ℕ\to \left(\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\to \left({x}\in ℝ\to ¬sup\left({T},ℝ,<\right)
155 154 com14 ${⊢}{x}\in ℝ\to \left({k}\in ℕ\to \left(\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\to ¬sup\left({T},ℝ,<\right)
156 155 3imp ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\wedge \frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\right)\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\to ¬sup\left({T},ℝ,<\right)
157 45 156 mt2d ${⊢}\left({x}\in ℝ\wedge {k}\in ℕ\wedge \frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\right)\to ¬sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}$
158 157 rexlimdv3a ${⊢}{x}\in ℝ\to \left(\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{x}-sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)}<{k}\to ¬sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)$
159 41 158 syld ${⊢}{x}\in ℝ\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\to ¬sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)$
160 159 pm2.01d ${⊢}{x}\in ℝ\to ¬sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}$
161 eqlelt ${⊢}\left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\in ℝ\wedge {x}\in ℝ\right)\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)={x}↔\left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\le {x}\wedge ¬sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\right)$
162 30 161 mpancom ${⊢}{x}\in ℝ\to \left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)={x}↔\left(sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)\le {x}\wedge ¬sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)<{x}\right)\right)$
163 29 160 162 mpbir2and ${⊢}{x}\in ℝ\to sup\left(\mathrm{ran}{F}\left({x}\right),ℝ,<\right)={x}$