Metamath Proof Explorer

Theorem climrecf

Description: A version of climrec using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses climrecf.1 
|- F/ k ph
climrecf.2 
|- F/_ k G
climrecf.3 
|- F/_ k H
climrecf.4 
|- Z = ( ZZ>= ` M )
climrecf.5 
|- ( ph -> M e. ZZ )
climrecf.6 
|- ( ph -> G ~~> A )
climrecf.7 
|- ( ph -> A =/= 0 )
climrecf.8 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. ( CC \ { 0 } ) )
climrecf.9 
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( 1 / ( G ` k ) ) )
climrecf.10 
|- ( ph -> H e. W )
Assertion climrecf 
|- ( ph -> H ~~> ( 1 / A ) )

Proof

Step Hyp Ref Expression
1 climrecf.1 
 |-  F/ k ph
2 climrecf.2 
 |-  F/_ k G
3 climrecf.3 
 |-  F/_ k H
4 climrecf.4 
 |-  Z = ( ZZ>= ` M )
5 climrecf.5 
 |-  ( ph -> M e. ZZ )
6 climrecf.6 
 |-  ( ph -> G ~~> A )
7 climrecf.7 
 |-  ( ph -> A =/= 0 )
8 climrecf.8 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. ( CC \ { 0 } ) )
9 climrecf.9 
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( 1 / ( G ` k ) ) )
10 climrecf.10 
 |-  ( ph -> H e. W )
11 nfv 
 |-  F/ k j e. Z
12 1 11 nfan 
 |-  F/ k ( ph /\ j e. Z )
13 nfcv 
 |-  F/_ k j
14 2 13 nffv 
 |-  F/_ k ( G ` j )
15 14 nfel1 
 |-  F/ k ( G ` j ) e. ( CC \ { 0 } )
16 12 15 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> ( G ` j ) e. ( CC \ { 0 } ) )
17 eleq1w 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
18 17 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
19 fveq2 
 |-  ( k = j -> ( G ` k ) = ( G ` j ) )
20 19 eleq1d 
 |-  ( k = j -> ( ( G ` k ) e. ( CC \ { 0 } ) <-> ( G ` j ) e. ( CC \ { 0 } ) ) )
21 18 20 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( G ` k ) e. ( CC \ { 0 } ) ) <-> ( ( ph /\ j e. Z ) -> ( G ` j ) e. ( CC \ { 0 } ) ) ) )
22 16 21 8 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> ( G ` j ) e. ( CC \ { 0 } ) )
23 3 13 nffv 
 |-  F/_ k ( H ` j )
24 nfcv 
 |-  F/_ k 1
25 nfcv 
 |-  F/_ k /
26 24 25 14 nfov 
 |-  F/_ k ( 1 / ( G ` j ) )
27 23 26 nfeq 
 |-  F/ k ( H ` j ) = ( 1 / ( G ` j ) )
28 12 27 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> ( H ` j ) = ( 1 / ( G ` j ) ) )
29 fveq2 
 |-  ( k = j -> ( H ` k ) = ( H ` j ) )
30 19 oveq2d 
 |-  ( k = j -> ( 1 / ( G ` k ) ) = ( 1 / ( G ` j ) ) )
31 29 30 eqeq12d 
 |-  ( k = j -> ( ( H ` k ) = ( 1 / ( G ` k ) ) <-> ( H ` j ) = ( 1 / ( G ` j ) ) ) )
32 18 31 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( H ` k ) = ( 1 / ( G ` k ) ) ) <-> ( ( ph /\ j e. Z ) -> ( H ` j ) = ( 1 / ( G ` j ) ) ) ) )
33 28 32 9 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> ( H ` j ) = ( 1 / ( G ` j ) ) )
34 4 5 6 7 22 33 10 climrec 
 |-  ( ph -> H ~~> ( 1 / A ) )