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 ⊢ Ⅎ k φ
climrecf.2 ⊢ Ⅎ _ k G
climrecf.3 ⊢ Ⅎ _ k H
climrecf.4 ⊢ Z = ℤ ≥ M
climrecf.5 ⊢ φ → M ∈ ℤ
climrecf.6 ⊢ φ → G ⇝ A
climrecf.7 ⊢ φ → A ≠ 0
climrecf.8 ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℂ ∖ 0
climrecf.9 ⊢ φ ∧ k ∈ Z → H ⁡ k = 1 G ⁡ k
climrecf.10 ⊢ φ → H ∈ W
Assertion climrecf ⊢ φ → H ⇝ 1 A

Proof

Step Hyp Ref Expression
1 climrecf.1 ⊢ Ⅎ k φ
2 climrecf.2 ⊢ Ⅎ _ k G
3 climrecf.3 ⊢ Ⅎ _ k H
4 climrecf.4 ⊢ Z = ℤ ≥ M
5 climrecf.5 ⊢ φ → M ∈ ℤ
6 climrecf.6 ⊢ φ → G ⇝ A
7 climrecf.7 ⊢ φ → A ≠ 0
8 climrecf.8 ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℂ ∖ 0
9 climrecf.9 ⊢ φ ∧ k ∈ Z → H ⁡ k = 1 G ⁡ k
10 climrecf.10 ⊢ φ → H ∈ W
11 nfv ⊢ Ⅎ k j ∈ Z
12 1 11 nfan ⊢ Ⅎ k φ ∧ j ∈ Z
13 nfcv ⊢ Ⅎ _ k j
14 2 13 nffv ⊢ Ⅎ _ k G ⁡ j
15 14 nfel1 ⊢ Ⅎ k G ⁡ j ∈ ℂ ∖ 0
16 12 15 nfim ⊢ Ⅎ k φ ∧ j ∈ Z → G ⁡ j ∈ ℂ ∖ 0
17 eleq1w ⊢ k = j → k ∈ Z ↔ j ∈ Z
18 17 anbi2d ⊢ k = j → φ ∧ k ∈ Z ↔ φ ∧ j ∈ Z
19 fveq2 ⊢ k = j → G ⁡ k = G ⁡ j
20 19 eleq1d ⊢ k = j → G ⁡ k ∈ ℂ ∖ 0 ↔ G ⁡ j ∈ ℂ ∖ 0
21 18 20 imbi12d ⊢ k = j → φ ∧ k ∈ Z → G ⁡ k ∈ ℂ ∖ 0 ↔ φ ∧ j ∈ Z → G ⁡ j ∈ ℂ ∖ 0
22 16 21 8 chvarfv ⊢ φ ∧ j ∈ Z → G ⁡ j ∈ ℂ ∖ 0
23 3 13 nffv ⊢ Ⅎ _ k H ⁡ j
24 nfcv ⊢ Ⅎ _ k 1
25 nfcv ⊢ Ⅎ _ k ÷
26 24 25 14 nfov ⊢ Ⅎ _ k 1 G ⁡ j
27 23 26 nfeq ⊢ Ⅎ k H ⁡ j = 1 G ⁡ j
28 12 27 nfim ⊢ Ⅎ k φ ∧ j ∈ 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 → φ ∧ k ∈ Z → H ⁡ k = 1 G ⁡ k ↔ φ ∧ j ∈ Z → H ⁡ j = 1 G ⁡ j
33 28 32 9 chvarfv ⊢ φ ∧ j ∈ Z → H ⁡ j = 1 G ⁡ j
34 4 5 6 7 22 33 10 climrec ⊢ φ → H ⇝ 1 A