| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
| 2 | 1 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑆 − (1 / 𝑛)) = (𝑆 − (1 / 𝑘))) |
| 3 | | supcvg.3 |
. . . . . . . . . . 11
⊢ 𝑅 = (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) |
| 4 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑆 − (1 / 𝑘)) ∈ V |
| 5 | 2, 3, 4 | fvmpt 7016 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝑅‘𝑘) = (𝑆 − (1 / 𝑘))) |
| 6 | 5 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑅‘𝑘) = (𝑆 − (1 / 𝑘))) |
| 7 | | supcvg.2 |
. . . . . . . . . . 11
⊢ 𝑆 = sup(𝐴, ℝ, < ) |
| 8 | | supcvg.6 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 9 | | supcvg.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ≠ ∅) |
| 10 | | supcvg.5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝑋–onto→𝐴) |
| 11 | | fof 6820 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑋–onto→𝐴 → 𝐹:𝑋⟶𝐴) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋⟶𝐴) |
| 13 | | feq3 6718 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = ∅ → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶∅)) |
| 14 | 12, 13 | syl5ibcom 245 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 = ∅ → 𝐹:𝑋⟶∅)) |
| 15 | | f00 6790 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋⟶∅ ↔ (𝐹 = ∅ ∧ 𝑋 = ∅)) |
| 16 | 15 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑋⟶∅ → 𝑋 = ∅) |
| 17 | 14, 16 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 = ∅ → 𝑋 = ∅)) |
| 18 | 17 | necon3d 2961 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ≠ ∅ → 𝐴 ≠ ∅)) |
| 19 | 9, 18 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≠ ∅) |
| 20 | | supcvg.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
| 21 | 8, 19, 20 | suprcld 12231 |
. . . . . . . . . . 11
⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈
ℝ) |
| 22 | 7, 21 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℝ) |
| 23 | | nnrp 13046 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
| 24 | 23 | rpreccld 13087 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
| 25 | | ltsubrp 13071 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ+)
→ (𝑆 − (1 /
𝑘)) < 𝑆) |
| 26 | 22, 24, 25 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆 − (1 / 𝑘)) < 𝑆) |
| 27 | 6, 26 | eqbrtrd 5165 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑅‘𝑘) < 𝑆) |
| 28 | 27, 7 | breqtrdi 5184 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑅‘𝑘) < sup(𝐴, ℝ, < )) |
| 29 | 8, 19, 20 | 3jca 1129 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) |
| 30 | | nnrecre 12308 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
| 31 | | resubcl 11573 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ) → (𝑆 − (1 / 𝑛)) ∈ ℝ) |
| 32 | 22, 30, 31 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆 − (1 / 𝑛)) ∈ ℝ) |
| 33 | 32, 3 | fmptd 7134 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅:ℕ⟶ℝ) |
| 34 | 33 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑅‘𝑘) ∈ ℝ) |
| 35 | | suprlub 12232 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝑅‘𝑘) ∈ ℝ) → ((𝑅‘𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) < 𝑧)) |
| 36 | 29, 34, 35 | syl2an2r 685 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑅‘𝑘) < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) < 𝑧)) |
| 37 | 28, 36 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) < 𝑧) |
| 38 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ⊆ ℝ) |
| 39 | 38 | sselda 3983 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
| 40 | | ltle 11349 |
. . . . . . . 8
⊢ (((𝑅‘𝑘) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑅‘𝑘) < 𝑧 → (𝑅‘𝑘) ≤ 𝑧)) |
| 41 | 34, 39, 40 | syl2an2r 685 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑧 ∈ 𝐴) → ((𝑅‘𝑘) < 𝑧 → (𝑅‘𝑘) ≤ 𝑧)) |
| 42 | 41 | reximdva 3168 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∃𝑧 ∈ 𝐴 (𝑅‘𝑘) < 𝑧 → ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) ≤ 𝑧)) |
| 43 | 37, 42 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) ≤ 𝑧) |
| 44 | | forn 6823 |
. . . . . . . . 9
⊢ (𝐹:𝑋–onto→𝐴 → ran 𝐹 = 𝐴) |
| 45 | 10, 44 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 = 𝐴) |
| 46 | 45 | rexeqdv 3327 |
. . . . . . 7
⊢ (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅‘𝑘) ≤ 𝑧 ↔ ∃𝑧 ∈ 𝐴 (𝑅‘𝑘) ≤ 𝑧)) |
| 47 | | ffn 6736 |
. . . . . . . 8
⊢ (𝐹:𝑋⟶𝐴 → 𝐹 Fn 𝑋) |
| 48 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑧 = (𝐹‘𝑥) → ((𝑅‘𝑘) ≤ 𝑧 ↔ (𝑅‘𝑘) ≤ (𝐹‘𝑥))) |
| 49 | 48 | rexrn 7107 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑋 → (∃𝑧 ∈ ran 𝐹(𝑅‘𝑘) ≤ 𝑧 ↔ ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥))) |
| 50 | 12, 47, 49 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (∃𝑧 ∈ ran 𝐹(𝑅‘𝑘) ≤ 𝑧 ↔ ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥))) |
| 51 | 46, 50 | bitr3d 281 |
. . . . . 6
⊢ (𝜑 → (∃𝑧 ∈ 𝐴 (𝑅‘𝑘) ≤ 𝑧 ↔ ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥))) |
| 52 | 51 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∃𝑧 ∈ 𝐴 (𝑅‘𝑘) ≤ 𝑧 ↔ ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥))) |
| 53 | 43, 52 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥)) |
| 54 | 53 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ ℕ ∃𝑥 ∈ 𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥)) |
| 55 | | supcvg.1 |
. . . 4
⊢ 𝑋 ∈ V |
| 56 | | nnenom 14021 |
. . . 4
⊢ ℕ
≈ ω |
| 57 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = (𝑓‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝑓‘𝑘))) |
| 58 | 57 | breq2d 5155 |
. . . 4
⊢ (𝑥 = (𝑓‘𝑘) → ((𝑅‘𝑘) ≤ (𝐹‘𝑥) ↔ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)))) |
| 59 | 55, 56, 58 | axcc4 10479 |
. . 3
⊢
(∀𝑘 ∈
ℕ ∃𝑥 ∈
𝑋 (𝑅‘𝑘) ≤ (𝐹‘𝑥) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)))) |
| 60 | 54, 59 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)))) |
| 61 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 62 | | 1zzd 12648 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 1 ∈ ℤ) |
| 63 | | 1zzd 12648 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
| 64 | 22 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℂ) |
| 65 | | 1z 12647 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
| 66 | 61 | eqimss2i 4045 |
. . . . . . . . . . 11
⊢
(ℤ≥‘1) ⊆ ℕ |
| 67 | | nnex 12272 |
. . . . . . . . . . 11
⊢ ℕ
∈ V |
| 68 | 66, 67 | climconst2 15584 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℂ ∧ 1 ∈
ℤ) → (ℕ × {𝑆}) ⇝ 𝑆) |
| 69 | 64, 65, 68 | sylancl 586 |
. . . . . . . . 9
⊢ (𝜑 → (ℕ × {𝑆}) ⇝ 𝑆) |
| 70 | 67 | mptex 7243 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ (𝑆 − (1 / 𝑛))) ∈ V |
| 71 | 3, 70 | eqeltri 2837 |
. . . . . . . . . 10
⊢ 𝑅 ∈ V |
| 72 | 71 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ V) |
| 73 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 74 | | divcnv 15889 |
. . . . . . . . . 10
⊢ (1 ∈
ℂ → (𝑛 ∈
ℕ ↦ (1 / 𝑛))
⇝ 0) |
| 75 | 73, 74 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0) |
| 76 | | fvconst2g 7222 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℝ ∧ 𝑘 ∈ ℕ) →
((ℕ × {𝑆})‘𝑘) = 𝑆) |
| 77 | 22, 76 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{𝑆})‘𝑘) = 𝑆) |
| 78 | 64 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑆 ∈ ℂ) |
| 79 | 77, 78 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{𝑆})‘𝑘) ∈
ℂ) |
| 80 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦ (1 /
𝑛)) = (𝑛 ∈ ℕ ↦ (1 / 𝑛)) |
| 81 | | ovex 7464 |
. . . . . . . . . . . 12
⊢ (1 /
𝑘) ∈
V |
| 82 | 1, 80, 81 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 /
𝑛))‘𝑘) = (1 / 𝑘)) |
| 83 | 82 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘)) |
| 84 | | nnrecre 12308 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
| 85 | 84 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℂ) |
| 86 | 85 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈
ℂ) |
| 87 | 83, 86 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℂ) |
| 88 | 77, 83 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((ℕ ×
{𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)) = (𝑆 − (1 / 𝑘))) |
| 89 | 6, 88 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑅‘𝑘) = (((ℕ × {𝑆})‘𝑘) − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘))) |
| 90 | 61, 63, 69, 72, 75, 79, 87, 89 | climsub 15670 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ⇝ (𝑆 − 0)) |
| 91 | 64 | subid1d 11609 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 − 0) = 𝑆) |
| 92 | 90, 91 | breqtrd 5169 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ⇝ 𝑆) |
| 93 | 92 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 𝑅 ⇝ 𝑆) |
| 94 | 12 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 𝐹:𝑋⟶𝐴) |
| 95 | | fex 7246 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶𝐴 ∧ 𝑋 ∈ V) → 𝐹 ∈ V) |
| 96 | 94, 55, 95 | sylancl 586 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 𝐹 ∈ V) |
| 97 | | vex 3484 |
. . . . . . 7
⊢ 𝑓 ∈ V |
| 98 | | coexg 7951 |
. . . . . . 7
⊢ ((𝐹 ∈ V ∧ 𝑓 ∈ V) → (𝐹 ∘ 𝑓) ∈ V) |
| 99 | 96, 97, 98 | sylancl 586 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → (𝐹 ∘ 𝑓) ∈ V) |
| 100 | 33 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 𝑅:ℕ⟶ℝ) |
| 101 | 100 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅‘𝑚) ∈ ℝ) |
| 102 | 12, 8 | fssd 6753 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
| 103 | | fco 6760 |
. . . . . . . . 9
⊢ ((𝐹:𝑋⟶ℝ ∧ 𝑓:ℕ⟶𝑋) → (𝐹 ∘ 𝑓):ℕ⟶ℝ) |
| 104 | 102, 103 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓:ℕ⟶𝑋) → (𝐹 ∘ 𝑓):ℕ⟶ℝ) |
| 105 | 104 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → (𝐹 ∘ 𝑓):ℕ⟶ℝ) |
| 106 | 105 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹 ∘ 𝑓)‘𝑚) ∈ ℝ) |
| 107 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝑅‘𝑘) = (𝑅‘𝑚)) |
| 108 | | 2fveq3 6911 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝐹‘(𝑓‘𝑘)) = (𝐹‘(𝑓‘𝑚))) |
| 109 | 107, 108 | breq12d 5156 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → ((𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)) ↔ (𝑅‘𝑚) ≤ (𝐹‘(𝑓‘𝑚)))) |
| 110 | 109 | rspccva 3621 |
. . . . . . . 8
⊢
((∀𝑘 ∈
ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)) ∧ 𝑚 ∈ ℕ) → (𝑅‘𝑚) ≤ (𝐹‘(𝑓‘𝑚))) |
| 111 | 110 | adantll 714 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅‘𝑚) ≤ (𝐹‘(𝑓‘𝑚))) |
| 112 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → 𝑓:ℕ⟶𝑋) |
| 113 | | fvco3 7008 |
. . . . . . . 8
⊢ ((𝑓:ℕ⟶𝑋 ∧ 𝑚 ∈ ℕ) → ((𝐹 ∘ 𝑓)‘𝑚) = (𝐹‘(𝑓‘𝑚))) |
| 114 | 112, 113 | sylan 580 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹 ∘ 𝑓)‘𝑚) = (𝐹‘(𝑓‘𝑚))) |
| 115 | 111, 114 | breqtrrd 5171 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑅‘𝑚) ≤ ((𝐹 ∘ 𝑓)‘𝑚)) |
| 116 | 29 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) |
| 117 | 112 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝑓‘𝑚) ∈ 𝑋) |
| 118 | 94 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ (𝑓‘𝑚) ∈ 𝑋) → (𝐹‘(𝑓‘𝑚)) ∈ 𝐴) |
| 119 | 117, 118 | syldan 591 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓‘𝑚)) ∈ 𝐴) |
| 120 | | suprub 12229 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐹‘(𝑓‘𝑚)) ∈ 𝐴) → (𝐹‘(𝑓‘𝑚)) ≤ sup(𝐴, ℝ, < )) |
| 121 | 116, 119,
120 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓‘𝑚)) ≤ sup(𝐴, ℝ, < )) |
| 122 | 121, 7 | breqtrrdi 5185 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → (𝐹‘(𝑓‘𝑚)) ≤ 𝑆) |
| 123 | 114, 122 | eqbrtrd 5165 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) ∧ 𝑚 ∈ ℕ) → ((𝐹 ∘ 𝑓)‘𝑚) ≤ 𝑆) |
| 124 | 61, 62, 93, 99, 101, 106, 115, 123 | climsqz 15677 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓:ℕ⟶𝑋) ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → (𝐹 ∘ 𝑓) ⇝ 𝑆) |
| 125 | 124 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ 𝑓:ℕ⟶𝑋) → (∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘)) → (𝐹 ∘ 𝑓) ⇝ 𝑆)) |
| 126 | 125 | imdistanda 571 |
. . 3
⊢ (𝜑 → ((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → (𝑓:ℕ⟶𝑋 ∧ (𝐹 ∘ 𝑓) ⇝ 𝑆))) |
| 127 | 126 | eximdv 1917 |
. 2
⊢ (𝜑 → (∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝑅‘𝑘) ≤ (𝐹‘(𝑓‘𝑘))) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹 ∘ 𝑓) ⇝ 𝑆))) |
| 128 | 60, 127 | mpd 15 |
1
⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ (𝐹 ∘ 𝑓) ⇝ 𝑆)) |