Step | Hyp | Ref
| Expression |
1 | | rpnnen1lem.n |
. . . . . . . 8
⊢ ℕ
∈ V |
2 | 1 | mptex 6999 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ ↦
(sup(𝑇, ℝ, < ) /
𝑘)) ∈
V |
3 | | rpnnen1lem.2 |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) |
4 | 3 | fvmpt2 6789 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ (𝑘 ∈ ℕ ↦
(sup(𝑇, ℝ, < ) /
𝑘)) ∈ V) → (𝐹‘𝑥) = (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) |
5 | 2, 4 | mpan2 691 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) = (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) |
6 | 5 | fveq1d 6679 |
. . . . 5
⊢ (𝑥 ∈ ℝ → ((𝐹‘𝑥)‘𝑘) = ((𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))‘𝑘)) |
7 | | ovex 7206 |
. . . . . 6
⊢
(sup(𝑇, ℝ,
< ) / 𝑘) ∈
V |
8 | | eqid 2739 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ ↦
(sup(𝑇, ℝ, < ) /
𝑘)) = (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘)) |
9 | 8 | fvmpt2 6789 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧ (sup(𝑇, ℝ, < ) / 𝑘) ∈ V) → ((𝑘 ∈ ℕ ↦
(sup(𝑇, ℝ, < ) /
𝑘))‘𝑘) = (sup(𝑇, ℝ, < ) / 𝑘)) |
10 | 7, 9 | mpan2 691 |
. . . . 5
⊢ (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦
(sup(𝑇, ℝ, < ) /
𝑘))‘𝑘) = (sup(𝑇, ℝ, < ) / 𝑘)) |
11 | 6, 10 | sylan9eq 2794 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥)‘𝑘) = (sup(𝑇, ℝ, < ) / 𝑘)) |
12 | | rpnnen1lem.1 |
. . . . . . . . 9
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} |
13 | 12 | rabeq2i 3390 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑇 ↔ (𝑛 ∈ ℤ ∧ (𝑛 / 𝑘) < 𝑥)) |
14 | | zre 12069 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℝ) |
15 | 14 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈
ℝ) |
16 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → 𝑥 ∈
ℝ) |
17 | | nnre 11726 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
18 | | nngt0 11750 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
19 | 17, 18 | jca 515 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
20 | 19 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
21 | | ltdivmul 11596 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → ((𝑛 / 𝑘) < 𝑥 ↔ 𝑛 < (𝑘 · 𝑥))) |
22 | 15, 16, 20, 21 | syl3anc 1372 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → ((𝑛 / 𝑘) < 𝑥 ↔ 𝑛 < (𝑘 · 𝑥))) |
23 | 17 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → 𝑘 ∈
ℝ) |
24 | | remulcl 10703 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑘 · 𝑥) ∈ ℝ) |
25 | 23, 16, 24 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑘 · 𝑥) ∈ ℝ) |
26 | | ltle 10810 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℝ ∧ (𝑘 · 𝑥) ∈ ℝ) → (𝑛 < (𝑘 · 𝑥) → 𝑛 ≤ (𝑘 · 𝑥))) |
27 | 15, 25, 26 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → (𝑛 < (𝑘 · 𝑥) → 𝑛 ≤ (𝑘 · 𝑥))) |
28 | 22, 27 | sylbid 243 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ ℤ) → ((𝑛 / 𝑘) < 𝑥 → 𝑛 ≤ (𝑘 · 𝑥))) |
29 | 28 | impr 458 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ ℤ ∧ (𝑛 / 𝑘) < 𝑥)) → 𝑛 ≤ (𝑘 · 𝑥)) |
30 | 13, 29 | sylan2b 597 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝑇) → 𝑛 ≤ (𝑘 · 𝑥)) |
31 | 30 | ralrimiva 3097 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
∀𝑛 ∈ 𝑇 𝑛 ≤ (𝑘 · 𝑥)) |
32 | | ssrab2 3970 |
. . . . . . . . . 10
⊢ {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} ⊆ ℤ |
33 | 12, 32 | eqsstri 3912 |
. . . . . . . . 9
⊢ 𝑇 ⊆
ℤ |
34 | | zssre 12072 |
. . . . . . . . 9
⊢ ℤ
⊆ ℝ |
35 | 33, 34 | sstri 3887 |
. . . . . . . 8
⊢ 𝑇 ⊆
ℝ |
36 | 35 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → 𝑇 ⊆
ℝ) |
37 | 24 | ancoms 462 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑘 · 𝑥) ∈ ℝ) |
38 | 17, 37 | sylan2 596 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑘 · 𝑥) ∈ ℝ) |
39 | | btwnz 12168 |
. . . . . . . . . . . 12
⊢ ((𝑘 · 𝑥) ∈ ℝ → (∃𝑛 ∈ ℤ 𝑛 < (𝑘 · 𝑥) ∧ ∃𝑛 ∈ ℤ (𝑘 · 𝑥) < 𝑛)) |
40 | 39 | simpld 498 |
. . . . . . . . . . 11
⊢ ((𝑘 · 𝑥) ∈ ℝ → ∃𝑛 ∈ ℤ 𝑛 < (𝑘 · 𝑥)) |
41 | 38, 40 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
∃𝑛 ∈ ℤ
𝑛 < (𝑘 · 𝑥)) |
42 | 22 | rexbidva 3207 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
(∃𝑛 ∈ ℤ
(𝑛 / 𝑘) < 𝑥 ↔ ∃𝑛 ∈ ℤ 𝑛 < (𝑘 · 𝑥))) |
43 | 41, 42 | mpbird 260 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
∃𝑛 ∈ ℤ
(𝑛 / 𝑘) < 𝑥) |
44 | | rabn0 4275 |
. . . . . . . . 9
⊢ ({𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} ≠ ∅ ↔ ∃𝑛 ∈ ℤ (𝑛 / 𝑘) < 𝑥) |
45 | 43, 44 | sylibr 237 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} ≠ ∅) |
46 | 12 | neeq1i 2999 |
. . . . . . . 8
⊢ (𝑇 ≠ ∅ ↔ {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} ≠ ∅) |
47 | 45, 46 | sylibr 237 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → 𝑇 ≠ ∅) |
48 | | breq2 5035 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑘 · 𝑥) → (𝑛 ≤ 𝑦 ↔ 𝑛 ≤ (𝑘 · 𝑥))) |
49 | 48 | ralbidv 3110 |
. . . . . . . . 9
⊢ (𝑦 = (𝑘 · 𝑥) → (∀𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ↔ ∀𝑛 ∈ 𝑇 𝑛 ≤ (𝑘 · 𝑥))) |
50 | 49 | rspcev 3527 |
. . . . . . . 8
⊢ (((𝑘 · 𝑥) ∈ ℝ ∧ ∀𝑛 ∈ 𝑇 𝑛 ≤ (𝑘 · 𝑥)) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑇 𝑛 ≤ 𝑦) |
51 | 38, 31, 50 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
∃𝑦 ∈ ℝ
∀𝑛 ∈ 𝑇 𝑛 ≤ 𝑦) |
52 | | suprleub 11687 |
. . . . . . 7
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑇 𝑛 ≤ 𝑦) ∧ (𝑘 · 𝑥) ∈ ℝ) → (sup(𝑇, ℝ, < ) ≤ (𝑘 · 𝑥) ↔ ∀𝑛 ∈ 𝑇 𝑛 ≤ (𝑘 · 𝑥))) |
53 | 36, 47, 51, 38, 52 | syl31anc 1374 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
(sup(𝑇, ℝ, < )
≤ (𝑘 · 𝑥) ↔ ∀𝑛 ∈ 𝑇 𝑛 ≤ (𝑘 · 𝑥))) |
54 | 31, 53 | mpbird 260 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
sup(𝑇, ℝ, < ) ≤
(𝑘 · 𝑥)) |
55 | 12, 3 | rpnnen1lem2 12462 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
sup(𝑇, ℝ, < )
∈ ℤ) |
56 | 55 | zred 12171 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
sup(𝑇, ℝ, < )
∈ ℝ) |
57 | | simpl 486 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → 𝑥 ∈
ℝ) |
58 | 19 | adantl 485 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
59 | | ledivmul 11597 |
. . . . . 6
⊢
((sup(𝑇, ℝ,
< ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → ((sup(𝑇, ℝ, < ) / 𝑘) ≤ 𝑥 ↔ sup(𝑇, ℝ, < ) ≤ (𝑘 · 𝑥))) |
60 | 56, 57, 58, 59 | syl3anc 1372 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
((sup(𝑇, ℝ, < ) /
𝑘) ≤ 𝑥 ↔ sup(𝑇, ℝ, < ) ≤ (𝑘 · 𝑥))) |
61 | 54, 60 | mpbird 260 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
(sup(𝑇, ℝ, < ) /
𝑘) ≤ 𝑥) |
62 | 11, 61 | eqbrtrd 5053 |
. . 3
⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑥)‘𝑘) ≤ 𝑥) |
63 | 62 | ralrimiva 3097 |
. 2
⊢ (𝑥 ∈ ℝ →
∀𝑘 ∈ ℕ
((𝐹‘𝑥)‘𝑘) ≤ 𝑥) |
64 | | rpnnen1lem.q |
. . . . 5
⊢ ℚ
∈ V |
65 | 12, 3, 1, 64 | rpnnen1lem1 12463 |
. . . 4
⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) ∈ (ℚ ↑m
ℕ)) |
66 | 64, 1 | elmap 8484 |
. . . 4
⊢ ((𝐹‘𝑥) ∈ (ℚ ↑m ℕ)
↔ (𝐹‘𝑥):ℕ⟶ℚ) |
67 | 65, 66 | sylib 221 |
. . 3
⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥):ℕ⟶ℚ) |
68 | | ffn 6505 |
. . 3
⊢ ((𝐹‘𝑥):ℕ⟶ℚ → (𝐹‘𝑥) Fn ℕ) |
69 | | breq1 5034 |
. . . 4
⊢ (𝑛 = ((𝐹‘𝑥)‘𝑘) → (𝑛 ≤ 𝑥 ↔ ((𝐹‘𝑥)‘𝑘) ≤ 𝑥)) |
70 | 69 | ralrn 6867 |
. . 3
⊢ ((𝐹‘𝑥) Fn ℕ → (∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝐹‘𝑥)‘𝑘) ≤ 𝑥)) |
71 | 67, 68, 70 | 3syl 18 |
. 2
⊢ (𝑥 ∈ ℝ →
(∀𝑛 ∈ ran
(𝐹‘𝑥)𝑛 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝐹‘𝑥)‘𝑘) ≤ 𝑥)) |
72 | 63, 71 | mpbird 260 |
1
⊢ (𝑥 ∈ ℝ →
∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥) |