Theorem aaliou3lem6

Description: Lemma for aaliou3 . (Contributed by Stefan O'Rear, 16-Nov-2014)

	Ref	Expression
Hypotheses	aaliou3lem.c	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
	aaliou3lem.d	⊢ 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 )
	aaliou3lem.e	⊢ 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) )
Assertion	aaliou3lem6	⊢ ( 𝐴 ∈ ℕ → ( ( 𝐻 ‘ 𝐴 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		aaliou3lem.c	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
2		aaliou3lem.d	⊢ 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 )
3		aaliou3lem.e	⊢ 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) )
4		oveq2	⊢ ( 𝑐 = 𝐴 → ( 1 ... 𝑐 ) = ( 1 ... 𝐴 ) )
5	4	sumeq1d	⊢ ( 𝑐 = 𝐴 → Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) )
6		sumex	⊢ Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) ∈ V
7	5 3 6	fvmpt	⊢ ( 𝐴 ∈ ℕ → ( 𝐻 ‘ 𝐴 ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) )
8	7	oveq1d	⊢ ( 𝐴 ∈ ℕ → ( ( 𝐻 ‘ 𝐴 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) = ( Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
9		fzfid	⊢ ( 𝐴 ∈ ℕ → ( 1 ... 𝐴 ) ∈ Fin )
10		2rp	⊢ 2 ∈ ℝ+
11		nnnn0	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
12	11	faccld	⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) ∈ ℕ )
13	12	nnzd	⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) ∈ ℤ )
14		rpexpcl	⊢ ( ( 2 ∈ ℝ+ ∧ ( ! ‘ 𝐴 ) ∈ ℤ ) → ( 2 ↑ ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
15	10 13 14	sylancr	⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
16	15	rpcnd	⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ ( ! ‘ 𝐴 ) ) ∈ ℂ )
17		elfznn	⊢ ( 𝑏 ∈ ( 1 ... 𝐴 ) → 𝑏 ∈ ℕ )
18		fveq2	⊢ ( 𝑎 = 𝑏 → ( ! ‘ 𝑎 ) = ( ! ‘ 𝑏 ) )
19	18	negeqd	⊢ ( 𝑎 = 𝑏 → - ( ! ‘ 𝑎 ) = - ( ! ‘ 𝑏 ) )
20	19	oveq2d	⊢ ( 𝑎 = 𝑏 → ( 2 ↑ - ( ! ‘ 𝑎 ) ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
21		ovex	⊢ ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ V
22	20 1 21	fvmpt	⊢ ( 𝑏 ∈ ℕ → ( 𝐹 ‘ 𝑏 ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
23	17 22	syl	⊢ ( 𝑏 ∈ ( 1 ... 𝐴 ) → ( 𝐹 ‘ 𝑏 ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
24	23	adantl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
25	17	adantl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → 𝑏 ∈ ℕ )
26	25	nnnn0d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → 𝑏 ∈ ℕ0 )
27	26	faccld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝑏 ) ∈ ℕ )
28	27	nnzd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝑏 ) ∈ ℤ )
29	28	znegcld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → - ( ! ‘ 𝑏 ) ∈ ℤ )
30		rpexpcl	⊢ ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ 𝑏 ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℝ+ )
31	10 29 30	sylancr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℝ+ )
32	31	rpcnd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℂ )
33	24 32	eqeltrd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℂ )
34	9 16 33	fsummulc1	⊢ ( 𝐴 ∈ ℕ → ( Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
35	24	oveq1d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑏 ) ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
36	13	adantr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℤ )
37		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
38		expaddz	⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( - ( ! ‘ 𝑏 ) ∈ ℤ ∧ ( ! ‘ 𝐴 ) ∈ ℤ ) ) → ( 2 ↑ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑏 ) ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
39	37 38	mpan	⊢ ( ( - ( ! ‘ 𝑏 ) ∈ ℤ ∧ ( ! ‘ 𝐴 ) ∈ ℤ ) → ( 2 ↑ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑏 ) ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
40	29 36 39	syl2anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 2 ↑ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑏 ) ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
41		2z	⊢ 2 ∈ ℤ
42	29	zcnd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → - ( ! ‘ 𝑏 ) ∈ ℂ )
43	36	zcnd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℂ )
44	42 43	addcomd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) = ( ( ! ‘ 𝐴 ) + - ( ! ‘ 𝑏 ) ) )
45	27	nncnd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝑏 ) ∈ ℂ )
46	43 45	negsubd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( ! ‘ 𝐴 ) + - ( ! ‘ 𝑏 ) ) = ( ( ! ‘ 𝐴 ) − ( ! ‘ 𝑏 ) ) )
47	44 46	eqtrd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) = ( ( ! ‘ 𝐴 ) − ( ! ‘ 𝑏 ) ) )
48	11	adantr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → 𝐴 ∈ ℕ0 )
49		elfzle2	⊢ ( 𝑏 ∈ ( 1 ... 𝐴 ) → 𝑏 ≤ 𝐴 )
50	49	adantl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → 𝑏 ≤ 𝐴 )
51		facwordi	⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝑏 ≤ 𝐴 ) → ( ! ‘ 𝑏 ) ≤ ( ! ‘ 𝐴 ) )
52	26 48 50 51	syl3anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝑏 ) ≤ ( ! ‘ 𝐴 ) )
53	27	nnnn0d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝑏 ) ∈ ℕ0 )
54	48	faccld	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℕ )
55	54	nnnn0d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℕ0 )
56		nn0sub	⊢ ( ( ( ! ‘ 𝑏 ) ∈ ℕ0 ∧ ( ! ‘ 𝐴 ) ∈ ℕ0 ) → ( ( ! ‘ 𝑏 ) ≤ ( ! ‘ 𝐴 ) ↔ ( ( ! ‘ 𝐴 ) − ( ! ‘ 𝑏 ) ) ∈ ℕ0 ) )
57	53 55 56	syl2anc	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( ! ‘ 𝑏 ) ≤ ( ! ‘ 𝐴 ) ↔ ( ( ! ‘ 𝐴 ) − ( ! ‘ 𝑏 ) ) ∈ ℕ0 ) )
58	52 57	mpbid	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( ! ‘ 𝐴 ) − ( ! ‘ 𝑏 ) ) ∈ ℕ0 )
59	47 58	eqeltrd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ∈ ℕ0 )
60		zexpcl	⊢ ( ( 2 ∈ ℤ ∧ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ∈ ℕ0 ) → ( 2 ↑ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
61	41 59 60	sylancr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 2 ↑ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
62	40 61	eqeltrrd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ 𝑏 ) ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
63	35 62	eqeltrd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
64	9 63	fsumzcl	⊢ ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
65	34 64	eqeltrd	⊢ ( 𝐴 ∈ ℕ → ( Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
66	8 65	eqeltrd	⊢ ( 𝐴 ∈ ℕ → ( ( 𝐻 ‘ 𝐴 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )