aaliou3lem8

		Ref	Expression
	Assertion	aaliou3lem8	$⊢ (A \in ℕ \land B \in ℝ^{+}) \to \exists x \in ℕ 2 2^{- (x + 1)!} \leq \frac{B}{{(2^{x!})}^{A}}$

Proof

Step	Hyp	Ref	Expression
1		2rp	$⊢ 2 \in ℝ^{+}$
2		rpdivcl	$⊢ (2 \in ℝ^{+} \land B \in ℝ^{+}) \to \frac{2}{B} \in ℝ^{+}$
3	1 2	mpan	$⊢ B \in ℝ^{+} \to \frac{2}{B} \in ℝ^{+}$
4	3	rpred	$⊢ B \in ℝ^{+} \to \frac{2}{B} \in ℝ$
5		2re	$⊢ 2 \in ℝ$
6		1lt2	$⊢ 1 < 2$
7		expnbnd	$⊢ (\frac{2}{B} \in ℝ \land 2 \in ℝ \land 1 < 2) \to \exists a \in ℕ \frac{2}{B} < 2^{a}$
8	5 6 7	mp3an23	$⊢ \frac{2}{B} \in ℝ \to \exists a \in ℕ \frac{2}{B} < 2^{a}$
9	4 8	syl	$⊢ B \in ℝ^{+} \to \exists a \in ℕ \frac{2}{B} < 2^{a}$
10	9	adantl	$⊢ (A \in ℕ \land B \in ℝ^{+}) \to \exists a \in ℕ \frac{2}{B} < 2^{a}$
11		simprl	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a \in ℕ$
12		simpll	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to A \in ℕ$
13		nnaddm1cl	$⊢ (a \in ℕ \land A \in ℕ) \to a + A - 1 \in ℕ$
14	11 12 13	syl2anc	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a + A - 1 \in ℕ$
15		simplr	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to B \in ℝ^{+}$
16		rerpdivcl	$⊢ (2 \in ℝ \land B \in ℝ^{+}) \to \frac{2}{B} \in ℝ$
17	5 15 16	sylancr	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{2}{B} \in ℝ$
18	11	nnnn0d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a \in ℕ_{0}$
19		reexpcl	$⊢ (2 \in ℝ \land a \in ℕ_{0}) \to 2^{a} \in ℝ$
20	5 18 19	sylancr	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{a} \in ℝ$
21	11 12	nnaddcld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a + A \in ℕ$
22		nnm1nn0	$⊢ a + A \in ℕ \to a + A - 1 \in ℕ_{0}$
23	21 22	syl	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a + A - 1 \in ℕ_{0}$
24		peano2nn0	$⊢ a + A - 1 \in ℕ_{0} \to (a + A) - 1 + 1 \in ℕ_{0}$
25	23 24	syl	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A) - 1 + 1 \in ℕ_{0}$
26	25	faccld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to ((a + A) - 1 + 1)! \in ℕ$
27	26	nnzd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to ((a + A) - 1 + 1)! \in ℤ$
28	23	faccld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A - 1)! \in ℕ$
29	28	nnzd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A - 1)! \in ℤ$
30	12	nnzd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to A \in ℤ$
31	29 30	zmulcld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A - 1)! A \in ℤ$
32	27 31	zsubcld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to ((a + A) - 1 + 1)! - (a + A - 1)! A \in ℤ$
33		rpexpcl	$⊢ (2 \in ℝ^{+} \land ((a + A) - 1 + 1)! - (a + A - 1)! A \in ℤ) \to 2^{((a + A) - 1 + 1)! - (a + A - 1)! A} \in ℝ^{+}$
34	1 32 33	sylancr	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{((a + A) - 1 + 1)! - (a + A - 1)! A} \in ℝ^{+}$
35	34	rpred	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{((a + A) - 1 + 1)! - (a + A - 1)! A} \in ℝ$
36		simprr	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{2}{B} < 2^{a}$
37	17 20 36	ltled	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{2}{B} \leq 2^{a}$
38	5	a1i	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2 \in ℝ$
39		1le2	$⊢ 1 \leq 2$
40	39	a1i	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 1 \leq 2$
41	11	nnred	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a \in ℝ$
42	28	nnred	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A - 1)! \in ℝ$
43	18	nn0ge0d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 0 \leq a$
44	28	nnge1d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 1 \leq (a + A - 1)!$
45	41 42 43 44	lemulge12d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a \leq (a + A - 1)! a$
46		facp1	$⊢ a + A - 1 \in ℕ_{0} \to ((a + A) - 1 + 1)! = (a + A - 1)! ((a + A) - 1 + 1)$
47	23 46	syl	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to ((a + A) - 1 + 1)! = (a + A - 1)! ((a + A) - 1 + 1)$
48	47	oveq1d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to ((a + A) - 1 + 1)! - (a + A - 1)! A = (a + A - 1)! ((a + A) - 1 + 1) - (a + A - 1)! A$
49	28	nncnd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A - 1)! \in ℂ$
50	25	nn0cnd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A) - 1 + 1 \in ℂ$
51	12	nncnd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to A \in ℂ$
52	49 50 51	subdid	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A - 1)! ((a + A - 1) + 1 - A) = (a + A - 1)! ((a + A) - 1 + 1) - (a + A - 1)! A$
53	11	nncnd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a \in ℂ$
54	21	nncnd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a + A \in ℂ$
55		1cnd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 1 \in ℂ$
56	54 55	npcand	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A) - 1 + 1 = a + A$
57	53 51 56	mvrraddd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A - 1) + 1 - A = a$
58	57	oveq2d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A - 1)! ((a + A - 1) + 1 - A) = (a + A - 1)! a$
59	48 52 58	3eqtr2d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to ((a + A) - 1 + 1)! - (a + A - 1)! A = (a + A - 1)! a$
60	45 59	breqtrrd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a \leq ((a + A) - 1 + 1)! - (a + A - 1)! A$
61	11	nnzd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to a \in ℤ$
62		eluz	$⊢ (a \in ℤ \land ((a + A) - 1 + 1)! - (a + A - 1)! A \in ℤ) \to (((a + A) - 1 + 1)! - (a + A - 1)! A \in ℤ_{\geq a} \leftrightarrow a \leq ((a + A) - 1 + 1)! - (a + A - 1)! A)$
63	61 32 62	syl2anc	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (((a + A) - 1 + 1)! - (a + A - 1)! A \in ℤ_{\geq a} \leftrightarrow a \leq ((a + A) - 1 + 1)! - (a + A - 1)! A)$
64	60 63	mpbird	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to ((a + A) - 1 + 1)! - (a + A - 1)! A \in ℤ_{\geq a}$
65	38 40 64	leexp2ad	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{a} \leq 2^{((a + A) - 1 + 1)! - (a + A - 1)! A}$
66	17 20 35 37 65	letrd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{2}{B} \leq 2^{((a + A) - 1 + 1)! - (a + A - 1)! A}$
67		rpcnne0	$⊢ 2 \in ℝ^{+} \to (2 \in ℂ \land 2 \neq 0)$
68	1 67	mp1i	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (2 \in ℂ \land 2 \neq 0)$
69		expsub	$⊢ ((2 \in ℂ \land 2 \neq 0) \land (((a + A) - 1 + 1)! \in ℤ \land (a + A - 1)! A \in ℤ)) \to 2^{((a + A) - 1 + 1)! - (a + A - 1)! A} = \frac{2^{((a + A) - 1 + 1)!}}{2^{(a + A - 1)! A}}$
70	68 27 31 69	syl12anc	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{((a + A) - 1 + 1)! - (a + A - 1)! A} = \frac{2^{((a + A) - 1 + 1)!}}{2^{(a + A - 1)! A}}$
71		2cn	$⊢ 2 \in ℂ$
72	71	a1i	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2 \in ℂ$
73	12	nnnn0d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to A \in ℕ_{0}$
74	28	nnnn0d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (a + A - 1)! \in ℕ_{0}$
75	72 73 74	expmuld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{(a + A - 1)! A} = {(2^{(a + A - 1)!})}^{A}$
76	75	oveq2d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{2^{((a + A) - 1 + 1)!}}{2^{(a + A - 1)! A}} = \frac{2^{((a + A) - 1 + 1)!}}{{(2^{(a + A - 1)!})}^{A}}$
77		rpexpcl	$⊢ (2 \in ℝ^{+} \land ((a + A) - 1 + 1)! \in ℤ) \to 2^{((a + A) - 1 + 1)!} \in ℝ^{+}$
78	1 27 77	sylancr	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{((a + A) - 1 + 1)!} \in ℝ^{+}$
79	78	rpcnd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{((a + A) - 1 + 1)!} \in ℂ$
80		rpexpcl	$⊢ (2 \in ℝ^{+} \land (a + A - 1)! \in ℤ) \to 2^{(a + A - 1)!} \in ℝ^{+}$
81	1 29 80	sylancr	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{(a + A - 1)!} \in ℝ^{+}$
82	81 30	rpexpcld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to {(2^{(a + A - 1)!})}^{A} \in ℝ^{+}$
83	82	rpcnd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to {(2^{(a + A - 1)!})}^{A} \in ℂ$
84	82	rpne0d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to {(2^{(a + A - 1)!})}^{A} \neq 0$
85	79 83 84	divrecd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{2^{((a + A) - 1 + 1)!}}{{(2^{(a + A - 1)!})}^{A}} = 2^{((a + A) - 1 + 1)!} (\frac{1}{{(2^{(a + A - 1)!})}^{A}})$
86	70 76 85	3eqtrrd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{((a + A) - 1 + 1)!} (\frac{1}{{(2^{(a + A - 1)!})}^{A}}) = 2^{((a + A) - 1 + 1)! - (a + A - 1)! A}$
87	66 86	breqtrrd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{2}{B} \leq 2^{((a + A) - 1 + 1)!} (\frac{1}{{(2^{(a + A - 1)!})}^{A}})$
88	82	rpreccld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{1}{{(2^{(a + A - 1)!})}^{A}} \in ℝ^{+}$
89	78 88	rpmulcld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{((a + A) - 1 + 1)!} (\frac{1}{{(2^{(a + A - 1)!})}^{A}}) \in ℝ^{+}$
90	89	rpred	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{((a + A) - 1 + 1)!} (\frac{1}{{(2^{(a + A - 1)!})}^{A}}) \in ℝ$
91	38 90 15	ledivmuld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (\frac{2}{B} \leq 2^{((a + A) - 1 + 1)!} (\frac{1}{{(2^{(a + A - 1)!})}^{A}}) \leftrightarrow 2 \leq B 2^{((a + A) - 1 + 1)!} (\frac{1}{{(2^{(a + A - 1)!})}^{A}}))$
92	87 91	mpbid	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2 \leq B 2^{((a + A) - 1 + 1)!} (\frac{1}{{(2^{(a + A - 1)!})}^{A}})$
93	15	rpcnd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to B \in ℂ$
94	88	rpcnd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{1}{{(2^{(a + A - 1)!})}^{A}} \in ℂ$
95	93 79 94	mul12d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to B 2^{((a + A) - 1 + 1)!} (\frac{1}{{(2^{(a + A - 1)!})}^{A}}) = 2^{((a + A) - 1 + 1)!} B (\frac{1}{{(2^{(a + A - 1)!})}^{A}})$
96	92 95	breqtrd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2 \leq 2^{((a + A) - 1 + 1)!} B (\frac{1}{{(2^{(a + A - 1)!})}^{A}})$
97	15 88	rpmulcld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to B (\frac{1}{{(2^{(a + A - 1)!})}^{A}}) \in ℝ^{+}$
98	97	rpred	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to B (\frac{1}{{(2^{(a + A - 1)!})}^{A}}) \in ℝ$
99	38 98 78	ledivmuld	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to (\frac{2}{2^{((a + A) - 1 + 1)!}} \leq B (\frac{1}{{(2^{(a + A - 1)!})}^{A}}) \leftrightarrow 2 \leq 2^{((a + A) - 1 + 1)!} B (\frac{1}{{(2^{(a + A - 1)!})}^{A}}))$
100	96 99	mpbird	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{2}{2^{((a + A) - 1 + 1)!}} \leq B (\frac{1}{{(2^{(a + A - 1)!})}^{A}})$
101	26	nnnn0d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to ((a + A) - 1 + 1)! \in ℕ_{0}$
102		expneg	$⊢ (2 \in ℂ \land ((a + A) - 1 + 1)! \in ℕ_{0}) \to 2^{- ((a + A) - 1 + 1)!} = \frac{1}{2^{((a + A) - 1 + 1)!}}$
103	71 101 102	sylancr	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{- ((a + A) - 1 + 1)!} = \frac{1}{2^{((a + A) - 1 + 1)!}}$
104	103	oveq2d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2 2^{- ((a + A) - 1 + 1)!} = 2 (\frac{1}{2^{((a + A) - 1 + 1)!}})$
105	78	rpne0d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2^{((a + A) - 1 + 1)!} \neq 0$
106	72 79 105	divrecd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{2}{2^{((a + A) - 1 + 1)!}} = 2 (\frac{1}{2^{((a + A) - 1 + 1)!}})$
107	104 106	eqtr4d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2 2^{- ((a + A) - 1 + 1)!} = \frac{2}{2^{((a + A) - 1 + 1)!}}$
108	93 83 84	divrecd	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \frac{B}{{(2^{(a + A - 1)!})}^{A}} = B (\frac{1}{{(2^{(a + A - 1)!})}^{A}})$
109	100 107 108	3brtr4d	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to 2 2^{- ((a + A) - 1 + 1)!} \leq \frac{B}{{(2^{(a + A - 1)!})}^{A}}$
110		fvoveq1	$⊢ x = a + A - 1 \to (x + 1)! = ((a + A) - 1 + 1)!$
111	110	negeqd	$⊢ x = a + A - 1 \to - (x + 1)! = - ((a + A) - 1 + 1)!$
112	111	oveq2d	$⊢ x = a + A - 1 \to 2^{- (x + 1)!} = 2^{- ((a + A) - 1 + 1)!}$
113	112	oveq2d	$⊢ x = a + A - 1 \to 2 2^{- (x + 1)!} = 2 2^{- ((a + A) - 1 + 1)!}$
114		fveq2	$⊢ x = a + A - 1 \to x! = (a + A - 1)!$
115	114	oveq2d	$⊢ x = a + A - 1 \to 2^{x!} = 2^{(a + A - 1)!}$
116	115	oveq1d	$⊢ x = a + A - 1 \to {(2^{x!})}^{A} = {(2^{(a + A - 1)!})}^{A}$
117	116	oveq2d	$⊢ x = a + A - 1 \to \frac{B}{{(2^{x!})}^{A}} = \frac{B}{{(2^{(a + A - 1)!})}^{A}}$
118	113 117	breq12d	$⊢ x = a + A - 1 \to (2 2^{- (x + 1)!} \leq \frac{B}{{(2^{x!})}^{A}} \leftrightarrow 2 2^{- ((a + A) - 1 + 1)!} \leq \frac{B}{{(2^{(a + A - 1)!})}^{A}})$
119	118	rspcev	$⊢ (a + A - 1 \in ℕ \land 2 2^{- ((a + A) - 1 + 1)!} \leq \frac{B}{{(2^{(a + A - 1)!})}^{A}}) \to \exists x \in ℕ 2 2^{- (x + 1)!} \leq \frac{B}{{(2^{x!})}^{A}}$
120	14 109 119	syl2anc	$⊢ ((A \in ℕ \land B \in ℝ^{+}) \land (a \in ℕ \land \frac{2}{B} < 2^{a})) \to \exists x \in ℕ 2 2^{- (x + 1)!} \leq \frac{B}{{(2^{x!})}^{A}}$
121	10 120	rexlimddv	$⊢ (A \in ℕ \land B \in ℝ^{+}) \to \exists x \in ℕ 2 2^{- (x + 1)!} \leq \frac{B}{{(2^{x!})}^{A}}$

Metamath Proof Explorer

Theorem aaliou3lem8

Proof