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 ( ( ๐น โ€˜ ๐‘ ) โˆ˜ ( ๐น โ€˜ ๐‘ ) ) ) ) ) )