| Step | Hyp | Ref
| Expression |
| 1 | | lmnn.4 |
. 2
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
| 2 | | rpreccl 13061 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) |
| 3 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ+) |
| 4 | 3 | rpred 13077 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ) |
| 5 | 3 | rpge0d 13081 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤ (1
/ 𝑥)) |
| 6 | | flge0nn0 13860 |
. . . . . 6
⊢ (((1 /
𝑥) ∈ ℝ ∧ 0
≤ (1 / 𝑥)) →
(⌊‘(1 / 𝑥))
∈ ℕ0) |
| 7 | 4, 5, 6 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘(1 / 𝑥))
∈ ℕ0) |
| 8 | | nn0p1nn 12565 |
. . . . 5
⊢
((⌊‘(1 / 𝑥)) ∈ ℕ0 →
((⌊‘(1 / 𝑥)) +
1) ∈ ℕ) |
| 9 | 7, 8 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘(1 / 𝑥)) +
1) ∈ ℕ) |
| 10 | | lmnn.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
| 11 | 10 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → 𝐷 ∈ (∞Met‘𝑋)) |
| 12 | | lmnn.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ⟶𝑋) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → 𝐹:ℕ⟶𝑋) |
| 14 | | eluznn 12960 |
. . . . . . . . 9
⊢
((((⌊‘(1 / 𝑥)) + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → 𝑘 ∈ ℕ) |
| 15 | 9, 14 | sylan 580 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → 𝑘 ∈ ℕ) |
| 16 | 13, 15 | ffvelcdmd 7105 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → (𝐹‘𝑘) ∈ 𝑋) |
| 17 | 1 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → 𝑃 ∈ 𝑋) |
| 18 | | xmetcl 24341 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝐹‘𝑘)𝐷𝑃) ∈
ℝ*) |
| 19 | 11, 16, 17, 18 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → ((𝐹‘𝑘)𝐷𝑃) ∈
ℝ*) |
| 20 | 15 | nnrecred 12317 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → (1 / 𝑘) ∈ ℝ) |
| 21 | 20 | rexrd 11311 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → (1 / 𝑘) ∈
ℝ*) |
| 22 | | rpxr 13044 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
| 23 | 22 | ad2antlr 727 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → 𝑥 ∈ ℝ*) |
| 24 | | lmnn.6 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷𝑃) < (1 / 𝑘)) |
| 25 | 24 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷𝑃) < (1 / 𝑘)) |
| 26 | 15, 25 | syldan 591 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → ((𝐹‘𝑘)𝐷𝑃) < (1 / 𝑘)) |
| 27 | 4 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → (1 / 𝑥) ∈ ℝ) |
| 28 | 9 | nnred 12281 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘(1 / 𝑥)) +
1) ∈ ℝ) |
| 29 | 28 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → ((⌊‘(1 / 𝑥)) + 1) ∈
ℝ) |
| 30 | 15 | nnred 12281 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → 𝑘 ∈ ℝ) |
| 31 | | flltp1 13840 |
. . . . . . . . 9
⊢ ((1 /
𝑥) ∈ ℝ → (1
/ 𝑥) <
((⌊‘(1 / 𝑥)) +
1)) |
| 32 | 27, 31 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → (1 / 𝑥) < ((⌊‘(1 / 𝑥)) + 1)) |
| 33 | | eluzle 12891 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1)) → ((⌊‘(1 / 𝑥)) + 1) ≤ 𝑘) |
| 34 | 33 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → ((⌊‘(1 / 𝑥)) + 1) ≤ 𝑘) |
| 35 | 27, 29, 30, 32, 34 | ltletrd 11421 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → (1 / 𝑥) < 𝑘) |
| 36 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → 𝑥 ∈ ℝ+) |
| 37 | | rpregt0 13049 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
| 38 | | nnrp 13046 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
| 39 | 38 | rpregt0d 13083 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
| 40 | | ltrec1 12155 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 0 <
𝑥) ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → ((1 / 𝑥) < 𝑘 ↔ (1 / 𝑘) < 𝑥)) |
| 41 | 37, 39, 40 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
→ ((1 / 𝑥) < 𝑘 ↔ (1 / 𝑘) < 𝑥)) |
| 42 | 36, 15, 41 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → ((1 / 𝑥) < 𝑘 ↔ (1 / 𝑘) < 𝑥)) |
| 43 | 35, 42 | mpbid 232 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → (1 / 𝑘) < 𝑥) |
| 44 | 19, 21, 23, 26, 43 | xrlttrd 13201 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) → ((𝐹‘𝑘)𝐷𝑃) < 𝑥) |
| 45 | 44 | ralrimiva 3146 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))((𝐹‘𝑘)𝐷𝑃) < 𝑥) |
| 46 | | fveq2 6906 |
. . . . . 6
⊢ (𝑗 = ((⌊‘(1 / 𝑥)) + 1) →
(ℤ≥‘𝑗) =
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))) |
| 47 | 46 | raleqdv 3326 |
. . . . 5
⊢ (𝑗 = ((⌊‘(1 / 𝑥)) + 1) → (∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)𝐷𝑃) < 𝑥 ↔ ∀𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))((𝐹‘𝑘)𝐷𝑃) < 𝑥)) |
| 48 | 47 | rspcev 3622 |
. . . 4
⊢
((((⌊‘(1 / 𝑥)) + 1) ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘((⌊‘(1 / 𝑥)) + 1))((𝐹‘𝑘)𝐷𝑃) < 𝑥) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘)𝐷𝑃) < 𝑥) |
| 49 | 9, 45, 48 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)𝐷𝑃) < 𝑥) |
| 50 | 49 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)𝐷𝑃) < 𝑥) |
| 51 | | lmnn.2 |
. . 3
⊢ 𝐽 = (MetOpen‘𝐷) |
| 52 | | nnuz 12921 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
| 53 | | 1zzd 12648 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
| 54 | | eqidd 2738 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
| 55 | 51, 10, 52, 53, 54, 12 | lmmbrf 25296 |
. 2
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)𝐷𝑃) < 𝑥))) |
| 56 | 1, 50, 55 | mpbir2and 713 |
1
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) |