aaliou3lem6

	Ref	Expression
Hypotheses	aaliou3lem.c	$⊢ F = (a \in ℕ ⟼ 2^{- a!})$
	aaliou3lem.d	$⊢ L = \sum_{b \in ℕ} F (b)$
	aaliou3lem.e	$⊢ H = (c \in ℕ ⟼ \sum_{b = 1}^{c} F (b))$
Assertion	aaliou3lem6	$⊢ A \in ℕ \to H (A) 2^{A!} \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		aaliou3lem.c	$⊢ F = (a \in ℕ ⟼ 2^{- a!})$
2		aaliou3lem.d	$⊢ L = \sum_{b \in ℕ} F (b)$
3		aaliou3lem.e	$⊢ H = (c \in ℕ ⟼ \sum_{b = 1}^{c} F (b))$
4		oveq2	$⊢ c = A \to (1 \dots c) = (1 \dots A)$
5	4	sumeq1d	$⊢ c = A \to \sum_{b = 1}^{c} F (b) = \sum_{b = 1}^{A} F (b)$
6		sumex	$⊢ \sum_{b = 1}^{A} F (b) \in V$
7	5 3 6	fvmpt	$⊢ A \in ℕ \to H (A) = \sum_{b = 1}^{A} F (b)$
8	7	oveq1d	$⊢ A \in ℕ \to H (A) 2^{A!} = \sum_{b = 1}^{A} F (b) 2^{A!}$
9		fzfid	$⊢ A \in ℕ \to (1 \dots A) \in Fin$
10		2rp	$⊢ 2 \in ℝ^{+}$
11		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
12	11	faccld	$⊢ A \in ℕ \to A! \in ℕ$
13	12	nnzd	$⊢ A \in ℕ \to A! \in ℤ$
14		rpexpcl	$⊢ (2 \in ℝ^{+} \land A! \in ℤ) \to 2^{A!} \in ℝ^{+}$
15	10 13 14	sylancr	$⊢ A \in ℕ \to 2^{A!} \in ℝ^{+}$
16	15	rpcnd	$⊢ A \in ℕ \to 2^{A!} \in ℂ$
17		elfznn	$⊢ b \in (1 \dots A) \to b \in ℕ$
18		fveq2	$⊢ a = b \to a! = b!$
19	18	negeqd	$⊢ a = b \to - a! = - b!$
20	19	oveq2d	$⊢ a = b \to 2^{- a!} = 2^{- b!}$
21		ovex	$⊢ 2^{- b!} \in V$
22	20 1 21	fvmpt	$⊢ b \in ℕ \to F (b) = 2^{- b!}$
23	17 22	syl	$⊢ b \in (1 \dots A) \to F (b) = 2^{- b!}$
24	23	adantl	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to F (b) = 2^{- b!}$
25	17	adantl	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to b \in ℕ$
26	25	nnnn0d	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to b \in ℕ_{0}$
27	26	faccld	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to b! \in ℕ$
28	27	nnzd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to b! \in ℤ$
29	28	znegcld	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to - b! \in ℤ$
30		rpexpcl	$⊢ (2 \in ℝ^{+} \land - b! \in ℤ) \to 2^{- b!} \in ℝ^{+}$
31	10 29 30	sylancr	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to 2^{- b!} \in ℝ^{+}$
32	31	rpcnd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to 2^{- b!} \in ℂ$
33	24 32	eqeltrd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to F (b) \in ℂ$
34	9 16 33	fsummulc1	$⊢ A \in ℕ \to \sum_{b = 1}^{A} F (b) 2^{A!} = \sum_{b = 1}^{A} F (b) 2^{A!}$
35	24	oveq1d	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to F (b) 2^{A!} = 2^{- b!} 2^{A!}$
36	13	adantr	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to A! \in ℤ$
37		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
38		expaddz	$⊢ ((2 \in ℂ \land 2 \neq 0) \land (- b! \in ℤ \land A! \in ℤ)) \to 2^{- b! + A!} = 2^{- b!} 2^{A!}$
39	37 38	mpan	$⊢ (- b! \in ℤ \land A! \in ℤ) \to 2^{- b! + A!} = 2^{- b!} 2^{A!}$
40	29 36 39	syl2anc	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to 2^{- b! + A!} = 2^{- b!} 2^{A!}$
41		2z	$⊢ 2 \in ℤ$
42	29	zcnd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to - b! \in ℂ$
43	36	zcnd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to A! \in ℂ$
44	42 43	addcomd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to - b! + A! = A! + (- b!)$
45	27	nncnd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to b! \in ℂ$
46	43 45	negsubd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to A! + (- b!) = A! - b!$
47	44 46	eqtrd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to - b! + A! = A! - b!$
48	11	adantr	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to A \in ℕ_{0}$
49		elfzle2	$⊢ b \in (1 \dots A) \to b \leq A$
50	49	adantl	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to b \leq A$
51		facwordi	$⊢ (b \in ℕ_{0} \land A \in ℕ_{0} \land b \leq A) \to b! \leq A!$
52	26 48 50 51	syl3anc	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to b! \leq A!$
53	27	nnnn0d	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to b! \in ℕ_{0}$
54	48	faccld	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to A! \in ℕ$
55	54	nnnn0d	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to A! \in ℕ_{0}$
56		nn0sub	$⊢ (b! \in ℕ_{0} \land A! \in ℕ_{0}) \to (b! \leq A! \leftrightarrow A! - b! \in ℕ_{0})$
57	53 55 56	syl2anc	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to (b! \leq A! \leftrightarrow A! - b! \in ℕ_{0})$
58	52 57	mpbid	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to A! - b! \in ℕ_{0}$
59	47 58	eqeltrd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to - b! + A! \in ℕ_{0}$
60		zexpcl	$⊢ (2 \in ℤ \land - b! + A! \in ℕ_{0}) \to 2^{- b! + A!} \in ℤ$
61	41 59 60	sylancr	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to 2^{- b! + A!} \in ℤ$
62	40 61	eqeltrrd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to 2^{- b!} 2^{A!} \in ℤ$
63	35 62	eqeltrd	$⊢ (A \in ℕ \land b \in (1 \dots A)) \to F (b) 2^{A!} \in ℤ$
64	9 63	fsumzcl	$⊢ A \in ℕ \to \sum_{b = 1}^{A} F (b) 2^{A!} \in ℤ$
65	34 64	eqeltrd	$⊢ A \in ℕ \to \sum_{b = 1}^{A} F (b) 2^{A!} \in ℤ$
66	8 65	eqeltrd	$⊢ A \in ℕ \to H (A) 2^{A!} \in ℤ$

Metamath Proof Explorer

Theorem aaliou3lem6

Proof