Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  climsup Structured version   Visualization version   GIF version

Theorem climsup 14619
 Description: A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
Hypotheses
Ref Expression
climsup.1 𝑍 = (ℤ𝑀)
climsup.2 (𝜑𝑀 ∈ ℤ)
climsup.3 (𝜑𝐹:𝑍⟶ℝ)
climsup.4 ((𝜑𝑘𝑍) → (𝐹𝑘) ≤ (𝐹‘(𝑘 + 1)))
climsup.5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘𝑍 (𝐹𝑘) ≤ 𝑥)
Assertion
Ref Expression
climsup (𝜑𝐹 ⇝ sup(ran 𝐹, ℝ, < ))
Distinct variable groups:   𝑥,𝑘,𝐹   𝜑,𝑘   𝑘,𝑍,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑀(𝑥,𝑘)

Proof of Theorem climsup
Dummy variables 𝑗 𝑛 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 climsup.3 . . . . . . . . . 10 (𝜑𝐹:𝑍⟶ℝ)
2 frn 6214 . . . . . . . . . 10 (𝐹:𝑍⟶ℝ → ran 𝐹 ⊆ ℝ)
31, 2syl 17 . . . . . . . . 9 (𝜑 → ran 𝐹 ⊆ ℝ)
4 ffn 6206 . . . . . . . . . . . 12 (𝐹:𝑍⟶ℝ → 𝐹 Fn 𝑍)
51, 4syl 17 . . . . . . . . . . 11 (𝜑𝐹 Fn 𝑍)
6 climsup.2 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℤ)
7 uzid 11914 . . . . . . . . . . . . 13 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
86, 7syl 17 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (ℤ𝑀))
9 climsup.1 . . . . . . . . . . . 12 𝑍 = (ℤ𝑀)
108, 9syl6eleqr 2850 . . . . . . . . . . 11 (𝜑𝑀𝑍)
11 fnfvelrn 6520 . . . . . . . . . . 11 ((𝐹 Fn 𝑍𝑀𝑍) → (𝐹𝑀) ∈ ran 𝐹)
125, 10, 11syl2anc 696 . . . . . . . . . 10 (𝜑 → (𝐹𝑀) ∈ ran 𝐹)
13 ne0i 4064 . . . . . . . . . 10 ((𝐹𝑀) ∈ ran 𝐹 → ran 𝐹 ≠ ∅)
1412, 13syl 17 . . . . . . . . 9 (𝜑 → ran 𝐹 ≠ ∅)
15 climsup.5 . . . . . . . . . 10 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘𝑍 (𝐹𝑘) ≤ 𝑥)
16 breq1 4807 . . . . . . . . . . . . 13 (𝑦 = (𝐹𝑘) → (𝑦𝑥 ↔ (𝐹𝑘) ≤ 𝑥))
1716ralrn 6526 . . . . . . . . . . . 12 (𝐹 Fn 𝑍 → (∀𝑦 ∈ ran 𝐹 𝑦𝑥 ↔ ∀𝑘𝑍 (𝐹𝑘) ≤ 𝑥))
1817rexbidv 3190 . . . . . . . . . . 11 (𝐹 Fn 𝑍 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘𝑍 (𝐹𝑘) ≤ 𝑥))
195, 18syl 17 . . . . . . . . . 10 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘𝑍 (𝐹𝑘) ≤ 𝑥))
2015, 19mpbird 247 . . . . . . . . 9 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦𝑥)
213, 14, 203jca 1123 . . . . . . . 8 (𝜑 → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦𝑥))
22 suprcl 11195 . . . . . . . 8 ((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦𝑥) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
2321, 22syl 17 . . . . . . 7 (𝜑 → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
24 ltsubrp 12079 . . . . . . 7 ((sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ 𝑦 ∈ ℝ+) → (sup(ran 𝐹, ℝ, < ) − 𝑦) < sup(ran 𝐹, ℝ, < ))
2523, 24sylan 489 . . . . . 6 ((𝜑𝑦 ∈ ℝ+) → (sup(ran 𝐹, ℝ, < ) − 𝑦) < sup(ran 𝐹, ℝ, < ))
2621adantr 472 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦𝑥))
27 rpre 12052 . . . . . . . 8 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
28 resubcl 10557 . . . . . . . 8 ((sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) − 𝑦) ∈ ℝ)
2923, 27, 28syl2an 495 . . . . . . 7 ((𝜑𝑦 ∈ ℝ+) → (sup(ran 𝐹, ℝ, < ) − 𝑦) ∈ ℝ)
30 suprlub 11199 . . . . . . 7 (((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦𝑥) ∧ (sup(ran 𝐹, ℝ, < ) − 𝑦) ∈ ℝ) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < sup(ran 𝐹, ℝ, < ) ↔ ∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘))
3126, 29, 30syl2anc 696 . . . . . 6 ((𝜑𝑦 ∈ ℝ+) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < sup(ran 𝐹, ℝ, < ) ↔ ∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘))
3225, 31mpbid 222 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → ∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘)
33 breq2 4808 . . . . . . . 8 (𝑘 = (𝐹𝑗) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘 ↔ (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗)))
3433rexrn 6525 . . . . . . 7 (𝐹 Fn 𝑍 → (∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘 ↔ ∃𝑗𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗)))
355, 34syl 17 . . . . . 6 (𝜑 → (∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘 ↔ ∃𝑗𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗)))
3635biimpa 502 . . . . 5 ((𝜑 ∧ ∃𝑘 ∈ ran 𝐹(sup(ran 𝐹, ℝ, < ) − 𝑦) < 𝑘) → ∃𝑗𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗))
3732, 36syldan 488 . . . 4 ((𝜑𝑦 ∈ ℝ+) → ∃𝑗𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗))
38 ffvelrn 6521 . . . . . . . . . . . 12 ((𝐹:𝑍⟶ℝ ∧ 𝑗𝑍) → (𝐹𝑗) ∈ ℝ)
391, 38sylan 489 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (𝐹𝑗) ∈ ℝ)
4039ad2ant2r 800 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝐹𝑗) ∈ ℝ)
411adantr 472 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ+) → 𝐹:𝑍⟶ℝ)
429uztrn2 11917 . . . . . . . . . . 11 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
43 ffvelrn 6521 . . . . . . . . . . 11 ((𝐹:𝑍⟶ℝ ∧ 𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
4441, 42, 43syl2an 495 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝐹𝑘) ∈ ℝ)
4523ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
46 simprr 813 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → 𝑘 ∈ (ℤ𝑗))
47 fzssuz 12595 . . . . . . . . . . . . . 14 (𝑗...𝑘) ⊆ (ℤ𝑗)
48 uzss 11920 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℤ𝑀) → (ℤ𝑗) ⊆ (ℤ𝑀))
4948, 9syl6sseqr 3793 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) → (ℤ𝑗) ⊆ 𝑍)
5049, 9eleq2s 2857 . . . . . . . . . . . . . . 15 (𝑗𝑍 → (ℤ𝑗) ⊆ 𝑍)
5150ad2antrl 766 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (ℤ𝑗) ⊆ 𝑍)
5247, 51syl5ss 3755 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝑗...𝑘) ⊆ 𝑍)
53 ffvelrn 6521 . . . . . . . . . . . . . . . 16 ((𝐹:𝑍⟶ℝ ∧ 𝑛𝑍) → (𝐹𝑛) ∈ ℝ)
5453ralrimiva 3104 . . . . . . . . . . . . . . 15 (𝐹:𝑍⟶ℝ → ∀𝑛𝑍 (𝐹𝑛) ∈ ℝ)
551, 54syl 17 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑛𝑍 (𝐹𝑛) ∈ ℝ)
5655ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ∀𝑛𝑍 (𝐹𝑛) ∈ ℝ)
57 ssralv 3807 . . . . . . . . . . . . 13 ((𝑗...𝑘) ⊆ 𝑍 → (∀𝑛𝑍 (𝐹𝑛) ∈ ℝ → ∀𝑛 ∈ (𝑗...𝑘)(𝐹𝑛) ∈ ℝ))
5852, 56, 57sylc 65 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ∀𝑛 ∈ (𝑗...𝑘)(𝐹𝑛) ∈ ℝ)
5958r19.21bi 3070 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) ∧ 𝑛 ∈ (𝑗...𝑘)) → (𝐹𝑛) ∈ ℝ)
60 fzssuz 12595 . . . . . . . . . . . . . 14 (𝑗...(𝑘 − 1)) ⊆ (ℤ𝑗)
6160, 51syl5ss 3755 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝑗...(𝑘 − 1)) ⊆ 𝑍)
6261sselda 3744 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) ∧ 𝑛 ∈ (𝑗...(𝑘 − 1))) → 𝑛𝑍)
63 climsup.4 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑍) → (𝐹𝑘) ≤ (𝐹‘(𝑘 + 1)))
6463ralrimiva 3104 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) ≤ (𝐹‘(𝑘 + 1)))
6564ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ∀𝑘𝑍 (𝐹𝑘) ≤ (𝐹‘(𝑘 + 1)))
66 fveq2 6353 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → (𝐹𝑘) = (𝐹𝑛))
67 oveq1 6821 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1))
6867fveq2d 6357 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1)))
6966, 68breq12d 4817 . . . . . . . . . . . . . 14 (𝑘 = 𝑛 → ((𝐹𝑘) ≤ (𝐹‘(𝑘 + 1)) ↔ (𝐹𝑛) ≤ (𝐹‘(𝑛 + 1))))
7069rspccva 3448 . . . . . . . . . . . . 13 ((∀𝑘𝑍 (𝐹𝑘) ≤ (𝐹‘(𝑘 + 1)) ∧ 𝑛𝑍) → (𝐹𝑛) ≤ (𝐹‘(𝑛 + 1)))
7165, 70sylan 489 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) ∧ 𝑛𝑍) → (𝐹𝑛) ≤ (𝐹‘(𝑛 + 1)))
7262, 71syldan 488 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) ∧ 𝑛 ∈ (𝑗...(𝑘 − 1))) → (𝐹𝑛) ≤ (𝐹‘(𝑛 + 1)))
7346, 59, 72monoord 13045 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝐹𝑗) ≤ (𝐹𝑘))
7440, 44, 45, 73lesub2dd 10856 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑘)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑗)))
7545, 44resubcld 10670 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑘)) ∈ ℝ)
7645, 40resubcld 10670 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑗)) ∈ ℝ)
7727ad2antlr 765 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → 𝑦 ∈ ℝ)
78 lelttr 10340 . . . . . . . . . 10 (((sup(ran 𝐹, ℝ, < ) − (𝐹𝑘)) ∈ ℝ ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑗)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((sup(ran 𝐹, ℝ, < ) − (𝐹𝑘)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑗)) ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑗)) < 𝑦) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑘)) < 𝑦))
7975, 76, 77, 78syl3anc 1477 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (((sup(ran 𝐹, ℝ, < ) − (𝐹𝑘)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑗)) ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑗)) < 𝑦) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑘)) < 𝑦))
8074, 79mpand 713 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((sup(ran 𝐹, ℝ, < ) − (𝐹𝑗)) < 𝑦 → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑘)) < 𝑦))
81 ltsub23 10720 . . . . . . . . 9 ((sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐹𝑗) ∈ ℝ) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗) ↔ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑗)) < 𝑦))
8245, 77, 40, 81syl3anc 1477 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗) ↔ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑗)) < 𝑦))
8321ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦𝑥))
845adantr 472 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ+) → 𝐹 Fn 𝑍)
85 fnfvelrn 6520 . . . . . . . . . . . 12 ((𝐹 Fn 𝑍𝑘𝑍) → (𝐹𝑘) ∈ ran 𝐹)
8684, 42, 85syl2an 495 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝐹𝑘) ∈ ran 𝐹)
87 suprub 11196 . . . . . . . . . . 11 (((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝐹 𝑦𝑥) ∧ (𝐹𝑘) ∈ ran 𝐹) → (𝐹𝑘) ≤ sup(ran 𝐹, ℝ, < ))
8883, 86, 87syl2anc 696 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝐹𝑘) ≤ sup(ran 𝐹, ℝ, < ))
8944, 45, 88abssuble0d 14390 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (abs‘((𝐹𝑘) − sup(ran 𝐹, ℝ, < ))) = (sup(ran 𝐹, ℝ, < ) − (𝐹𝑘)))
9089breq1d 4814 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((abs‘((𝐹𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦 ↔ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑘)) < 𝑦))
9180, 82, 903imtr4d 283 . . . . . . 7 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗) → (abs‘((𝐹𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦))
9291anassrs 683 . . . . . 6 ((((𝜑𝑦 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗) → (abs‘((𝐹𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦))
9392ralrimdva 3107 . . . . 5 (((𝜑𝑦 ∈ ℝ+) ∧ 𝑗𝑍) → ((sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗) → ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦))
9493reximdva 3155 . . . 4 ((𝜑𝑦 ∈ ℝ+) → (∃𝑗𝑍 (sup(ran 𝐹, ℝ, < ) − 𝑦) < (𝐹𝑗) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦))
9537, 94mpd 15 . . 3 ((𝜑𝑦 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦)
9695ralrimiva 3104 . 2 (𝜑 → ∀𝑦 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦)
97 fvex 6363 . . . . 5 (ℤ𝑀) ∈ V
989, 97eqeltri 2835 . . . 4 𝑍 ∈ V
99 fex 6654 . . . 4 ((𝐹:𝑍⟶ℝ ∧ 𝑍 ∈ V) → 𝐹 ∈ V)
1001, 98, 99sylancl 697 . . 3 (𝜑𝐹 ∈ V)
101 eqidd 2761 . . 3 ((𝜑𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
10223recnd 10280 . . 3 (𝜑 → sup(ran 𝐹, ℝ, < ) ∈ ℂ)
1031, 43sylan 489 . . . 4 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
104103recnd 10280 . . 3 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
1059, 6, 100, 101, 102, 104clim2c 14455 . 2 (𝜑 → (𝐹 ⇝ sup(ran 𝐹, ℝ, < ) ↔ ∀𝑦 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − sup(ran 𝐹, ℝ, < ))) < 𝑦))
10696, 105mpbird 247 1 (𝜑𝐹 ⇝ sup(ran 𝐹, ℝ, < ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139   ≠ wne 2932  ∀wral 3050  ∃wrex 3051  Vcvv 3340   ⊆ wss 3715  ∅c0 4058   class class class wbr 4804  ran crn 5267   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049  (class class class)co 6814  supcsup 8513  ℝcr 10147  1c1 10149   + caddc 10151   < clt 10286   ≤ cle 10287   − cmin 10478  ℤcz 11589  ℤ≥cuz 11899  ℝ+crp 12045  ...cfz 12539  abscabs 14193   ⇝ cli 14434 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-sup 8515  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-n0 11505  df-z 11590  df-uz 11900  df-rp 12046  df-fz 12540  df-seq 13016  df-exp 13075  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-clim 14438 This theorem is referenced by:  isumsup2  14797  climcnds  14802  itg1climres  23700  itg2monolem1  23736  itg2i1fseq  23741  itg2i1fseq2  23742  emcllem6  24947  lmdvg  30329  esumpcvgval  30470  meaiuninclem  41218
 Copyright terms: Public domain W3C validator