Step | Hyp | Ref
| Expression |
1 | | climsup.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) |
2 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐹:𝑍⟶ℝ → ran 𝐹 ⊆ ℝ) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
4 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑍⟶ℝ → 𝐹 Fn 𝑍) |
5 | 1, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 Fn 𝑍) |
6 | | climsup.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℤ) |
7 | | uzid 11578 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
9 | | climsup.1 |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ≥‘𝑀) |
10 | 8, 9 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
11 | | fnfvelrn 6264 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝑍 ∧ 𝑀 ∈ 𝑍) → (𝐹‘𝑀) ∈ ran 𝐹) |
12 | 5, 10, 11 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑀) ∈ ran 𝐹) |
13 | | ne0i 3880 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑀) ∈ ran 𝐹 → ran 𝐹 ≠ ∅) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ≠ ∅) |
15 | | climsup.5 |
. . . . . . . . . 10
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥) |
16 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝐹‘𝑘) → (𝑦 ≤ 𝑥 ↔ (𝐹‘𝑘) ≤ 𝑥)) |
17 | 16 | ralrn 6270 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝑍 → (∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥)) |
18 | 17 | rexbidv 3034 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝑍 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥)) |
19 | 5, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ 𝑥)) |
20 | 15, 19 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) |
21 | 3, 14, 20 | 3jca 1235 |
. . . . . . . 8
⊢ (𝜑 → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥)) |
22 | | suprcl 10862 |
. . . . . . . 8
⊢ ((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
24 | | ltsubrp 11742 |
. . . . . . 7
⊢ ((sup(ran
𝐹, ℝ, < ) ∈
ℝ ∧ 𝑦 ∈
ℝ+) → (sup(ran 𝐹, ℝ, < ) − 𝑦) < sup(ran 𝐹, ℝ, < )) |
25 | 23, 24 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (sup(ran
𝐹, ℝ, < ) −
𝑦) < sup(ran 𝐹, ℝ, <
)) |
26 | 21 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥)) |
27 | | rpre 11715 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
28 | | resubcl 10224 |
. . . . . . . 8
⊢ ((sup(ran
𝐹, ℝ, < ) ∈
ℝ ∧ 𝑦 ∈
ℝ) → (sup(ran 𝐹,
ℝ, < ) − 𝑦)
∈ ℝ) |
29 | 23, 27, 28 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (sup(ran
𝐹, ℝ, < ) −
𝑦) ∈
ℝ) |
30 | | suprlub 10864 |
. . . . . . 7
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) − 𝑦) ∈ ℝ) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < sup(ran 𝐹, ℝ, < ) ↔ ∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘)) |
31 | 26, 29, 30 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ((sup(ran
𝐹, ℝ, < ) −
𝑦) < sup(ran 𝐹, ℝ, < ) ↔
∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘)) |
32 | 25, 31 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘) |
33 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑘 = (𝐹‘𝑗) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘 ↔ (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗))) |
34 | 33 | rexrn 6269 |
. . . . . . 7
⊢ (𝐹 Fn 𝑍 → (∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘 ↔ ∃𝑗 ∈ 𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗))) |
35 | 5, 34 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘 ↔ ∃𝑗 ∈ 𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗))) |
36 | 35 | biimpa 500 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘) → ∃𝑗 ∈ 𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗)) |
37 | 32, 36 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗)) |
38 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈ ℝ) |
39 | 1, 38 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈ ℝ) |
40 | 39 | ad2ant2r 779 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑗) ∈ ℝ) |
41 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹:𝑍⟶ℝ) |
42 | 9 | uztrn2 11581 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
43 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
44 | 41, 42, 43 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑘) ∈ ℝ) |
45 | 23 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
46 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝑘 ∈ (ℤ≥‘𝑗)) |
47 | | fzssuz 12253 |
. . . . . . . . . . . . . 14
⊢ (𝑗...𝑘) ⊆ (ℤ≥‘𝑗) |
48 | | uzss 11584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑗) ⊆
(ℤ≥‘𝑀)) |
49 | 48, 9 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑗) ⊆ 𝑍) |
50 | 49, 9 | eleq2s 2706 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → (ℤ≥‘𝑗) ⊆ 𝑍) |
51 | 50 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) →
(ℤ≥‘𝑗) ⊆ 𝑍) |
52 | 47, 51 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝑗...𝑘) ⊆ 𝑍) |
53 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ ℝ) |
54 | 53 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑍⟶ℝ → ∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ) |
55 | 1, 54 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ) |
56 | 55 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ) |
57 | | ssralv 3629 |
. . . . . . . . . . . . 13
⊢ ((𝑗...𝑘) ⊆ 𝑍 → (∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ → ∀𝑛 ∈ (𝑗...𝑘)(𝐹‘𝑛) ∈ ℝ)) |
58 | 52, 56, 57 | sylc 63 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ∀𝑛 ∈ (𝑗...𝑘)(𝐹‘𝑛) ∈ ℝ) |
59 | 58 | r19.21bi 2916 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) ∧ 𝑛 ∈ (𝑗...𝑘)) → (𝐹‘𝑛) ∈ ℝ) |
60 | | fzssuz 12253 |
. . . . . . . . . . . . . 14
⊢ (𝑗...(𝑘 − 1)) ⊆
(ℤ≥‘𝑗) |
61 | 60, 51 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝑗...(𝑘 − 1)) ⊆ 𝑍) |
62 | 61 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) ∧ 𝑛 ∈ (𝑗...(𝑘 − 1))) → 𝑛 ∈ 𝑍) |
63 | | climsup.4 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
64 | 63 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
65 | 64 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
66 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
67 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1)) |
68 | 67 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1))) |
69 | 66, 68 | breq12d 4596 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1)))) |
70 | 69 | rspccva 3281 |
. . . . . . . . . . . . 13
⊢
((∀𝑘 ∈
𝑍 (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1))) |
71 | 65, 70 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1))) |
72 | 62, 71 | syldan 486 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) ∧ 𝑛 ∈ (𝑗...(𝑘 − 1))) → (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1))) |
73 | 46, 59, 72 | monoord 12693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑗) ≤ (𝐹‘𝑘)) |
74 | 40, 44, 45, 73 | lesub2dd 10523 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗))) |
75 | 45, 44 | resubcld 10337 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) ∈ ℝ) |
76 | 45, 40 | resubcld 10337 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) ∈ ℝ) |
77 | 27 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝑦 ∈ ℝ) |
78 | | lelttr 10007 |
. . . . . . . . . 10
⊢
(((sup(ran 𝐹,
ℝ, < ) − (𝐹‘𝑘)) ∈ ℝ ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) < 𝑦) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) < 𝑦)) |
79 | 75, 76, 77, 78 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (((sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) < 𝑦) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) < 𝑦)) |
80 | 74, 79 | mpand 707 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) < 𝑦 → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) < 𝑦)) |
81 | | ltsub23 10387 |
. . . . . . . . 9
⊢ ((sup(ran
𝐹, ℝ, < ) ∈
ℝ ∧ 𝑦 ∈
ℝ ∧ (𝐹‘𝑗) ∈ ℝ) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) ↔ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) < 𝑦)) |
82 | 45, 77, 40, 81 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) ↔ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑗)) < 𝑦)) |
83 | 21 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥)) |
84 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹 Fn 𝑍) |
85 | | fnfvelrn 6264 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ran 𝐹) |
86 | 84, 42, 85 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑘) ∈ ran 𝐹) |
87 | | suprub 10863 |
. . . . . . . . . . 11
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) ∧ (𝐹‘𝑘) ∈ ran 𝐹) → (𝐹‘𝑘) ≤ sup(ran 𝐹, ℝ, < )) |
88 | 83, 86, 87 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑘) ≤ sup(ran 𝐹, ℝ, < )) |
89 | 44, 45, 88 | abssuble0d 14019 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) = (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘))) |
90 | 89 | breq1d 4593 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦 ↔ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑘)) < 𝑦)) |
91 | 80, 82, 90 | 3imtr4d 282 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) → (abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦)) |
92 | 91 | anassrs 678 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) → (abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦)) |
93 | 92 | ralrimdva 2952 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) → ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦)) |
94 | 93 | reximdva 3000 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹‘𝑗) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦)) |
95 | 37, 94 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦) |
96 | 95 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦) |
97 | | fvex 6113 |
. . . . 5
⊢
(ℤ≥‘𝑀) ∈ V |
98 | 9, 97 | eqeltri 2684 |
. . . 4
⊢ 𝑍 ∈ V |
99 | | fex 6394 |
. . . 4
⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑍 ∈ V) → 𝐹 ∈ V) |
100 | 1, 98, 99 | sylancl 693 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
101 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
102 | 23 | recnd 9947 |
. . 3
⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈
ℂ) |
103 | 1, 43 | sylan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
104 | 103 | recnd 9947 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
105 | 9, 6, 100, 101, 102, 104 | clim2c 14084 |
. 2
⊢ (𝜑 → (𝐹 ⇝ sup(ran 𝐹, ℝ, < ) ↔ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦)) |
106 | 96, 105 | mpbird 246 |
1
⊢ (𝜑 → 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) |