This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑘 𝜑
climrecf.2 ⊢ Ⅎ 𝑘 𝐺
climrecf.3 ⊢ Ⅎ 𝑘 𝐻
climrecf.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climrecf.5 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climrecf.6 ⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )
climrecf.7 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
climrecf.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) )
climrecf.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
climrecf.10 ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
Assertion climrecf ( 𝜑 → 𝐻 ⇝ ( 1 / 𝐴 ) )

Proof

Step Hyp Ref Expression
1 climrecf.1 ⊢ Ⅎ 𝑘 𝜑
2 climrecf.2 ⊢ Ⅎ 𝑘 𝐺
3 climrecf.3 ⊢ Ⅎ 𝑘 𝐻
4 climrecf.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 climrecf.5 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
6 climrecf.6 ⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )
7 climrecf.7 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
8 climrecf.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) )
9 climrecf.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
10 climrecf.10 ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
11 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
12 1 11 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
13 nfcv ⊢ Ⅎ 𝑘 𝑗
14 2 13 nffv ⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 )
15 14 nfel1 ⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 ) ∈ ( ℂ ∖ { 0 } )
16 12 15 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ℂ ∖ { 0 } ) )
17 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
18 17 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
19 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑗 ) )
20 19 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐺 ‘ 𝑗 ) ∈ ( ℂ ∖ { 0 } ) ) )
21 18 20 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
22 16 21 8 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ℂ ∖ { 0 } ) )
23 3 13 nffv ⊢ Ⅎ 𝑘 ( 𝐻 ‘ 𝑗 )
24 nfcv ⊢ Ⅎ 𝑘 1
25 nfcv ⊢ Ⅎ 𝑘 /
26 24 25 14 nfov ⊢ Ⅎ 𝑘 ( 1 / ( 𝐺 ‘ 𝑗 ) )
27 23 26 nfeq ⊢ Ⅎ 𝑘 ( 𝐻 ‘ 𝑗 ) = ( 1 / ( 𝐺 ‘ 𝑗 ) )
28 12 27 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( 1 / ( 𝐺 ‘ 𝑗 ) ) )
29 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐻 ‘ 𝑘 ) = ( 𝐻 ‘ 𝑗 ) )
30 19 oveq2d ⊢ ( 𝑘 = 𝑗 → ( 1 / ( 𝐺 ‘ 𝑘 ) ) = ( 1 / ( 𝐺 ‘ 𝑗 ) ) )
31 29 30 eqeq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐻 ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐻 ‘ 𝑗 ) = ( 1 / ( 𝐺 ‘ 𝑗 ) ) ) )
32 18 31 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( 1 / ( 𝐺 ‘ 𝑗 ) ) ) ) )
33 28 32 9 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( 1 / ( 𝐺 ‘ 𝑗 ) ) )
34 4 5 6 7 22 33 10 climrec ⊢ ( 𝜑 → 𝐻 ⇝ ( 1 / 𝐴 ) )