aaliou3lem1

		Ref	Expression
	Hypothesis	aaliou3lem.a	$⊢ G = (c \in ℤ_{\geq A} ⟼ 2^{- A!} {(\frac{1}{2})}^{c - A})$
	Assertion	aaliou3lem1	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to G (B) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		aaliou3lem.a	$⊢ G = (c \in ℤ_{\geq A} ⟼ 2^{- A!} {(\frac{1}{2})}^{c - A})$
2		oveq1	$⊢ c = B \to c - A = B - A$
3	2	oveq2d	$⊢ c = B \to {(\frac{1}{2})}^{c - A} = {(\frac{1}{2})}^{B - A}$
4	3	oveq2d	$⊢ c = B \to 2^{- A!} {(\frac{1}{2})}^{c - A} = 2^{- A!} {(\frac{1}{2})}^{B - A}$
5		ovex	$⊢ 2^{- A!} {(\frac{1}{2})}^{B - A} \in V$
6	4 1 5	fvmpt	$⊢ B \in ℤ_{\geq A} \to G (B) = 2^{- A!} {(\frac{1}{2})}^{B - A}$
7	6	adantl	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to G (B) = 2^{- A!} {(\frac{1}{2})}^{B - A}$
8		2rp	$⊢ 2 \in ℝ^{+}$
9		simpl	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to A \in ℕ$
10	9	nnnn0d	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to A \in ℕ_{0}$
11	10	faccld	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to A! \in ℕ$
12	11	nnzd	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to A! \in ℤ$
13	12	znegcld	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to - A! \in ℤ$
14		rpexpcl	$⊢ (2 \in ℝ^{+} \land - A! \in ℤ) \to 2^{- A!} \in ℝ^{+}$
15	8 13 14	sylancr	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to 2^{- A!} \in ℝ^{+}$
16		halfre	$⊢ \frac{1}{2} \in ℝ$
17		halfgt0	$⊢ 0 < \frac{1}{2}$
18	16 17	elrpii	$⊢ \frac{1}{2} \in ℝ^{+}$
19		eluzelz	$⊢ B \in ℤ_{\geq A} \to B \in ℤ$
20		nnz	$⊢ A \in ℕ \to A \in ℤ$
21		zsubcl	$⊢ (B \in ℤ \land A \in ℤ) \to B - A \in ℤ$
22	19 20 21	syl2anr	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to B - A \in ℤ$
23		rpexpcl	$⊢ (\frac{1}{2} \in ℝ^{+} \land B - A \in ℤ) \to {(\frac{1}{2})}^{B - A} \in ℝ^{+}$
24	18 22 23	sylancr	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to {(\frac{1}{2})}^{B - A} \in ℝ^{+}$
25	15 24	rpmulcld	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to 2^{- A!} {(\frac{1}{2})}^{B - A} \in ℝ^{+}$
26	25	rpred	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to 2^{- A!} {(\frac{1}{2})}^{B - A} \in ℝ$
27	7 26	eqeltrd	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to G (B) \in ℝ$

Metamath Proof Explorer

Theorem aaliou3lem1

Proof