Metamath Proof Explorer

Theorem opsqrlem5

Description: Lemma for opsqri . (Contributed by NM, 17-Aug-2006) (New usage is discouraged.)

Ref Expression
Hypotheses opsqrlem2.1 ⊢ 𝑇 ∈ HrmOp
opsqrlem2.2 ⊢ 𝑆 = ( 𝑥 ∈ HrmOp , 𝑦 ∈ HrmOp ↦ ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) )
opsqrlem2.3 ⊢ 𝐹 = seq 1 ( 𝑆 , ( ℕ × { 0hop } ) )
Assertion opsqrlem5 ( 𝑁 ∈ ℕ → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = ( ( 𝐹 ‘ 𝑁 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑁 ) ∘ ( 𝐹 ‘ 𝑁 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 opsqrlem2.1 ⊢ 𝑇 ∈ HrmOp
2 opsqrlem2.2 ⊢ 𝑆 = ( 𝑥 ∈ HrmOp , 𝑦 ∈ HrmOp ↦ ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) )
3 opsqrlem2.3 ⊢ 𝐹 = seq 1 ( 𝑆 , ( ℕ × { 0hop } ) )
4 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
5 seqp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) ‘ 𝑁 ) 𝑆 ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) ) )
6 4 5 sylbi ⊢ ( 𝑁 ∈ ℕ → ( seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) ‘ 𝑁 ) 𝑆 ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) ) )
7 3 fveq1i ⊢ ( 𝐹 ‘ ( 𝑁 + 1 ) ) = ( seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) ‘ ( 𝑁 + 1 ) )
8 3 fveq1i ⊢ ( 𝐹 ‘ 𝑁 ) = ( seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) ‘ 𝑁 )
9 8 oveq1i ⊢ ( ( 𝐹 ‘ 𝑁 ) 𝑆 ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) ‘ 𝑁 ) 𝑆 ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) )
10 6 7 9 3eqtr4g ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = ( ( 𝐹 ‘ 𝑁 ) 𝑆 ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) ) )
11 1 2 3 opsqrlem4 ⊢ 𝐹 : ℕ ⟶ HrmOp
12 11 ffvelcdmi ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) ∈ HrmOp )
13 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
14 0hmop ⊢ 0hop ∈ HrmOp
15 14 elexi ⊢ 0hop ∈ V
16 15 fvconst2 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ → ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) = 0hop )
17 13 16 syl ⊢ ( 𝑁 ∈ ℕ → ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) = 0hop )
18 17 14 eqeltrdi ⊢ ( 𝑁 ∈ ℕ → ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) ∈ HrmOp )
19 1 2 3 opsqrlem3 ⊢ ( ( ( 𝐹 ‘ 𝑁 ) ∈ HrmOp ∧ ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) ∈ HrmOp ) → ( ( 𝐹 ‘ 𝑁 ) 𝑆 ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑁 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑁 ) ∘ ( 𝐹 ‘ 𝑁 ) ) ) ) ) )
20 12 18 19 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐹 ‘ 𝑁 ) 𝑆 ( ( ℕ × { 0hop } ) ‘ ( 𝑁 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑁 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑁 ) ∘ ( 𝐹 ‘ 𝑁 ) ) ) ) ) )
21 10 20 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = ( ( 𝐹 ‘ 𝑁 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑁 ) ∘ ( 𝐹 ‘ 𝑁 ) ) ) ) ) )