Metamath Proof Explorer

Theorem opsqrlem5

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

Ref Expression
Hypotheses opsqrlem2.1 
|- T e. HrmOp
opsqrlem2.2 
|- S = ( x e. HrmOp , y e. HrmOp |-> ( x +op ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) ) )
opsqrlem2.3 
|- F = seq 1 ( S , ( NN X. { 0hop } ) )
Assertion opsqrlem5 
|- ( N e. NN -> ( F ` ( N + 1 ) ) = ( ( F ` N ) +op ( ( 1 / 2 ) .op ( T -op ( ( F ` N ) o. ( F ` N ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 opsqrlem2.1 
 |-  T e. HrmOp
2 opsqrlem2.2 
 |-  S = ( x e. HrmOp , y e. HrmOp |-> ( x +op ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) ) )
3 opsqrlem2.3 
 |-  F = seq 1 ( S , ( NN X. { 0hop } ) )
4 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
5 seqp1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( seq 1 ( S , ( NN X. { 0hop } ) ) ` ( N + 1 ) ) = ( ( seq 1 ( S , ( NN X. { 0hop } ) ) ` N ) S ( ( NN X. { 0hop } ) ` ( N + 1 ) ) ) )
6 4 5 sylbi 
 |-  ( N e. NN -> ( seq 1 ( S , ( NN X. { 0hop } ) ) ` ( N + 1 ) ) = ( ( seq 1 ( S , ( NN X. { 0hop } ) ) ` N ) S ( ( NN X. { 0hop } ) ` ( N + 1 ) ) ) )
7 3 fveq1i 
 |-  ( F ` ( N + 1 ) ) = ( seq 1 ( S , ( NN X. { 0hop } ) ) ` ( N + 1 ) )
8 3 fveq1i 
 |-  ( F ` N ) = ( seq 1 ( S , ( NN X. { 0hop } ) ) ` N )
9 8 oveq1i 
 |-  ( ( F ` N ) S ( ( NN X. { 0hop } ) ` ( N + 1 ) ) ) = ( ( seq 1 ( S , ( NN X. { 0hop } ) ) ` N ) S ( ( NN X. { 0hop } ) ` ( N + 1 ) ) )
10 6 7 9 3eqtr4g 
 |-  ( N e. NN -> ( F ` ( N + 1 ) ) = ( ( F ` N ) S ( ( NN X. { 0hop } ) ` ( N + 1 ) ) ) )
11 1 2 3 opsqrlem4 
 |-  F : NN --> HrmOp
12 11 ffvelcdmi 
 |-  ( N e. NN -> ( F ` N ) e. HrmOp )
13 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
14 0hmop 
 |-  0hop e. HrmOp
15 14 elexi 
 |-  0hop e. _V
16 15 fvconst2 
 |-  ( ( N + 1 ) e. NN -> ( ( NN X. { 0hop } ) ` ( N + 1 ) ) = 0hop )
17 13 16 syl 
 |-  ( N e. NN -> ( ( NN X. { 0hop } ) ` ( N + 1 ) ) = 0hop )
18 17 14 eqeltrdi 
 |-  ( N e. NN -> ( ( NN X. { 0hop } ) ` ( N + 1 ) ) e. HrmOp )
19 1 2 3 opsqrlem3 
 |-  ( ( ( F ` N ) e. HrmOp /\ ( ( NN X. { 0hop } ) ` ( N + 1 ) ) e. HrmOp ) -> ( ( F ` N ) S ( ( NN X. { 0hop } ) ` ( N + 1 ) ) ) = ( ( F ` N ) +op ( ( 1 / 2 ) .op ( T -op ( ( F ` N ) o. ( F ` N ) ) ) ) ) )
20 12 18 19 syl2anc 
 |-  ( N e. NN -> ( ( F ` N ) S ( ( NN X. { 0hop } ) ` ( N + 1 ) ) ) = ( ( F ` N ) +op ( ( 1 / 2 ) .op ( T -op ( ( F ` N ) o. ( F ` N ) ) ) ) ) )
21 10 20 eqtrd 
 |-  ( N e. NN -> ( F ` ( N + 1 ) ) = ( ( F ` N ) +op ( ( 1 / 2 ) .op ( T -op ( ( F ` N ) o. ( F ` N ) ) ) ) ) )