This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ruclem7

Description: Lemma for ruc . Successor value for the interval sequence. (Contributed by Mario Carneiro, 28-May-2014)

Ref Expression
Hypotheses ruc.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
ruc.2 ⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
ruc.4 ⊢ 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
ruc.5 ⊢ 𝐺 = seq 0 ( 𝐷 , 𝐶 )
Assertion ruclem7 ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐺 ‘ ( 𝑁 + 1 ) ) = ( ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 ruc.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
2 ruc.2 ⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
3 ruc.4 ⊢ 𝐶 = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
4 ruc.5 ⊢ 𝐺 = seq 0 ( 𝐷 , 𝐶 )
5 simpr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
6 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
7 5 6 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
8 seqp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( seq 0 ( 𝐷 , 𝐶 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 0 ( 𝐷 , 𝐶 ) ‘ 𝑁 ) 𝐷 ( 𝐶 ‘ ( 𝑁 + 1 ) ) ) )
9 7 8 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( seq 0 ( 𝐷 , 𝐶 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 0 ( 𝐷 , 𝐶 ) ‘ 𝑁 ) 𝐷 ( 𝐶 ‘ ( 𝑁 + 1 ) ) ) )
10 4 fveq1i ⊢ ( 𝐺 ‘ ( 𝑁 + 1 ) ) = ( seq 0 ( 𝐷 , 𝐶 ) ‘ ( 𝑁 + 1 ) )
11 4 fveq1i ⊢ ( 𝐺 ‘ 𝑁 ) = ( seq 0 ( 𝐷 , 𝐶 ) ‘ 𝑁 )
12 11 oveq1i ⊢ ( ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐶 ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 0 ( 𝐷 , 𝐶 ) ‘ 𝑁 ) 𝐷 ( 𝐶 ‘ ( 𝑁 + 1 ) ) )
13 9 10 12 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐺 ‘ ( 𝑁 + 1 ) ) = ( ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐶 ‘ ( 𝑁 + 1 ) ) ) )
14 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℕ )
16 15 nnne0d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ≠ 0 )
17 16 necomd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → 0 ≠ ( 𝑁 + 1 ) )
18 3 equncomi ⊢ 𝐶 = ( 𝐹 ∪ { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } )
19 18 fveq1i ⊢ ( 𝐶 ‘ ( 𝑁 + 1 ) ) = ( ( 𝐹 ∪ { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ) ‘ ( 𝑁 + 1 ) )
20 fvunsn ⊢ ( 0 ≠ ( 𝑁 + 1 ) → ( ( 𝐹 ∪ { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ) ‘ ( 𝑁 + 1 ) ) = ( 𝐹 ‘ ( 𝑁 + 1 ) ) )
21 19 20 eqtrid ⊢ ( 0 ≠ ( 𝑁 + 1 ) → ( 𝐶 ‘ ( 𝑁 + 1 ) ) = ( 𝐹 ‘ ( 𝑁 + 1 ) ) )
22 17 21 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐶 ‘ ( 𝑁 + 1 ) ) = ( 𝐹 ‘ ( 𝑁 + 1 ) ) )
23 22 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐶 ‘ ( 𝑁 + 1 ) ) ) = ( ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
24 13 23 eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐺 ‘ ( 𝑁 + 1 ) ) = ( ( 𝐺 ‘ 𝑁 ) 𝐷 ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )