Metamath Proof Explorer

Theorem climaddf

Description: A version of climadd using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses climaddf.1 
|- F/ k ph
climaddf.2 
|- F/_ k F
climaddf.3 
|- F/_ k G
climaddf.4 
|- F/_ k H
climaddf.5 
|- Z = ( ZZ>= ` M )
climaddf.6 
|- ( ph -> M e. ZZ )
climaddf.7 
|- ( ph -> F ~~> A )
climaddf.8 
|- ( ph -> H e. X )
climaddf.9 
|- ( ph -> G ~~> B )
climaddf.10 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
climaddf.11 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
climaddf.12 
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) )
Assertion climaddf 
|- ( ph -> H ~~> ( A + B ) )

Proof

Step Hyp Ref Expression
1 climaddf.1 
 |-  F/ k ph
2 climaddf.2 
 |-  F/_ k F
3 climaddf.3 
 |-  F/_ k G
4 climaddf.4 
 |-  F/_ k H
5 climaddf.5 
 |-  Z = ( ZZ>= ` M )
6 climaddf.6 
 |-  ( ph -> M e. ZZ )
7 climaddf.7 
 |-  ( ph -> F ~~> A )
8 climaddf.8 
 |-  ( ph -> H e. X )
9 climaddf.9 
 |-  ( ph -> G ~~> B )
10 climaddf.10 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
11 climaddf.11 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
12 climaddf.12 
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) )
13 nfv 
 |-  F/ k j e. Z
14 1 13 nfan 
 |-  F/ k ( ph /\ j e. Z )
15 nfcv 
 |-  F/_ k j
16 2 15 nffv 
 |-  F/_ k ( F ` j )
17 16 nfel1 
 |-  F/ k ( F ` j ) e. CC
18 14 17 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> ( F ` j ) e. CC )
19 eleq1w 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
20 19 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
21 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
22 21 eleq1d 
 |-  ( k = j -> ( ( F ` k ) e. CC <-> ( F ` j ) e. CC ) )
23 20 22 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) <-> ( ( ph /\ j e. Z ) -> ( F ` j ) e. CC ) ) )
24 18 23 10 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. CC )
25 3 15 nffv 
 |-  F/_ k ( G ` j )
26 25 nfel1 
 |-  F/ k ( G ` j ) e. CC
27 14 26 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> ( G ` j ) e. CC )
28 fveq2 
 |-  ( k = j -> ( G ` k ) = ( G ` j ) )
29 28 eleq1d 
 |-  ( k = j -> ( ( G ` k ) e. CC <-> ( G ` j ) e. CC ) )
30 20 29 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC ) <-> ( ( ph /\ j e. Z ) -> ( G ` j ) e. CC ) ) )
31 27 30 11 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> ( G ` j ) e. CC )
32 4 15 nffv 
 |-  F/_ k ( H ` j )
33 nfcv 
 |-  F/_ k +
34 16 33 25 nfov 
 |-  F/_ k ( ( F ` j ) + ( G ` j ) )
35 32 34 nfeq 
 |-  F/ k ( H ` j ) = ( ( F ` j ) + ( G ` j ) )
36 14 35 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( F ` j ) + ( G ` j ) ) )
37 fveq2 
 |-  ( k = j -> ( H ` k ) = ( H ` j ) )
38 21 28 oveq12d 
 |-  ( k = j -> ( ( F ` k ) + ( G ` k ) ) = ( ( F ` j ) + ( G ` j ) ) )
39 37 38 eqeq12d 
 |-  ( k = j -> ( ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) <-> ( H ` j ) = ( ( F ` j ) + ( G ` j ) ) ) )
40 20 39 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) ) <-> ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( F ` j ) + ( G ` j ) ) ) ) )
41 36 40 12 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> ( H ` j ) = ( ( F ` j ) + ( G ` j ) ) )
42 5 6 7 8 9 24 31 41 climadd 
 |-  ( ph -> H ~~> ( A + B ) )