Step | Hyp | Ref
| Expression |
1 | | climinf.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) |
2 | | frn 5966 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑍⟶ℝ → ran 𝐹 ⊆ ℝ) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
4 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝑍⟶ℝ → 𝐹 Fn 𝑍) |
5 | 1, 4 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn 𝑍) |
6 | | climinf.4 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℤ) |
7 | | uzid 11578 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
9 | | climinf.3 |
. . . . . . . . . . . . . 14
⊢ 𝑍 =
(ℤ≥‘𝑀) |
10 | 8, 9 | syl6eleqr 2699 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
11 | | fnfvelrn 6264 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝑍 ∧ 𝑀 ∈ 𝑍) → (𝐹‘𝑀) ∈ ran 𝐹) |
12 | 5, 10, 11 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑀) ∈ ran 𝐹) |
13 | | ne0i 3880 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑀) ∈ ran 𝐹 → ran 𝐹 ≠ ∅) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝐹 ≠ ∅) |
15 | | climinf.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘)) |
16 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝐹‘𝑘) → (𝑥 ≤ 𝑦 ↔ 𝑥 ≤ (𝐹‘𝑘))) |
17 | 16 | ralrn 6270 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝑍 → (∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ↔ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘))) |
18 | 17 | rexbidv 3034 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝑍 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘))) |
19 | 5, 18 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘))) |
20 | 15, 19 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) |
21 | 3, 14, 20 | 3jca 1235 |
. . . . . . . . . 10
⊢ (𝜑 → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦)) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦)) |
23 | | infrecl 10882 |
. . . . . . . . 9
⊢ ((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) → inf(ran 𝐹, ℝ, < ) ∈
ℝ) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → inf(ran
𝐹, ℝ, < ) ∈
ℝ) |
25 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ+) |
26 | 24, 25 | ltaddrpd 11781 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → inf(ran
𝐹, ℝ, < ) <
(inf(ran 𝐹, ℝ, < )
+ 𝑦)) |
27 | | rpre 11715 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
28 | 27 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ) |
29 | 24, 28 | readdcld 9948 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (inf(ran
𝐹, ℝ, < ) + 𝑦) ∈
ℝ) |
30 | | infrglb 38657 |
. . . . . . . 8
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) ∧ (inf(ran 𝐹, ℝ, < ) + 𝑦) ∈ ℝ) → (inf(ran 𝐹, ℝ, < ) < (inf(ran
𝐹, ℝ, < ) + 𝑦) ↔ ∃𝑘 ∈ ran 𝐹 𝑘 < (inf(ran 𝐹, ℝ, < ) + 𝑦))) |
31 | 22, 29, 30 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (inf(ran
𝐹, ℝ, < ) <
(inf(ran 𝐹, ℝ, < )
+ 𝑦) ↔ ∃𝑘 ∈ ran 𝐹 𝑘 < (inf(ran 𝐹, ℝ, < ) + 𝑦))) |
32 | 26, 31 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑘 ∈ ran 𝐹 𝑘 < (inf(ran 𝐹, ℝ, < ) + 𝑦)) |
33 | 3 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ran 𝐹) → 𝑘 ∈ ℝ) |
34 | 33 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → 𝑘 ∈ ℝ) |
35 | 24 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → inf(ran 𝐹, ℝ, < ) ∈
ℝ) |
36 | 27 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → 𝑦 ∈ ℝ) |
37 | 35, 36 | readdcld 9948 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → (inf(ran 𝐹, ℝ, < ) + 𝑦) ∈ ℝ) |
38 | 34, 37, 36 | ltsub1d 10515 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → (𝑘 < (inf(ran 𝐹, ℝ, < ) + 𝑦) ↔ (𝑘 − 𝑦) < ((inf(ran 𝐹, ℝ, < ) + 𝑦) − 𝑦))) |
39 | 3, 14, 20, 23 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → inf(ran 𝐹, ℝ, < ) ∈
ℝ) |
40 | 39 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → inf(ran 𝐹, ℝ, < ) ∈
ℂ) |
41 | 40 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → inf(ran 𝐹, ℝ, < ) ∈
ℂ) |
42 | 36 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → 𝑦 ∈ ℂ) |
43 | 41, 42 | pncand 10272 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → ((inf(ran 𝐹, ℝ, < ) + 𝑦) − 𝑦) = inf(ran 𝐹, ℝ, < )) |
44 | 43 | breq2d 4595 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → ((𝑘 − 𝑦) < ((inf(ran 𝐹, ℝ, < ) + 𝑦) − 𝑦) ↔ (𝑘 − 𝑦) < inf(ran 𝐹, ℝ, < ))) |
45 | 38, 44 | bitrd 267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → (𝑘 < (inf(ran 𝐹, ℝ, < ) + 𝑦) ↔ (𝑘 − 𝑦) < inf(ran 𝐹, ℝ, < ))) |
46 | 45 | biimpd 218 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ ran 𝐹) → (𝑘 < (inf(ran 𝐹, ℝ, < ) + 𝑦) → (𝑘 − 𝑦) < inf(ran 𝐹, ℝ, < ))) |
47 | 46 | reximdva 3000 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑘 ∈ ran 𝐹 𝑘 < (inf(ran 𝐹, ℝ, < ) + 𝑦) → ∃𝑘 ∈ ran 𝐹(𝑘 − 𝑦) < inf(ran 𝐹, ℝ, < ))) |
48 | 32, 47 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑘 ∈ ran 𝐹(𝑘 − 𝑦) < inf(ran 𝐹, ℝ, < )) |
49 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = (𝐹‘𝑗) → (𝑘 − 𝑦) = ((𝐹‘𝑗) − 𝑦)) |
50 | 49 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑘 = (𝐹‘𝑗) → ((𝑘 − 𝑦) < inf(ran 𝐹, ℝ, < ) ↔ ((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < ))) |
51 | 50 | rexrn 6269 |
. . . . . . 7
⊢ (𝐹 Fn 𝑍 → (∃𝑘 ∈ ran 𝐹(𝑘 − 𝑦) < inf(ran 𝐹, ℝ, < ) ↔ ∃𝑗 ∈ 𝑍 ((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < ))) |
52 | 5, 51 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∃𝑘 ∈ ran 𝐹(𝑘 − 𝑦) < inf(ran 𝐹, ℝ, < ) ↔ ∃𝑗 ∈ 𝑍 ((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < ))) |
53 | 52 | biimpa 500 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑘 ∈ ran 𝐹(𝑘 − 𝑦) < inf(ran 𝐹, ℝ, < )) → ∃𝑗 ∈ 𝑍 ((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < )) |
54 | 48, 53 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < )) |
55 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹:𝑍⟶ℝ) |
56 | 9 | uztrn2 11581 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
57 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
58 | 55, 56, 57 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑘) ∈ ℝ) |
59 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑗 ∈ 𝑍) |
60 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈ ℝ) |
61 | 55, 59, 60 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑗) ∈ ℝ) |
62 | 39 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → inf(ran 𝐹, ℝ, < ) ∈
ℝ) |
63 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝑘 ∈ (ℤ≥‘𝑗)) |
64 | | fzssuz 12253 |
. . . . . . . . . . . . . 14
⊢ (𝑗...𝑘) ⊆ (ℤ≥‘𝑗) |
65 | | uzss 11584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑗) ⊆
(ℤ≥‘𝑀)) |
66 | 65, 9 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑗) ⊆ 𝑍) |
67 | 66, 9 | eleq2s 2706 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → (ℤ≥‘𝑗) ⊆ 𝑍) |
68 | 67 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) →
(ℤ≥‘𝑗) ⊆ 𝑍) |
69 | 64, 68 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝑗...𝑘) ⊆ 𝑍) |
70 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ ℝ) |
71 | 70 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑍⟶ℝ → ∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ) |
72 | 1, 71 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ) |
73 | 72 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ) |
74 | | ssralv 3629 |
. . . . . . . . . . . . 13
⊢ ((𝑗...𝑘) ⊆ 𝑍 → (∀𝑛 ∈ 𝑍 (𝐹‘𝑛) ∈ ℝ → ∀𝑛 ∈ (𝑗...𝑘)(𝐹‘𝑛) ∈ ℝ)) |
75 | 69, 73, 74 | sylc 63 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ∀𝑛 ∈ (𝑗...𝑘)(𝐹‘𝑛) ∈ ℝ) |
76 | 75 | r19.21bi 2916 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) ∧ 𝑛 ∈ (𝑗...𝑘)) → (𝐹‘𝑛) ∈ ℝ) |
77 | | fzssuz 12253 |
. . . . . . . . . . . . . 14
⊢ (𝑗...(𝑘 − 1)) ⊆
(ℤ≥‘𝑗) |
78 | 77, 68 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝑗...(𝑘 − 1)) ⊆ 𝑍) |
79 | 78 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) ∧ 𝑛 ∈ (𝑗...(𝑘 − 1))) → 𝑛 ∈ 𝑍) |
80 | | climinf.6 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
81 | 80 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
82 | 81 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ∀𝑘 ∈ 𝑍 (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
83 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1)) |
84 | 83 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1))) |
85 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
86 | 84, 85 | breq12d 4596 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ↔ (𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛))) |
87 | 86 | rspccva 3281 |
. . . . . . . . . . . . 13
⊢
((∀𝑘 ∈
𝑍 (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ∧ 𝑛 ∈ 𝑍) → (𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛)) |
88 | 82, 87 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) ∧ 𝑛 ∈ 𝑍) → (𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛)) |
89 | 79, 88 | syldan 486 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) ∧ 𝑛 ∈ (𝑗...(𝑘 − 1))) → (𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛)) |
90 | 63, 76, 89 | monoord2 12694 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑘) ≤ (𝐹‘𝑗)) |
91 | 58, 61, 62, 90 | lesub1dd 10522 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < )) ≤ ((𝐹‘𝑗) − inf(ran 𝐹, ℝ, < ))) |
92 | 58, 62 | resubcld 10337 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < )) ∈
ℝ) |
93 | 61, 62 | resubcld 10337 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑗) − inf(ran 𝐹, ℝ, < )) ∈
ℝ) |
94 | 27 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝑦 ∈ ℝ) |
95 | | lelttr 10007 |
. . . . . . . . . 10
⊢ ((((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < )) ∈ ℝ ∧
((𝐹‘𝑗) − inf(ran 𝐹, ℝ, < )) ∈
ℝ ∧ 𝑦 ∈
ℝ) → ((((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < )) ≤ ((𝐹‘𝑗) − inf(ran 𝐹, ℝ, < )) ∧ ((𝐹‘𝑗) − inf(ran 𝐹, ℝ, < )) < 𝑦) → ((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < )) < 𝑦)) |
96 | 92, 93, 94, 95 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < )) ≤ ((𝐹‘𝑗) − inf(ran 𝐹, ℝ, < )) ∧ ((𝐹‘𝑗) − inf(ran 𝐹, ℝ, < )) < 𝑦) → ((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < )) < 𝑦)) |
97 | 91, 96 | mpand 707 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (((𝐹‘𝑗) − inf(ran 𝐹, ℝ, < )) < 𝑦 → ((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < )) < 𝑦)) |
98 | | ltsub23 10387 |
. . . . . . . . 9
⊢ (((𝐹‘𝑗) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ inf(ran 𝐹, ℝ, < ) ∈
ℝ) → (((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < ) ↔ ((𝐹‘𝑗) − inf(ran 𝐹, ℝ, < )) < 𝑦)) |
99 | 61, 94, 62, 98 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < ) ↔ ((𝐹‘𝑗) − inf(ran 𝐹, ℝ, < )) < 𝑦)) |
100 | 3 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ran 𝐹 ⊆ ℝ) |
101 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹 Fn 𝑍) |
102 | | fnfvelrn 6264 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ran 𝐹) |
103 | 101, 56, 102 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑘) ∈ ran 𝐹) |
104 | 100, 103 | sseldd 3569 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑘) ∈ ℝ) |
105 | 20 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦) |
106 | | infrelb 10885 |
. . . . . . . . . . 11
⊢ ((ran
𝐹 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ∧ (𝐹‘𝑘) ∈ ran 𝐹) → inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑘)) |
107 | 100, 105,
103, 106 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → inf(ran 𝐹, ℝ, < ) ≤ (𝐹‘𝑘)) |
108 | 62, 104, 107 | abssubge0d 14018 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (abs‘((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < ))) = ((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < ))) |
109 | 108 | breq1d 4593 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((abs‘((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < ))) < 𝑦 ↔ ((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < )) < 𝑦)) |
110 | 97, 99, 109 | 3imtr4d 282 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < ) → (abs‘((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < ))) < 𝑦)) |
111 | 110 | anassrs 678 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < ) → (abs‘((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < ))) < 𝑦)) |
112 | 111 | ralrimdva 2952 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < ) → ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < ))) < 𝑦)) |
113 | 112 | reximdva 3000 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 ((𝐹‘𝑗) − 𝑦) < inf(ran 𝐹, ℝ, < ) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < ))) < 𝑦)) |
114 | 54, 113 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < ))) < 𝑦) |
115 | 114 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < ))) < 𝑦) |
116 | | fvex 6113 |
. . . . 5
⊢
(ℤ≥‘𝑀) ∈ V |
117 | 9, 116 | eqeltri 2684 |
. . . 4
⊢ 𝑍 ∈ V |
118 | | fex 6394 |
. . . 4
⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑍 ∈ V) → 𝐹 ∈ V) |
119 | 1, 117, 118 | sylancl 693 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
120 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
121 | 1 | ffvelrnda 6267 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
122 | 121 | recnd 9947 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
123 | 9, 6, 119, 120, 40, 122 | clim2c 14084 |
. 2
⊢ (𝜑 → (𝐹 ⇝ inf(ran 𝐹, ℝ, < ) ↔ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − inf(ran 𝐹, ℝ, < ))) < 𝑦)) |
124 | 115, 123 | mpbird 246 |
1
⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ, < )) |