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

Proof

Step Hyp Ref Expression
1 rpnnen1lem.1 ⊢ T = n ∈ ℤ | n k < x
2 rpnnen1lem.2 ⊢ F = x ∈ ℝ ⟼ k ∈ ℕ ⟼ sup T ℝ < k
3 rpnnen1lem.n ⊢ ℕ ∈ V
4 rpnnen1lem.q ⊢ ℚ ∈ V
5 1 2 3 4 rpnnen1lem3 ⊢ x ∈ ℝ → ∀ n ∈ ran ⁡ F ⁡ x n ≤ 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 ⁡ x n ≤ y ↔ ∀ n ∈ ran ⁡ F ⁡ x n ≤ x
24 23 rspcev ⊢ x ∈ ℝ ∧ ∀ n ∈ ran ⁡ F ⁡ x n ≤ x → ∃ y ∈ ℝ ∀ n ∈ ran ⁡ F ⁡ x n ≤ y
25 5 24 mpdan ⊢ x ∈ ℝ → ∃ y ∈ ℝ ∀ n ∈ ran ⁡ F ⁡ x n ≤ y
26 id ⊢ x ∈ ℝ → x ∈ ℝ
27 suprleub ⊢ ran ⁡ F ⁡ x ⊆ ℝ ∧ ran ⁡ F ⁡ x ≠ ∅ ∧ ∃ y ∈ ℝ ∀ n ∈ ran ⁡ F ⁡ x n ≤ y ∧ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < ≤ x ↔ ∀ n ∈ ran ⁡ F ⁡ x n ≤ x
28 12 21 25 26 27 syl31anc ⊢ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < ≤ x ↔ ∀ n ∈ ran ⁡ F ⁡ x n ≤ x
29 5 28 mpbird ⊢ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < ≤ x
30 1 2 3 4 rpnnen1lem4 ⊢ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < ∈ ℝ
31 resubcl ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < ∈ ℝ → x − sup ran ⁡ F ⁡ x ℝ < ∈ ℝ
32 30 31 mpdan ⊢ x ∈ ℝ → x − sup ran ⁡ F ⁡ x ℝ < ∈ ℝ
33 32 adantr ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x → x − sup ran ⁡ F ⁡ x ℝ < ∈ ℝ
34 posdif ⊢ sup ran ⁡ F ⁡ x ℝ < ∈ ℝ ∧ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < < x ↔ 0 < x − sup ran ⁡ F ⁡ x ℝ <
35 30 34 mpancom ⊢ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < < x ↔ 0 < x − sup ran ⁡ F ⁡ x ℝ <
36 35 biimpa ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x → 0 < x − sup ran ⁡ F ⁡ x ℝ <
37 36 gt0ne0d ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x → x − sup ran ⁡ F ⁡ x ℝ < ≠ 0
38 33 37 rereccld ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x → 1 x − sup ran ⁡ F ⁡ x ℝ < ∈ ℝ
39 arch ⊢ 1 x − sup ran ⁡ F ⁡ x ℝ < ∈ ℝ → ∃ k ∈ ℕ 1 x − sup ran ⁡ F ⁡ x ℝ < < k
40 38 39 syl ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x → ∃ k ∈ ℕ 1 x − sup ran ⁡ F ⁡ x ℝ < < k
41 40 ex ⊢ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < < x → ∃ k ∈ ℕ 1 x − sup ran ⁡ F ⁡ x ℝ < < k
42 1 2 rpnnen1lem2 ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup T ℝ < ∈ ℤ
43 42 zred ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup T ℝ < ∈ ℝ
44 43 3adant3 ⊢ x ∈ ℝ ∧ k ∈ ℕ ∧ 1 x − sup ran ⁡ F ⁡ x ℝ < < k → sup T ℝ < ∈ ℝ
45 44 ltp1d ⊢ x ∈ ℝ ∧ k ∈ ℕ ∧ 1 x − sup ran ⁡ F ⁡ x ℝ < < k → sup T ℝ < < sup T ℝ < + 1
46 33 36 jca ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x → x − sup ran ⁡ F ⁡ x ℝ < ∈ ℝ ∧ 0 < x − sup ran ⁡ F ⁡ x ℝ <
47 nnre ⊢ k ∈ ℕ → k ∈ ℝ
48 nngt0 ⊢ k ∈ ℕ → 0 < k
49 47 48 jca ⊢ k ∈ ℕ → k ∈ ℝ ∧ 0 < k
50 ltrec1 ⊢ x − sup ran ⁡ F ⁡ x ℝ < ∈ ℝ ∧ 0 < x − sup ran ⁡ F ⁡ x ℝ < ∧ k ∈ ℝ ∧ 0 < k → 1 x − sup ran ⁡ F ⁡ x ℝ < < k ↔ 1 k < x − sup ran ⁡ F ⁡ x ℝ <
51 46 49 50 syl2an ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x ∧ k ∈ ℕ → 1 x − sup ran ⁡ F ⁡ x ℝ < < k ↔ 1 k < x − sup ran ⁡ F ⁡ x ℝ <
52 30 ad2antrr ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x ∧ k ∈ ℕ → sup ran ⁡ F ⁡ x ℝ < ∈ ℝ
53 nnrecre ⊢ k ∈ ℕ → 1 k ∈ ℝ
54 53 adantl ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x ∧ k ∈ ℕ → 1 k ∈ ℝ
55 simpll ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x ∧ k ∈ ℕ → x ∈ ℝ
56 52 54 55 ltaddsub2d ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x ∧ k ∈ ℕ → sup ran ⁡ F ⁡ x ℝ < + 1 k < x ↔ 1 k < x − sup ran ⁡ F ⁡ x ℝ <
57 12 adantr ⊢ x ∈ ℝ ∧ k ∈ ℕ → ran ⁡ F ⁡ x ⊆ ℝ
58 ffn ⊢ F ⁡ x : ℕ ⟶ ℚ → F ⁡ x Fn ℕ
59 8 58 syl ⊢ x ∈ ℝ → F ⁡ x Fn ℕ
60 fnfvelrn ⊢ F ⁡ x Fn ℕ ∧ 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 ∈ ℕ → sup ran ⁡ F ⁡ x ℝ < ∈ ℝ
64 53 adantl ⊢ x ∈ ℝ ∧ k ∈ ℕ → 1 k ∈ ℝ
65 12 21 25 3jca ⊢ x ∈ ℝ → ran ⁡ F ⁡ x ⊆ ℝ ∧ ran ⁡ F ⁡ x ≠ ∅ ∧ ∃ y ∈ ℝ ∀ n ∈ ran ⁡ F ⁡ x n ≤ y
66 65 adantr ⊢ x ∈ ℝ ∧ k ∈ ℕ → ran ⁡ F ⁡ x ⊆ ℝ ∧ ran ⁡ F ⁡ x ≠ ∅ ∧ ∃ y ∈ ℝ ∀ n ∈ ran ⁡ F ⁡ x n ≤ y
67 suprub ⊢ ran ⁡ F ⁡ x ⊆ ℝ ∧ ran ⁡ F ⁡ x ≠ ∅ ∧ ∃ y ∈ ℝ ∀ n ∈ ran ⁡ F ⁡ x n ≤ y ∧ F ⁡ x ⁡ k ∈ ran ⁡ F ⁡ x → F ⁡ x ⁡ k ≤ sup ran ⁡ F ⁡ x ℝ <
68 66 61 67 syl2anc ⊢ x ∈ ℝ ∧ k ∈ ℕ → F ⁡ x ⁡ k ≤ sup ran ⁡ F ⁡ x ℝ <
69 62 63 64 68 leadd1dd ⊢ x ∈ ℝ ∧ k ∈ ℕ → F ⁡ x ⁡ k + 1 k ≤ sup ran ⁡ F ⁡ x ℝ < + 1 k
70 62 64 readdcld ⊢ x ∈ ℝ ∧ k ∈ ℕ → F ⁡ x ⁡ k + 1 k ∈ ℝ
71 readdcl ⊢ sup ran ⁡ F ⁡ x ℝ < ∈ ℝ ∧ 1 k ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < + 1 k ∈ ℝ
72 30 53 71 syl2an ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup ran ⁡ F ⁡ x ℝ < + 1 k ∈ ℝ
73 simpl ⊢ x ∈ ℝ ∧ k ∈ ℕ → x ∈ ℝ
74 lelttr ⊢ F ⁡ x ⁡ k + 1 k ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < + 1 k ∈ ℝ ∧ x ∈ ℝ → F ⁡ x ⁡ k + 1 k ≤ sup ran ⁡ F ⁡ x ℝ < + 1 k ∧ sup ran ⁡ F ⁡ x ℝ < + 1 k < x → F ⁡ x ⁡ k + 1 k < x
75 74 expd ⊢ F ⁡ x ⁡ k + 1 k ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < + 1 k ∈ ℝ ∧ x ∈ ℝ → F ⁡ x ⁡ k + 1 k ≤ sup ran ⁡ F ⁡ x ℝ < + 1 k → sup ran ⁡ F ⁡ x ℝ < + 1 k < x → F ⁡ x ⁡ k + 1 k < x
76 70 72 73 75 syl3anc ⊢ x ∈ ℝ ∧ k ∈ ℕ → F ⁡ x ⁡ k + 1 k ≤ sup ran ⁡ F ⁡ x ℝ < + 1 k → sup ran ⁡ F ⁡ x ℝ < + 1 k < x → F ⁡ x ⁡ k + 1 k < x
77 69 76 mpd ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup ran ⁡ F ⁡ x ℝ < + 1 k < x → F ⁡ x ⁡ k + 1 k < x
78 77 adantlr ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x ∧ k ∈ ℕ → sup ran ⁡ F ⁡ x ℝ < + 1 k < x → F ⁡ x ⁡ k + 1 k < x
79 56 78 sylbird ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x ∧ k ∈ ℕ → 1 k < x − sup ran ⁡ F ⁡ x ℝ < → F ⁡ x ⁡ k + 1 k < x
80 51 79 sylbid ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x ∧ k ∈ ℕ → 1 x − sup ran ⁡ F ⁡ x ℝ < < k → F ⁡ x ⁡ k + 1 k < x
81 42 peano2zd ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup T ℝ < + 1 ∈ ℤ
82 oveq1 ⊢ n = sup T ℝ < + 1 → n k = sup T ℝ < + 1 k
83 82 breq1d ⊢ n = sup T ℝ < + 1 → n k < x ↔ sup T ℝ < + 1 k < x
84 83 1 elrab2 ⊢ sup T ℝ < + 1 ∈ T ↔ sup T ℝ < + 1 ∈ ℤ ∧ sup T ℝ < + 1 k < x
85 84 biimpri ⊢ sup T ℝ < + 1 ∈ ℤ ∧ sup T ℝ < + 1 k < x → sup T ℝ < + 1 ∈ T
86 81 85 sylan ⊢ x ∈ ℝ ∧ k ∈ ℕ ∧ sup T ℝ < + 1 k < x → sup T ℝ < + 1 ∈ T
87 ssrab2 ⊢ n ∈ ℤ | n k < 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 → n k < x ↔ n < k ⁢ x
103 99 100 101 102 syl3anc ⊢ x ∈ ℝ ∧ k ∈ ℕ ∧ n ∈ ℤ → n k < x ↔ n < k ⁢ x
104 103 rexbidva ⊢ x ∈ ℝ ∧ k ∈ ℕ → ∃ n ∈ ℤ n k < x ↔ ∃ n ∈ ℤ n < k ⁢ x
105 97 104 mpbird ⊢ x ∈ ℝ ∧ k ∈ ℕ → ∃ n ∈ ℤ n k < x
106 rabn0 ⊢ n ∈ ℤ | n k < x ≠ ∅ ↔ ∃ n ∈ ℤ n k < x
107 105 106 sylibr ⊢ x ∈ ℝ ∧ k ∈ ℕ → n ∈ ℤ | n k < x ≠ ∅
108 1 neeq1i ⊢ T ≠ ∅ ↔ n ∈ ℤ | n k < x ≠ ∅
109 107 108 sylibr ⊢ x ∈ ℝ ∧ k ∈ ℕ → T ≠ ∅
110 1 rabeq2i ⊢ n ∈ T ↔ n ∈ ℤ ∧ n k < 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 ∈ ℤ → n k < x → n ≤ k ⁢ x
116 115 impr ⊢ x ∈ ℝ ∧ k ∈ ℕ ∧ n ∈ ℤ ∧ n k < x → n ≤ k ⁢ x
117 110 116 sylan2b ⊢ x ∈ ℝ ∧ k ∈ ℕ ∧ n ∈ T → n ≤ k ⁢ x
118 117 ralrimiva ⊢ x ∈ ℝ ∧ k ∈ ℕ → ∀ n ∈ T n ≤ k ⁢ x
119 breq2 ⊢ y = k ⁢ x → n ≤ y ↔ n ≤ k ⁢ x
120 119 ralbidv ⊢ y = k ⁢ x → ∀ n ∈ T n ≤ y ↔ ∀ n ∈ T n ≤ k ⁢ x
121 120 rspcev ⊢ k ⁢ x ∈ ℝ ∧ ∀ n ∈ T n ≤ k ⁢ x → ∃ y ∈ ℝ ∀ n ∈ T n ≤ y
122 94 118 121 syl2anc ⊢ x ∈ ℝ ∧ k ∈ ℕ → ∃ y ∈ ℝ ∀ n ∈ T n ≤ y
123 91 109 122 3jca ⊢ x ∈ ℝ ∧ k ∈ ℕ → T ⊆ ℝ ∧ T ≠ ∅ ∧ ∃ y ∈ ℝ ∀ n ∈ T n ≤ y
124 suprub ⊢ T ⊆ ℝ ∧ T ≠ ∅ ∧ ∃ y ∈ ℝ ∀ n ∈ T n ≤ y ∧ sup T ℝ < + 1 ∈ T → sup T ℝ < + 1 ≤ sup T ℝ <
125 123 124 sylan ⊢ x ∈ ℝ ∧ k ∈ ℕ ∧ sup T ℝ < + 1 ∈ T → sup T ℝ < + 1 ≤ sup T ℝ <
126 86 125 syldan ⊢ x ∈ ℝ ∧ k ∈ ℕ ∧ sup T ℝ < + 1 k < x → sup T ℝ < + 1 ≤ sup T ℝ <
127 126 ex ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup T ℝ < + 1 k < x → sup T ℝ < + 1 ≤ sup T ℝ <
128 42 zcnd ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup T ℝ < ∈ ℂ
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 ⊢ sup T ℝ < ∈ ℂ ∧ 1 ∈ ℂ ∧ k ∈ ℂ ∧ k ≠ 0 → sup T ℝ < + 1 k = sup T ℝ < k + 1 k
135 128 129 133 134 syl3anc ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup T ℝ < + 1 k = sup T ℝ < k + 1 k
136 3 mptex ⊢ k ∈ ℕ ⟼ sup T ℝ < k ∈ V
137 2 fvmpt2 ⊢ x ∈ ℝ ∧ k ∈ ℕ ⟼ sup T ℝ < k ∈ V → F ⁡ x = k ∈ ℕ ⟼ sup T ℝ < k
138 136 137 mpan2 ⊢ x ∈ ℝ → F ⁡ x = k ∈ ℕ ⟼ sup T ℝ < k
139 138 fveq1d ⊢ x ∈ ℝ → F ⁡ x ⁡ k = k ∈ ℕ ⟼ sup T ℝ < k ⁡ k
140 ovex ⊢ sup T ℝ < k ∈ V
141 eqid ⊢ k ∈ ℕ ⟼ sup T ℝ < k = k ∈ ℕ ⟼ sup T ℝ < k
142 141 fvmpt2 ⊢ k ∈ ℕ ∧ sup T ℝ < k ∈ V → k ∈ ℕ ⟼ sup T ℝ < k ⁡ k = sup T ℝ < k
143 140 142 mpan2 ⊢ k ∈ ℕ → k ∈ ℕ ⟼ sup T ℝ < k ⁡ k = sup T ℝ < k
144 139 143 sylan9eq ⊢ x ∈ ℝ ∧ k ∈ ℕ → F ⁡ x ⁡ k = sup T ℝ < k
145 144 oveq1d ⊢ x ∈ ℝ ∧ k ∈ ℕ → F ⁡ x ⁡ k + 1 k = sup T ℝ < k + 1 k
146 135 145 eqtr4d ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup T ℝ < + 1 k = F ⁡ x ⁡ k + 1 k
147 146 breq1d ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup T ℝ < + 1 k < x ↔ F ⁡ x ⁡ k + 1 k < x
148 81 zred ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup T ℝ < + 1 ∈ ℝ
149 148 43 lenltd ⊢ x ∈ ℝ ∧ k ∈ ℕ → sup T ℝ < + 1 ≤ sup T ℝ < ↔ ¬ sup T ℝ < < sup T ℝ < + 1
150 127 147 149 3imtr3d ⊢ x ∈ ℝ ∧ k ∈ ℕ → F ⁡ x ⁡ k + 1 k < x → ¬ sup T ℝ < < sup T ℝ < + 1
151 150 adantlr ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x ∧ k ∈ ℕ → F ⁡ x ⁡ k + 1 k < x → ¬ sup T ℝ < < sup T ℝ < + 1
152 80 151 syld ⊢ x ∈ ℝ ∧ sup ran ⁡ F ⁡ x ℝ < < x ∧ k ∈ ℕ → 1 x − sup ran ⁡ F ⁡ x ℝ < < k → ¬ sup T ℝ < < sup T ℝ < + 1
153 152 exp31 ⊢ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < < x → k ∈ ℕ → 1 x − sup ran ⁡ F ⁡ x ℝ < < k → ¬ sup T ℝ < < sup T ℝ < + 1
154 153 com4l ⊢ sup ran ⁡ F ⁡ x ℝ < < x → k ∈ ℕ → 1 x − sup ran ⁡ F ⁡ x ℝ < < k → x ∈ ℝ → ¬ sup T ℝ < < sup T ℝ < + 1
155 154 com14 ⊢ x ∈ ℝ → k ∈ ℕ → 1 x − sup ran ⁡ F ⁡ x ℝ < < k → sup ran ⁡ F ⁡ x ℝ < < x → ¬ sup T ℝ < < sup T ℝ < + 1
156 155 3imp ⊢ x ∈ ℝ ∧ k ∈ ℕ ∧ 1 x − sup ran ⁡ F ⁡ x ℝ < < k → sup ran ⁡ F ⁡ x ℝ < < x → ¬ sup T ℝ < < sup T ℝ < + 1
157 45 156 mt2d ⊢ x ∈ ℝ ∧ k ∈ ℕ ∧ 1 x − sup ran ⁡ F ⁡ x ℝ < < k → ¬ sup ran ⁡ F ⁡ x ℝ < < x
158 157 rexlimdv3a ⊢ x ∈ ℝ → ∃ k ∈ ℕ 1 x − sup ran ⁡ F ⁡ x ℝ < < k → ¬ sup ran ⁡ F ⁡ x ℝ < < x
159 41 158 syld ⊢ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < < x → ¬ sup ran ⁡ F ⁡ x ℝ < < x
160 159 pm2.01d ⊢ x ∈ ℝ → ¬ sup ran ⁡ F ⁡ x ℝ < < x
161 eqlelt ⊢ sup ran ⁡ F ⁡ x ℝ < ∈ ℝ ∧ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < = x ↔ sup ran ⁡ F ⁡ x ℝ < ≤ x ∧ ¬ sup ran ⁡ F ⁡ x ℝ < < x
162 30 161 mpancom ⊢ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < = x ↔ sup ran ⁡ F ⁡ x ℝ < ≤ x ∧ ¬ sup ran ⁡ F ⁡ x ℝ < < x
163 29 160 162 mpbir2and ⊢ x ∈ ℝ → sup ran ⁡ F ⁡ x ℝ < = x