Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
2 | 1 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑆 − (1 / 𝑛)) = (𝑆 − (1 / 𝑘))) |
3 | | supcvg.3 |
. . . . . . . . . . 11
⊢ 𝑅 = (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) |
4 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (𝑆 − (1 / 𝑘)) ∈ V |
5 | 2, 3, 4 | fvmpt 6282 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝑅‘𝑘) = (𝑆 − (1 / 𝑘))) |
6 | 5 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑅‘𝑘) = (𝑆 − (1 / 𝑘))) |
7 | | supcvg.2 |
. . . . . . . . . . 11
⊢ 𝑆 = sup(𝐴, ℝ, < ) |
8 | | supcvg.6 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
9 | | supcvg.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ≠ ∅) |
10 | | supcvg.5 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:𝑋–onto→𝐴) |
11 | | fof 6115 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑋–onto→𝐴 → 𝐹:𝑋⟶𝐴) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝑋⟶𝐴) |
13 | | feq3 6028 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 = ∅ → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶∅)) |
14 | 12, 13 | syl5ibcom 235 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 = ∅ → 𝐹:𝑋⟶∅)) |
15 | | f00 6087 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑋⟶∅ ↔ (𝐹 = ∅ ∧ 𝑋 = ∅)) |
16 | 15 | simprbi 480 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋⟶∅ → 𝑋 = ∅) |
17 | 14, 16 | syl6 35 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 = ∅ → 𝑋 = ∅)) |
18 | 17 | necon3d 2815 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 ≠ ∅ → 𝐴 ≠ ∅)) |
19 | 9, 18 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≠ ∅) |
20 | | supcvg.7 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
21 | 8, 19, 20 | 3jca 1242 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) |
22 | | suprcl 10983 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈
ℝ) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈
ℝ) |
24 | 7, 23 | syl5eqel 2705 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℝ) |
25 | | nnrp 11842 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
26 | 25 | rpreccld 11882 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
27 | | ltsubrp 11866 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ+)
→ (𝑆 − (1 /
𝑘)) < 𝑆) |
28 | 24, 26, 27 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆 − (1 / 𝑘)) < 𝑆) |
29 | 6, 28 | eqbrtrd 4675 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑅‘𝑘) < 𝑆) |
30 | 29, 7 | syl6breq 4694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑅‘𝑘) < sup(𝐴, ℝ, < )) |
31 | 21 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) |
32 | | nnrecre 11057 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
33 | | resubcl 10345 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ) → (𝑆 − (1 / 𝑛)) ∈ ℝ) |
34 | 24, 32, 33 | syl2an 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆 − (1 / 𝑛)) ∈ ℝ) |
35 | 34, 3 | fmptd 6385 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅:ℕ⟶ℝ) |
36 | 35 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑅‘𝑘) ∈ ℝ) |
37 | | suprlub 10987 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝑅‘𝑘) ∈ ℝ) → ((𝑅‘𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) < 𝑧)) |
38 | 31, 36, 37 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑅‘𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) < 𝑧)) |
39 | 30, 38 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) < 𝑧) |
40 | 36 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑧 ∈ 𝐴) → (𝑅‘𝑘) ∈ ℝ) |
41 | 8 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ⊆ ℝ) |
42 | 41 | sselda 3603 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
43 | | ltle 10126 |
. . . . . . . 8
⊢ (((𝑅‘𝑘) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑅‘𝑘) < 𝑧 → (𝑅‘𝑘) ≤ 𝑧)) |
44 | 40, 42, 43 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑧 ∈ 𝐴) → ((𝑅‘𝑘) < 𝑧 → (𝑅‘𝑘) ≤ 𝑧)) |
45 | 44 | reximdva 3017 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∃𝑧 ∈ 𝐴 (𝑅‘𝑘) < 𝑧 → ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) ≤ 𝑧)) |
46 | 39, 45 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) ≤ 𝑧) |
47 | | forn 6118 |
. . . . . . . . 9
⊢ (𝐹:𝑋–onto→𝐴 → ran 𝐹 = 𝐴) |
48 | 10, 47 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 = 𝐴) |
49 | 48 | rexeqdv 3145 |
. . . . . . 7
⊢ (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅‘𝑘) ≤ 𝑧 ↔ ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) ≤ 𝑧)) |
50 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐹:𝑋⟶𝐴 → 𝐹 Fn 𝑋) |
51 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑧 = (𝐹‘𝑥) → ((𝑅‘𝑘) ≤ 𝑧 ↔ (𝑅‘𝑘) ≤ (𝐹‘𝑥))) |
52 | 51 | rexrn 6361 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑋 → (∃𝑧 ∈ ran 𝐹(𝑅‘𝑘) ≤ 𝑧 ↔ ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥))) |
53 | 12, 50, 52 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅‘𝑘) ≤ 𝑧 ↔ ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥))) |
54 | 49, 53 | bitr3d 270 |
. . . . . 6
⊢ (𝜑 → (∃𝑧 ∈ 𝐴 (𝑅‘𝑘) ≤ 𝑧 ↔ ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥))) |
55 | 54 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∃𝑧 ∈ 𝐴 (𝑅‘𝑘) ≤ 𝑧 ↔ ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥))) |
56 | 46, 55 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥)) |
57 | 56 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ ℕ ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥)) |
58 | | supcvg.1 |
. . . 4
⊢ 𝑋 ∈ V |
59 | | nnenom 12779 |
. . . 4
⊢ ℕ
≈ ω |
60 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = (𝑓‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝑓‘𝑘))) |
61 | 60 | breq2d 4665 |
. . . 4
⊢ (𝑥 = (𝑓‘𝑘) → ((𝑅‘𝑘) ≤ (𝐹‘𝑥) ↔ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)))) |
62 | 58, 59, 61 | axcc4 9261 |
. . 3
⊢
(∀𝑘 ∈
ℕ ∃𝑥 ∈
𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)))) |
63 | 57, 62 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)))) |
64 | | nnuz 11723 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
65 | | 1zzd 11408 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 1 ∈ ℤ) |
66 | | 1zzd 11408 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
67 | 24 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℂ) |
68 | | 1z 11407 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
69 | 64 | eqimss2i 3660 |
. . . . . . . . . . 11
⊢
(ℤ≥‘1) ⊆ ℕ |
70 | | nnex 11026 |
. . . . . . . . . . 11
⊢ ℕ
∈ V |
71 | 69, 70 | climconst2 14279 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℂ ∧ 1 ∈
ℤ) → (ℕ × {𝑆}) ⇝ 𝑆) |
72 | 67, 68, 71 | sylancl 694 |
. . . . . . . . 9
⊢ (𝜑 → (ℕ × {𝑆}) ⇝ 𝑆) |
73 | 70 | mptex 6486 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) ∈ V |
74 | 3, 73 | eqeltri 2697 |
. . . . . . . . . 10
⊢ 𝑅 ∈ V |
75 | 74 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ V) |
76 | | ax-1cn 9994 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
77 | | divcnv 14585 |
. . . . . . . . . 10
⊢ (1 ∈
ℂ → (𝑛 ∈
ℕ ↦ (1 / 𝑛))
⇝ 0) |
78 | 76, 77 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0) |
79 | | fvconst2g 6467 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
((ℕ × {𝑆})‘𝑘) = 𝑆) |
80 | 24, 79 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{𝑆})‘𝑘) = 𝑆) |
81 | 67 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑆 ∈ ℂ) |
82 | 80, 81 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{𝑆})‘𝑘) ∈
ℂ) |
83 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦ (1 /
𝑛)) = (𝑛 ∈ ℕ ↦ (1 / 𝑛)) |
84 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (1 /
𝑘) ∈
V |
85 | 1, 83, 84 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
𝑛))‘𝑘) = (1 / 𝑘)) |
86 | 85 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘)) |
87 | | nnrecre 11057 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
88 | 87 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℂ) |
89 | 88 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℂ) |
90 | 86, 89 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℂ) |
91 | 80, 86 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((ℕ ×
{𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)) = (𝑆 − (1 / 𝑘))) |
92 | 6, 91 | eqtr4d 2659 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑅‘𝑘) = (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘))) |
93 | 64, 66, 72, 75, 78, 82, 90, 92 | climsub 14364 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ⇝ (𝑆 − 0)) |
94 | 67 | subid1d 10381 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 − 0) = 𝑆) |
95 | 93, 94 | breqtrd 4679 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ⇝ 𝑆) |
96 | 95 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 𝑅 ⇝ 𝑆) |
97 | 12 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 𝐹:𝑋⟶𝐴) |
98 | | fex 6490 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶𝐴 ∧ 𝑋 ∈ V) → 𝐹 ∈ V) |
99 | 97, 58, 98 | sylancl 694 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 𝐹 ∈ V) |
100 | | vex 3203 |
. . . . . . 7
⊢ 𝑓 ∈ V |
101 | | coexg 7117 |
. . . . . . 7
⊢ ((𝐹 ∈ V ∧ 𝑓 ∈ V) → (𝐹 ∘ 𝑓) ∈ V) |
102 | 99, 100, 101 | sylancl 694 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → (𝐹 ∘ 𝑓) ∈ V) |
103 | 35 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 𝑅:ℕ⟶ℝ) |
104 | 103 | ffvelrnda 6359 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅‘𝑚) ∈ ℝ) |
105 | 12, 8 | fssd 6057 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
106 | | fco 6058 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑓:ℕ⟶𝑋) → (𝐹 ∘ 𝑓):ℕ⟶ℝ) |
107 | 105, 106 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:ℕ⟶𝑋) → (𝐹 ∘ 𝑓):ℕ⟶ℝ) |
108 | 107 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → (𝐹 ∘ 𝑓):ℕ⟶ℝ) |
109 | 108 | ffvelrnda 6359 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹 ∘ 𝑓)‘𝑚) ∈ ℝ) |
110 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝑅‘𝑘) = (𝑅‘𝑚)) |
111 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑓‘𝑘) = (𝑓‘𝑚)) |
112 | 111 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝐹‘(𝑓‘𝑘)) = (𝐹‘(𝑓‘𝑚))) |
113 | 110, 112 | breq12d 4666 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → ((𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)) ↔ (𝑅‘𝑚) ≤ (𝐹‘(𝑓‘𝑚)))) |
114 | 113 | rspccva 3308 |
. . . . . . . 8
⊢
((∀𝑘 ∈
ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)) ∧ 𝑚 ∈ ℕ) → (𝑅‘𝑚) ≤ (𝐹‘(𝑓‘𝑚))) |
115 | 114 | adantll 750 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅‘𝑚) ≤ (𝐹‘(𝑓‘𝑚))) |
116 | | simplr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 𝑓:ℕ⟶𝑋) |
117 | | fvco3 6275 |
. . . . . . . 8
⊢ ((𝑓:ℕ⟶𝑋 ∧ 𝑚 ∈ ℕ) → ((𝐹 ∘ 𝑓)‘𝑚) = (𝐹‘(𝑓‘𝑚))) |
118 | 116, 117 | sylan 488 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹 ∘ 𝑓)‘𝑚) = (𝐹‘(𝑓‘𝑚))) |
119 | 115, 118 | breqtrrd 4681 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅‘𝑚) ≤ ((𝐹 ∘ 𝑓)‘𝑚)) |
120 | 21 | ad3antrrr 766 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) |
121 | 116 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑓‘𝑚) ∈ 𝑋) |
122 | 97 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ (𝑓‘𝑚) ∈ 𝑋) → (𝐹‘(𝑓‘𝑚)) ∈ 𝐴) |
123 | 121, 122 | syldan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓‘𝑚)) ∈ 𝐴) |
124 | | suprub 10984 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐹‘(𝑓‘𝑚)) ∈ 𝐴) → (𝐹‘(𝑓‘𝑚)) ≤ sup(𝐴, ℝ, < )) |
125 | 120, 123,
124 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓‘𝑚)) ≤ sup(𝐴, ℝ, < )) |
126 | 125, 7 | syl6breqr 4695 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓‘𝑚)) ≤ 𝑆) |
127 | 118, 126 | eqbrtrd 4675 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹 ∘ 𝑓)‘𝑚) ≤ 𝑆) |
128 | 64, 65, 96, 102, 104, 109, 119, 127 | climsqz 14371 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → (𝐹 ∘ 𝑓) ⇝ 𝑆) |
129 | 128 | ex 450 |
. . . 4
⊢ ((𝜑 ∧ 𝑓:ℕ⟶𝑋) → (∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)) → (𝐹 ∘ 𝑓) ⇝ 𝑆)) |
130 | 129 | imdistanda 729 |
. . 3
⊢ (𝜑 → ((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → (𝑓:ℕ⟶𝑋 ∧ (𝐹 ∘ 𝑓) ⇝ 𝑆))) |
131 | 130 | eximdv 1846 |
. 2
⊢ (𝜑 → (∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹 ∘ 𝑓) ⇝ 𝑆))) |
132 | 63, 131 | mpd 15 |
1
⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹 ∘ 𝑓) ⇝ 𝑆)) |