Metamath Proof Explorer

Theorem seqcl2

Description: Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqcl2.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ 𝐶 )
seqcl2.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐶 )
seqcl2.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqcl2.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
Assertion seqcl2 ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 seqcl2.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ 𝐶 )
2 seqcl2.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐶 )
3 seqcl2.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4 seqcl2.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
5 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
6 3 5 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
7 eleq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) )
8 fveq2 ⊢ ( 𝑥 = 𝑀 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) )
9 8 eleq1d ⊢ ( 𝑥 = 𝑀 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ∈ 𝐶 ) )
10 7 9 imbi12d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ∈ 𝐶 ) ) )
11 10 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ∈ 𝐶 ) ) ) )
12 eleq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
13 fveq2 ⊢ ( 𝑥 = 𝑛 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) )
14 13 eleq1d ⊢ ( 𝑥 = 𝑛 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 ) )
15 12 14 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 ) ) )
16 15 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 ) ) ) )
17 eleq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) )
18 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
19 18 eleq1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ 𝐶 ) )
20 17 19 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ 𝐶 ) ) )
21 20 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ 𝐶 ) ) ) )
22 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) )
23 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
24 23 eleq1d ⊢ ( 𝑥 = 𝑁 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ 𝐶 ) )
25 22 24 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ 𝐶 ) ) )
26 25 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ 𝐶 ) ) ) )
27 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
28 27 eleq1d ⊢ ( 𝑀 ∈ ℤ → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑀 ) ∈ 𝐶 ) )
29 1 28 imbitrrid ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ∈ 𝐶 ) )
30 29 a1dd ⊢ ( 𝑀 ∈ ℤ → ( 𝜑 → ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) ∈ 𝐶 ) ) )
31 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
32 31 adantl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
33 32 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
34 33 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 ) → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 ) ) )
35 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
36 35 eleq1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝐷 ) )
37 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ∀ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) ∈ 𝐷 )
39 eluzp1p1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
40 39 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
41 elfzuz3 ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
42 41 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
43 elfzuzb ⊢ ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) )
44 40 42 43 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
45 36 38 44 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝐷 )
46 2 caovclg ⊢ ( ( 𝜑 ∧ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝐷 ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∈ 𝐶 )
47 46 ex ⊢ ( 𝜑 → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝐷 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∈ 𝐶 ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝐷 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∈ 𝐶 ) )
49 45 48 mpan2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∈ 𝐶 ) )
50 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
51 50 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
52 51 eleq1d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ 𝐶 ↔ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ∈ 𝐶 ) )
53 49 52 sylibrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ 𝐶 ) )
54 34 53 animpimp2impd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝐶 ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ∈ 𝐶 ) ) ) )
55 11 16 21 26 30 54 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ 𝐶 ) ) )
56 3 55 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ 𝐶 ) )
57 6 56 mpd ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ 𝐶 )