Metamath Proof Explorer

Theorem aaliou3lem8

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

Ref Expression
Assertion aaliou3lem8 ⊢A∈ℕ∧B∈ℝ+→∃x∈ℕ2⁢2−x+1!≤B2x!A

Proof

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