Step | Hyp | Ref
| Expression |
1 | | lmdvg.3 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ ) |
2 | | nnuz 11723 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
3 | | 1zzd 11408 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 1 ∈ ℤ) |
4 | | lmdvg.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞)) |
5 | | rge0ssre 12280 |
. . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ ℝ |
6 | | fss 6056 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℕ⟶ℝ) |
7 | 4, 5, 6 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
8 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 𝐹:ℕ⟶ℝ) |
9 | | lmdvg.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
10 | 9 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
11 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (𝐹‘𝑘) = (𝐹‘𝑙)) |
12 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑙 → (𝑘 + 1) = (𝑙 + 1)) |
13 | 12 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑙 + 1))) |
14 | 11, 13 | breq12d 4666 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑙 → ((𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1)))) |
15 | 14 | cbvralv 3171 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
ℕ (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ↔ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) |
16 | 10, 15 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) |
17 | 16 | r19.21bi 2932 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) |
18 | 17 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) ∧ 𝑙 ∈ ℕ) → (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) |
19 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) |
20 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑙 → (𝐹‘𝑗) = (𝐹‘𝑙)) |
21 | 20 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑙 → ((𝐹‘𝑗) ≤ 𝑥 ↔ (𝐹‘𝑙) ≤ 𝑥)) |
22 | 21 | cbvralv 3171 |
. . . . . . . . . . 11
⊢
(∀𝑗 ∈
ℕ (𝐹‘𝑗) ≤ 𝑥 ↔ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ 𝑥) |
23 | 22 | rexbii 3041 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
ℝ ∀𝑗 ∈
ℕ (𝐹‘𝑗) ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ 𝑥) |
24 | 19, 23 | sylib 208 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ 𝑥) |
25 | 2, 3, 8, 18, 24 | climsup 14400 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) |
26 | | nnex 11026 |
. . . . . . . . . . 11
⊢ ℕ
∈ V |
27 | | fex 6490 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ ℕ ∈ V) → 𝐹 ∈ V) |
28 | 4, 26, 27 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ V) |
29 | 28 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ∈ V) |
30 | | ltso 10118 |
. . . . . . . . . . 11
⊢ < Or
ℝ |
31 | 30 | supex 8369 |
. . . . . . . . . 10
⊢ sup(ran
𝐹, ℝ, < ) ∈
V |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → sup(ran 𝐹, ℝ, < ) ∈
V) |
33 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) |
34 | | breldmg 5330 |
. . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ sup(ran 𝐹, ℝ, < ) ∈ V ∧
𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ∈ dom ⇝
) |
35 | 29, 32, 33, 34 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ∈ dom ⇝ ) |
36 | 25, 35 | syldan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 𝐹 ∈ dom ⇝ ) |
37 | 1, 36 | mtand 691 |
. . . . . 6
⊢ (𝜑 → ¬ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) |
38 | | ralnex 2992 |
. . . . . 6
⊢
(∀𝑥 ∈
ℝ ¬ ∀𝑗
∈ ℕ (𝐹‘𝑗) ≤ 𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) |
39 | 37, 38 | sylibr 224 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) |
40 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈ ℝ) |
41 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐹:ℕ⟶ℝ) |
42 | 41 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ) |
43 | 40, 42 | ltnled 10184 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑥 < (𝐹‘𝑗) ↔ ¬ (𝐹‘𝑗) ≤ 𝑥)) |
44 | 43 | rexbidva 3049 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) ↔ ∃𝑗 ∈ ℕ ¬ (𝐹‘𝑗) ≤ 𝑥)) |
45 | | rexnal 2995 |
. . . . . . 7
⊢
(∃𝑗 ∈
ℕ ¬ (𝐹‘𝑗) ≤ 𝑥 ↔ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) |
46 | 44, 45 | syl6bb 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) ↔ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥)) |
47 | 46 | ralbidva 2985 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) ↔ ∀𝑥 ∈ ℝ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥)) |
48 | 39, 47 | mpbird 247 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗)) |
49 | 48 | r19.21bi 2932 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗)) |
50 | 40 | ad2antrr 762 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 ∈ ℝ) |
51 | 42 | ad2antrr 762 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ∈ ℝ) |
52 | 41 | ad3antrrr 766 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐹:ℕ⟶ℝ) |
53 | | uznnssnn 11735 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ →
(ℤ≥‘𝑗) ⊆ ℕ) |
54 | 53 | ad3antlr 767 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) →
(ℤ≥‘𝑗) ⊆ ℕ) |
55 | | simpr 477 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ (ℤ≥‘𝑗)) |
56 | 54, 55 | sseldd 3604 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
57 | 52, 56 | ffvelrnd 6360 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℝ) |
58 | | simplr 792 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 < (𝐹‘𝑗)) |
59 | | simp-4l 806 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝜑) |
60 | | simpllr 799 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑗 ∈ ℕ) |
61 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ (ℤ≥‘𝑗)) |
62 | 7 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → 𝐹:ℕ⟶ℝ) |
63 | | fzssnn 12385 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗...𝑘) ⊆ ℕ) |
64 | 63 | ad3antlr 767 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → (𝑗...𝑘) ⊆ ℕ) |
65 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → 𝑙 ∈ (𝑗...𝑘)) |
66 | 64, 65 | sseldd 3604 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → 𝑙 ∈ ℕ) |
67 | 62, 66 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → (𝐹‘𝑙) ∈ ℝ) |
68 | | simplll 798 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → 𝜑) |
69 | | fzssnn 12385 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗...(𝑘 − 1)) ⊆
ℕ) |
70 | 69 | ad3antlr 767 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → (𝑗...(𝑘 − 1)) ⊆
ℕ) |
71 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → 𝑙 ∈ (𝑗...(𝑘 − 1))) |
72 | 70, 71 | sseldd 3604 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → 𝑙 ∈ ℕ) |
73 | 68, 72, 17 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) |
74 | 61, 67, 73 | monoord 12831 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ≤ (𝐹‘𝑘)) |
75 | 59, 60, 55, 74 | syl21anc 1325 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ≤ (𝐹‘𝑘)) |
76 | 50, 51, 57, 58, 75 | ltletrd 10197 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 < (𝐹‘𝑘)) |
77 | 76 | ralrimiva 2966 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) → ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |
78 | 77 | ex 450 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑥 < (𝐹‘𝑗) → ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))) |
79 | 78 | reximdva 3017 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))) |
80 | 49, 79 | mpd 15 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |
81 | 80 | ralrimiva 2966 |
1
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |