Metamath Proof Explorer

Theorem opsqrlem4

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 opsqrlem4 
|- F : NN --> HrmOp

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 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 1zzd 
 |-  ( T. -> 1 e. ZZ )
6 0hmop 
 |-  0hop e. HrmOp
7 6 elexi 
 |-  0hop e. _V
8 7 fvconst2 
 |-  ( z e. NN -> ( ( NN X. { 0hop } ) ` z ) = 0hop )
9 8 6 eqeltrdi 
 |-  ( z e. NN -> ( ( NN X. { 0hop } ) ` z ) e. HrmOp )
10 9 adantl 
 |-  ( ( T. /\ z e. NN ) -> ( ( NN X. { 0hop } ) ` z ) e. HrmOp )
11 1 2 3 opsqrlem3 
 |-  ( ( z e. HrmOp /\ w e. HrmOp ) -> ( z S w ) = ( z +op ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) ) )
12 halfre 
 |-  ( 1 / 2 ) e. RR
13 simpl 
 |-  ( ( z e. HrmOp /\ w e. HrmOp ) -> z e. HrmOp )
14 eqidd 
 |-  ( ( z e. HrmOp /\ w e. HrmOp ) -> ( z o. z ) = ( z o. z ) )
15 hmopco 
 |-  ( ( z e. HrmOp /\ z e. HrmOp /\ ( z o. z ) = ( z o. z ) ) -> ( z o. z ) e. HrmOp )
16 13 13 14 15 syl3anc 
 |-  ( ( z e. HrmOp /\ w e. HrmOp ) -> ( z o. z ) e. HrmOp )
17 hmopd 
 |-  ( ( T e. HrmOp /\ ( z o. z ) e. HrmOp ) -> ( T -op ( z o. z ) ) e. HrmOp )
18 1 16 17 sylancr 
 |-  ( ( z e. HrmOp /\ w e. HrmOp ) -> ( T -op ( z o. z ) ) e. HrmOp )
19 hmopm 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( T -op ( z o. z ) ) e. HrmOp ) -> ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) e. HrmOp )
20 12 18 19 sylancr 
 |-  ( ( z e. HrmOp /\ w e. HrmOp ) -> ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) e. HrmOp )
21 hmops 
 |-  ( ( z e. HrmOp /\ ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) e. HrmOp ) -> ( z +op ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) ) e. HrmOp )
22 20 21 syldan 
 |-  ( ( z e. HrmOp /\ w e. HrmOp ) -> ( z +op ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) ) e. HrmOp )
23 11 22 eqeltrd 
 |-  ( ( z e. HrmOp /\ w e. HrmOp ) -> ( z S w ) e. HrmOp )
24 23 adantl 
 |-  ( ( T. /\ ( z e. HrmOp /\ w e. HrmOp ) ) -> ( z S w ) e. HrmOp )
25 4 5 10 24 seqf 
 |-  ( T. -> seq 1 ( S , ( NN X. { 0hop } ) ) : NN --> HrmOp )
26 25 mptru 
 |-  seq 1 ( S , ( NN X. { 0hop } ) ) : NN --> HrmOp
27 3 feq1i 
 |-  ( F : NN --> HrmOp <-> seq 1 ( S , ( NN X. { 0hop } ) ) : NN --> HrmOp )
28 26 27 mpbir 
 |-  F : NN --> HrmOp