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	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) )
	eirr.2	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
	eirr.3	⊢ ( 𝜑 → 𝑄 ∈ ℕ )
	eirr.4	⊢ ( 𝜑 → e = ( 𝑃 / 𝑄 ) )
Assertion	eirrlem	⊢ ¬ 𝜑

Proof

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