Theorem aaliou3lem8

Description: Lemma for aaliou3 . (Contributed by Stefan O'Rear, 20-Nov-2014)

	Ref	Expression
Assertion	aaliou3lem8	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℕ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝐵 / ( ( 2 ↑ ( ! ‘ 𝑥 ) ) ↑ 𝐴 ) ) )

Proof

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