Metamath Proof Explorer

Theorem climub

Description: The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 10-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climub.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
climub.3 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climub.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
climub.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
Assertion climub ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climub.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 climub.3 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
4 climub.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
5 climub.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
6 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
7 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
9 7 8 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
10 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑁 ) )
11 10 eleq1d ⊢ ( 𝑘 = 𝑁 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑁 ) ∈ ℝ ) )
12 11 imbi2d ⊢ ( 𝑘 = 𝑁 → ( ( 𝜑 → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ ) ) )
13 4 expcom ⊢ ( 𝑘 ∈ 𝑍 → ( 𝜑 → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) )
14 12 13 vtoclga ⊢ ( 𝑁 ∈ 𝑍 → ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ ) )
15 2 14 mpcom ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
16 1 uztrn2 ⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑗 ∈ 𝑍 )
17 2 16 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑗 ∈ 𝑍 )
18 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
19 18 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) )
20 19 imbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) ) )
21 20 13 vtoclga ⊢ ( 𝑗 ∈ 𝑍 → ( 𝜑 → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) )
22 21 impcom ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
23 17 22 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) )
25 elfzuz ⊢ ( 𝑘 ∈ ( 𝑁 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
26 1 uztrn2 ⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ 𝑍 )
27 2 26 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ 𝑍 )
28 27 4 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
29 25 28 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
30 29 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
31 elfzuz ⊢ ( 𝑘 ∈ ( 𝑁 ... ( 𝑗 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
32 27 5 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
33 31 32 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑁 ... ( 𝑗 − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
34 33 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ... ( 𝑗 − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
35 24 30 34 monoord ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑁 ) ≤ ( 𝐹 ‘ 𝑗 ) )
36 6 9 15 3 23 35 climlec2 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ 𝐴 )