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 ⊢Ⅎ_kG
climrecf.3 ⊢Ⅎ_kH
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=1G⁡k
climrecf.10 ⊢φ→H∈W
Assertion climrecf ⊢φ→H⇝1A

Proof

Step Hyp Ref Expression
1 climrecf.1 ⊢Ⅎkφ
2 climrecf.2 ⊢Ⅎ_kG
3 climrecf.3 ⊢Ⅎ_kH
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=1G⁡k
10 climrecf.10 ⊢φ→H∈W
11 nfv ⊢Ⅎkj∈Z
12 1 11 nfan ⊢Ⅎkφ∧j∈Z
13 nfcv ⊢Ⅎ_kj
14 2 13 nffv ⊢Ⅎ_kG⁡j
15 14 nfel1 ⊢ℲkG⁡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 ⊢Ⅎ_kH⁡j
24 nfcv ⊢Ⅎ_k1
25 nfcv ⊢Ⅎ_k÷
26 24 25 14 nfov ⊢Ⅎ_k1G⁡j
27 23 26 nfeq ⊢ℲkH⁡j=1G⁡j
28 12 27 nfim ⊢Ⅎkφ∧j∈Z→H⁡j=1G⁡j
29 fveq2 ⊢k=j→H⁡k=H⁡j
30 19 oveq2d ⊢k=j→1G⁡k=1G⁡j
31 29 30 eqeq12d ⊢k=j→H⁡k=1G⁡k↔H⁡j=1G⁡j
32 18 31 imbi12d ⊢k=j→φ∧k∈Z→H⁡k=1G⁡k↔φ∧j∈Z→H⁡j=1G⁡j
33 28 32 9 chvarfv ⊢φ∧j∈Z→H⁡j=1G⁡j
34 4 5 6 7 22 33 10 climrec ⊢φ→H⇝1A