etransclem47

Description: _e is transcendental. Section *5 of Juillerat p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem47.q	$⊢ φ \to Q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
	etransclem47.qe0	$⊢ φ \to Q (e) = 0$
	etransclem47.a	$⊢ A = coeff (Q)$
	etransclem47.a0	$⊢ φ \to A (0) \neq 0$
	etransclem47.m	$⊢ M = \deg (Q)$
	etransclem47.p	$⊢ φ \to P \in ℙ$
	etransclem47.ap	$⊢ φ \to \|A (0)\| < P$
	etransclem47.mp	$⊢ φ \to M! < P$
	etransclem47.9	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{P - 1}}{(P - 1)!}) < 1$
	etransclem47.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem47.l	$⊢ L = \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x$
	etransclem47.k	$⊢ K = \frac{L}{(P - 1)!}$
Assertion	etransclem47	$⊢ φ \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$

Proof

Step	Hyp	Ref	Expression
1		etransclem47.q	$⊢ φ \to Q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
2		etransclem47.qe0	$⊢ φ \to Q (e) = 0$
3		etransclem47.a	$⊢ A = coeff (Q)$
4		etransclem47.a0	$⊢ φ \to A (0) \neq 0$
5		etransclem47.m	$⊢ M = \deg (Q)$
6		etransclem47.p	$⊢ φ \to P \in ℙ$
7		etransclem47.ap	$⊢ φ \to \|A (0)\| < P$
8		etransclem47.mp	$⊢ φ \to M! < P$
9		etransclem47.9	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{P - 1}}{(P - 1)!}) < 1$
10		etransclem47.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
11		etransclem47.l	$⊢ L = \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x$
12		etransclem47.k	$⊢ K = \frac{L}{(P - 1)!}$
13	12	a1i	$⊢ φ \to K = \frac{L}{(P - 1)!}$
14		ssid	$⊢ ℝ \subseteq ℝ$
15	14	a1i	$⊢ φ \to ℝ \subseteq ℝ$
16		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
17	16	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
18		reopn	$⊢ ℝ \in topGen (ran (.))$
19		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
20	19	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
21	18 20	eleqtri	$⊢ ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
22	21	a1i	$⊢ φ \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
23		prmnn	$⊢ P \in ℙ \to P \in ℕ$
24	6 23	syl	$⊢ φ \to P \in ℕ$
25		eqid	$⊢ M P + P - 1 = M P + P - 1$
26		fveq2	$⊢ y = x \to (ℝ D^{n} F) (i) (y) = (ℝ D^{n} F) (i) (x)$
27	26	sumeq2sdv	$⊢ y = x \to \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y) = \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (x)$
28	27	cbvmptv	$⊢ (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) = (x \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (x))$
29		negeq	$⊢ z = x \to - z = - x$
30	29	oveq2d	$⊢ z = x \to e^{- z} = e^{- x}$
31		fveq2	$⊢ z = x \to (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (z) = (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (x)$
32	30 31	oveq12d	$⊢ z = x \to e^{- z} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (z) = e^{- x} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (x)$
33	32	negeqd	$⊢ z = x \to - e^{- z} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (z) = - e^{- x} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (x)$
34	33	cbvmptv	$⊢ (z \in [0, j] ⟼ - e^{- z} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (z)) = (x \in [0, j] ⟼ - e^{- x} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (x))$
35	1 2 3 5 15 17 22 24 10 11 25 28 34	etransclem46	$⊢ φ \to \frac{L}{(P - 1)!} = \frac{- \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
36		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
37		fzfid	$⊢ φ \to (0 \dots M P + P - 1) \in Fin$
38		xpfi	$⊢ ((0 \dots M) \in Fin \land (0 \dots M P + P - 1) \in Fin) \to (0 \dots M) \times (0 \dots M P + P - 1) \in Fin$
39	36 37 38	syl2anc	$⊢ φ \to (0 \dots M) \times (0 \dots M P + P - 1) \in Fin$
40	1	eldifad	$⊢ φ \to Q \in Poly (ℤ)$
41		0zd	$⊢ φ \to 0 \in ℤ$
42	3	coef2	$⊢ (Q \in Poly (ℤ) \land 0 \in ℤ) \to A : ℕ_{0} ⟶ ℤ$
43	40 41 42	syl2anc	$⊢ φ \to A : ℕ_{0} ⟶ ℤ$
44	43	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A : ℕ_{0} ⟶ ℤ$
45		xp1st	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 1^{st} (k) \in (0 \dots M)$
46		elfznn0	$⊢ 1^{st} (k) \in (0 \dots M) \to 1^{st} (k) \in ℕ_{0}$
47	45 46	syl	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 1^{st} (k) \in ℕ_{0}$
48	47	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to 1^{st} (k) \in ℕ_{0}$
49	44 48	ffvelrnd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A (1^{st} (k)) \in ℤ$
50	49	zcnd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A (1^{st} (k)) \in ℂ$
51	16	a1i	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to ℝ \in \{ℝ, ℂ\}$
52	21	a1i	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
53	24	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to P \in ℕ$
54		dgrcl	$⊢ Q \in Poly (ℤ) \to \deg (Q) \in ℕ_{0}$
55	40 54	syl	$⊢ φ \to \deg (Q) \in ℕ_{0}$
56	5 55	eqeltrid	$⊢ φ \to M \in ℕ_{0}$
57	56	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to M \in ℕ_{0}$
58		xp2nd	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 2^{nd} (k) \in (0 \dots M P + P - 1)$
59		elfznn0	$⊢ 2^{nd} (k) \in (0 \dots M P + P - 1) \to 2^{nd} (k) \in ℕ_{0}$
60	58 59	syl	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 2^{nd} (k) \in ℕ_{0}$
61	60	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to 2^{nd} (k) \in ℕ_{0}$
62	51 52 53 57 10 61	etransclem33	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to (ℝ D^{n} F) (2^{nd} (k)) : ℝ ⟶ ℂ$
63	48	nn0red	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to 1^{st} (k) \in ℝ$
64	62 63	ffvelrnd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
65	50 64	mulcld	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
66	39 65	fsumcl	$⊢ φ \to \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
67		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
68	24 67	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
69	68	faccld	$⊢ φ \to (P - 1)! \in ℕ$
70	69	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
71	69	nnne0d	$⊢ φ \to (P - 1)! \neq 0$
72	66 70 71	divnegd	$⊢ φ \to - \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = \frac{- \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
73	72	eqcomd	$⊢ φ \to \frac{- \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = - \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
74	13 35 73	3eqtrd	$⊢ φ \to K = - \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
75		eqid	$⊢ \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
76	24 56 10 43 75	etransclem45	$⊢ φ \to \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ$
77	76	znegcld	$⊢ φ \to - \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ$
78	74 77	eqeltrd	$⊢ φ \to K \in ℤ$
79	12 35	eqtrid	$⊢ φ \to K = \frac{- \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
80	66 70 71	divcld	$⊢ φ \to \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℂ$
81	43 4 56 6 7 8 10 75	etransclem44	$⊢ φ \to \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \neq 0$
82	80 81	negne0d	$⊢ φ \to - \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \neq 0$
83	73 82	eqnetrd	$⊢ φ \to \frac{- \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \neq 0$
84	79 83	eqnetrd	$⊢ φ \to K \neq 0$
85		eldifsni	$⊢ Q \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \to Q \neq 0_{𝑝}$
86	1 85	syl	$⊢ φ \to Q \neq 0_{𝑝}$
87		ere	$⊢ e \in ℝ$
88	87	recni	$⊢ e \in ℂ$
89	88	a1i	$⊢ φ \to e \in ℂ$
90		dgrnznn	$⊢ ((Q \in Poly (ℤ) \land Q \neq 0_{𝑝}) \land (e \in ℂ \land Q (e) = 0)) \to \deg (Q) \in ℕ$
91	40 86 89 2 90	syl22anc	$⊢ φ \to \deg (Q) \in ℕ$
92	5 91	eqeltrid	$⊢ φ \to M \in ℕ$
93	43 11 12 24 92 10 9	etransclem23	$⊢ φ \to \|K\| < 1$
94		neeq1	$⊢ k = K \to (k \neq 0 \leftrightarrow K \neq 0)$
95		fveq2	$⊢ k = K \to \|k\| = \|K\|$
96	95	breq1d	$⊢ k = K \to (\|k\| < 1 \leftrightarrow \|K\| < 1)$
97	94 96	anbi12d	$⊢ k = K \to ((k \neq 0 \land \|k\| < 1) \leftrightarrow (K \neq 0 \land \|K\| < 1))$
98	97	rspcev	$⊢ (K \in ℤ \land (K \neq 0 \land \|K\| < 1)) \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$
99	78 84 93 98	syl12anc	$⊢ φ \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$

Metamath Proof Explorer

Theorem etransclem47

Proof