| Step | Hyp | Ref
| Expression |
| 1 | | rpnnen1lem.1 |
. . . 4
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} |
| 2 | | rpnnen1lem.2 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) |
| 3 | | rpnnen1lem.n |
. . . 4
⊢ ℕ
∈ V |
| 4 | | rpnnen1lem.q |
. . . 4
⊢ ℚ
∈ V |
| 5 | 1, 2, 3, 4 | rpnnen1lem3 13021 |
. . 3
⊢ (𝑥 ∈ ℝ →
∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥) |
| 6 | 1, 2, 3, 4 | rpnnen1lem1 13020 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) ∈ (ℚ ↑m
ℕ)) |
| 7 | 4, 3 | elmap 8911 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ (ℚ ↑m ℕ)
↔ (𝐹‘𝑥):ℕ⟶ℚ) |
| 8 | 6, 7 | sylib 218 |
. . . . 5
⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥):ℕ⟶ℚ) |
| 9 | | frn 6743 |
. . . . . 6
⊢ ((𝐹‘𝑥):ℕ⟶ℚ → ran (𝐹‘𝑥) ⊆ ℚ) |
| 10 | | qssre 13001 |
. . . . . 6
⊢ ℚ
⊆ ℝ |
| 11 | 9, 10 | sstrdi 3996 |
. . . . 5
⊢ ((𝐹‘𝑥):ℕ⟶ℚ → ran (𝐹‘𝑥) ⊆ ℝ) |
| 12 | 8, 11 | syl 17 |
. . . 4
⊢ (𝑥 ∈ ℝ → ran
(𝐹‘𝑥) ⊆ ℝ) |
| 13 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 14 | 13 | ne0ii 4344 |
. . . . . . 7
⊢ ℕ
≠ ∅ |
| 15 | | fdm 6745 |
. . . . . . . 8
⊢ ((𝐹‘𝑥):ℕ⟶ℚ → dom (𝐹‘𝑥) = ℕ) |
| 16 | 15 | neeq1d 3000 |
. . . . . . 7
⊢ ((𝐹‘𝑥):ℕ⟶ℚ → (dom (𝐹‘𝑥) ≠ ∅ ↔ ℕ ≠
∅)) |
| 17 | 14, 16 | mpbiri 258 |
. . . . . 6
⊢ ((𝐹‘𝑥):ℕ⟶ℚ → dom (𝐹‘𝑥) ≠ ∅) |
| 18 | | dm0rn0 5935 |
. . . . . . 7
⊢ (dom
(𝐹‘𝑥) = ∅ ↔ ran (𝐹‘𝑥) = ∅) |
| 19 | 18 | necon3bii 2993 |
. . . . . 6
⊢ (dom
(𝐹‘𝑥) ≠ ∅ ↔ ran (𝐹‘𝑥) ≠ ∅) |
| 20 | 17, 19 | sylib 218 |
. . . . 5
⊢ ((𝐹‘𝑥):ℕ⟶ℚ → ran (𝐹‘𝑥) ≠ ∅) |
| 21 | 8, 20 | syl 17 |
. . . 4
⊢ (𝑥 ∈ ℝ → ran
(𝐹‘𝑥) ≠ ∅) |
| 22 | | breq2 5147 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝑛 ≤ 𝑦 ↔ 𝑛 ≤ 𝑥)) |
| 23 | 22 | ralbidv 3178 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑦 ↔ ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥)) |
| 24 | 23 | rspcev 3622 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧
∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑦) |
| 25 | 5, 24 | mpdan 687 |
. . . 4
⊢ (𝑥 ∈ ℝ →
∃𝑦 ∈ ℝ
∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑦) |
| 26 | | id 22 |
. . . 4
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ) |
| 27 | | suprleub 12234 |
. . . 4
⊢ (((ran
(𝐹‘𝑥) ⊆ ℝ ∧ ran (𝐹‘𝑥) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑦) ∧ 𝑥 ∈ ℝ) → (sup(ran (𝐹‘𝑥), ℝ, < ) ≤ 𝑥 ↔ ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥)) |
| 28 | 12, 21, 25, 26, 27 | syl31anc 1375 |
. . 3
⊢ (𝑥 ∈ ℝ → (sup(ran
(𝐹‘𝑥), ℝ, < ) ≤ 𝑥 ↔ ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥)) |
| 29 | 5, 28 | mpbird 257 |
. 2
⊢ (𝑥 ∈ ℝ → sup(ran
(𝐹‘𝑥), ℝ, < ) ≤ 𝑥) |
| 30 | 1, 2, 3, 4 | rpnnen1lem4 13022 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → sup(ran
(𝐹‘𝑥), ℝ, < ) ∈
ℝ) |
| 31 | | resubcl 11573 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) ∈ ℝ) →
(𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )) ∈
ℝ) |
| 32 | 30, 31 | mpdan 687 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )) ∈
ℝ) |
| 33 | 32 | adantr 480 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) → (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )) ∈
ℝ) |
| 34 | | posdif 11756 |
. . . . . . . . . 10
⊢ ((sup(ran
(𝐹‘𝑥), ℝ, < ) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥 ↔ 0 < (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )))) |
| 35 | 30, 34 | mpancom 688 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥 ↔ 0 < (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )))) |
| 36 | 35 | biimpa 476 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) → 0 < (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) |
| 37 | 36 | gt0ne0d 11827 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) → (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )) ≠ 0) |
| 38 | 33, 37 | rereccld 12094 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) → (1 / (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) ∈
ℝ) |
| 39 | | arch 12523 |
. . . . . 6
⊢ ((1 /
(𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) ∈ ℝ →
∃𝑘 ∈ ℕ (1
/ (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘) |
| 40 | 38, 39 | syl 17 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) → ∃𝑘 ∈ ℕ (1 / (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘) |
| 41 | 40 | ex 412 |
. . . 4
⊢ (𝑥 ∈ ℝ → (sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥 → ∃𝑘 ∈ ℕ (1 / (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘)) |
| 42 | 1, 2 | rpnnen1lem2 13019 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
sup(𝑇, ℝ, < )
∈ ℤ) |
| 43 | 42 | zred 12722 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
sup(𝑇, ℝ, < )
∈ ℝ) |
| 44 | 43 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ∧ (1 /
(𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘) → sup(𝑇, ℝ, < ) ∈
ℝ) |
| 45 | 44 | ltp1d 12198 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ∧ (1 /
(𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘) → sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) +
1)) |
| 46 | 33, 36 | jca 511 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) → ((𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )) ∈ ℝ ∧ 0
< (𝑥 − sup(ran
(𝐹‘𝑥), ℝ, < )))) |
| 47 | | nnre 12273 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
| 48 | | nngt0 12297 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
| 49 | 47, 48 | jca 511 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
| 50 | | ltrec1 12155 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )) ∈ ℝ ∧ 0
< (𝑥 − sup(ran
(𝐹‘𝑥), ℝ, < ))) ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → ((1 / (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘 ↔ (1 / 𝑘) < (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )))) |
| 51 | 46, 49, 50 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) ∧ 𝑘 ∈ ℕ) → ((1 / (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘 ↔ (1 / 𝑘) < (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )))) |
| 52 | 30 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) ∧ 𝑘 ∈ ℕ) → sup(ran (𝐹‘𝑥), ℝ, < ) ∈
ℝ) |
| 53 | | nnrecre 12308 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
| 54 | 53 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℝ) |
| 55 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈ ℝ) |
| 56 | 52, 54, 55 | ltaddsub2d 11864 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) ∧ 𝑘 ∈ ℕ) → ((sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) < 𝑥 ↔ (1 / 𝑘) < (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )))) |
| 57 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ran
(𝐹‘𝑥) ⊆ ℝ) |
| 58 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑥):ℕ⟶ℚ → (𝐹‘𝑥) Fn ℕ) |
| 59 | 8, 58 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) Fn ℕ) |
| 60 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑥) Fn ℕ ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥)‘𝑘) ∈ ran (𝐹‘𝑥)) |
| 61 | 59, 60 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥)‘𝑘) ∈ ran (𝐹‘𝑥)) |
| 62 | 57, 61 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥)‘𝑘) ∈ ℝ) |
| 63 | 30 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → sup(ran
(𝐹‘𝑥), ℝ, < ) ∈
ℝ) |
| 64 | 53 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (1 /
𝑘) ∈
ℝ) |
| 65 | 12, 21, 25 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → (ran
(𝐹‘𝑥) ⊆ ℝ ∧ ran (𝐹‘𝑥) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑦)) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (ran
(𝐹‘𝑥) ⊆ ℝ ∧ ran (𝐹‘𝑥) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑦)) |
| 67 | | suprub 12229 |
. . . . . . . . . . . . . . . . 17
⊢ (((ran
(𝐹‘𝑥) ⊆ ℝ ∧ ran (𝐹‘𝑥) ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑦) ∧ ((𝐹‘𝑥)‘𝑘) ∈ ran (𝐹‘𝑥)) → ((𝐹‘𝑥)‘𝑘) ≤ sup(ran (𝐹‘𝑥), ℝ, < )) |
| 68 | 66, 61, 67 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥)‘𝑘) ≤ sup(ran (𝐹‘𝑥), ℝ, < )) |
| 69 | 62, 63, 64, 68 | leadd1dd 11877 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) ≤ (sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘))) |
| 70 | 62, 64 | readdcld 11290 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) ∈ ℝ) |
| 71 | | readdcl 11238 |
. . . . . . . . . . . . . . . . 17
⊢ ((sup(ran
(𝐹‘𝑥), ℝ, < ) ∈ ℝ ∧ (1 /
𝑘) ∈ ℝ) →
(sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) ∈
ℝ) |
| 72 | 30, 53, 71 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (sup(ran
(𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) ∈ ℝ) |
| 73 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → 𝑥 ∈
ℝ) |
| 74 | | lelttr 11351 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) ∈ ℝ ∧ (sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) ≤ (sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) ∧ (sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) < 𝑥) → (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) < 𝑥)) |
| 75 | 74 | expd 415 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) ∈ ℝ ∧ (sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) ≤ (sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) → ((sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) < 𝑥 → (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) < 𝑥))) |
| 76 | 70, 72, 73, 75 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
((((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) ≤ (sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) → ((sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) < 𝑥 → (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) < 𝑥))) |
| 77 | 69, 76 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
((sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) < 𝑥 → (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) < 𝑥)) |
| 78 | 77 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) ∧ 𝑘 ∈ ℕ) → ((sup(ran (𝐹‘𝑥), ℝ, < ) + (1 / 𝑘)) < 𝑥 → (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) < 𝑥)) |
| 79 | 56, 78 | sylbird 260 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑘) < (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < )) → (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) < 𝑥)) |
| 80 | 51, 79 | sylbid 240 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) ∧ 𝑘 ∈ ℕ) → ((1 / (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘 → (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) < 𝑥)) |
| 81 | 42 | peano2zd 12725 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
(sup(𝑇, ℝ, < ) +
1) ∈ ℤ) |
| 82 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (sup(𝑇, ℝ, < ) + 1) → (𝑛 / 𝑘) = ((sup(𝑇, ℝ, < ) + 1) / 𝑘)) |
| 83 | 82 | breq1d 5153 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (sup(𝑇, ℝ, < ) + 1) → ((𝑛 / 𝑘) < 𝑥 ↔ ((sup(𝑇, ℝ, < ) + 1) / 𝑘) < 𝑥)) |
| 84 | 83, 1 | elrab2 3695 |
. . . . . . . . . . . . . . . . 17
⊢
((sup(𝑇, ℝ,
< ) + 1) ∈ 𝑇 ↔
((sup(𝑇, ℝ, < ) +
1) ∈ ℤ ∧ ((sup(𝑇, ℝ, < ) + 1) / 𝑘) < 𝑥)) |
| 85 | 84 | biimpri 228 |
. . . . . . . . . . . . . . . 16
⊢
(((sup(𝑇, ℝ,
< ) + 1) ∈ ℤ ∧ ((sup(𝑇, ℝ, < ) + 1) / 𝑘) < 𝑥) → (sup(𝑇, ℝ, < ) + 1) ∈ 𝑇) |
| 86 | 81, 85 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧
((sup(𝑇, ℝ, < ) +
1) / 𝑘) < 𝑥) → (sup(𝑇, ℝ, < ) + 1) ∈ 𝑇) |
| 87 | | ssrab2 4080 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} ⊆ ℤ |
| 88 | 1, 87 | eqsstri 4030 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 ⊆
ℤ |
| 89 | | zssre 12620 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℤ
⊆ ℝ |
| 90 | 88, 89 | sstri 3993 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑇 ⊆
ℝ |
| 91 | 90 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → 𝑇 ⊆
ℝ) |
| 92 | | remulcl 11240 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑘 · 𝑥) ∈ ℝ) |
| 93 | 92 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑘 · 𝑥) ∈ ℝ) |
| 94 | 47, 93 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑘 · 𝑥) ∈ ℝ) |
| 95 | | btwnz 12721 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 · 𝑥) ∈ ℝ → (∃𝑛 ∈ ℤ 𝑛 < (𝑘 · 𝑥) ∧ ∃𝑛 ∈ ℤ (𝑘 · 𝑥) < 𝑛)) |
| 96 | 95 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 · 𝑥) ∈ ℝ → ∃𝑛 ∈ ℤ 𝑛 < (𝑘 · 𝑥)) |
| 97 | 94, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
∃𝑛 ∈ ℤ
𝑛 < (𝑘 · 𝑥)) |
| 98 | | zre 12617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℝ) |
| 99 | 98 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈
ℝ) |
| 100 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → 𝑥 ∈
ℝ) |
| 101 | 49 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
| 102 | | ltdivmul 12143 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → ((𝑛 / 𝑘) < 𝑥 ↔ 𝑛 < (𝑘 · 𝑥))) |
| 103 | 99, 100, 101, 102 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → ((𝑛 / 𝑘) < 𝑥 ↔ 𝑛 < (𝑘 · 𝑥))) |
| 104 | 103 | rexbidva 3177 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
(∃𝑛 ∈ ℤ
(𝑛 / 𝑘) < 𝑥 ↔ ∃𝑛 ∈ ℤ 𝑛 < (𝑘 · 𝑥))) |
| 105 | 97, 104 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
∃𝑛 ∈ ℤ
(𝑛 / 𝑘) < 𝑥) |
| 106 | | rabn0 4389 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} ≠ ∅ ↔ ∃𝑛 ∈ ℤ (𝑛 / 𝑘) < 𝑥) |
| 107 | 105, 106 | sylibr 234 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} ≠ ∅) |
| 108 | 1 | neeq1i 3005 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ≠ ∅ ↔ {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} ≠ ∅) |
| 109 | 107, 108 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → 𝑇 ≠ ∅) |
| 110 | 1 | reqabi 3460 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ 𝑇 ↔ (𝑛 ∈ ℤ ∧ (𝑛 / 𝑘) < 𝑥)) |
| 111 | 47 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → 𝑘 ∈
ℝ) |
| 112 | 111, 100,
92 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑘 · 𝑥) ∈ ℝ) |
| 113 | | ltle 11349 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ ℝ ∧ (𝑘 · 𝑥) ∈ ℝ) → (𝑛 < (𝑘 · 𝑥) → 𝑛 ≤ (𝑘 · 𝑥))) |
| 114 | 99, 112, 113 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑛 < (𝑘 · 𝑥) → 𝑛 ≤ (𝑘 · 𝑥))) |
| 115 | 103, 114 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → ((𝑛 / 𝑘) < 𝑥 → 𝑛 ≤ (𝑘 · 𝑥))) |
| 116 | 115 | impr 454 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ ℤ ∧ (𝑛 / 𝑘) < 𝑥)) → 𝑛 ≤ (𝑘 · 𝑥)) |
| 117 | 110, 116 | sylan2b 594 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑇) → 𝑛 ≤ (𝑘 · 𝑥)) |
| 118 | 117 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
∀𝑛 ∈ 𝑇 𝑛 ≤ (𝑘 · 𝑥)) |
| 119 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑘 · 𝑥) → (𝑛 ≤ 𝑦 ↔ 𝑛 ≤ (𝑘 · 𝑥))) |
| 120 | 119 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑘 · 𝑥) → (∀𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑇 𝑛 ≤ (𝑘 · 𝑥))) |
| 121 | 120 | rspcev 3622 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑘 · 𝑥) ∈ ℝ ∧ ∀𝑛 ∈ 𝑇 𝑛 ≤ (𝑘 · 𝑥)) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑇 𝑛 ≤ 𝑦) |
| 122 | 94, 118, 121 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
∃𝑦 ∈ ℝ
∀𝑛 ∈ 𝑇 𝑛 ≤ 𝑦) |
| 123 | 91, 109, 122 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑇 𝑛 ≤ 𝑦)) |
| 124 | | suprub 12229 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑇 𝑛 ≤ 𝑦) ∧ (sup(𝑇, ℝ, < ) + 1) ∈ 𝑇) → (sup(𝑇, ℝ, < ) + 1) ≤ sup(𝑇, ℝ, <
)) |
| 125 | 123, 124 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧
(sup(𝑇, ℝ, < ) +
1) ∈ 𝑇) →
(sup(𝑇, ℝ, < ) +
1) ≤ sup(𝑇, ℝ,
< )) |
| 126 | 86, 125 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧
((sup(𝑇, ℝ, < ) +
1) / 𝑘) < 𝑥) → (sup(𝑇, ℝ, < ) + 1) ≤ sup(𝑇, ℝ, <
)) |
| 127 | 126 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
(((sup(𝑇, ℝ, < ) +
1) / 𝑘) < 𝑥 → (sup(𝑇, ℝ, < ) + 1) ≤ sup(𝑇, ℝ, <
))) |
| 128 | 42 | zcnd 12723 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
sup(𝑇, ℝ, < )
∈ ℂ) |
| 129 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → 1 ∈
ℂ) |
| 130 | | nncn 12274 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
| 131 | | nnne0 12300 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
| 132 | 130, 131 | jca 511 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0)) |
| 133 | 132 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0)) |
| 134 | | divdir 11947 |
. . . . . . . . . . . . . . . 16
⊢
((sup(𝑇, ℝ,
< ) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0)) → ((sup(𝑇, ℝ, < ) + 1) / 𝑘) = ((sup(𝑇, ℝ, < ) / 𝑘) + (1 / 𝑘))) |
| 135 | 128, 129,
133, 134 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
((sup(𝑇, ℝ, < ) +
1) / 𝑘) = ((sup(𝑇, ℝ, < ) / 𝑘) + (1 / 𝑘))) |
| 136 | 3 | mptex 7243 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ ↦
(sup(𝑇, ℝ, < ) /
𝑘)) ∈
V |
| 137 | 2 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ (𝑘 ∈ ℕ ↦
(sup(𝑇, ℝ, < ) /
𝑘)) ∈ V) → (𝐹‘𝑥) = (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) |
| 138 | 136, 137 | mpan2 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) = (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) |
| 139 | 138 | fveq1d 6908 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → ((𝐹‘𝑥)‘𝑘) = ((𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))‘𝑘)) |
| 140 | | ovex 7464 |
. . . . . . . . . . . . . . . . . 18
⊢
(sup(𝑇, ℝ,
< ) / 𝑘) ∈
V |
| 141 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ ↦
(sup(𝑇, ℝ, < ) /
𝑘)) = (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)) |
| 142 | 141 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ ∧ (sup(𝑇, ℝ, < ) / 𝑘) ∈ V) → ((𝑘 ∈ ℕ ↦
(sup(𝑇, ℝ, < ) /
𝑘))‘𝑘) = (sup(𝑇, ℝ, < ) / 𝑘)) |
| 143 | 140, 142 | mpan2 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(sup(𝑇, ℝ, < ) /
𝑘))‘𝑘) = (sup(𝑇, ℝ, < ) / 𝑘)) |
| 144 | 139, 143 | sylan9eq 2797 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥)‘𝑘) = (sup(𝑇, ℝ, < ) / 𝑘)) |
| 145 | 144 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) = ((sup(𝑇, ℝ, < ) / 𝑘) + (1 / 𝑘))) |
| 146 | 135, 145 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
((sup(𝑇, ℝ, < ) +
1) / 𝑘) = (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘))) |
| 147 | 146 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
(((sup(𝑇, ℝ, < ) +
1) / 𝑘) < 𝑥 ↔ (((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) < 𝑥)) |
| 148 | 81 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
(sup(𝑇, ℝ, < ) +
1) ∈ ℝ) |
| 149 | 148, 43 | lenltd 11407 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
((sup(𝑇, ℝ, < ) +
1) ≤ sup(𝑇, ℝ,
< ) ↔ ¬ sup(𝑇,
ℝ, < ) < (sup(𝑇, ℝ, < ) + 1))) |
| 150 | 127, 147,
149 | 3imtr3d 293 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
((((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) < 𝑥 → ¬ sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) +
1))) |
| 151 | 150 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) ∧ 𝑘 ∈ ℕ) → ((((𝐹‘𝑥)‘𝑘) + (1 / 𝑘)) < 𝑥 → ¬ sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) +
1))) |
| 152 | 80, 151 | syld 47 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥) ∧ 𝑘 ∈ ℕ) → ((1 / (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘 → ¬ sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) +
1))) |
| 153 | 152 | exp31 419 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥 → (𝑘 ∈ ℕ → ((1 / (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘 → ¬ sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) +
1))))) |
| 154 | 153 | com4l 92 |
. . . . . . . 8
⊢ (sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥 → (𝑘 ∈ ℕ → ((1 / (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘 → (𝑥 ∈ ℝ → ¬ sup(𝑇, ℝ, < ) <
(sup(𝑇, ℝ, < ) +
1))))) |
| 155 | 154 | com14 96 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (𝑘 ∈ ℕ → ((1 /
(𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘 → (sup(ran (𝐹‘𝑥), ℝ, < ) < 𝑥 → ¬ sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) +
1))))) |
| 156 | 155 | 3imp 1111 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ∧ (1 /
(𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘) → (sup(ran (𝐹‘𝑥), ℝ, < ) < 𝑥 → ¬ sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) +
1))) |
| 157 | 45, 156 | mt2d 136 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ∧ (1 /
(𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘) → ¬ sup(ran (𝐹‘𝑥), ℝ, < ) < 𝑥) |
| 158 | 157 | rexlimdv3a 3159 |
. . . 4
⊢ (𝑥 ∈ ℝ →
(∃𝑘 ∈ ℕ (1
/ (𝑥 − sup(ran (𝐹‘𝑥), ℝ, < ))) < 𝑘 → ¬ sup(ran (𝐹‘𝑥), ℝ, < ) < 𝑥)) |
| 159 | 41, 158 | syld 47 |
. . 3
⊢ (𝑥 ∈ ℝ → (sup(ran
(𝐹‘𝑥), ℝ, < ) < 𝑥 → ¬ sup(ran (𝐹‘𝑥), ℝ, < ) < 𝑥)) |
| 160 | 159 | pm2.01d 190 |
. 2
⊢ (𝑥 ∈ ℝ → ¬
sup(ran (𝐹‘𝑥), ℝ, < ) < 𝑥) |
| 161 | | eqlelt 11348 |
. . 3
⊢ ((sup(ran
(𝐹‘𝑥), ℝ, < ) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (sup(ran
(𝐹‘𝑥), ℝ, < ) = 𝑥 ↔ (sup(ran (𝐹‘𝑥), ℝ, < ) ≤ 𝑥 ∧ ¬ sup(ran (𝐹‘𝑥), ℝ, < ) < 𝑥))) |
| 162 | 30, 161 | mpancom 688 |
. 2
⊢ (𝑥 ∈ ℝ → (sup(ran
(𝐹‘𝑥), ℝ, < ) = 𝑥 ↔ (sup(ran (𝐹‘𝑥), ℝ, < ) ≤ 𝑥 ∧ ¬ sup(ran (𝐹‘𝑥), ℝ, < ) < 𝑥))) |
| 163 | 29, 160, 162 | mpbir2and 713 |
1
⊢ (𝑥 ∈ ℝ → sup(ran
(𝐹‘𝑥), ℝ, < ) = 𝑥) |