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=n∈ℤ|nk<x
rpnnen1lem.2 ⊢F=x∈ℝ⟼k∈ℕ⟼supTℝ<k
rpnnen1lem.n ⊢ℕ∈V
rpnnen1lem.q ⊢ℚ∈V
Assertion rpnnen1lem5 ⊢x∈ℝ→supran⁡F⁡xℝ<=x

Proof

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