Step | Hyp | Ref
| Expression |
1 | | lmdvg.3 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ ) |
2 | | nnuz 12630 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
3 | | 1zzd 12360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 1 ∈ ℤ) |
4 | | lmdvg.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞)) |
5 | | rge0ssre 13197 |
. . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ ℝ |
6 | | fss 6626 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℕ⟶ℝ) |
7 | 4, 5, 6 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
8 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 𝐹:ℕ⟶ℝ) |
9 | | lmdvg.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
10 | 9 | ralrimiva 3104 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
11 | | fveq2 6783 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (𝐹‘𝑘) = (𝐹‘𝑙)) |
12 | | fvoveq1 7307 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑙 + 1))) |
13 | 11, 12 | breq12d 5088 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑙 → ((𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1)))) |
14 | 13 | cbvralvw 3384 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
ℕ (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ↔ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) |
15 | 10, 14 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) |
16 | 15 | r19.21bi 3135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) |
17 | 16 | adantlr 712 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) ∧ 𝑙 ∈ ℕ) → (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) |
18 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) |
19 | | fveq2 6783 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑙 → (𝐹‘𝑗) = (𝐹‘𝑙)) |
20 | 19 | breq1d 5085 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑙 → ((𝐹‘𝑗) ≤ 𝑥 ↔ (𝐹‘𝑙) ≤ 𝑥)) |
21 | 20 | cbvralvw 3384 |
. . . . . . . . . . 11
⊢
(∀𝑗 ∈
ℕ (𝐹‘𝑗) ≤ 𝑥 ↔ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ 𝑥) |
22 | 21 | rexbii 3182 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
ℝ ∀𝑗 ∈
ℕ (𝐹‘𝑗) ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ 𝑥) |
23 | 18, 22 | sylib 217 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ 𝑥) |
24 | 2, 3, 8, 17, 23 | climsup 15390 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) |
25 | | nnex 11988 |
. . . . . . . . . . 11
⊢ ℕ
∈ V |
26 | | fex 7111 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ ℕ ∈ V) → 𝐹 ∈ V) |
27 | 4, 25, 26 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ V) |
28 | 27 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ∈ V) |
29 | | ltso 11064 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
30 | 29 | supex 9231 |
. . . . . . . . . 10
⊢ sup(ran
𝐹, ℝ, < ) ∈
V |
31 | 30 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → sup(ran 𝐹, ℝ, < ) ∈
V) |
32 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) |
33 | | breldmg 5821 |
. . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ sup(ran 𝐹, ℝ, < ) ∈ V ∧
𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ∈ dom ⇝
) |
34 | 28, 31, 32, 33 | syl3anc 1370 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ∈ dom ⇝ ) |
35 | 24, 34 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 𝐹 ∈ dom ⇝ ) |
36 | 1, 35 | mtand 813 |
. . . . . 6
⊢ (𝜑 → ¬ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) |
37 | | ralnex 3168 |
. . . . . 6
⊢
(∀𝑥 ∈
ℝ ¬ ∀𝑗
∈ ℕ (𝐹‘𝑗) ≤ 𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) |
38 | 36, 37 | sylibr 233 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) |
39 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈ ℝ) |
40 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐹:ℕ⟶ℝ) |
41 | 40 | ffvelrnda 6970 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ) |
42 | 39, 41 | ltnled 11131 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑥 < (𝐹‘𝑗) ↔ ¬ (𝐹‘𝑗) ≤ 𝑥)) |
43 | 42 | rexbidva 3226 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) ↔ ∃𝑗 ∈ ℕ ¬ (𝐹‘𝑗) ≤ 𝑥)) |
44 | | rexnal 3170 |
. . . . . . 7
⊢
(∃𝑗 ∈
ℕ ¬ (𝐹‘𝑗) ≤ 𝑥 ↔ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) |
45 | 43, 44 | bitrdi 287 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) ↔ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥)) |
46 | 45 | ralbidva 3112 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) ↔ ∀𝑥 ∈ ℝ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥)) |
47 | 38, 46 | mpbird 256 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗)) |
48 | 47 | r19.21bi 3135 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗)) |
49 | 39 | ad2antrr 723 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 ∈ ℝ) |
50 | 41 | ad2antrr 723 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ∈ ℝ) |
51 | 40 | ad3antrrr 727 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐹:ℕ⟶ℝ) |
52 | | uznnssnn 12644 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ →
(ℤ≥‘𝑗) ⊆ ℕ) |
53 | 52 | ad3antlr 728 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) →
(ℤ≥‘𝑗) ⊆ ℕ) |
54 | | simpr 485 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ (ℤ≥‘𝑗)) |
55 | 53, 54 | sseldd 3923 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
56 | 51, 55 | ffvelrnd 6971 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℝ) |
57 | | simplr 766 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 < (𝐹‘𝑗)) |
58 | | simp-4l 780 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝜑) |
59 | | simpllr 773 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑗 ∈ ℕ) |
60 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ (ℤ≥‘𝑗)) |
61 | 7 | ad3antrrr 727 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → 𝐹:ℕ⟶ℝ) |
62 | | fzssnn 13309 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗...𝑘) ⊆ ℕ) |
63 | 62 | ad3antlr 728 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → (𝑗...𝑘) ⊆ ℕ) |
64 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → 𝑙 ∈ (𝑗...𝑘)) |
65 | 63, 64 | sseldd 3923 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → 𝑙 ∈ ℕ) |
66 | 61, 65 | ffvelrnd 6971 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → (𝐹‘𝑙) ∈ ℝ) |
67 | | simplll 772 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → 𝜑) |
68 | | fzssnn 13309 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗...(𝑘 − 1)) ⊆
ℕ) |
69 | 68 | ad3antlr 728 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → (𝑗...(𝑘 − 1)) ⊆
ℕ) |
70 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → 𝑙 ∈ (𝑗...(𝑘 − 1))) |
71 | 69, 70 | sseldd 3923 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → 𝑙 ∈ ℕ) |
72 | 67, 71, 16 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) |
73 | 60, 66, 72 | monoord 13762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ≤ (𝐹‘𝑘)) |
74 | 58, 59, 54, 73 | syl21anc 835 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ≤ (𝐹‘𝑘)) |
75 | 49, 50, 56, 57, 74 | ltletrd 11144 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 < (𝐹‘𝑘)) |
76 | 75 | ralrimiva 3104 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) → ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |
77 | 76 | ex 413 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑥 < (𝐹‘𝑗) → ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))) |
78 | 77 | reximdva 3204 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))) |
79 | 48, 78 | mpd 15 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |
80 | 79 | ralrimiva 3104 |
1
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |