Theorem eirrlem

Description: Lemma for eirr . (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 29-Apr-2014)

	Ref	Expression
Hypotheses	eirr.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{1}{n!}\right)$$
	eirr.2	$$⊢\phi \to P\in \mathbb{Z}$$
	eirr.3	$$⊢\phi \to Q\in \mathbb{N}$$
	eirr.4	$$⊢\phi \to \mathrm{e}=\frac{P}{Q}$$
Assertion	eirrlem	$$⊢\neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		eirr.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{1}{n!}\right)$$
2		eirr.2	$$⊢\phi \to P\in \mathbb{Z}$$
3		eirr.3	$$⊢\phi \to Q\in \mathbb{N}$$
4		eirr.4	$$⊢\phi \to \mathrm{e}=\frac{P}{Q}$$
5		fzfid	$$⊢\phi \to \left(0\dots Q\right)\in \mathrm{Fin}$$
6		elfznn0	$$⊢k\in \left(0\dots Q\right)\to k\in {\mathbb{N}}_0$$
7		nn0z	$$⊢n\in {\mathbb{N}}_0\to n\in \mathbb{Z}$$
8		1exp	$$⊢n\in \mathbb{Z}\to 1^n=1$$
9	7 8	syl	$$⊢n\in {\mathbb{N}}_0\to 1^n=1$$
10	9	oveq1d	$$⊢n\in {\mathbb{N}}_0\to \frac{1^n}{n!}=\frac{1}{n!}$$
11	10	mpteq2ia	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{1^n}{n!}\right)=\left(n\in {\mathbb{N}}_0⟼\frac{1}{n!}\right)$$
12	1 11	eqtr4i	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{1^n}{n!}\right)$$
13	12	eftval	$$⊢k\in {\mathbb{N}}_0\to F\left(k\right)=\frac{1^k}{k!}$$
14	13	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)=\frac{1^k}{k!}$$
15		ax-1cn	$$⊢1\in ℂ$$
16	15	a1i	$$⊢\phi \to 1\in ℂ$$
17		eftcl	$$⊢\left(1\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \frac{1^k}{k!}\in ℂ$$
18	16 17	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \frac{1^k}{k!}\in ℂ$$
19	14 18	eqeltrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)\in ℂ$$
20	6 19	sylan2	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to F\left(k\right)\in ℂ$$
21	5 20	fsumcl	$$⊢\phi \to \sum _{k=0}^{Q}F\left(k\right)\in ℂ$$
22		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
23		eqid	$$⊢{\mathbb{Z}}_{\ge \left(Q+1\right)}={\mathbb{Z}}_{\ge \left(Q+1\right)}$$
24	3	peano2nnd	$$⊢\phi \to Q+1\in \mathbb{N}$$
25	24	nnnn0d	$$⊢\phi \to Q+1\in {\mathbb{N}}_0$$
26		eqidd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)=F\left(k\right)$$
27		fveq2	$$⊢n=k\to n!=k!$$
28	27	oveq2d	$$⊢n=k\to \frac{1}{n!}=\frac{1}{k!}$$
29		ovex	$$⊢\frac{1}{k!}\in \mathrm{V}$$
30	28 1 29	fvmpt	$$⊢k\in {\mathbb{N}}_0\to F\left(k\right)=\frac{1}{k!}$$
31	30	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)=\frac{1}{k!}$$
32		faccl	$$⊢k\in {\mathbb{N}}_0\to k!\in \mathbb{N}$$
33	32	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k!\in \mathbb{N}$$
34	33	nnrpd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k!\in {ℝ}^{+}$$
35	34	rpreccld	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \frac{1}{k!}\in {ℝ}^{+}$$
36	31 35	eqeltrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)\in {ℝ}^{+}$$
37	12	efcllem	$$⊢1\in ℂ\to seq0\left(+,F\right)\in \mathrm{dom}⇝$$
38	16 37	syl	$$⊢\phi \to seq0\left(+,F\right)\in \mathrm{dom}⇝$$
39	22 23 25 26 36 38	isumrpcl	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\in {ℝ}^{+}$$
40	39	rpred	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\in ℝ$$
41	40	recnd	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\in ℂ$$
42		esum	$$⊢\mathrm{e}=\sum _{k\in {\mathbb{N}}_0}\left(\frac{1}{k!}\right)$$
43	30	sumeq2i	$$⊢\sum _{k\in {\mathbb{N}}_0}F\left(k\right)=\sum _{k\in {\mathbb{N}}_0}\left(\frac{1}{k!}\right)$$
44	42 43	eqtr4i	$$⊢\mathrm{e}=\sum _{k\in {\mathbb{N}}_0}F\left(k\right)$$
45	22 23 25 26 19 38	isumsplit	$$⊢\phi \to \sum _{k\in {\mathbb{N}}_0}F\left(k\right)=\sum _{k=0}^{Q+1-1}F\left(k\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)$$
46	44 45	eqtrid	$$⊢\phi \to \mathrm{e}=\sum _{k=0}^{Q+1-1}F\left(k\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)$$
47	3	nncnd	$$⊢\phi \to Q\in ℂ$$
48		pncan	$$⊢\left(Q\in ℂ\wedge 1\in ℂ\right)\to Q+1-1=Q$$
49	47 15 48	sylancl	$$⊢\phi \to Q+1-1=Q$$
50	49	oveq2d	$$⊢\phi \to \left(0\dots Q+1-1\right)=\left(0\dots Q\right)$$
51	50	sumeq1d	$$⊢\phi \to \sum _{k=0}^{Q+1-1}F\left(k\right)=\sum _{k=0}^{Q}F\left(k\right)$$
52	51	oveq1d	$$⊢\phi \to \sum _{k=0}^{Q+1-1}F\left(k\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)=\sum _{k=0}^{Q}F\left(k\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)$$
53	46 52	eqtrd	$$⊢\phi \to \mathrm{e}=\sum _{k=0}^{Q}F\left(k\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)$$
54	21 41 53	mvrladdd	$$⊢\phi \to \mathrm{e}-\sum _{k=0}^{Q}F\left(k\right)=\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)$$
55	54	oveq2d	$$⊢\phi \to Q!\left(\mathrm{e}-\sum _{k=0}^{Q}F\left(k\right)\right)=Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)$$
56	3	nnnn0d	$$⊢\phi \to Q\in {\mathbb{N}}_0$$
57	56	faccld	$$⊢\phi \to Q!\in \mathbb{N}$$
58	57	nncnd	$$⊢\phi \to Q!\in ℂ$$
59		ere	$$⊢\mathrm{e}\in ℝ$$
60	59	recni	$$⊢\mathrm{e}\in ℂ$$
61	60	a1i	$$⊢\phi \to \mathrm{e}\in ℂ$$
62	58 61 21	subdid	$$⊢\phi \to Q!\left(\mathrm{e}-\sum _{k=0}^{Q}F\left(k\right)\right)=Q!\mathrm{e}-Q!\sum _{k=0}^{Q}F\left(k\right)$$
63	55 62	eqtr3d	$$⊢\phi \to Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)=Q!\mathrm{e}-Q!\sum _{k=0}^{Q}F\left(k\right)$$
64	4	oveq2d	$$⊢\phi \to Q!\mathrm{e}=Q!\left(\frac{P}{Q}\right)$$
65	2	zcnd	$$⊢\phi \to P\in ℂ$$
66	3	nnne0d	$$⊢\phi \to Q\ne 0$$
67	58 65 47 66	div12d	$$⊢\phi \to Q!\left(\frac{P}{Q}\right)=P\left(\frac{Q!}{Q}\right)$$
68	64 67	eqtrd	$$⊢\phi \to Q!\mathrm{e}=P\left(\frac{Q!}{Q}\right)$$
69	3	nnred	$$⊢\phi \to Q\in ℝ$$
70	69	leidd	$$⊢\phi \to Q\le Q$$
71		facdiv	$$⊢\left(Q\in {\mathbb{N}}_0\wedge Q\in \mathbb{N}\wedge Q\le Q\right)\to \frac{Q!}{Q}\in \mathbb{N}$$
72	56 3 70 71	syl3anc	$$⊢\phi \to \frac{Q!}{Q}\in \mathbb{N}$$
73	72	nnzd	$$⊢\phi \to \frac{Q!}{Q}\in \mathbb{Z}$$
74	2 73	zmulcld	$$⊢\phi \to P\left(\frac{Q!}{Q}\right)\in \mathbb{Z}$$
75	68 74	eqeltrd	$$⊢\phi \to Q!\mathrm{e}\in \mathbb{Z}$$
76	5 58 20	fsummulc2	$$⊢\phi \to Q!\sum _{k=0}^{Q}F\left(k\right)=\sum _{k=0}^{Q}Q!F\left(k\right)$$
77	6	adantl	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to k\in {\mathbb{N}}_0$$
78	77 30	syl	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to F\left(k\right)=\frac{1}{k!}$$
79	78	oveq2d	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to Q!F\left(k\right)=Q!\left(\frac{1}{k!}\right)$$
80	58	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to Q!\in ℂ$$
81	6 33	sylan2	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to k!\in \mathbb{N}$$
82	81	nncnd	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to k!\in ℂ$$
83		facne0	$$⊢k\in {\mathbb{N}}_0\to k!\ne 0$$
84	77 83	syl	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to k!\ne 0$$
85	80 82 84	divrecd	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to \frac{Q!}{k!}=Q!\left(\frac{1}{k!}\right)$$
86	79 85	eqtr4d	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to Q!F\left(k\right)=\frac{Q!}{k!}$$
87		permnn	$$⊢k\in \left(0\dots Q\right)\to \frac{Q!}{k!}\in \mathbb{N}$$
88	87	adantl	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to \frac{Q!}{k!}\in \mathbb{N}$$
89	86 88	eqeltrd	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to Q!F\left(k\right)\in \mathbb{N}$$
90	89	nnzd	$$⊢\left(\phi \wedge k\in \left(0\dots Q\right)\right)\to Q!F\left(k\right)\in \mathbb{Z}$$
91	5 90	fsumzcl	$$⊢\phi \to \sum _{k=0}^{Q}Q!F\left(k\right)\in \mathbb{Z}$$
92	76 91	eqeltrd	$$⊢\phi \to Q!\sum _{k=0}^{Q}F\left(k\right)\in \mathbb{Z}$$
93	75 92	zsubcld	$$⊢\phi \to Q!\mathrm{e}-Q!\sum _{k=0}^{Q}F\left(k\right)\in \mathbb{Z}$$
94	63 93	eqeltrd	$$⊢\phi \to Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\in \mathbb{Z}$$
95		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
96	57	nnrpd	$$⊢\phi \to Q!\in {ℝ}^{+}$$
97	96 39	rpmulcld	$$⊢\phi \to Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\in {ℝ}^{+}$$
98	97	rpgt0d	$$⊢\phi \to 0<Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)$$
99	24	peano2nnd	$$⊢\phi \to Q+1+1\in \mathbb{N}$$
100	99	nnred	$$⊢\phi \to Q+1+1\in ℝ$$
101	25	faccld	$$⊢\phi \to \left(Q+1\right)!\in \mathbb{N}$$
102	101 24	nnmulcld	$$⊢\phi \to \left(Q+1\right)!\left(Q+1\right)\in \mathbb{N}$$
103	100 102	nndivred	$$⊢\phi \to \frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}\in ℝ$$
104	57	nnrecred	$$⊢\phi \to \frac{1}{Q!}\in ℝ$$
105		abs1	$$⊢\left|1\right|=1$$
106	105	oveq1i	$$⊢{\left|1\right|}^n=1^n$$
107	106	oveq1i	$$⊢\frac{{\left|1\right|}^n}{n!}=\frac{1^n}{n!}$$
108	107	mpteq2i	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{{\left|1\right|}^n}{n!}\right)=\left(n\in {\mathbb{N}}_0⟼\frac{1^n}{n!}\right)$$
109	12 108	eqtr4i	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{{\left|1\right|}^n}{n!}\right)$$
110		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\left(\frac{{\left|1\right|}^{Q+1}}{\left(Q+1\right)!}\right){\left(\frac{1}{Q+1+1}\right)}^n\right)=\left(n\in {\mathbb{N}}_0⟼\left(\frac{{\left|1\right|}^{Q+1}}{\left(Q+1\right)!}\right){\left(\frac{1}{Q+1+1}\right)}^n\right)$$
111		1le1	$$⊢1\le 1$$
112	105 111	eqbrtri	$$⊢\left|1\right|\le 1$$
113	112	a1i	$$⊢\phi \to \left|1\right|\le 1$$
114	12 109 110 24 16 113	eftlub	$$⊢\phi \to \left|\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\right|\le {\left|1\right|}^{Q+1}\left(\frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}\right)$$
115	39	rprege0d	$$⊢\phi \to \left(\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\in ℝ\wedge 0\le \sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\right)$$
116		absid	$$⊢\left(\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\in ℝ\wedge 0\le \sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\right)\to \left|\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\right|=\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)$$
117	115 116	syl	$$⊢\phi \to \left|\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\right|=\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)$$
118	105	oveq1i	$$⊢{\left|1\right|}^{Q+1}=1^{Q+1}$$
119	24	nnzd	$$⊢\phi \to Q+1\in \mathbb{Z}$$
120		1exp	$$⊢Q+1\in \mathbb{Z}\to 1^{Q+1}=1$$
121	119 120	syl	$$⊢\phi \to 1^{Q+1}=1$$
122	118 121	eqtrid	$$⊢\phi \to {\left|1\right|}^{Q+1}=1$$
123	122	oveq1d	$$⊢\phi \to {\left|1\right|}^{Q+1}\left(\frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}\right)=1\left(\frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}\right)$$
124	103	recnd	$$⊢\phi \to \frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}\in ℂ$$
125	124	mullidd	$$⊢\phi \to 1\left(\frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}\right)=\frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}$$
126	123 125	eqtrd	$$⊢\phi \to {\left|1\right|}^{Q+1}\left(\frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}\right)=\frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}$$
127	114 117 126	3brtr3d	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\le \frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}$$
128	24	nnred	$$⊢\phi \to Q+1\in ℝ$$
129	128 128	readdcld	$$⊢\phi \to Q+1+Q+1\in ℝ$$
130	128 128	remulcld	$$⊢\phi \to \left(Q+1\right)\left(Q+1\right)\in ℝ$$
131		1red	$$⊢\phi \to 1\in ℝ$$
132	3	nnge1d	$$⊢\phi \to 1\le Q$$
133		1nn	$$⊢1\in \mathbb{N}$$
134		nnleltp1	$$⊢\left(1\in \mathbb{N}\wedge Q\in \mathbb{N}\right)\to \left(1\le Q\leftrightarrow 1<Q+1\right)$$
135	133 3 134	sylancr	$$⊢\phi \to \left(1\le Q\leftrightarrow 1<Q+1\right)$$
136	132 135	mpbid	$$⊢\phi \to 1<Q+1$$
137	131 128 128 136	ltadd2dd	$$⊢\phi \to Q+1+1<Q+1+Q+1$$
138	24	nncnd	$$⊢\phi \to Q+1\in ℂ$$
139	138	2timesd	$$⊢\phi \to 2\left(Q+1\right)=Q+1+Q+1$$
140		df-2	$$⊢2=1+1$$
141	131 69 131 132	leadd1dd	$$⊢\phi \to 1+1\le Q+1$$
142	140 141	eqbrtrid	$$⊢\phi \to 2\le Q+1$$
143		2re	$$⊢2\in ℝ$$
144	143	a1i	$$⊢\phi \to 2\in ℝ$$
145	24	nngt0d	$$⊢\phi \to 0<Q+1$$
146		lemul1	$$⊢\left(2\in ℝ\wedge Q+1\in ℝ\wedge \left(Q+1\in ℝ\wedge 0<Q+1\right)\right)\to \left(2\le Q+1\leftrightarrow 2\left(Q+1\right)\le \left(Q+1\right)\left(Q+1\right)\right)$$
147	144 128 128 145 146	syl112anc	$$⊢\phi \to \left(2\le Q+1\leftrightarrow 2\left(Q+1\right)\le \left(Q+1\right)\left(Q+1\right)\right)$$
148	142 147	mpbid	$$⊢\phi \to 2\left(Q+1\right)\le \left(Q+1\right)\left(Q+1\right)$$
149	139 148	eqbrtrrd	$$⊢\phi \to Q+1+Q+1\le \left(Q+1\right)\left(Q+1\right)$$
150	100 129 130 137 149	ltletrd	$$⊢\phi \to Q+1+1<\left(Q+1\right)\left(Q+1\right)$$
151		facp1	$$⊢Q\in {\mathbb{N}}_0\to \left(Q+1\right)!=Q!\left(Q+1\right)$$
152	56 151	syl	$$⊢\phi \to \left(Q+1\right)!=Q!\left(Q+1\right)$$
153	152	oveq1d	$$⊢\phi \to \frac{\left(Q+1\right)!}{Q!}=\frac{Q!\left(Q+1\right)}{Q!}$$
154	101	nncnd	$$⊢\phi \to \left(Q+1\right)!\in ℂ$$
155	57	nnne0d	$$⊢\phi \to Q!\ne 0$$
156	154 58 155	divrecd	$$⊢\phi \to \frac{\left(Q+1\right)!}{Q!}=\left(Q+1\right)!\left(\frac{1}{Q!}\right)$$
157	138 58 155	divcan3d	$$⊢\phi \to \frac{Q!\left(Q+1\right)}{Q!}=Q+1$$
158	153 156 157	3eqtr3rd	$$⊢\phi \to Q+1=\left(Q+1\right)!\left(\frac{1}{Q!}\right)$$
159	158	oveq1d	$$⊢\phi \to \left(Q+1\right)\left(Q+1\right)=\left(Q+1\right)!\left(\frac{1}{Q!}\right)\left(Q+1\right)$$
160	104	recnd	$$⊢\phi \to \frac{1}{Q!}\in ℂ$$
161	154 160 138	mul32d	$$⊢\phi \to \left(Q+1\right)!\left(\frac{1}{Q!}\right)\left(Q+1\right)=\left(Q+1\right)!\left(Q+1\right)\left(\frac{1}{Q!}\right)$$
162	159 161	eqtrd	$$⊢\phi \to \left(Q+1\right)\left(Q+1\right)=\left(Q+1\right)!\left(Q+1\right)\left(\frac{1}{Q!}\right)$$
163	150 162	breqtrd	$$⊢\phi \to Q+1+1<\left(Q+1\right)!\left(Q+1\right)\left(\frac{1}{Q!}\right)$$
164	102	nnred	$$⊢\phi \to \left(Q+1\right)!\left(Q+1\right)\in ℝ$$
165	102	nngt0d	$$⊢\phi \to 0<\left(Q+1\right)!\left(Q+1\right)$$
166		ltdivmul	$$⊢\left(Q+1+1\in ℝ\wedge \frac{1}{Q!}\in ℝ\wedge \left(\left(Q+1\right)!\left(Q+1\right)\in ℝ\wedge 0<\left(Q+1\right)!\left(Q+1\right)\right)\right)\to \left(\frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}<\frac{1}{Q!}\leftrightarrow Q+1+1<\left(Q+1\right)!\left(Q+1\right)\left(\frac{1}{Q!}\right)\right)$$
167	100 104 164 165 166	syl112anc	$$⊢\phi \to \left(\frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}<\frac{1}{Q!}\leftrightarrow Q+1+1<\left(Q+1\right)!\left(Q+1\right)\left(\frac{1}{Q!}\right)\right)$$
168	163 167	mpbird	$$⊢\phi \to \frac{Q+1+1}{\left(Q+1\right)!\left(Q+1\right)}<\frac{1}{Q!}$$
169	40 103 104 127 168	lelttrd	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)<\frac{1}{Q!}$$
170	40 131 96	ltmuldiv2d	$$⊢\phi \to \left(Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)<1\leftrightarrow \sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)<\frac{1}{Q!}\right)$$
171	169 170	mpbird	$$⊢\phi \to Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)<1$$
172		0p1e1	$$⊢0+1=1$$
173	171 172	breqtrrdi	$$⊢\phi \to Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)<0+1$$
174		btwnnz	$$⊢\left(0\in \mathbb{Z}\wedge 0<Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\wedge Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)<0+1\right)\to \neg Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\in \mathbb{Z}$$
175	95 98 173 174	syl3anc	$$⊢\phi \to \neg Q!\sum _{k\in {\mathbb{Z}}_{\ge \left(Q+1\right)}}F\left(k\right)\in \mathbb{Z}$$
176	94 175	pm2.65i	$$⊢\neg \phi$$