Theorem etransclem48 47565

Description: e is transcendental. Section *5 of [Juillerat] p. 11 can be used as a reference for this proof. In this lemma, a large enough prime 𝑝 is chosen: it will be used by subsequent lemmas. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 28-Sep-2020.)

Hypotheses

Ref	Expression
etransclem48.q	⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
etransclem48.qe0	⊢ (𝜑 → (𝑄‘e) = 0)
etransclem48.a	⊢ 𝐴 = (coeff‘𝑄)
etransclem48.a0	⊢ (𝜑 → (𝐴‘0) ≠ 0)
etransclem48.m	⊢ 𝑀 = (deg‘𝑄)
etransclem48.c	⊢ 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1))))
etransclem48.s	⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
etransclem48.i	⊢ 𝐼 = inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < )
etransclem48.t	⊢ 𝑇 = sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < )

Assertion

Ref	Expression
etransclem48	⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))

Distinct variable groups:   𝐴,𝑗,𝑘   𝐴,𝑛,𝑗   𝐶,𝑖,𝑛   𝑖,𝐼,𝑛   𝑗,𝑀,𝑘   𝑛,𝑀   𝑄,𝑗   𝑆,𝑖   𝑇,𝑗,𝑘   𝜑,𝑖,𝑛   𝜑,𝑗,𝑘

Allowed substitution hints:   𝐴(𝑖)   𝐶(𝑗, 𝑘)   𝑄(𝑖, 𝑘, 𝑛)   𝑆(𝑗, 𝑘, 𝑛)   𝑇(𝑖, 𝑛)   𝐼(𝑗, 𝑘)   𝑀(𝑖)

Proof of Theorem etransclem48

Dummy variables 𝑥 𝑦 𝑧 𝑒 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		etransclem48.q	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
2	1	eldifad 4054	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
3		0zd 12745	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
4		etransclem48.a	. . . . . . . . . 10 ⊢ 𝐴 = (coeff‘𝑄)
5	4	coef2 26605	. . . . . . . . 9 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ0⟶ℤ)
6	2, 3, 5	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → 𝐴:ℕ0⟶ℤ)
7		0nn0 12661	. . . . . . . . 9 ⊢ 0 ∈ ℕ0
8	7	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℕ0)
9	6, 8	ffvelcdmd 7117	. . . . . . 7 ⊢ (𝜑 → (𝐴‘0) ∈ ℤ)
10		zabscl 15523	. . . . . . 7 ⊢ ((𝐴‘0) ∈ ℤ → (abs‘(𝐴‘0)) ∈ ℤ)
11	9, 10	syl 18	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐴‘0)) ∈ ℤ)
12		etransclem48.m	. . . . . . . . 9 ⊢ 𝑀 = (deg‘𝑄)
13		dgrcl 26607	. . . . . . . . . 10 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ0)
14	2, 13	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ0)
15	12, 14	eqeltrid 2868	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
16	15	faccld 14469	. . . . . . 7 ⊢ (𝜑 → (!‘𝑀) ∈ ℕ)
17	16	nnzd 12759	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) ∈ ℤ)
18		ssrab2 4008	. . . . . . . 8 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ ℕ0
19		nn0ssz 12756	. . . . . . . 8 ⊢ ℕ0 ⊆ ℤ
20	18, 19	sstri 3922	. . . . . . 7 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ ℤ
21		etransclem48.i	. . . . . . . 8 ⊢ 𝐼 = inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < )
22		nn0uz 13043	. . . . . . . . . 10 ⊢ ℕ0 = (ℤ≥‘0)
23	18, 22	sseqtri 3961	. . . . . . . . 9 ⊢ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ (ℤ≥‘0)
24		1rp 13164	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ+
25		nfv 1949	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝜑
26		nfmpt1 5210	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ 𝐶)
27		nfmpt1 5210	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
28		etransclem48.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
29		nfmpt1 5210	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
30	28, 29	nfcxfr 2924	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛𝑆
31		nn0ex 12652	. . . . . . . . . . . . . . . . 17 ⊢ ℕ0 ∈ V
32	31	mptex 7260	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ 𝐶) ∈ V
33	32	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ 𝐶) ∈ V)
34		etransclem48.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1))))
35		fzfid 14156	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
36	6	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ)
37		elfznn0 13794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
38	37	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
39	36, 38	ffvelcdmd 7117	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
40	39	zcnd 12844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
41		ere 16299	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ e ∈ ℝ
42	41	recni 11362	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ e ∈ ℂ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ)
44		elfzelz 13696	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
45	44	zcnd 12844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
46	45	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
47	43, 46	cxpcld 27093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈ ℂ)
48	40, 47	mulcld 11368	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑐𝑗)) ∈ ℂ)
49	48	abscld 15650	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈ ℝ)
50	49	recnd 11376	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈ ℂ)
51	15	nn0cnd 12709	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
52		peano2nn0 12686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
53	15, 52	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ0)
54	51, 53	expcld 14329	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ)
55	51, 54	mulcld 11368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
56	55	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
57	50, 56	mulcld 11368	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
58	35, 57	fsumcl 15943	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
59	34, 58	eqeltrid 2868	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℂ)
60		eqidd 2764	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑛 ∈ ℕ0 ↦ 𝐶) = (𝑛 ∈ ℕ0 ↦ 𝐶))
61		eqidd 2764	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 = 𝑖) → 𝐶 = 𝐶)
62		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
63	59	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐶 ∈ ℂ)
64	60, 61, 62, 63	fvmptd 7032	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑖) = 𝐶)
65	22, 3, 33, 59, 64	climconst 15754	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ 𝐶) ⇝ 𝐶)
66	31	mptex 7260	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))) ∈ V
67	28, 66	eqeltri 2860	. . . . . . . . . . . . . . 15 ⊢ 𝑆 ∈ V
68	67	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ V)
69		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
70	69	expfac 46940	. . . . . . . . . . . . . . 15 ⊢ ((𝑀↑(𝑀 + 1)) ∈ ℂ → (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ⇝ 0)
71	54, 70	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ⇝ 0)
72		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
73	59	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝐶 ∈ ℂ)
74		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ0 ↦ 𝐶) = (𝑛 ∈ ℕ0 ↦ 𝐶)
75	74	fvmpt2 7036	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ0 ∧ 𝐶 ∈ ℂ) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) = 𝐶)
76	72, 73, 75	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) = 𝐶)
77	76, 73	eqeltrd 2864	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) ∈ ℂ)
78		ovex 7484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ V
79	69	fvmpt2 7036	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ0 ∧ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ V) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) = (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
80	78, 79	mpan2 704	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) = (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
81	80	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) = (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))
82	54	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑀↑(𝑀 + 1)) ∈ ℂ)
83	82, 72	expcld 14329	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑀↑(𝑀 + 1))↑𝑛) ∈ ℂ)
84	72	faccld 14469	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ∈ ℕ)
85	84	nncnd 12391	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ∈ ℂ)
86	84	nnne0d 12428	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (!‘𝑛) ≠ 0)
87	83, 85, 86	divcld 12133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) ∈ ℂ)
88	81, 87	eqeltrd 2864	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛) ∈ ℂ)
89		ovex 7484	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ∈ V
90	28	fvmpt2 7036	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ0 ∧ (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) ∈ V) → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
91	89, 90	mpan2 704	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
92	91	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
93	76, 81	oveq12d 7469	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)) = (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))))
94	92, 93	eqtr4d 2801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)))
95	25, 26, 27, 30, 22, 3, 65, 68, 71, 77, 88, 94	climmulf 46889	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ⇝ (𝐶 · 0))
96	59	mul01d 11548	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 · 0) = 0)
97	95, 96	breqtrd 5137	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ⇝ 0)
98		eqidd 2764	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) = (𝑆‘𝑛))
99	77, 88	mulcld 11368	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑛 ∈ ℕ0 ↦ 𝐶)‘𝑛) · ((𝑛 ∈ ℕ0 ↦ (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)))‘𝑛)) ∈ ℂ)
100	94, 99	eqeltrd 2864	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑆‘𝑛) ∈ ℂ)
101	30, 22, 3, 68, 98, 100	clim0cf 46937	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ⇝ 0 ↔ ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒))
102	97, 101	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒)
103		breq2 5112	. . . . . . . . . . . . 13 ⊢ (𝑒 = 1 → ((abs‘(𝑆‘𝑛)) < 𝑒 ↔ (abs‘(𝑆‘𝑛)) < 1))
104	103	rexralbidv 3232	. . . . . . . . . . . 12 ⊢ (𝑒 = 1 → (∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒 ↔ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1))
105	104	rspcva 3578	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ+ ∧ ∀𝑒 ∈ ℝ+ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 𝑒) → ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
106	24, 102, 105	sylancr 599	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
107		rabn0 4342	. . . . . . . . . 10 ⊢ ({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅ ↔ ∃𝑖 ∈ ℕ0 ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1)
108	106, 107	sylibr 237	. . . . . . . . 9 ⊢ (𝜑 → {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅)
109		infssuzcl 13099	. . . . . . . . 9 ⊢ (({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ⊆ (ℤ≥‘0) ∧ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ≠ ∅) → inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < ) ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
110	23, 108, 109	sylancr 599	. . . . . . . 8 ⊢ (𝜑 → inf({𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1}, ℝ, < ) ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
111	21, 110	eqeltrid 2868	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
112	20, 111	sselid 3911	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ ℤ)
113		tpssi 4798	. . . . . 6 ⊢ (((abs‘(𝐴‘0)) ∈ ℤ ∧ (!‘𝑀) ∈ ℤ ∧ 𝐼 ∈ ℤ) → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℤ)
114	11, 17, 112, 113	syl3anc 1399	. . . . 5 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℤ)
115		etransclem48.t	. . . . . 6 ⊢ 𝑇 = sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < )
116		xrltso 13310	. . . . . . . 8 ⊢ < Or ℝ*
117	116	a1i 11	. . . . . . 7 ⊢ (𝜑 → < Or ℝ*)
118		tpfi 9355	. . . . . . . 8 ⊢ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin
119	118	a1i 11	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin)
120	11	tpnzd 4743	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ≠ ∅)
121		zssre 12740	. . . . . . . . 9 ⊢ ℤ ⊆ ℝ
122		ressxr 11392	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ*
123	121, 122	sstri 3922	. . . . . . . 8 ⊢ ℤ ⊆ ℝ*
124	114, 123	sstrdi 3925	. . . . . . 7 ⊢ (𝜑 → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)
125		fisupcl 9499	. . . . . . 7 ⊢ (( < Or ℝ* ∧ ({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ∈ Fin ∧ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ≠ ∅ ∧ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)) → sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
126	117, 119, 120, 124, 125	syl13anc 1400	. . . . . 6 ⊢ (𝜑 → sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
127	115, 126	eqeltrid 2868	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
128	114, 127	sseldd 3914	. . . 4 ⊢ (𝜑 → 𝑇 ∈ ℤ)
129		0red 11350	. . . . 5 ⊢ (𝜑 → 0 ∈ ℝ)
130	16	nnred 12390	. . . . 5 ⊢ (𝜑 → (!‘𝑀) ∈ ℝ)
131	128	zred 12843	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℝ)
132	16	nngt0d 12427	. . . . 5 ⊢ (𝜑 → 0 < (!‘𝑀))
133		fvex 6929	. . . . . . . 8 ⊢ (!‘𝑀) ∈ V
134	133	tpid2 4733	. . . . . . 7 ⊢ (!‘𝑀) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}
135		supxrub 13494	. . . . . . 7 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ (!‘𝑀) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → (!‘𝑀) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
136	124, 134, 135	sylancl 598	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
137	136, 115	breqtrrdi 5153	. . . . 5 ⊢ (𝜑 → (!‘𝑀) ≤ 𝑇)
138	129, 130, 131, 132, 137	ltletrd 11509	. . . 4 ⊢ (𝜑 → 0 < 𝑇)
139		elnnz 12743	. . . 4 ⊢ (𝑇 ∈ ℕ ↔ (𝑇 ∈ ℤ ∧ 0 < 𝑇))
140	128, 138, 139	sylanbrc 595	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℕ)
141		prmunb 17136	. . 3 ⊢ (𝑇 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑇 < 𝑝)
142	140, 141	syl 18	. 2 ⊢ (𝜑 → ∃𝑝 ∈ ℙ 𝑇 < 𝑝)
143	1	3ad2ant1 1151	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
144		etransclem48.qe0	. . . . 5 ⊢ (𝜑 → (𝑄‘e) = 0)
145	144	3ad2ant1 1151	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑄‘e) = 0)
146		etransclem48.a0	. . . . 5 ⊢ (𝜑 → (𝐴‘0) ≠ 0)
147	146	3ad2ant1 1151	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐴‘0) ≠ 0)
148		simp2 1155	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℙ)
149	9	zcnd 12844	. . . . . . 7 ⊢ (𝜑 → (𝐴‘0) ∈ ℂ)
150	149	3ad2ant1 1151	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐴‘0) ∈ ℂ)
151	150	abscld 15650	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) ∈ ℝ)
152	131	3ad2ant1 1151	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑇 ∈ ℝ)
153		prmz 16894	. . . . . . 7 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
154	153	zred 12843	. . . . . 6 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
155	154	3ad2ant2 1152	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℝ)
156	124	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ*)
157		fvex 6929	. . . . . . . . 9 ⊢ (abs‘(𝐴‘0)) ∈ V
158	157	tpid1 4731	. . . . . . . 8 ⊢ (abs‘(𝐴‘0)) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}
159		supxrub 13494	. . . . . . . 8 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ (abs‘(𝐴‘0)) ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → (abs‘(𝐴‘0)) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
160	156, 158, 159	sylancl 598	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (abs‘(𝐴‘0)) ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
161	160, 115	breqtrrdi 5153	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (abs‘(𝐴‘0)) ≤ 𝑇)
162	161	3adant3 1150	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) ≤ 𝑇)
163		simp3 1156	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑇 < 𝑝)
164	151, 152, 155, 162, 163	lelttrd 11507	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝐴‘0)) < 𝑝)
165	130	3ad2ant1 1151	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) ∈ ℝ)
166	137	3ad2ant1 1151	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) ≤ 𝑇)
167	165, 152, 155, 166, 163	lelttrd 11507	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (!‘𝑀) < 𝑝)
168	34	a1i 11	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → 𝐶 = Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))))
169		oveq2 7459	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → ((𝑀↑(𝑀 + 1))↑𝑛) = ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)))
170		fveq2 6916	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → (!‘𝑛) = (!‘(𝑝 − 1)))
171	169, 170	oveq12d 7469	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛)) = (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))))
172	168, 171	oveq12d 7469	. . . . . . . 8 ⊢ (𝑛 = (𝑝 − 1) → (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
173		prmnn 16893	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
174		nnm1nn0 12687	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℕ → (𝑝 − 1) ∈ ℕ0)
175	173, 174	syl 18	. . . . . . . . 9 ⊢ (𝑝 ∈ ℙ → (𝑝 − 1) ∈ ℕ0)
176	175	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ0)
177	58	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
178	54	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀↑(𝑀 + 1)) ∈ ℂ)
179	178, 176	expcld 14329	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) ∈ ℂ)
180	175	faccld 14469	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℕ)
181	180	nncnd 12391	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℂ)
182	181	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ∈ ℂ)
183	180	nnne0d 12428	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ≠ 0)
184	183	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ≠ 0)
185	179, 182, 184	divcld 12133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))) ∈ ℂ)
186	177, 185	mulcld 11368	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ ℂ)
187	28, 172, 176, 186	fvmptd3 7048	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
188	187	eqcomd 2769	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) = (𝑆‘(𝑝 − 1)))
189	188	3adant3 1150	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) = (𝑆‘(𝑝 − 1)))
190	112	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ ℤ)
191		1zzd 12767	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 1 ∈ ℤ)
192	153, 191	zsubcld 12848	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → (𝑝 − 1) ∈ ℤ)
193	192	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑝 − 1) ∈ ℤ)
194	190	zred 12843	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ ℝ)
195		tpid3g 4735	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
196	112, 195	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼})
197		supxrub 13494	. . . . . . . . . . . . . 14 ⊢ (({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼} ⊆ ℝ* ∧ 𝐼 ∈ {(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}) → 𝐼 ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
198	124, 196, 197	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐼 ≤ sup({(abs‘(𝐴‘0)), (!‘𝑀), 𝐼}, ℝ*, < ))
199	198, 115	breqtrrdi 5153	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ≤ 𝑇)
200	199	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ≤ 𝑇)
201	194, 152, 155, 200, 163	lelttrd 11507	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 < 𝑝)
202	153	3ad2ant2 1152	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝑝 ∈ ℤ)
203		zltlem1 12789	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℤ ∧ 𝑝 ∈ ℤ) → (𝐼 < 𝑝 ↔ 𝐼 ≤ (𝑝 − 1)))
204	190, 202, 203	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐼 < 𝑝 ↔ 𝐼 ≤ (𝑝 − 1)))
205	201, 204	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ≤ (𝑝 − 1))
206		eluz2 13011	. . . . . . . . 9 ⊢ ((𝑝 − 1) ∈ (ℤ≥‘𝐼) ↔ (𝐼 ∈ ℤ ∧ (𝑝 − 1) ∈ ℤ ∧ 𝐼 ≤ (𝑝 − 1)))
207	190, 193, 205, 206	syl3anbrc 1362	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑝 − 1) ∈ (ℤ≥‘𝐼))
208	111	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1})
209		fveq2 6916	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝐼 → (ℤ≥‘𝑖) = (ℤ≥‘𝐼))
210	209	raleqdv 3323	. . . . . . . . . . 11 ⊢ (𝑖 = 𝐼 → (∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1 ↔ ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1))
211	210	elrab 3648	. . . . . . . . . 10 ⊢ (𝐼 ∈ {𝑖 ∈ ℕ0 ∣ ∀𝑛 ∈ (ℤ≥‘𝑖)(abs‘(𝑆‘𝑛)) < 1} ↔ (𝐼 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1))
212	208, 211	sylib 221	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝐼 ∈ ℕ0 ∧ ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1))
213	212	simprd 501	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → ∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1)
214		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑛abs
215		nfcv 2926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑝 − 1)
216	30, 215	nffv 6926	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝑆‘(𝑝 − 1))
217	214, 216	nffv 6926	. . . . . . . . . 10 ⊢ Ⅎ𝑛(abs‘(𝑆‘(𝑝 − 1)))
218		nfcv 2926	. . . . . . . . . 10 ⊢ Ⅎ𝑛 <
219		nfcv 2926	. . . . . . . . . 10 ⊢ Ⅎ𝑛1
220	217, 218, 219	nfbr 5158	. . . . . . . . 9 ⊢ Ⅎ𝑛(abs‘(𝑆‘(𝑝 − 1))) < 1
221		2fveq3 6921	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − 1) → (abs‘(𝑆‘𝑛)) = (abs‘(𝑆‘(𝑝 − 1))))
222	221	breq1d 5118	. . . . . . . . 9 ⊢ (𝑛 = (𝑝 − 1) → ((abs‘(𝑆‘𝑛)) < 1 ↔ (abs‘(𝑆‘(𝑝 − 1))) < 1))
223	220, 222	rspc 3568	. . . . . . . 8 ⊢ ((𝑝 − 1) ∈ (ℤ≥‘𝐼) → (∀𝑛 ∈ (ℤ≥‘𝐼)(abs‘(𝑆‘𝑛)) < 1 → (abs‘(𝑆‘(𝑝 − 1))) < 1))
224	207, 213, 223	sylc 66	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (abs‘(𝑆‘(𝑝 − 1))) < 1)
225	171	oveq2d 7467	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝 − 1) → (𝐶 · (((𝑀↑(𝑀 + 1))↑𝑛) / (!‘𝑛))) = (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
226		ovexd 7486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ V)
227	28, 225, 176, 226	fvmptd3 7048	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) = (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))))
228	15	nn0red 12708	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℝ)
229	228, 53	reexpcld 14346	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ)
230	228, 229	remulcld 11378	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℝ)
231	230	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℝ)
232	49, 231	remulcld 11378	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℝ)
233	35, 232	fsumrecl 15944	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℝ)
234	34, 233	eqeltrid 2868	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℝ)
235	234	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝐶 ∈ ℝ)
236	229	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀↑(𝑀 + 1)) ∈ ℝ)
237	236, 176	reexpcld 14346	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) ∈ ℝ)
238	180	nnred 12390	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → (!‘(𝑝 − 1)) ∈ ℝ)
239	238	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(𝑝 − 1)) ∈ ℝ)
240	237, 239, 184	redivcld 12185	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1))) ∈ ℝ)
241	235, 240	remulcld 11378	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐶 · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) ∈ ℝ)
242	227, 241	eqeltrd 2864	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑆‘(𝑝 − 1)) ∈ ℝ)
243	242	3adant3 1150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑆‘(𝑝 − 1)) ∈ ℝ)
244		1red 11348	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → 1 ∈ ℝ)
245	243, 244	absltd 15643	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → ((abs‘(𝑆‘(𝑝 − 1))) < 1 ↔ ( -1 < (𝑆‘(𝑝 − 1)) ∧ (𝑆‘(𝑝 − 1)) < 1)))
246	224, 245	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → ( -1 < (𝑆‘(𝑝 − 1)) ∧ (𝑆‘(𝑝 − 1)) < 1))
247	246	simprd 501	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (𝑆‘(𝑝 − 1)) < 1)
248	189, 247	eqbrtrd 5133	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑝 − 1)) / (!‘(𝑝 − 1)))) < 1)
249		etransclem6 47523	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑝 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑝)))
250		eqid 2763	. . . 4 ⊢ Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐 -𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐 -𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥)
251		eqid 2763	. . . 4 ⊢ (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐 -𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥) / (!‘(𝑝 − 1))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐 -𝑥) · ((𝑦 ∈ ℝ ↦ ((𝑦↑(𝑝 − 1)) · ∏𝑧 ∈ (1...𝑀)((𝑦 − 𝑧)↑𝑝)))‘𝑥)) d𝑥) / (!‘(𝑝 − 1)))
252	143, 145, 4, 147, 12, 148, 164, 167, 248, 249, 250, 251	etransclem47 47564	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ ∧ 𝑇 < 𝑝) → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))
253	252	rexlimdv3a 3171	. 2 ⊢ (𝜑 → (∃𝑝 ∈ ℙ 𝑇 < 𝑝 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1)))
254	142, 253	mpd 16	1 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048  ∅c0 4281  {csn 4588  {ctp 4592   class class class wbr 5108   ↦ cmpt 5192   Or wor 5565  ⟶wf 6562  ‘cfv 6566  (class class class)co 7451  Fincfn 9011  supcsup 9469  infcinf 9470  ℂcc 11237  ℝcr 11238  0cc0 11239  1c1 11240   + caddc 11242   · cmul 11244  ℝ^*cxr 11381   < clt 11382   ≤ cle 11383   − cmin 11580   -cneg 11581   / cdiv 12013  ℕcn 12375  ℕ₀cn0 12646  ℤcz 12733  ℤ_≥cuz 13005  ℝ⁺crp 13160  (,)cioo 13516  ...cfz 13679  ↑cexp 14244  !cfa 14458  abscabs 15444   ⇝ cli 15695  Σcsu 15897  ∏cprod 16116  eceu 16272  ℙcprime 16890  ∫citg 25994  0_𝑝c0p 26045  Polycply 26557  coeffccoe 26559  degcdgr 26560  ↑_𝑐ccxp 26940

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-inf2 9679  ax-cc 10552  ax-cnex 11295  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316  ax-pre-sup 11317  ax-addf 11318

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-symdif 4201  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-disj 5076  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-isom 6575  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-of 7725  df-ofr 7726  df-om 7912  df-1st 8035  df-2nd 8036  df-supp 8215  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-1o 8514  df-2o 8515  df-oadd 8518  df-omul 8519  df-er 8755  df-map 8887  df-pm 8888  df-ixp 8964  df-en 9012  df-dom 9013  df-sdom 9014  df-fin 9015  df-fsupp 9392  df-fi 9440  df-sup 9471  df-inf 9472  df-oi 9541  df-dju 10019  df-card 10057  df-acn 10060  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-div 12014  df-nn 12376  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450  df-8 12451  df-9 12452  df-n0 12647  df-z 12734  df-dec 12855  df-uz 13006  df-q 13116  df-rp 13161  df-xneg 13281  df-xadd 13282  df-xmul 13283  df-ioo 13520  df-ioc 13521  df-ico 13522  df-icc 13523  df-fz 13680  df-fzo 13829  df-fl 13972  df-mod 14050  df-seq 14185  df-exp 14245  df-fac 14459  df-bc 14488  df-hash 14516  df-shft 15263  df-cj 15309  df-re 15310  df-im 15311  df-sqrt 15445  df-abs 15446  df-limsup 15682  df-clim 15699  df-rlim 15700  df-sum 15898  df-prod 16117  df-ef 16277  df-e 16278  df-sin 16279  df-cos 16280  df-tan 16281  df-pi 16282  df-dvds 16467  df-gcd 16709  df-prm 16891  df-struct 17369  df-sets 17386  df-slot 17404  df-ndx 17416  df-base 17432  df-ress 17453  df-plusg 17486  df-mulr 17487  df-starv 17488  df-sca 17489  df-vsca 17490  df-ip 17491  df-tset 17492  df-ple 17493  df-ds 17495  df-unif 17496  df-hom 17497  df-cco 17498  df-euf 17499  df-rest 17643  df-topn 17644  df-0g 17662  df-gsum 17663  df-topgen 17664  df-pt 17665  df-prds 17668  df-xrs 17724  df-qtop 17729  df-imas 17730  df-xps 17732  df-mre 17806  df-mrc 17807  df-acs 17809  df-mgm 18866  df-sgrp 18958  df-mnd 18974  df-submnd 19029  df-mulg 19328  df-cntz 19582  df-cmn 20047  df-psmet 21721  df-xmet 21722  df-met 21723  df-bl 21724  df-mopn 21725  df-fbas 21726  df-fg 21727  df-cnfld 21730  df-top 23267  df-topon 23284  df-topsp 23306  df-bases 23319  df-cld 23392  df-ntr 23393  df-cls 23394  df-nei 23471  df-lp 23509  df-perf 23510  df-cn 23600  df-cnp 23601  df-haus 23688  df-cmp 23760  df-tx 23936  df-hmeo 24129  df-fil 24220  df-fm 24312  df-flim 24313  df-flf 24314  df-xms 24694  df-ms 24695  df-tms 24696  df-cncf 25254  df-ovol 25840  df-vol 25841  df-mbf 25995  df-itg1 25996  df-itg2 25997  df-ibl 25998  df-itg 25999  df-0p 26046  df-limc 26241  df-dv 26242  df-dvn 26243  df-ply 26561  df-coe 26563  df-dgr 26564  df-log 26941  df-cxp 26942

This theorem is used by:  etransc  47566