aaliou3lem3

	Ref	Expression
Hypotheses	aaliou3lem.a	$⊢ G = (c \in ℤ_{\geq A} ⟼ 2^{- A!} {(\frac{1}{2})}^{c - A})$
	aaliou3lem.b	$⊢ F = (a \in ℕ ⟼ 2^{- a!})$
Assertion	aaliou3lem3	$⊢ A \in ℕ \to (seq A (+ F) \in dom ⇝ \land \sum_{b \in ℤ_{\geq A}} F (b) \in ℝ^{+} \land \sum_{b \in ℤ_{\geq A}} F (b) \leq 2 2^{- A!})$

Proof

Step	Hyp	Ref	Expression
1		aaliou3lem.a	$⊢ G = (c \in ℤ_{\geq A} ⟼ 2^{- A!} {(\frac{1}{2})}^{c - A})$
2		aaliou3lem.b	$⊢ F = (a \in ℕ ⟼ 2^{- a!})$
3		eqid	$⊢ ℤ_{\geq A} = ℤ_{\geq A}$
4		nnz	$⊢ A \in ℕ \to A \in ℤ$
5		uzid	$⊢ A \in ℤ \to A \in ℤ_{\geq A}$
6	4 5	syl	$⊢ A \in ℕ \to A \in ℤ_{\geq A}$
7	1	aaliou3lem1	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to G (b) \in ℝ$
8	1 2	aaliou3lem2	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to F (b) \in (0, G (b)]$
9		0xr	$⊢ 0 \in ℝ^{*}$
10		elioc2	$⊢ (0 \in ℝ^{*} \land G (b) \in ℝ) \to (F (b) \in (0, G (b)] \leftrightarrow (F (b) \in ℝ \land 0 < F (b) \land F (b) \leq G (b)))$
11	9 7 10	sylancr	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to (F (b) \in (0, G (b)] \leftrightarrow (F (b) \in ℝ \land 0 < F (b) \land F (b) \leq G (b)))$
12	8 11	mpbid	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to (F (b) \in ℝ \land 0 < F (b) \land F (b) \leq G (b))$
13	12	simp1d	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to F (b) \in ℝ$
14		halfcn	$⊢ \frac{1}{2} \in ℂ$
15	14	a1i	$⊢ A \in ℕ \to \frac{1}{2} \in ℂ$
16		halfre	$⊢ \frac{1}{2} \in ℝ$
17		halfgt0	$⊢ 0 < \frac{1}{2}$
18	16 17	elrpii	$⊢ \frac{1}{2} \in ℝ^{+}$
19		rprege0	$⊢ \frac{1}{2} \in ℝ^{+} \to (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2})$
20		absid	$⊢ (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2}) \to \|\frac{1}{2}\| = \frac{1}{2}$
21	18 19 20	mp2b	$⊢ \|\frac{1}{2}\| = \frac{1}{2}$
22		halflt1	$⊢ \frac{1}{2} < 1$
23	21 22	eqbrtri	$⊢ \|\frac{1}{2}\| < 1$
24	23	a1i	$⊢ A \in ℕ \to \|\frac{1}{2}\| < 1$
25		2rp	$⊢ 2 \in ℝ^{+}$
26		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
27	26	faccld	$⊢ A \in ℕ \to A! \in ℕ$
28	27	nnzd	$⊢ A \in ℕ \to A! \in ℤ$
29	28	znegcld	$⊢ A \in ℕ \to - A! \in ℤ$
30		rpexpcl	$⊢ (2 \in ℝ^{+} \land - A! \in ℤ) \to 2^{- A!} \in ℝ^{+}$
31	25 29 30	sylancr	$⊢ A \in ℕ \to 2^{- A!} \in ℝ^{+}$
32	31	rpcnd	$⊢ A \in ℕ \to 2^{- A!} \in ℂ$
33	4 15 24 32 1	geolim3	$⊢ A \in ℕ \to seq A (+ G) ⇝ (\frac{2^{- A!}}{1 - (\frac{1}{2})})$
34		seqex	$⊢ seq A (+ G) \in V$
35		ovex	$⊢ \frac{2^{- A!}}{1 - (\frac{1}{2})} \in V$
36	34 35	breldm	$⊢ seq A (+ G) ⇝ (\frac{2^{- A!}}{1 - (\frac{1}{2})}) \to seq A (+ G) \in dom ⇝$
37	33 36	syl	$⊢ A \in ℕ \to seq A (+ G) \in dom ⇝$
38	12	simp2d	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to 0 < F (b)$
39	13 38	elrpd	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to F (b) \in ℝ^{+}$
40	39	rpge0d	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to 0 \leq F (b)$
41	12	simp3d	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to F (b) \leq G (b)$
42	3 6 7 13 37 40 41	cvgcmp	$⊢ A \in ℕ \to seq A (+ F) \in dom ⇝$
43		eqidd	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to F (b) = F (b)$
44	3 3 6 43 39 42	isumrpcl	$⊢ A \in ℕ \to \sum_{b \in ℤ_{\geq A}} F (b) \in ℝ^{+}$
45		eqidd	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to G (b) = G (b)$
46	3 4 43 13 45 7 41 42 37	isumle	$⊢ A \in ℕ \to \sum_{b \in ℤ_{\geq A}} F (b) \leq \sum_{b \in ℤ_{\geq A}} G (b)$
47	7	recnd	$⊢ (A \in ℕ \land b \in ℤ_{\geq A}) \to G (b) \in ℂ$
48	3 4 45 47 33	isumclim	$⊢ A \in ℕ \to \sum_{b \in ℤ_{\geq A}} G (b) = \frac{2^{- A!}}{1 - (\frac{1}{2})}$
49		1mhlfehlf	$⊢ 1 - (\frac{1}{2}) = \frac{1}{2}$
50	49	oveq2i	$⊢ \frac{2^{- A!}}{1 - (\frac{1}{2})} = \frac{2^{- A!}}{\frac{1}{2}}$
51		2cn	$⊢ 2 \in ℂ$
52		mulcl	$⊢ (2^{- A!} \in ℂ \land 2 \in ℂ) \to 2^{- A!} \cdot 2 \in ℂ$
53	32 51 52	sylancl	$⊢ A \in ℕ \to 2^{- A!} \cdot 2 \in ℂ$
54	53	div1d	$⊢ A \in ℕ \to \frac{2^{- A!} \cdot 2}{1} = 2^{- A!} \cdot 2$
55		1rp	$⊢ 1 \in ℝ^{+}$
56		rpcnne0	$⊢ 1 \in ℝ^{+} \to (1 \in ℂ \land 1 \neq 0)$
57	55 56	ax-mp	$⊢ (1 \in ℂ \land 1 \neq 0)$
58		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
59		divdiv2	$⊢ (2^{- A!} \in ℂ \land (1 \in ℂ \land 1 \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2^{- A!}}{\frac{1}{2}} = \frac{2^{- A!} \cdot 2}{1}$
60	57 58 59	mp3an23	$⊢ 2^{- A!} \in ℂ \to \frac{2^{- A!}}{\frac{1}{2}} = \frac{2^{- A!} \cdot 2}{1}$
61	32 60	syl	$⊢ A \in ℕ \to \frac{2^{- A!}}{\frac{1}{2}} = \frac{2^{- A!} \cdot 2}{1}$
62		mulcom	$⊢ (2 \in ℂ \land 2^{- A!} \in ℂ) \to 2 2^{- A!} = 2^{- A!} \cdot 2$
63	51 32 62	sylancr	$⊢ A \in ℕ \to 2 2^{- A!} = 2^{- A!} \cdot 2$
64	54 61 63	3eqtr4d	$⊢ A \in ℕ \to \frac{2^{- A!}}{\frac{1}{2}} = 2 2^{- A!}$
65	50 64	eqtrid	$⊢ A \in ℕ \to \frac{2^{- A!}}{1 - (\frac{1}{2})} = 2 2^{- A!}$
66	48 65	eqtrd	$⊢ A \in ℕ \to \sum_{b \in ℤ_{\geq A}} G (b) = 2 2^{- A!}$
67	46 66	breqtrd	$⊢ A \in ℕ \to \sum_{b \in ℤ_{\geq A}} F (b) \leq 2 2^{- A!}$
68	42 44 67	3jca	$⊢ A \in ℕ \to (seq A (+ F) \in dom ⇝ \land \sum_{b \in ℤ_{\geq A}} F (b) \in ℝ^{+} \land \sum_{b \in ℤ_{\geq A}} F (b) \leq 2 2^{- A!})$

Metamath Proof Explorer

Theorem aaliou3lem3

Proof