Metamath Proof Explorer

Theorem aaliou3lem7

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

Ref Expression
Hypotheses aaliou3lem.c ⊢F=a∈ℕ⟼2−a!
aaliou3lem.d ⊢L=∑b∈ℕF⁡b
aaliou3lem.e ⊢H=c∈ℕ⟼∑b=1cF⁡b
Assertion aaliou3lem7 ⊢A∈ℕ→H⁡A≠L∧L−H⁡A≤2⁢2−A+1!

Proof

Step Hyp Ref Expression
1 aaliou3lem.c ⊢F=a∈ℕ⟼2−a!
2 aaliou3lem.d ⊢L=∑b∈ℕF⁡b
3 aaliou3lem.e ⊢H=c∈ℕ⟼∑b=1cF⁡b
4 peano2nn ⊢A∈ℕ→A+1∈ℕ
5 eqid ⊢c∈ℤ≥A+1⟼2−A+1!⁢12c−A+1=c∈ℤ≥A+1⟼2−A+1!⁢12c−A+1
6 5 1 aaliou3lem3 ⊢A+1∈ℕ→seqA+1+F∈dom⁡⇝∧∑b∈ℤ≥A+1F⁡b∈ℝ+∧∑b∈ℤ≥A+1F⁡b≤2⁢2−A+1!
7 3simpc ⊢seqA+1+F∈dom⁡⇝∧∑b∈ℤ≥A+1F⁡b∈ℝ+∧∑b∈ℤ≥A+1F⁡b≤2⁢2−A+1!→∑b∈ℤ≥A+1F⁡b∈ℝ+∧∑b∈ℤ≥A+1F⁡b≤2⁢2−A+1!
8 4 6 7 3syl ⊢A∈ℕ→∑b∈ℤ≥A+1F⁡b∈ℝ+∧∑b∈ℤ≥A+1F⁡b≤2⁢2−A+1!
9 nncn ⊢A∈ℕ→A∈ℂ
10 ax-1cn ⊢1∈ℂ
11 pncan ⊢A∈ℂ∧1∈ℂ→A+1-1=A
12 9 10 11 sylancl ⊢A∈ℕ→A+1-1=A
13 12 oveq2d ⊢A∈ℕ→1…A+1-1=1…A
14 13 sumeq1d ⊢A∈ℕ→∑b=1A+1-1F⁡b=∑b=1AF⁡b
15 14 oveq1d ⊢A∈ℕ→∑b=1A+1-1F⁡b+∑b∈ℤ≥A+1F⁡b=∑b=1AF⁡b+∑b∈ℤ≥A+1F⁡b
16 nnuz ⊢ℕ=ℤ≥1
17 eqid ⊢ℤ≥A+1=ℤ≥A+1
18 eqidd ⊢A∈ℕ∧b∈ℕ→F⁡b=F⁡b
19 fveq2 ⊢a=b→a!=b!
20 19 negeqd ⊢a=b→−a!=−b!
21 20 oveq2d ⊢a=b→2−a!=2−b!
22 ovex ⊢2−b!∈V
23 21 1 22 fvmpt ⊢b∈ℕ→F⁡b=2−b!
24 2rp ⊢2∈ℝ+
25 nnnn0 ⊢b∈ℕ→b∈ℕ0
26 faccl ⊢b∈ℕ0→b!∈ℕ
27 25 26 syl ⊢b∈ℕ→b!∈ℕ
28 27 nnzd ⊢b∈ℕ→b!∈ℤ
29 28 znegcld ⊢b∈ℕ→−b!∈ℤ
30 rpexpcl ⊢2∈ℝ+∧−b!∈ℤ→2−b!∈ℝ+
31 24 29 30 sylancr ⊢b∈ℕ→2−b!∈ℝ+
32 31 rpcnd ⊢b∈ℕ→2−b!∈ℂ
33 23 32 eqeltrd ⊢b∈ℕ→F⁡b∈ℂ
34 33 adantl ⊢A∈ℕ∧b∈ℕ→F⁡b∈ℂ
35 1nn ⊢1∈ℕ
36 eqid ⊢c∈ℤ≥1⟼2−1!⁢12c−1=c∈ℤ≥1⟼2−1!⁢12c−1
37 36 1 aaliou3lem3 ⊢1∈ℕ→seq1+F∈dom⁡⇝∧∑b∈ℤ≥1F⁡b∈ℝ+∧∑b∈ℤ≥1F⁡b≤2⁢2−1!
38 37 simp1d ⊢1∈ℕ→seq1+F∈dom⁡⇝
39 35 38 mp1i ⊢A∈ℕ→seq1+F∈dom⁡⇝
40 16 17 4 18 34 39 isumsplit ⊢A∈ℕ→∑b∈ℕF⁡b=∑b=1A+1-1F⁡b+∑b∈ℤ≥A+1F⁡b
41 oveq2 ⊢c=A→1…c=1…A
42 41 sumeq1d ⊢c=A→∑b=1cF⁡b=∑b=1AF⁡b
43 sumex ⊢∑b=1AF⁡b∈V
44 42 3 43 fvmpt ⊢A∈ℕ→H⁡A=∑b=1AF⁡b
45 44 oveq1d ⊢A∈ℕ→H⁡A+∑b∈ℤ≥A+1F⁡b=∑b=1AF⁡b+∑b∈ℤ≥A+1F⁡b
46 15 40 45 3eqtr4rd ⊢A∈ℕ→H⁡A+∑b∈ℤ≥A+1F⁡b=∑b∈ℕF⁡b
47 46 2 eqtr4di ⊢A∈ℕ→H⁡A+∑b∈ℤ≥A+1F⁡b=L
48 1 2 3 aaliou3lem4 ⊢L∈ℝ
49 48 recni ⊢L∈ℂ
50 49 a1i ⊢A∈ℕ→L∈ℂ
51 1 2 3 aaliou3lem5 ⊢A∈ℕ→H⁡A∈ℝ
52 51 recnd ⊢A∈ℕ→H⁡A∈ℂ
53 6 simp2d ⊢A+1∈ℕ→∑b∈ℤ≥A+1F⁡b∈ℝ+
54 4 53 syl ⊢A∈ℕ→∑b∈ℤ≥A+1F⁡b∈ℝ+
55 54 rpcnd ⊢A∈ℕ→∑b∈ℤ≥A+1F⁡b∈ℂ
56 50 52 55 subaddd ⊢A∈ℕ→L−H⁡A=∑b∈ℤ≥A+1F⁡b↔H⁡A+∑b∈ℤ≥A+1F⁡b=L
57 47 56 mpbird ⊢A∈ℕ→L−H⁡A=∑b∈ℤ≥A+1F⁡b
58 57 eqcomd ⊢A∈ℕ→∑b∈ℤ≥A+1F⁡b=L−H⁡A
59 eleq1 ⊢∑b∈ℤ≥A+1F⁡b=L−H⁡A→∑b∈ℤ≥A+1F⁡b∈ℝ+↔L−H⁡A∈ℝ+
60 breq1 ⊢∑b∈ℤ≥A+1F⁡b=L−H⁡A→∑b∈ℤ≥A+1F⁡b≤2⁢2−A+1!↔L−H⁡A≤2⁢2−A+1!
61 59 60 anbi12d ⊢∑b∈ℤ≥A+1F⁡b=L−H⁡A→∑b∈ℤ≥A+1F⁡b∈ℝ+∧∑b∈ℤ≥A+1F⁡b≤2⁢2−A+1!↔L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!
62 58 61 syl ⊢A∈ℕ→∑b∈ℤ≥A+1F⁡b∈ℝ+∧∑b∈ℤ≥A+1F⁡b≤2⁢2−A+1!↔L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!
63 51 adantr ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→H⁡A∈ℝ
64 simprl ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→L−H⁡A∈ℝ+
65 difrp ⊢H⁡A∈ℝ∧L∈ℝ→H⁡A<L↔L−H⁡A∈ℝ+
66 63 48 65 sylancl ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→H⁡A<L↔L−H⁡A∈ℝ+
67 64 66 mpbird ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→H⁡A<L
68 63 67 ltned ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→H⁡A≠L
69 nnnn0 ⊢A+1∈ℕ→A+1∈ℕ0
70 faccl ⊢A+1∈ℕ0→A+1!∈ℕ
71 4 69 70 3syl ⊢A∈ℕ→A+1!∈ℕ
72 71 nnzd ⊢A∈ℕ→A+1!∈ℤ
73 72 znegcld ⊢A∈ℕ→−A+1!∈ℤ
74 rpexpcl ⊢2∈ℝ+∧−A+1!∈ℤ→2−A+1!∈ℝ+
75 24 73 74 sylancr ⊢A∈ℕ→2−A+1!∈ℝ+
76 rpmulcl ⊢2∈ℝ+∧2−A+1!∈ℝ+→2⁢2−A+1!∈ℝ+
77 24 75 76 sylancr ⊢A∈ℕ→2⁢2−A+1!∈ℝ+
78 77 adantr ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→2⁢2−A+1!∈ℝ+
79 78 rpred ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→2⁢2−A+1!∈ℝ
80 63 79 resubcld ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→H⁡A−2⁢2−A+1!∈ℝ
81 48 a1i ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→L∈ℝ
82 63 78 ltsubrpd ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→H⁡A−2⁢2−A+1!<H⁡A
83 80 63 81 82 67 lttrd ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→H⁡A−2⁢2−A+1!<L
84 80 81 83 ltled ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→H⁡A−2⁢2−A+1!≤L
85 simprr ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→L−H⁡A≤2⁢2−A+1!
86 81 63 79 lesubadd2d ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→L−H⁡A≤2⁢2−A+1!↔L≤H⁡A+2⁢2−A+1!
87 85 86 mpbid ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→L≤H⁡A+2⁢2−A+1!
88 81 63 79 absdifled ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→L−H⁡A≤2⁢2−A+1!↔H⁡A−2⁢2−A+1!≤L∧L≤H⁡A+2⁢2−A+1!
89 84 87 88 mpbir2and ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→L−H⁡A≤2⁢2−A+1!
90 68 89 jca ⊢A∈ℕ∧L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→H⁡A≠L∧L−H⁡A≤2⁢2−A+1!
91 90 ex ⊢A∈ℕ→L−H⁡A∈ℝ+∧L−H⁡A≤2⁢2−A+1!→H⁡A≠L∧L−H⁡A≤2⁢2−A+1!
92 62 91 sylbid ⊢A∈ℕ→∑b∈ℤ≥A+1F⁡b∈ℝ+∧∑b∈ℤ≥A+1F⁡b≤2⁢2−A+1!→H⁡A≠L∧L−H⁡A≤2⁢2−A+1!
93 8 92 mpd ⊢A∈ℕ→H⁡A≠L∧L−H⁡A≤2⁢2−A+1!