| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lmdvg.3 | . . . . . . 7
⊢ (𝜑 → ¬ 𝐹 ∈ dom ⇝ ) | 
| 2 |  | nnuz 12921 | . . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) | 
| 3 |  | 1zzd 12648 | . . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 1 ∈ ℤ) | 
| 4 |  | lmdvg.1 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶(0[,)+∞)) | 
| 5 |  | rge0ssre 13496 | . . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ ℝ | 
| 6 |  | fss 6752 | . . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℕ⟶ℝ) | 
| 7 | 4, 5, 6 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) | 
| 8 | 7 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 𝐹:ℕ⟶ℝ) | 
| 9 |  | lmdvg.2 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) | 
| 10 | 9 | ralrimiva 3146 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) | 
| 11 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (𝐹‘𝑘) = (𝐹‘𝑙)) | 
| 12 |  | fvoveq1 7454 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑙 + 1))) | 
| 13 | 11, 12 | breq12d 5156 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑙 → ((𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1)))) | 
| 14 | 13 | cbvralvw 3237 | . . . . . . . . . . . 12
⊢
(∀𝑘 ∈
ℕ (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ↔ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) | 
| 15 | 10, 14 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) | 
| 16 | 15 | r19.21bi 3251 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) | 
| 17 | 16 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) ∧ 𝑙 ∈ ℕ) → (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) | 
| 18 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) | 
| 19 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑗 = 𝑙 → (𝐹‘𝑗) = (𝐹‘𝑙)) | 
| 20 | 19 | breq1d 5153 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝑙 → ((𝐹‘𝑗) ≤ 𝑥 ↔ (𝐹‘𝑙) ≤ 𝑥)) | 
| 21 | 20 | cbvralvw 3237 | . . . . . . . . . . 11
⊢
(∀𝑗 ∈
ℕ (𝐹‘𝑗) ≤ 𝑥 ↔ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ 𝑥) | 
| 22 | 21 | rexbii 3094 | . . . . . . . . . 10
⊢
(∃𝑥 ∈
ℝ ∀𝑗 ∈
ℕ (𝐹‘𝑗) ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ 𝑥) | 
| 23 | 18, 22 | sylib 218 | . . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ ℕ (𝐹‘𝑙) ≤ 𝑥) | 
| 24 | 2, 3, 8, 17, 23 | climsup 15706 | . . . . . . . 8
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) | 
| 25 |  | nnex 12272 | . . . . . . . . . . 11
⊢ ℕ
∈ V | 
| 26 |  | fex 7246 | . . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶(0[,)+∞)
∧ ℕ ∈ V) → 𝐹 ∈ V) | 
| 27 | 4, 25, 26 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ V) | 
| 28 | 27 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ∈ V) | 
| 29 |  | ltso 11341 | . . . . . . . . . . 11
⊢  < Or
ℝ | 
| 30 | 29 | supex 9503 | . . . . . . . . . 10
⊢ sup(ran
𝐹, ℝ, < ) ∈
V | 
| 31 | 30 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → sup(ran 𝐹, ℝ, < ) ∈
V) | 
| 32 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) | 
| 33 |  | breldmg 5920 | . . . . . . . . 9
⊢ ((𝐹 ∈ V ∧ sup(ran 𝐹, ℝ, < ) ∈ V ∧
𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ∈ dom ⇝
) | 
| 34 | 28, 31, 32, 33 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ⇝ sup(ran 𝐹, ℝ, < )) → 𝐹 ∈ dom ⇝ ) | 
| 35 | 24, 34 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) → 𝐹 ∈ dom ⇝ ) | 
| 36 | 1, 35 | mtand 816 | . . . . . 6
⊢ (𝜑 → ¬ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) | 
| 37 |  | ralnex 3072 | . . . . . 6
⊢
(∀𝑥 ∈
ℝ ¬ ∀𝑗
∈ ℕ (𝐹‘𝑗) ≤ 𝑥 ↔ ¬ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) | 
| 38 | 36, 37 | sylibr 234 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) | 
| 39 |  | simplr 769 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈ ℝ) | 
| 40 | 7 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐹:ℕ⟶ℝ) | 
| 41 | 40 | ffvelcdmda 7104 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ) | 
| 42 | 39, 41 | ltnled 11408 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑥 < (𝐹‘𝑗) ↔ ¬ (𝐹‘𝑗) ≤ 𝑥)) | 
| 43 | 42 | rexbidva 3177 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) ↔ ∃𝑗 ∈ ℕ ¬ (𝐹‘𝑗) ≤ 𝑥)) | 
| 44 |  | rexnal 3100 | . . . . . . 7
⊢
(∃𝑗 ∈
ℕ ¬ (𝐹‘𝑗) ≤ 𝑥 ↔ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥) | 
| 45 | 43, 44 | bitrdi 287 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) ↔ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥)) | 
| 46 | 45 | ralbidva 3176 | . . . . 5
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) ↔ ∀𝑥 ∈ ℝ ¬ ∀𝑗 ∈ ℕ (𝐹‘𝑗) ≤ 𝑥)) | 
| 47 | 38, 46 | mpbird 257 | . . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗)) | 
| 48 | 47 | r19.21bi 3251 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗)) | 
| 49 | 39 | ad2antrr 726 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 ∈ ℝ) | 
| 50 | 41 | ad2antrr 726 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ∈ ℝ) | 
| 51 | 40 | ad3antrrr 730 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐹:ℕ⟶ℝ) | 
| 52 |  | uznnssnn 12937 | . . . . . . . . . 10
⊢ (𝑗 ∈ ℕ →
(ℤ≥‘𝑗) ⊆ ℕ) | 
| 53 | 52 | ad3antlr 731 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) →
(ℤ≥‘𝑗) ⊆ ℕ) | 
| 54 |  | simpr 484 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ (ℤ≥‘𝑗)) | 
| 55 | 53, 54 | sseldd 3984 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) | 
| 56 | 51, 55 | ffvelcdmd 7105 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ ℝ) | 
| 57 |  | simplr 769 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 < (𝐹‘𝑗)) | 
| 58 |  | simp-4l 783 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝜑) | 
| 59 |  | simpllr 776 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑗 ∈ ℕ) | 
| 60 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ (ℤ≥‘𝑗)) | 
| 61 | 7 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → 𝐹:ℕ⟶ℝ) | 
| 62 |  | fzssnn 13608 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗...𝑘) ⊆ ℕ) | 
| 63 | 62 | ad3antlr 731 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → (𝑗...𝑘) ⊆ ℕ) | 
| 64 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → 𝑙 ∈ (𝑗...𝑘)) | 
| 65 | 63, 64 | sseldd 3984 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → 𝑙 ∈ ℕ) | 
| 66 | 61, 65 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...𝑘)) → (𝐹‘𝑙) ∈ ℝ) | 
| 67 |  | simplll 775 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → 𝜑) | 
| 68 |  | fzssnn 13608 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗...(𝑘 − 1)) ⊆
ℕ) | 
| 69 | 68 | ad3antlr 731 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → (𝑗...(𝑘 − 1)) ⊆
ℕ) | 
| 70 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → 𝑙 ∈ (𝑗...(𝑘 − 1))) | 
| 71 | 69, 70 | sseldd 3984 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → 𝑙 ∈ ℕ) | 
| 72 | 67, 71, 16 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑙 ∈ (𝑗...(𝑘 − 1))) → (𝐹‘𝑙) ≤ (𝐹‘(𝑙 + 1))) | 
| 73 | 60, 66, 72 | monoord 14073 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ≤ (𝐹‘𝑘)) | 
| 74 | 58, 59, 54, 73 | syl21anc 838 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ≤ (𝐹‘𝑘)) | 
| 75 | 49, 50, 56, 57, 74 | ltletrd 11421 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑥 < (𝐹‘𝑘)) | 
| 76 | 75 | ralrimiva 3146 | . . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) ∧ 𝑥 < (𝐹‘𝑗)) → ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) | 
| 77 | 76 | ex 412 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → (𝑥 < (𝐹‘𝑗) → ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))) | 
| 78 | 77 | reximdva 3168 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ ℕ 𝑥 < (𝐹‘𝑗) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))) | 
| 79 | 48, 78 | mpd 15 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) | 
| 80 | 79 | ralrimiva 3146 | 1
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |