Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . . . 5
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ 1 ∈ ℤ) |
3 | | rge0ssre 12151 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
4 | | fss 5969 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℕ⟶ℝ) |
5 | 3, 4 | mpan2 703 |
. . . . . 6
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ 𝐹:ℕ⟶ℝ) |
6 | 5 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) |
7 | 1, 2, 6 | serfre 12692 |
. . . 4
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ seq1( + , 𝐹):ℕ⟶ℝ) |
8 | | frn 5966 |
. . . 4
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ ran seq1( + , 𝐹)
⊆ ℝ) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ ran seq1( + , 𝐹)
⊆ ℝ) |
10 | 9 | adantr 480 |
. 2
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ran seq1( + , 𝐹) ⊆ ℝ) |
11 | | 1nn 10908 |
. . . . 5
⊢ 1 ∈
ℕ |
12 | | fdm 5964 |
. . . . 5
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ dom seq1( + , 𝐹) =
ℕ) |
13 | 11, 12 | syl5eleqr 2695 |
. . . 4
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ 1 ∈ dom seq1( + , 𝐹)) |
14 | | ne0i 3880 |
. . . . 5
⊢ (1 ∈
dom seq1( + , 𝐹) → dom
seq1( + , 𝐹) ≠
∅) |
15 | | dm0rn0 5263 |
. . . . . 6
⊢ (dom
seq1( + , 𝐹) = ∅
↔ ran seq1( + , 𝐹) =
∅) |
16 | 15 | necon3bii 2834 |
. . . . 5
⊢ (dom
seq1( + , 𝐹) ≠ ∅
↔ ran seq1( + , 𝐹)
≠ ∅) |
17 | 14, 16 | sylib 207 |
. . . 4
⊢ (1 ∈
dom seq1( + , 𝐹) → ran
seq1( + , 𝐹) ≠
∅) |
18 | 7, 13, 17 | 3syl 18 |
. . 3
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ ran seq1( + , 𝐹)
≠ ∅) |
19 | 18 | adantr 480 |
. 2
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ran seq1( + , 𝐹) ≠ ∅) |
20 | | 1zzd 11285 |
. . . . 5
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → 1 ∈ ℤ) |
21 | | climdm 14133 |
. . . . . . 7
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
↔ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
22 | 21 | biimpi 205 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
23 | 22 | adantl 481 |
. . . . 5
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹))) |
24 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → seq1( + , 𝐹):ℕ⟶ℝ) |
25 | 24 | ffvelrnda 6267 |
. . . . 5
⊢ (((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℝ) |
26 | 1, 20, 23, 25 | climrecl 14162 |
. . . 4
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ) |
27 | | simpr 476 |
. . . . . 6
⊢ (((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) → 𝑘
∈ ℕ) |
28 | 23 | adantr 480 |
. . . . . 6
⊢ (((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹))) |
29 | | simplll 794 |
. . . . . . 7
⊢ ((((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ ℕ) → 𝐹:ℕ⟶(0[,)+∞)) |
30 | | ffvelrn 6265 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
(0[,)+∞)) |
31 | 3, 30 | sseldi 3566 |
. . . . . . 7
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) |
32 | 29, 31 | sylancom 698 |
. . . . . 6
⊢ ((((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ ℕ) → (𝐹‘𝑗) ∈ ℝ) |
33 | | elrege0 12149 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑗) ∈ (0[,)+∞) ↔ ((𝐹‘𝑗) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑗))) |
34 | 33 | simprbi 479 |
. . . . . . . . 9
⊢ ((𝐹‘𝑗) ∈ (0[,)+∞) → 0 ≤ (𝐹‘𝑗)) |
35 | 30, 34 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (𝐹‘𝑗)) |
36 | 35 | adantlr 747 |
. . . . . . 7
⊢ (((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑗
∈ ℕ) → 0 ≤ (𝐹‘𝑗)) |
37 | 36 | adantlr 747 |
. . . . . 6
⊢ ((((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) ∧ 𝑗
∈ ℕ) → 0 ≤ (𝐹‘𝑗)) |
38 | 1, 27, 28, 32, 37 | climserle 14241 |
. . . . 5
⊢ (((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) ∧ 𝑘
∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) |
39 | 38 | ralrimiva 2949 |
. . . 4
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) |
40 | | breq2 4587 |
. . . . . 6
⊢ (𝑥 = ( ⇝ ‘seq1( + ,
𝐹)) → ((seq1( + ,
𝐹)‘𝑘) ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))) |
41 | 40 | ralbidv 2969 |
. . . . 5
⊢ (𝑥 = ( ⇝ ‘seq1( + ,
𝐹)) → (∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))) |
42 | 41 | rspcev 3282 |
. . . 4
⊢ (((
⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
43 | 26, 39, 42 | syl2anc 691 |
. . 3
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
44 | | ffn 5958 |
. . . . . 6
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ seq1( + , 𝐹) Fn
ℕ) |
45 | | breq1 4586 |
. . . . . . 7
⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
46 | 45 | ralrn 6270 |
. . . . . 6
⊢ (seq1( +
, 𝐹) Fn ℕ →
(∀𝑧 ∈ ran seq1(
+ , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
47 | 7, 44, 46 | 3syl 18 |
. . . . 5
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ (∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
48 | 47 | rexbidv 3034 |
. . . 4
⊢ (𝐹:ℕ⟶(0[,)+∞)
→ (∃𝑥 ∈
ℝ ∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
49 | 48 | adantr 480 |
. . 3
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
50 | 43, 49 | mpbird 246 |
. 2
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥) |
51 | | suprcl 10862 |
. 2
⊢ ((ran
seq1( + , 𝐹) ⊆
ℝ ∧ ran seq1( + , 𝐹) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈
ℝ) |
52 | 10, 19, 50, 51 | syl3anc 1318 |
1
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ seq1( + , 𝐹) ∈
dom ⇝ ) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈
ℝ) |