| Step | Hyp | Ref
| Expression |
| 1 | | nnuz 12921 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
| 2 | | 1zzd 12648 |
. . . . 5
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ 1 ∈ ℤ) |
| 3 | | rge0ssre 13496 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
| 4 | | fss 6752 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℕ⟶ℝ) |
| 5 | 3, 4 | mpan2 691 |
. . . . . 6
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ 𝐹:ℕ⟶ℝ) |
| 6 | 5 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) |
| 7 | 1, 2, 6 | serfre 14072 |
. . . 4
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ seq1( + , 𝐹):ℕ⟶ℝ) |
| 8 | 7 | frnd 6744 |
. . 3
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ ran seq1( + , 𝐹)
⊆ ℝ) |
| 9 | 8 | adantr 480 |
. 2
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ran seq1( + , 𝐹) ⊆ ℝ) |
| 10 | | 1nn 12277 |
. . . . 5
⊢ 1 ∈
ℕ |
| 11 | | fdm 6745 |
. . . . 5
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ dom seq1( + , 𝐹) =
ℕ) |
| 12 | 10, 11 | eleqtrrid 2848 |
. . . 4
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ 1 ∈ dom seq1( + , 𝐹)) |
| 13 | | ne0i 4341 |
. . . . 5
⊢ (1 ∈
dom seq1( + , 𝐹) → dom
seq1( + , 𝐹) ≠
∅) |
| 14 | | dm0rn0 5935 |
. . . . . 6
⊢ (dom
seq1( + , 𝐹) = ∅
↔ ran seq1( + , 𝐹) =
∅) |
| 15 | 14 | necon3bii 2993 |
. . . . 5
⊢ (dom
seq1( + , 𝐹) ≠ ∅
↔ ran seq1( + , 𝐹)
≠ ∅) |
| 16 | 13, 15 | sylib 218 |
. . . 4
⊢ (1 ∈
dom seq1( + , 𝐹) → ran
seq1( + , 𝐹) ≠
∅) |
| 17 | 7, 12, 16 | 3syl 18 |
. . 3
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ ran seq1( + , 𝐹)
≠ ∅) |
| 18 | 17 | adantr 480 |
. 2
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ran seq1( + , 𝐹) ≠ ∅) |
| 19 | | 1zzd 12648 |
. . . . 5
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → 1 ∈ ℤ) |
| 20 | | climdm 15590 |
. . . . . . 7
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
↔ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
| 21 | 20 | biimpi 216 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
| 22 | 21 | adantl 481 |
. . . . 5
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹))) |
| 23 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → seq1( + , 𝐹):ℕ⟶ℝ) |
| 24 | 23 | ffvelcdmda 7104 |
. . . . 5
⊢ (((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℝ) |
| 25 | 1, 19, 22, 24 | climrecl 15619 |
. . . 4
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ) |
| 26 | | simpr 484 |
. . . . . 6
⊢ (((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) → 𝑘
∈ ℕ) |
| 27 | 22 | adantr 480 |
. . . . . 6
⊢ (((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹))) |
| 28 | | simplll 775 |
. . . . . . 7
⊢ ((((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ ℕ) → 𝐹:ℕ⟶(0[,)+∞)) |
| 29 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
(0[,)+∞)) |
| 30 | 3, 29 | sselid 3981 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) |
| 31 | 28, 30 | sylancom 588 |
. . . . . 6
⊢ ((((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ ℕ) → (𝐹‘𝑗) ∈ ℝ) |
| 32 | | elrege0 13494 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑗) ∈ (0[,)+∞) ↔ ((𝐹‘𝑗) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑗))) |
| 33 | 32 | simprbi 496 |
. . . . . . . . 9
⊢ ((𝐹‘𝑗) ∈ (0[,)+∞) → 0 ≤ (𝐹‘𝑗)) |
| 34 | 29, 33 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (𝐹‘𝑗)) |
| 35 | 34 | adantlr 715 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑗
∈ ℕ) → 0 ≤ (𝐹‘𝑗)) |
| 36 | 35 | adantlr 715 |
. . . . . 6
⊢ ((((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ ℕ) → 0 ≤ (𝐹‘𝑗)) |
| 37 | 1, 26, 27, 31, 36 | climserle 15699 |
. . . . 5
⊢ (((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) |
| 38 | 37 | ralrimiva 3146 |
. . . 4
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) |
| 39 | | brralrspcev 5203 |
. . . 4
⊢ (((
⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
| 40 | 25, 38, 39 | syl2anc 584 |
. . 3
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
| 41 | | ffn 6736 |
. . . . . 6
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ seq1( + , 𝐹) Fn
ℕ) |
| 42 | | breq1 5146 |
. . . . . . 7
⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
| 43 | 42 | ralrn 7108 |
. . . . . 6
⊢ (seq1( +
, 𝐹) Fn ℕ →
(∀𝑧 ∈ ran seq1(
+ , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
| 44 | 7, 41, 43 | 3syl 18 |
. . . . 5
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ (∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
| 45 | 44 | rexbidv 3179 |
. . . 4
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ (∃𝑥 ∈
ℝ ∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
| 46 | 45 | adantr 480 |
. . 3
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
| 47 | 40, 46 | mpbird 257 |
. 2
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥) |
| 48 | | suprcl 12228 |
. 2
⊢ ((ran
seq1( + , 𝐹) ⊆
ℝ ∧ ran seq1( + , 𝐹) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈
ℝ) |
| 49 | 9, 18, 47, 48 | syl3anc 1373 |
1
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈
ℝ) |