aaliou3lem2

	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	aaliou3lem2	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to F (B) \in (0, G (B)]$

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		eluznn	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to B \in ℕ$
4		fveq2	$⊢ a = B \to a! = B!$
5	4	negeqd	$⊢ a = B \to - a! = - B!$
6	5	oveq2d	$⊢ a = B \to 2^{- a!} = 2^{- B!}$
7		ovex	$⊢ 2^{- B!} \in V$
8	6 2 7	fvmpt	$⊢ B \in ℕ \to F (B) = 2^{- B!}$
9	3 8	syl	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to F (B) = 2^{- B!}$
10		2rp	$⊢ 2 \in ℝ^{+}$
11	3	nnnn0d	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to B \in ℕ_{0}$
12	11	faccld	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to B! \in ℕ$
13	12	nnzd	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to B! \in ℤ$
14	13	znegcld	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to - B! \in ℤ$
15		rpexpcl	$⊢ (2 \in ℝ^{+} \land - B! \in ℤ) \to 2^{- B!} \in ℝ^{+}$
16	10 14 15	sylancr	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to 2^{- B!} \in ℝ^{+}$
17	9 16	eqeltrd	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to F (B) \in ℝ^{+}$
18	17	rpred	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to F (B) \in ℝ$
19	17	rpgt0d	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to 0 < F (B)$
20		fveq2	$⊢ b = A \to F (b) = F (A)$
21		fveq2	$⊢ b = A \to G (b) = G (A)$
22	20 21	breq12d	$⊢ b = A \to (F (b) \leq G (b) \leftrightarrow F (A) \leq G (A))$
23	22	imbi2d	$⊢ b = A \to ((A \in ℕ \to F (b) \leq G (b)) \leftrightarrow (A \in ℕ \to F (A) \leq G (A)))$
24		fveq2	$⊢ b = d \to F (b) = F (d)$
25		fveq2	$⊢ b = d \to G (b) = G (d)$
26	24 25	breq12d	$⊢ b = d \to (F (b) \leq G (b) \leftrightarrow F (d) \leq G (d))$
27	26	imbi2d	$⊢ b = d \to ((A \in ℕ \to F (b) \leq G (b)) \leftrightarrow (A \in ℕ \to F (d) \leq G (d)))$
28		fveq2	$⊢ b = d + 1 \to F (b) = F (d + 1)$
29		fveq2	$⊢ b = d + 1 \to G (b) = G (d + 1)$
30	28 29	breq12d	$⊢ b = d + 1 \to (F (b) \leq G (b) \leftrightarrow F (d + 1) \leq G (d + 1))$
31	30	imbi2d	$⊢ b = d + 1 \to ((A \in ℕ \to F (b) \leq G (b)) \leftrightarrow (A \in ℕ \to F (d + 1) \leq G (d + 1)))$
32		fveq2	$⊢ b = B \to F (b) = F (B)$
33		fveq2	$⊢ b = B \to G (b) = G (B)$
34	32 33	breq12d	$⊢ b = B \to (F (b) \leq G (b) \leftrightarrow F (B) \leq G (B))$
35	34	imbi2d	$⊢ b = B \to ((A \in ℕ \to F (b) \leq G (b)) \leftrightarrow (A \in ℕ \to F (B) \leq G (B)))$
36		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
37	36	faccld	$⊢ A \in ℕ \to A! \in ℕ$
38	37	nnzd	$⊢ A \in ℕ \to A! \in ℤ$
39	38	znegcld	$⊢ A \in ℕ \to - A! \in ℤ$
40		rpexpcl	$⊢ (2 \in ℝ^{+} \land - A! \in ℤ) \to 2^{- A!} \in ℝ^{+}$
41	10 39 40	sylancr	$⊢ A \in ℕ \to 2^{- A!} \in ℝ^{+}$
42	41	rpred	$⊢ A \in ℕ \to 2^{- A!} \in ℝ$
43	42	leidd	$⊢ A \in ℕ \to 2^{- A!} \leq 2^{- A!}$
44		nncn	$⊢ A \in ℕ \to A \in ℂ$
45	44	subidd	$⊢ A \in ℕ \to A - A = 0$
46	45	oveq2d	$⊢ A \in ℕ \to {(\frac{1}{2})}^{A - A} = {(\frac{1}{2})}^{0}$
47		halfcn	$⊢ \frac{1}{2} \in ℂ$
48		exp0	$⊢ \frac{1}{2} \in ℂ \to {(\frac{1}{2})}^{0} = 1$
49	47 48	ax-mp	$⊢ {(\frac{1}{2})}^{0} = 1$
50	46 49	eqtrdi	$⊢ A \in ℕ \to {(\frac{1}{2})}^{A - A} = 1$
51	50	oveq2d	$⊢ A \in ℕ \to 2^{- A!} {(\frac{1}{2})}^{A - A} = 2^{- A!} \cdot 1$
52	41	rpcnd	$⊢ A \in ℕ \to 2^{- A!} \in ℂ$
53	52	mulid1d	$⊢ A \in ℕ \to 2^{- A!} \cdot 1 = 2^{- A!}$
54	51 53	eqtrd	$⊢ A \in ℕ \to 2^{- A!} {(\frac{1}{2})}^{A - A} = 2^{- A!}$
55	43 54	breqtrrd	$⊢ A \in ℕ \to 2^{- A!} \leq 2^{- A!} {(\frac{1}{2})}^{A - A}$
56		fveq2	$⊢ a = A \to a! = A!$
57	56	negeqd	$⊢ a = A \to - a! = - A!$
58	57	oveq2d	$⊢ a = A \to 2^{- a!} = 2^{- A!}$
59		ovex	$⊢ 2^{- A!} \in V$
60	58 2 59	fvmpt	$⊢ A \in ℕ \to F (A) = 2^{- A!}$
61		nnz	$⊢ A \in ℕ \to A \in ℤ$
62		uzid	$⊢ A \in ℤ \to A \in ℤ_{\geq A}$
63		oveq1	$⊢ c = A \to c - A = A - A$
64	63	oveq2d	$⊢ c = A \to {(\frac{1}{2})}^{c - A} = {(\frac{1}{2})}^{A - A}$
65	64	oveq2d	$⊢ c = A \to 2^{- A!} {(\frac{1}{2})}^{c - A} = 2^{- A!} {(\frac{1}{2})}^{A - A}$
66		ovex	$⊢ 2^{- A!} {(\frac{1}{2})}^{A - A} \in V$
67	65 1 66	fvmpt	$⊢ A \in ℤ_{\geq A} \to G (A) = 2^{- A!} {(\frac{1}{2})}^{A - A}$
68	61 62 67	3syl	$⊢ A \in ℕ \to G (A) = 2^{- A!} {(\frac{1}{2})}^{A - A}$
69	55 60 68	3brtr4d	$⊢ A \in ℕ \to F (A) \leq G (A)$
70		eluznn	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d \in ℕ$
71	70	nnnn0d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d \in ℕ_{0}$
72	71	faccld	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d! \in ℕ$
73	72	nnzd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d! \in ℤ$
74	73	znegcld	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to - d! \in ℤ$
75		rpexpcl	$⊢ (2 \in ℝ^{+} \land - d! \in ℤ) \to 2^{- d!} \in ℝ^{+}$
76	10 74 75	sylancr	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- d!} \in ℝ^{+}$
77	76	rpred	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- d!} \in ℝ$
78	76	rpge0d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 0 \leq 2^{- d!}$
79		simpl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to A \in ℕ$
80	79	nnnn0d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to A \in ℕ_{0}$
81	80	faccld	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to A! \in ℕ$
82	81	nnzd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to A! \in ℤ$
83	82	znegcld	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to - A! \in ℤ$
84	10 83 40	sylancr	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- A!} \in ℝ^{+}$
85		halfre	$⊢ \frac{1}{2} \in ℝ$
86		halfgt0	$⊢ 0 < \frac{1}{2}$
87	85 86	elrpii	$⊢ \frac{1}{2} \in ℝ^{+}$
88		eluzelz	$⊢ d \in ℤ_{\geq A} \to d \in ℤ$
89		zsubcl	$⊢ (d \in ℤ \land A \in ℤ) \to d - A \in ℤ$
90	88 61 89	syl2anr	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d - A \in ℤ$
91		rpexpcl	$⊢ (\frac{1}{2} \in ℝ^{+} \land d - A \in ℤ) \to {(\frac{1}{2})}^{d - A} \in ℝ^{+}$
92	87 90 91	sylancr	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to {(\frac{1}{2})}^{d - A} \in ℝ^{+}$
93	84 92	rpmulcld	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- A!} {(\frac{1}{2})}^{d - A} \in ℝ^{+}$
94	93	rpred	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- A!} {(\frac{1}{2})}^{d - A} \in ℝ$
95	77 78 94	jca31	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to ((2^{- d!} \in ℝ \land 0 \leq 2^{- d!}) \land 2^{- A!} {(\frac{1}{2})}^{d - A} \in ℝ)$
96	95	adantr	$⊢ ((A \in ℕ \land d \in ℤ_{\geq A}) \land 2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A}) \to ((2^{- d!} \in ℝ \land 0 \leq 2^{- d!}) \land 2^{- A!} {(\frac{1}{2})}^{d - A} \in ℝ)$
97	88	adantl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d \in ℤ$
98	74 97	zmulcld	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (- d!) d \in ℤ$
99		rpexpcl	$⊢ (2 \in ℝ^{+} \land (- d!) d \in ℤ) \to 2^{(- d!) d} \in ℝ^{+}$
100	10 98 99	sylancr	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{(- d!) d} \in ℝ^{+}$
101	100	rpred	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{(- d!) d} \in ℝ$
102	100	rpge0d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 0 \leq 2^{(- d!) d}$
103	85	a1i	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to \frac{1}{2} \in ℝ$
104	101 102 103	jca31	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to ((2^{(- d!) d} \in ℝ \land 0 \leq 2^{(- d!) d}) \land \frac{1}{2} \in ℝ)$
105	104	adantr	$⊢ ((A \in ℕ \land d \in ℤ_{\geq A}) \land 2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A}) \to ((2^{(- d!) d} \in ℝ \land 0 \leq 2^{(- d!) d}) \land \frac{1}{2} \in ℝ)$
106		simpr	$⊢ ((A \in ℕ \land d \in ℤ_{\geq A}) \land 2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A}) \to 2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A}$
107		2re	$⊢ 2 \in ℝ$
108		1le2	$⊢ 1 \leq 2$
109	72	nncnd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d! \in ℂ$
110	97	zcnd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d \in ℂ$
111	109 110	mulneg1d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (- d!) d = - d! d$
112	72 70	nnmulcld	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d! d \in ℕ$
113	112	nnge1d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 1 \leq d! d$
114		1re	$⊢ 1 \in ℝ$
115	112	nnred	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d! d \in ℝ$
116		leneg	$⊢ (1 \in ℝ \land d! d \in ℝ) \to (1 \leq d! d \leftrightarrow - d! d \leq - 1)$
117	114 115 116	sylancr	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (1 \leq d! d \leftrightarrow - d! d \leq - 1)$
118	113 117	mpbid	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to - d! d \leq - 1$
119	111 118	eqbrtrd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (- d!) d \leq - 1$
120		neg1z	$⊢ - 1 \in ℤ$
121		eluz	$⊢ ((- d!) d \in ℤ \land - 1 \in ℤ) \to (- 1 \in ℤ_{\geq (- d!) d} \leftrightarrow (- d!) d \leq - 1)$
122	98 120 121	sylancl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (- 1 \in ℤ_{\geq (- d!) d} \leftrightarrow (- d!) d \leq - 1)$
123	119 122	mpbird	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to - 1 \in ℤ_{\geq (- d!) d}$
124		leexp2a	$⊢ (2 \in ℝ \land 1 \leq 2 \land - 1 \in ℤ_{\geq (- d!) d}) \to 2^{(- d!) d} \leq 2^{- 1}$
125	107 108 123 124	mp3an12i	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{(- d!) d} \leq 2^{- 1}$
126		2cn	$⊢ 2 \in ℂ$
127		expn1	$⊢ 2 \in ℂ \to 2^{- 1} = \frac{1}{2}$
128	126 127	ax-mp	$⊢ 2^{- 1} = \frac{1}{2}$
129	125 128	breqtrdi	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{(- d!) d} \leq \frac{1}{2}$
130	129	adantr	$⊢ ((A \in ℕ \land d \in ℤ_{\geq A}) \land 2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A}) \to 2^{(- d!) d} \leq \frac{1}{2}$
131		lemul12a	$⊢ (((2^{- d!} \in ℝ \land 0 \leq 2^{- d!}) \land 2^{- A!} {(\frac{1}{2})}^{d - A} \in ℝ) \land ((2^{(- d!) d} \in ℝ \land 0 \leq 2^{(- d!) d}) \land \frac{1}{2} \in ℝ)) \to ((2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A} \land 2^{(- d!) d} \leq \frac{1}{2}) \to 2^{- d!} 2^{(- d!) d} \leq 2^{- A!} {(\frac{1}{2})}^{d - A} (\frac{1}{2}))$
132	131	3impia	$⊢ (((2^{- d!} \in ℝ \land 0 \leq 2^{- d!}) \land 2^{- A!} {(\frac{1}{2})}^{d - A} \in ℝ) \land ((2^{(- d!) d} \in ℝ \land 0 \leq 2^{(- d!) d}) \land \frac{1}{2} \in ℝ) \land (2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A} \land 2^{(- d!) d} \leq \frac{1}{2})) \to 2^{- d!} 2^{(- d!) d} \leq 2^{- A!} {(\frac{1}{2})}^{d - A} (\frac{1}{2})$
133	96 105 106 130 132	syl112anc	$⊢ ((A \in ℕ \land d \in ℤ_{\geq A}) \land 2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A}) \to 2^{- d!} 2^{(- d!) d} \leq 2^{- A!} {(\frac{1}{2})}^{d - A} (\frac{1}{2})$
134	133	ex	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A} \to 2^{- d!} 2^{(- d!) d} \leq 2^{- A!} {(\frac{1}{2})}^{d - A} (\frac{1}{2}))$
135		facp1	$⊢ d \in ℕ_{0} \to (d + 1)! = d! (d + 1)$
136	71 135	syl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (d + 1)! = d! (d + 1)$
137	136	negeqd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to - (d + 1)! = - d! (d + 1)$
138		ax-1cn	$⊢ 1 \in ℂ$
139		addcom	$⊢ (d \in ℂ \land 1 \in ℂ) \to d + 1 = 1 + d$
140	110 138 139	sylancl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d + 1 = 1 + d$
141	140	oveq2d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (- d!) (d + 1) = (- d!) (1 + d)$
142		peano2cn	$⊢ d \in ℂ \to d + 1 \in ℂ$
143	110 142	syl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d + 1 \in ℂ$
144	109 143	mulneg1d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (- d!) (d + 1) = - d! (d + 1)$
145	74	zcnd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to - d! \in ℂ$
146		1cnd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 1 \in ℂ$
147	145 146 110	adddid	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (- d!) (1 + d) = (- d!) \cdot 1 + (- d!) d$
148	145	mulid1d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (- d!) \cdot 1 = - d!$
149	148	oveq1d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (- d!) \cdot 1 + (- d!) d = - d! + (- d!) d$
150	147 149	eqtrd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (- d!) (1 + d) = - d! + (- d!) d$
151	141 144 150	3eqtr3d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to - d! (d + 1) = - d! + (- d!) d$
152	137 151	eqtrd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to - (d + 1)! = - d! + (- d!) d$
153	152	oveq2d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- (d + 1)!} = 2^{- d! + (- d!) d}$
154		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
155		expaddz	$⊢ ((2 \in ℂ \land 2 \neq 0) \land (- d! \in ℤ \land (- d!) d \in ℤ)) \to 2^{- d! + (- d!) d} = 2^{- d!} 2^{(- d!) d}$
156	154 155	mpan	$⊢ (- d! \in ℤ \land (- d!) d \in ℤ) \to 2^{- d! + (- d!) d} = 2^{- d!} 2^{(- d!) d}$
157	74 98 156	syl2anc	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- d! + (- d!) d} = 2^{- d!} 2^{(- d!) d}$
158	153 157	eqtrd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- (d + 1)!} = 2^{- d!} 2^{(- d!) d}$
159	44	adantr	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to A \in ℂ$
160	110 146 159	addsubd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d + 1 - A = d - A + 1$
161	160	oveq2d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to {(\frac{1}{2})}^{d + 1 - A} = {(\frac{1}{2})}^{d - A + 1}$
162		uznn0sub	$⊢ d \in ℤ_{\geq A} \to d - A \in ℕ_{0}$
163	162	adantl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d - A \in ℕ_{0}$
164		expp1	$⊢ (\frac{1}{2} \in ℂ \land d - A \in ℕ_{0}) \to {(\frac{1}{2})}^{d - A + 1} = {(\frac{1}{2})}^{d - A} (\frac{1}{2})$
165	47 163 164	sylancr	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to {(\frac{1}{2})}^{d - A + 1} = {(\frac{1}{2})}^{d - A} (\frac{1}{2})$
166	161 165	eqtrd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to {(\frac{1}{2})}^{d + 1 - A} = {(\frac{1}{2})}^{d - A} (\frac{1}{2})$
167	166	oveq2d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- A!} {(\frac{1}{2})}^{d + 1 - A} = 2^{- A!} {(\frac{1}{2})}^{d - A} (\frac{1}{2})$
168	84	rpcnd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- A!} \in ℂ$
169	92	rpcnd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to {(\frac{1}{2})}^{d - A} \in ℂ$
170	47	a1i	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to \frac{1}{2} \in ℂ$
171	168 169 170	mulassd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- A!} {(\frac{1}{2})}^{d - A} (\frac{1}{2}) = 2^{- A!} {(\frac{1}{2})}^{d - A} (\frac{1}{2})$
172	167 171	eqtr4d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to 2^{- A!} {(\frac{1}{2})}^{d + 1 - A} = 2^{- A!} {(\frac{1}{2})}^{d - A} (\frac{1}{2})$
173	158 172	breq12d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (2^{- (d + 1)!} \leq 2^{- A!} {(\frac{1}{2})}^{d + 1 - A} \leftrightarrow 2^{- d!} 2^{(- d!) d} \leq 2^{- A!} {(\frac{1}{2})}^{d - A} (\frac{1}{2}))$
174	134 173	sylibrd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A} \to 2^{- (d + 1)!} \leq 2^{- A!} {(\frac{1}{2})}^{d + 1 - A})$
175		fveq2	$⊢ a = d \to a! = d!$
176	175	negeqd	$⊢ a = d \to - a! = - d!$
177	176	oveq2d	$⊢ a = d \to 2^{- a!} = 2^{- d!}$
178		ovex	$⊢ 2^{- d!} \in V$
179	177 2 178	fvmpt	$⊢ d \in ℕ \to F (d) = 2^{- d!}$
180	70 179	syl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to F (d) = 2^{- d!}$
181		oveq1	$⊢ c = d \to c - A = d - A$
182	181	oveq2d	$⊢ c = d \to {(\frac{1}{2})}^{c - A} = {(\frac{1}{2})}^{d - A}$
183	182	oveq2d	$⊢ c = d \to 2^{- A!} {(\frac{1}{2})}^{c - A} = 2^{- A!} {(\frac{1}{2})}^{d - A}$
184		ovex	$⊢ 2^{- A!} {(\frac{1}{2})}^{d - A} \in V$
185	183 1 184	fvmpt	$⊢ d \in ℤ_{\geq A} \to G (d) = 2^{- A!} {(\frac{1}{2})}^{d - A}$
186	185	adantl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to G (d) = 2^{- A!} {(\frac{1}{2})}^{d - A}$
187	180 186	breq12d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (F (d) \leq G (d) \leftrightarrow 2^{- d!} \leq 2^{- A!} {(\frac{1}{2})}^{d - A})$
188	70	peano2nnd	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to d + 1 \in ℕ$
189		fveq2	$⊢ a = d + 1 \to a! = (d + 1)!$
190	189	negeqd	$⊢ a = d + 1 \to - a! = - (d + 1)!$
191	190	oveq2d	$⊢ a = d + 1 \to 2^{- a!} = 2^{- (d + 1)!}$
192		ovex	$⊢ 2^{- (d + 1)!} \in V$
193	191 2 192	fvmpt	$⊢ d + 1 \in ℕ \to F (d + 1) = 2^{- (d + 1)!}$
194	188 193	syl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to F (d + 1) = 2^{- (d + 1)!}$
195		peano2uz	$⊢ d \in ℤ_{\geq A} \to d + 1 \in ℤ_{\geq A}$
196		oveq1	$⊢ c = d + 1 \to c - A = d + 1 - A$
197	196	oveq2d	$⊢ c = d + 1 \to {(\frac{1}{2})}^{c - A} = {(\frac{1}{2})}^{d + 1 - A}$
198	197	oveq2d	$⊢ c = d + 1 \to 2^{- A!} {(\frac{1}{2})}^{c - A} = 2^{- A!} {(\frac{1}{2})}^{d + 1 - A}$
199		ovex	$⊢ 2^{- A!} {(\frac{1}{2})}^{d + 1 - A} \in V$
200	198 1 199	fvmpt	$⊢ d + 1 \in ℤ_{\geq A} \to G (d + 1) = 2^{- A!} {(\frac{1}{2})}^{d + 1 - A}$
201	195 200	syl	$⊢ d \in ℤ_{\geq A} \to G (d + 1) = 2^{- A!} {(\frac{1}{2})}^{d + 1 - A}$
202	201	adantl	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to G (d + 1) = 2^{- A!} {(\frac{1}{2})}^{d + 1 - A}$
203	194 202	breq12d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (F (d + 1) \leq G (d + 1) \leftrightarrow 2^{- (d + 1)!} \leq 2^{- A!} {(\frac{1}{2})}^{d + 1 - A})$
204	174 187 203	3imtr4d	$⊢ (A \in ℕ \land d \in ℤ_{\geq A}) \to (F (d) \leq G (d) \to F (d + 1) \leq G (d + 1))$
205	204	expcom	$⊢ d \in ℤ_{\geq A} \to (A \in ℕ \to (F (d) \leq G (d) \to F (d + 1) \leq G (d + 1)))$
206	205	a2d	$⊢ d \in ℤ_{\geq A} \to ((A \in ℕ \to F (d) \leq G (d)) \to (A \in ℕ \to F (d + 1) \leq G (d + 1)))$
207	23 27 31 35 69 206	uzind4i	$⊢ B \in ℤ_{\geq A} \to (A \in ℕ \to F (B) \leq G (B))$
208	207	impcom	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to F (B) \leq G (B)$
209		0xr	$⊢ 0 \in ℝ^{*}$
210	1	aaliou3lem1	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to G (B) \in ℝ$
211		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)))$
212	209 210 211	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)))$
213	18 19 208 212	mpbir3and	$⊢ (A \in ℕ \land B \in ℤ_{\geq A}) \to F (B) \in (0, G (B)]$

Metamath Proof Explorer

Theorem aaliou3lem2

Proof