etransclem48

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 p is chosen: it will be used by subsequent lemmas. (Contributed by Glauco Siliprandi, 5-Apr-2020) (Revised by AV, 28-Sep-2020)

	Ref	Expression
Hypotheses	etransclem48.q	$⊢ φ \to Q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
	etransclem48.qe0	$⊢ φ \to Q (e) = 0$
	etransclem48.a	$⊢ A = coeff (Q)$
	etransclem48.a0	$⊢ φ \to A (0) \neq 0$
	etransclem48.m	$⊢ M = \deg (Q)$
	etransclem48.c	$⊢ C = \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1}$
	etransclem48.s	$⊢ S = (n \in ℕ_{0} ⟼ C (\frac{{(M^{M + 1})}^{n}}{n!}))$
	etransclem48.i	$⊢ I = sup (\{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} ℝ <)$
	etransclem48.t	$⊢ T = sup (\{\|A (0)\|, M!, I\} ℝ^{*} <)$
Assertion	etransclem48	$⊢ φ \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$

Proof

Step	Hyp	Ref	Expression
1		etransclem48.q	$⊢ φ \to Q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
2		etransclem48.qe0	$⊢ φ \to Q (e) = 0$
3		etransclem48.a	$⊢ A = coeff (Q)$
4		etransclem48.a0	$⊢ φ \to A (0) \neq 0$
5		etransclem48.m	$⊢ M = \deg (Q)$
6		etransclem48.c	$⊢ C = \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1}$
7		etransclem48.s	$⊢ S = (n \in ℕ_{0} ⟼ C (\frac{{(M^{M + 1})}^{n}}{n!}))$
8		etransclem48.i	$⊢ I = sup (\{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} ℝ <)$
9		etransclem48.t	$⊢ T = sup (\{\|A (0)\|, M!, I\} ℝ^{*} <)$
10	1	eldifad	$⊢ φ \to Q \in Poly (ℤ)$
11		0zd	$⊢ φ \to 0 \in ℤ$
12	3	coef2	$⊢ (Q \in Poly (ℤ) \land 0 \in ℤ) \to A : ℕ_{0} ⟶ ℤ$
13	10 11 12	syl2anc	$⊢ φ \to A : ℕ_{0} ⟶ ℤ$
14		0nn0	$⊢ 0 \in ℕ_{0}$
15	14	a1i	$⊢ φ \to 0 \in ℕ_{0}$
16	13 15	ffvelrnd	$⊢ φ \to A (0) \in ℤ$
17		zabscl	$⊢ A (0) \in ℤ \to \|A (0)\| \in ℤ$
18	16 17	syl	$⊢ φ \to \|A (0)\| \in ℤ$
19		dgrcl	$⊢ Q \in Poly (ℤ) \to \deg (Q) \in ℕ_{0}$
20	10 19	syl	$⊢ φ \to \deg (Q) \in ℕ_{0}$
21	5 20	eqeltrid	$⊢ φ \to M \in ℕ_{0}$
22	21	faccld	$⊢ φ \to M! \in ℕ$
23	22	nnzd	$⊢ φ \to M! \in ℤ$
24		ssrab2	$⊢ \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} \subseteq ℕ_{0}$
25		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
26	24 25	sstri	$⊢ \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} \subseteq ℤ$
27		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
28	24 27	sseqtri	$⊢ \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} \subseteq ℤ_{\geq 0}$
29		1rp	$⊢ 1 \in ℝ^{+}$
30		nfv	$⊢ Ⅎ n φ$
31		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ_{0} ⟼ C)$
32		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!})$
33		nfmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ_{0} ⟼ C (\frac{{(M^{M + 1})}^{n}}{n!}))$
34	7 33	nfcxfr	$⊢ \underline{Ⅎ} n S$
35		nn0ex	$⊢ ℕ_{0} \in V$
36	35	mptex	$⊢ (n \in ℕ_{0} ⟼ C) \in V$
37	36	a1i	$⊢ φ \to (n \in ℕ_{0} ⟼ C) \in V$
38		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
39	13	adantr	$⊢ (φ \land j \in (0 \dots M)) \to A : ℕ_{0} ⟶ ℤ$
40		elfznn0	$⊢ j \in (0 \dots M) \to j \in ℕ_{0}$
41	40	adantl	$⊢ (φ \land j \in (0 \dots M)) \to j \in ℕ_{0}$
42	39 41	ffvelrnd	$⊢ (φ \land j \in (0 \dots M)) \to A (j) \in ℤ$
43	42	zcnd	$⊢ (φ \land j \in (0 \dots M)) \to A (j) \in ℂ$
44		ere	$⊢ e \in ℝ$
45	44	recni	$⊢ e \in ℂ$
46	45	a1i	$⊢ (φ \land j \in (0 \dots M)) \to e \in ℂ$
47		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
48	47	zcnd	$⊢ j \in (0 \dots M) \to j \in ℂ$
49	48	adantl	$⊢ (φ \land j \in (0 \dots M)) \to j \in ℂ$
50	46 49	cxpcld	$⊢ (φ \land j \in (0 \dots M)) \to e^{j} \in ℂ$
51	43 50	mulcld	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} \in ℂ$
52	51	abscld	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| \in ℝ$
53	52	recnd	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| \in ℂ$
54	21	nn0cnd	$⊢ φ \to M \in ℂ$
55		peano2nn0	$⊢ M \in ℕ_{0} \to M + 1 \in ℕ_{0}$
56	21 55	syl	$⊢ φ \to M + 1 \in ℕ_{0}$
57	54 56	expcld	$⊢ φ \to M^{M + 1} \in ℂ$
58	54 57	mulcld	$⊢ φ \to M M^{M + 1} \in ℂ$
59	58	adantr	$⊢ (φ \land j \in (0 \dots M)) \to M M^{M + 1} \in ℂ$
60	53 59	mulcld	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| M M^{M + 1} \in ℂ$
61	38 60	fsumcl	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} \in ℂ$
62	6 61	eqeltrid	$⊢ φ \to C \in ℂ$
63		eqidd	$⊢ (φ \land i \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ C) = (n \in ℕ_{0} ⟼ C)$
64		eqidd	$⊢ ((φ \land i \in ℕ_{0}) \land n = i) \to C = C$
65		simpr	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℕ_{0}$
66	62	adantr	$⊢ (φ \land i \in ℕ_{0}) \to C \in ℂ$
67	63 64 65 66	fvmptd	$⊢ (φ \land i \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ C) (i) = C$
68	27 11 37 62 67	climconst	$⊢ φ \to (n \in ℕ_{0} ⟼ C) ⇝ C$
69	35	mptex	$⊢ (n \in ℕ_{0} ⟼ C (\frac{{(M^{M + 1})}^{n}}{n!})) \in V$
70	7 69	eqeltri	$⊢ S \in V$
71	70	a1i	$⊢ φ \to S \in V$
72		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!}) = (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!})$
73	72	expfac	$⊢ M^{M + 1} \in ℂ \to (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!}) ⇝ 0$
74	57 73	syl	$⊢ φ \to (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!}) ⇝ 0$
75		simpr	$⊢ (φ \land n \in ℕ_{0}) \to n \in ℕ_{0}$
76	62	adantr	$⊢ (φ \land n \in ℕ_{0}) \to C \in ℂ$
77		eqid	$⊢ (n \in ℕ_{0} ⟼ C) = (n \in ℕ_{0} ⟼ C)$
78	77	fvmpt2	$⊢ (n \in ℕ_{0} \land C \in ℂ) \to (n \in ℕ_{0} ⟼ C) (n) = C$
79	75 76 78	syl2anc	$⊢ (φ \land n \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ C) (n) = C$
80	79 76	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ C) (n) \in ℂ$
81		ovex	$⊢ \frac{{(M^{M + 1})}^{n}}{n!} \in V$
82	72	fvmpt2	$⊢ (n \in ℕ_{0} \land \frac{{(M^{M + 1})}^{n}}{n!} \in V) \to (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!}) (n) = \frac{{(M^{M + 1})}^{n}}{n!}$
83	81 82	mpan2	$⊢ n \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!}) (n) = \frac{{(M^{M + 1})}^{n}}{n!}$
84	83	adantl	$⊢ (φ \land n \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!}) (n) = \frac{{(M^{M + 1})}^{n}}{n!}$
85	57	adantr	$⊢ (φ \land n \in ℕ_{0}) \to M^{M + 1} \in ℂ$
86	85 75	expcld	$⊢ (φ \land n \in ℕ_{0}) \to {(M^{M + 1})}^{n} \in ℂ$
87	75	faccld	$⊢ (φ \land n \in ℕ_{0}) \to n! \in ℕ$
88	87	nncnd	$⊢ (φ \land n \in ℕ_{0}) \to n! \in ℂ$
89	87	nnne0d	$⊢ (φ \land n \in ℕ_{0}) \to n! \neq 0$
90	86 88 89	divcld	$⊢ (φ \land n \in ℕ_{0}) \to \frac{{(M^{M + 1})}^{n}}{n!} \in ℂ$
91	84 90	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!}) (n) \in ℂ$
92		ovex	$⊢ C (\frac{{(M^{M + 1})}^{n}}{n!}) \in V$
93	7	fvmpt2	$⊢ (n \in ℕ_{0} \land C (\frac{{(M^{M + 1})}^{n}}{n!}) \in V) \to S (n) = C (\frac{{(M^{M + 1})}^{n}}{n!})$
94	92 93	mpan2	$⊢ n \in ℕ_{0} \to S (n) = C (\frac{{(M^{M + 1})}^{n}}{n!})$
95	94	adantl	$⊢ (φ \land n \in ℕ_{0}) \to S (n) = C (\frac{{(M^{M + 1})}^{n}}{n!})$
96	79 84	oveq12d	$⊢ (φ \land n \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ C) (n) (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!}) (n) = C (\frac{{(M^{M + 1})}^{n}}{n!})$
97	95 96	eqtr4d	$⊢ (φ \land n \in ℕ_{0}) \to S (n) = (n \in ℕ_{0} ⟼ C) (n) (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!}) (n)$
98	30 31 32 34 27 11 68 71 74 80 91 97	climmulf	$⊢ φ \to S ⇝ C \cdot 0$
99	62	mul01d	$⊢ φ \to C \cdot 0 = 0$
100	98 99	breqtrd	$⊢ φ \to S ⇝ 0$
101		eqidd	$⊢ (φ \land n \in ℕ_{0}) \to S (n) = S (n)$
102	80 91	mulcld	$⊢ (φ \land n \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ C) (n) (n \in ℕ_{0} ⟼ \frac{{(M^{M + 1})}^{n}}{n!}) (n) \in ℂ$
103	97 102	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to S (n) \in ℂ$
104	34 27 11 71 101 103	clim0cf	$⊢ φ \to (S ⇝ 0 \leftrightarrow \forall e \in ℝ^{+} \exists i \in ℕ_{0} \forall n \in ℤ_{\geq i} \|S (n)\| < e)$
105	100 104	mpbid	$⊢ φ \to \forall e \in ℝ^{+} \exists i \in ℕ_{0} \forall n \in ℤ_{\geq i} \|S (n)\| < e$
106		breq2	$⊢ e = 1 \to (\|S (n)\| < e \leftrightarrow \|S (n)\| < 1)$
107	106	rexralbidv	$⊢ e = 1 \to (\exists i \in ℕ_{0} \forall n \in ℤ_{\geq i} \|S (n)\| < e \leftrightarrow \exists i \in ℕ_{0} \forall n \in ℤ_{\geq i} \|S (n)\| < 1)$
108	107	rspcva	$⊢ (1 \in ℝ^{+} \land \forall e \in ℝ^{+} \exists i \in ℕ_{0} \forall n \in ℤ_{\geq i} \|S (n)\| < e) \to \exists i \in ℕ_{0} \forall n \in ℤ_{\geq i} \|S (n)\| < 1$
109	29 105 108	sylancr	$⊢ φ \to \exists i \in ℕ_{0} \forall n \in ℤ_{\geq i} \|S (n)\| < 1$
110		rabn0	$⊢ \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} \neq \emptyset \leftrightarrow \exists i \in ℕ_{0} \forall n \in ℤ_{\geq i} \|S (n)\| < 1$
111	109 110	sylibr	$⊢ φ \to \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} \neq \emptyset$
112		infssuzcl	$⊢ (\{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} \subseteq ℤ_{\geq 0} \land \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} \neq \emptyset) \to sup (\{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} ℝ <) \in \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\}$
113	28 111 112	sylancr	$⊢ φ \to sup (\{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} ℝ <) \in \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\}$
114	8 113	eqeltrid	$⊢ φ \to I \in \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\}$
115	26 114	sselid	$⊢ φ \to I \in ℤ$
116		tpssi	$⊢ (\|A (0)\| \in ℤ \land M! \in ℤ \land I \in ℤ) \to \{\|A (0)\|, M!, I\} \subseteq ℤ$
117	18 23 115 116	syl3anc	$⊢ φ \to \{\|A (0)\|, M!, I\} \subseteq ℤ$
118		xrltso	$⊢ < Or ℝ^{*}$
119	118	a1i	$⊢ φ \to < Or ℝ^{*}$
120		tpfi	$⊢ \{\|A (0)\|, M!, I\} \in Fin$
121	120	a1i	$⊢ φ \to \{\|A (0)\|, M!, I\} \in Fin$
122	18	tpnzd	$⊢ φ \to \{\|A (0)\|, M!, I\} \neq \emptyset$
123		zssre	$⊢ ℤ \subseteq ℝ$
124		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
125	123 124	sstri	$⊢ ℤ \subseteq ℝ^{*}$
126	117 125	sstrdi	$⊢ φ \to \{\|A (0)\|, M!, I\} \subseteq ℝ^{*}$
127		fisupcl	$⊢ (< Or ℝ^{} \land (\{\|A (0)\|, M!, I\} \in Fin \land \{\|A (0)\|, M!, I\} \neq \emptyset \land \{\|A (0)\|, M!, I\} \subseteq ℝ^{})) \to sup (\{\|A (0)\|, M!, I\} ℝ^{*} <) \in \{\|A (0)\|, M!, I\}$
128	119 121 122 126 127	syl13anc	$⊢ φ \to sup (\{\|A (0)\|, M!, I\} ℝ^{*} <) \in \{\|A (0)\|, M!, I\}$
129	9 128	eqeltrid	$⊢ φ \to T \in \{\|A (0)\|, M!, I\}$
130	117 129	sseldd	$⊢ φ \to T \in ℤ$
131		0red	$⊢ φ \to 0 \in ℝ$
132	22	nnred	$⊢ φ \to M! \in ℝ$
133	130	zred	$⊢ φ \to T \in ℝ$
134	22	nngt0d	$⊢ φ \to 0 < M!$
135		fvex	$⊢ M! \in V$
136	135	tpid2	$⊢ M! \in \{\|A (0)\|, M!, I\}$
137		supxrub	$⊢ (\{\|A (0)\|, M!, I\} \subseteq ℝ^{} \land M! \in \{\|A (0)\|, M!, I\}) \to M! \leq sup (\{\|A (0)\|, M!, I\} ℝ^{} <)$
138	126 136 137	sylancl	$⊢ φ \to M! \leq sup (\{\|A (0)\|, M!, I\} ℝ^{*} <)$
139	138 9	breqtrrdi	$⊢ φ \to M! \leq T$
140	131 132 133 134 139	ltletrd	$⊢ φ \to 0 < T$
141		elnnz	$⊢ T \in ℕ \leftrightarrow (T \in ℤ \land 0 < T)$
142	130 140 141	sylanbrc	$⊢ φ \to T \in ℕ$
143		prmunb	$⊢ T \in ℕ \to \exists p \in ℙ T < p$
144	142 143	syl	$⊢ φ \to \exists p \in ℙ T < p$
145	1	3ad2ant1	$⊢ (φ \land p \in ℙ \land T < p) \to Q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
146	2	3ad2ant1	$⊢ (φ \land p \in ℙ \land T < p) \to Q (e) = 0$
147	4	3ad2ant1	$⊢ (φ \land p \in ℙ \land T < p) \to A (0) \neq 0$
148		simp2	$⊢ (φ \land p \in ℙ \land T < p) \to p \in ℙ$
149	16	zcnd	$⊢ φ \to A (0) \in ℂ$
150	149	3ad2ant1	$⊢ (φ \land p \in ℙ \land T < p) \to A (0) \in ℂ$
151	150	abscld	$⊢ (φ \land p \in ℙ \land T < p) \to \|A (0)\| \in ℝ$
152	133	3ad2ant1	$⊢ (φ \land p \in ℙ \land T < p) \to T \in ℝ$
153		prmz	$⊢ p \in ℙ \to p \in ℤ$
154	153	zred	$⊢ p \in ℙ \to p \in ℝ$
155	154	3ad2ant2	$⊢ (φ \land p \in ℙ \land T < p) \to p \in ℝ$
156	126	adantr	$⊢ (φ \land p \in ℙ) \to \{\|A (0)\|, M!, I\} \subseteq ℝ^{*}$
157		fvex	$⊢ \|A (0)\| \in V$
158	157	tpid1	$⊢ \|A (0)\| \in \{\|A (0)\|, M!, I\}$
159		supxrub	$⊢ (\{\|A (0)\|, M!, I\} \subseteq ℝ^{} \land \|A (0)\| \in \{\|A (0)\|, M!, I\}) \to \|A (0)\| \leq sup (\{\|A (0)\|, M!, I\} ℝ^{} <)$
160	156 158 159	sylancl	$⊢ (φ \land p \in ℙ) \to \|A (0)\| \leq sup (\{\|A (0)\|, M!, I\} ℝ^{*} <)$
161	160 9	breqtrrdi	$⊢ (φ \land p \in ℙ) \to \|A (0)\| \leq T$
162	161	3adant3	$⊢ (φ \land p \in ℙ \land T < p) \to \|A (0)\| \leq T$
163		simp3	$⊢ (φ \land p \in ℙ \land T < p) \to T < p$
164	151 152 155 162 163	lelttrd	$⊢ (φ \land p \in ℙ \land T < p) \to \|A (0)\| < p$
165	132	3ad2ant1	$⊢ (φ \land p \in ℙ \land T < p) \to M! \in ℝ$
166	139	3ad2ant1	$⊢ (φ \land p \in ℙ \land T < p) \to M! \leq T$
167	165 152 155 166 163	lelttrd	$⊢ (φ \land p \in ℙ \land T < p) \to M! < p$
168	6	a1i	$⊢ n = p - 1 \to C = \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1}$
169		oveq2	$⊢ n = p - 1 \to {(M^{M + 1})}^{n} = {(M^{M + 1})}^{p - 1}$
170		fveq2	$⊢ n = p - 1 \to n! = (p - 1)!$
171	169 170	oveq12d	$⊢ n = p - 1 \to \frac{{(M^{M + 1})}^{n}}{n!} = \frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!}$
172	168 171	oveq12d	$⊢ n = p - 1 \to C (\frac{{(M^{M + 1})}^{n}}{n!}) = \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!})$
173		prmnn	$⊢ p \in ℙ \to p \in ℕ$
174		nnm1nn0	$⊢ p \in ℕ \to p - 1 \in ℕ_{0}$
175	173 174	syl	$⊢ p \in ℙ \to p - 1 \in ℕ_{0}$
176	175	adantl	$⊢ (φ \land p \in ℙ) \to p - 1 \in ℕ_{0}$
177	61	adantr	$⊢ (φ \land p \in ℙ) \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} \in ℂ$
178	57	adantr	$⊢ (φ \land p \in ℙ) \to M^{M + 1} \in ℂ$
179	178 176	expcld	$⊢ (φ \land p \in ℙ) \to {(M^{M + 1})}^{p - 1} \in ℂ$
180	175	faccld	$⊢ p \in ℙ \to (p - 1)! \in ℕ$
181	180	nncnd	$⊢ p \in ℙ \to (p - 1)! \in ℂ$
182	181	adantl	$⊢ (φ \land p \in ℙ) \to (p - 1)! \in ℂ$
183	180	nnne0d	$⊢ p \in ℙ \to (p - 1)! \neq 0$
184	183	adantl	$⊢ (φ \land p \in ℙ) \to (p - 1)! \neq 0$
185	179 182 184	divcld	$⊢ (φ \land p \in ℙ) \to \frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!} \in ℂ$
186	177 185	mulcld	$⊢ (φ \land p \in ℙ) \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!}) \in ℂ$
187	7 172 176 186	fvmptd3	$⊢ (φ \land p \in ℙ) \to S (p - 1) = \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!})$
188	187	eqcomd	$⊢ (φ \land p \in ℙ) \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!}) = S (p - 1)$
189	188	3adant3	$⊢ (φ \land p \in ℙ \land T < p) \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!}) = S (p - 1)$
190	115	3ad2ant1	$⊢ (φ \land p \in ℙ \land T < p) \to I \in ℤ$
191		1zzd	$⊢ p \in ℙ \to 1 \in ℤ$
192	153 191	zsubcld	$⊢ p \in ℙ \to p - 1 \in ℤ$
193	192	3ad2ant2	$⊢ (φ \land p \in ℙ \land T < p) \to p - 1 \in ℤ$
194	190	zred	$⊢ (φ \land p \in ℙ \land T < p) \to I \in ℝ$
195		tpid3g	$⊢ I \in ℤ \to I \in \{\|A (0)\|, M!, I\}$
196	115 195	syl	$⊢ φ \to I \in \{\|A (0)\|, M!, I\}$
197		supxrub	$⊢ (\{\|A (0)\|, M!, I\} \subseteq ℝ^{} \land I \in \{\|A (0)\|, M!, I\}) \to I \leq sup (\{\|A (0)\|, M!, I\} ℝ^{} <)$
198	126 196 197	syl2anc	$⊢ φ \to I \leq sup (\{\|A (0)\|, M!, I\} ℝ^{*} <)$
199	198 9	breqtrrdi	$⊢ φ \to I \leq T$
200	199	3ad2ant1	$⊢ (φ \land p \in ℙ \land T < p) \to I \leq T$
201	194 152 155 200 163	lelttrd	$⊢ (φ \land p \in ℙ \land T < p) \to I < p$
202	153	3ad2ant2	$⊢ (φ \land p \in ℙ \land T < p) \to p \in ℤ$
203		zltlem1	$⊢ (I \in ℤ \land p \in ℤ) \to (I < p \leftrightarrow I \leq p - 1)$
204	190 202 203	syl2anc	$⊢ (φ \land p \in ℙ \land T < p) \to (I < p \leftrightarrow I \leq p - 1)$
205	201 204	mpbid	$⊢ (φ \land p \in ℙ \land T < p) \to I \leq p - 1$
206		eluz2	$⊢ p - 1 \in ℤ_{\geq I} \leftrightarrow (I \in ℤ \land p - 1 \in ℤ \land I \leq p - 1)$
207	190 193 205 206	syl3anbrc	$⊢ (φ \land p \in ℙ \land T < p) \to p - 1 \in ℤ_{\geq I}$
208	114	3ad2ant1	$⊢ (φ \land p \in ℙ \land T < p) \to I \in \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\}$
209		fveq2	$⊢ i = I \to ℤ_{\geq i} = ℤ_{\geq I}$
210	209	raleqdv	$⊢ i = I \to (\forall n \in ℤ_{\geq i} \|S (n)\| < 1 \leftrightarrow \forall n \in ℤ_{\geq I} \|S (n)\| < 1)$
211	210	elrab	$⊢ I \in \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|S (n)\| < 1\} \leftrightarrow (I \in ℕ_{0} \land \forall n \in ℤ_{\geq I} \|S (n)\| < 1)$
212	208 211	sylib	$⊢ (φ \land p \in ℙ \land T < p) \to (I \in ℕ_{0} \land \forall n \in ℤ_{\geq I} \|S (n)\| < 1)$
213	212	simprd	$⊢ (φ \land p \in ℙ \land T < p) \to \forall n \in ℤ_{\geq I} \|S (n)\| < 1$
214		nfcv	$⊢ \underline{Ⅎ} n abs$
215		nfcv	$⊢ \underline{Ⅎ} n (p - 1)$
216	34 215	nffv	$⊢ \underline{Ⅎ} n S (p - 1)$
217	214 216	nffv	$⊢ \underline{Ⅎ} n \|S (p - 1)\|$
218		nfcv	$⊢ \underline{Ⅎ} n <$
219		nfcv	$⊢ \underline{Ⅎ} n 1$
220	217 218 219	nfbr	$⊢ Ⅎ n \|S (p - 1)\| < 1$
221		2fveq3	$⊢ n = p - 1 \to \|S (n)\| = \|S (p - 1)\|$
222	221	breq1d	$⊢ n = p - 1 \to (\|S (n)\| < 1 \leftrightarrow \|S (p - 1)\| < 1)$
223	220 222	rspc	$⊢ p - 1 \in ℤ_{\geq I} \to (\forall n \in ℤ_{\geq I} \|S (n)\| < 1 \to \|S (p - 1)\| < 1)$
224	207 213 223	sylc	$⊢ (φ \land p \in ℙ \land T < p) \to \|S (p - 1)\| < 1$
225	171	oveq2d	$⊢ n = p - 1 \to C (\frac{{(M^{M + 1})}^{n}}{n!}) = C (\frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!})$
226		ovexd	$⊢ (φ \land p \in ℙ) \to C (\frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!}) \in V$
227	7 225 176 226	fvmptd3	$⊢ (φ \land p \in ℙ) \to S (p - 1) = C (\frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!})$
228	21	nn0red	$⊢ φ \to M \in ℝ$
229	228 56	reexpcld	$⊢ φ \to M^{M + 1} \in ℝ$
230	228 229	remulcld	$⊢ φ \to M M^{M + 1} \in ℝ$
231	230	adantr	$⊢ (φ \land j \in (0 \dots M)) \to M M^{M + 1} \in ℝ$
232	52 231	remulcld	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| M M^{M + 1} \in ℝ$
233	38 232	fsumrecl	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} \in ℝ$
234	6 233	eqeltrid	$⊢ φ \to C \in ℝ$
235	234	adantr	$⊢ (φ \land p \in ℙ) \to C \in ℝ$
236	229	adantr	$⊢ (φ \land p \in ℙ) \to M^{M + 1} \in ℝ$
237	236 176	reexpcld	$⊢ (φ \land p \in ℙ) \to {(M^{M + 1})}^{p - 1} \in ℝ$
238	180	nnred	$⊢ p \in ℙ \to (p - 1)! \in ℝ$
239	238	adantl	$⊢ (φ \land p \in ℙ) \to (p - 1)! \in ℝ$
240	237 239 184	redivcld	$⊢ (φ \land p \in ℙ) \to \frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!} \in ℝ$
241	235 240	remulcld	$⊢ (φ \land p \in ℙ) \to C (\frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!}) \in ℝ$
242	227 241	eqeltrd	$⊢ (φ \land p \in ℙ) \to S (p - 1) \in ℝ$
243	242	3adant3	$⊢ (φ \land p \in ℙ \land T < p) \to S (p - 1) \in ℝ$
244		1red	$⊢ (φ \land p \in ℙ \land T < p) \to 1 \in ℝ$
245	243 244	absltd	$⊢ (φ \land p \in ℙ \land T < p) \to (\|S (p - 1)\| < 1 \leftrightarrow (- 1 < S (p - 1) \land S (p - 1) < 1))$
246	224 245	mpbid	$⊢ (φ \land p \in ℙ \land T < p) \to (- 1 < S (p - 1) \land S (p - 1) < 1)$
247	246	simprd	$⊢ (φ \land p \in ℙ \land T < p) \to S (p - 1) < 1$
248	189 247	eqbrtrd	$⊢ (φ \land p \in ℙ \land T < p) \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{p - 1}}{(p - 1)!}) < 1$
249		etransclem6	$⊢ (y \in ℝ ⟼ y^{p - 1} \prod_{z = 1}^{M} {(y - z)}^{p}) = (x \in ℝ ⟼ x^{p - 1} \prod_{j = 1}^{M} {(x - j)}^{p})$
250		eqid	$⊢ \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} (y \in ℝ ⟼ y^{p - 1} \prod_{z = 1}^{M} {(y - z)}^{p}) (x) d x = \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} (y \in ℝ ⟼ y^{p - 1} \prod_{z = 1}^{M} {(y - z)}^{p}) (x) d x$
251		eqid	$⊢ \frac{\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} (y \in ℝ ⟼ y^{p - 1} \prod_{z = 1}^{M} {(y - z)}^{p}) (x) d x}{(p - 1)!} = \frac{\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} (y \in ℝ ⟼ y^{p - 1} \prod_{z = 1}^{M} {(y - z)}^{p}) (x) d x}{(p - 1)!}$
252	145 146 3 147 5 148 164 167 248 249 250 251	etransclem47	$⊢ (φ \land p \in ℙ \land T < p) \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$
253	252	rexlimdv3a	$⊢ φ \to (\exists p \in ℙ T < p \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1))$
254	144 253	mpd	$⊢ φ \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$

Metamath Proof Explorer

Theorem etransclem48

Proof