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	⊢ Ⅎ 𝑘 𝜑
	climaddf.2	⊢ Ⅎ 𝑘 𝐹
	climaddf.3	⊢ Ⅎ 𝑘 𝐺
	climaddf.4	⊢ Ⅎ 𝑘 𝐻
	climaddf.5	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climaddf.6	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climaddf.7	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
	climaddf.8	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
	climaddf.9	⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
	climaddf.10	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
	climaddf.11	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
	climaddf.12	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) )
Assertion	climaddf	⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		climaddf.1	⊢ Ⅎ 𝑘 𝜑
2		climaddf.2	⊢ Ⅎ 𝑘 𝐹
3		climaddf.3	⊢ Ⅎ 𝑘 𝐺
4		climaddf.4	⊢ Ⅎ 𝑘 𝐻
5		climaddf.5	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
6		climaddf.6	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7		climaddf.7	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
8		climaddf.8	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
9		climaddf.9	⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
10		climaddf.10	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
11		climaddf.11	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
12		climaddf.12	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) )
13		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
14	1 13	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
15		nfcv	⊢ Ⅎ 𝑘 𝑗
16	2 15	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
17	16	nfel1	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) ∈ ℂ
18	14 17	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
19		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
20	19	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
21		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
22	21	eleq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) )
23	20 22	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) ) )
24	18 23 10	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
25	3 15	nffv	⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 )
26	25	nfel1	⊢ Ⅎ 𝑘 ( 𝐺 ‘ 𝑗 ) ∈ ℂ
27	14 26	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ℂ )
28		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑗 ) )
29	28	eleq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐺 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐺 ‘ 𝑗 ) ∈ ℂ ) )
30	20 29	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ℂ ) ) )
31	27 30 11	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ℂ )
32	4 15	nffv	⊢ Ⅎ 𝑘 ( 𝐻 ‘ 𝑗 )
33		nfcv	⊢ Ⅎ 𝑘 +
34	16 33 25	nfov	⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑗 ) + ( 𝐺 ‘ 𝑗 ) )
35	32 34	nfeq	⊢ Ⅎ 𝑘 ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) + ( 𝐺 ‘ 𝑗 ) )
36	14 35	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) + ( 𝐺 ‘ 𝑗 ) ) )
37		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐻 ‘ 𝑘 ) = ( 𝐻 ‘ 𝑗 ) )
38	21 28	oveq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑗 ) + ( 𝐺 ‘ 𝑗 ) ) )
39	37 38	eqeq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) + ( 𝐺 ‘ 𝑗 ) ) ) )
40	20 39	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) + ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) + ( 𝐺 ‘ 𝑗 ) ) ) ) )
41	36 40 12	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝑗 ) + ( 𝐺 ‘ 𝑗 ) ) )
42	5 6 7 8 9 24 31 41	climadd	⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 + 𝐵 ) )