aaliou3lem9

Description: Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014)

	Ref	Expression
Hypotheses	aaliou3lem.c	$⊢ F = (a \in ℕ ⟼ 2^{- a!})$
	aaliou3lem.d	$⊢ L = \sum_{b \in ℕ} F (b)$
	aaliou3lem.e	$⊢ H = (c \in ℕ ⟼ \sum_{b = 1}^{c} F (b))$
Assertion	aaliou3lem9	$⊢ \neg L \in 𝔸$

Proof

Step	Hyp	Ref	Expression
1		aaliou3lem.c	$⊢ F = (a \in ℕ ⟼ 2^{- a!})$
2		aaliou3lem.d	$⊢ L = \sum_{b \in ℕ} F (b)$
3		aaliou3lem.e	$⊢ H = (c \in ℕ ⟼ \sum_{b = 1}^{c} F (b))$
4		aaliou3lem8	$⊢ (a \in ℕ \land b \in ℝ^{+}) \to \exists e \in ℕ 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}}$
5	1 2 3	aaliou3lem6	$⊢ e \in ℕ \to H (e) 2^{e!} \in ℤ$
6	5	ad2antrl	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to H (e) 2^{e!} \in ℤ$
7		2nn	$⊢ 2 \in ℕ$
8		nnnn0	$⊢ e \in ℕ \to e \in ℕ_{0}$
9	8	ad2antrl	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to e \in ℕ_{0}$
10		faccl	$⊢ e \in ℕ_{0} \to e! \in ℕ$
11		nnnn0	$⊢ e! \in ℕ \to e! \in ℕ_{0}$
12	9 10 11	3syl	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to e! \in ℕ_{0}$
13		nnexpcl	$⊢ (2 \in ℕ \land e! \in ℕ_{0}) \to 2^{e!} \in ℕ$
14	7 12 13	sylancr	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to 2^{e!} \in ℕ$
15	1 2 3	aaliou3lem5	$⊢ e \in ℕ \to H (e) \in ℝ$
16	15	ad2antrl	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to H (e) \in ℝ$
17	16	recnd	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to H (e) \in ℂ$
18	14	nncnd	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to 2^{e!} \in ℂ$
19	14	nnne0d	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to 2^{e!} \neq 0$
20	17 18 19	divcan4d	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \frac{H (e) 2^{e!}}{2^{e!}} = H (e)$
21	1 2 3	aaliou3lem7	$⊢ e \in ℕ \to (H (e) \neq L \land \|L - H (e)\| \leq 2 2^{- (e + 1)!})$
22	21	simpld	$⊢ e \in ℕ \to H (e) \neq L$
23	22	ad2antrl	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to H (e) \neq L$
24	20 23	eqnetrd	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \frac{H (e) 2^{e!}}{2^{e!}} \neq L$
25	24	necomd	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to L \neq \frac{H (e) 2^{e!}}{2^{e!}}$
26	25	neneqd	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \neg L = \frac{H (e) 2^{e!}}{2^{e!}}$
27	1 2 3	aaliou3lem4	$⊢ L \in ℝ$
28	14	nnred	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to 2^{e!} \in ℝ$
29	16 28	remulcld	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to H (e) 2^{e!} \in ℝ$
30	29 14	nndivred	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \frac{H (e) 2^{e!}}{2^{e!}} \in ℝ$
31		resubcl	$⊢ (L \in ℝ \land \frac{H (e) 2^{e!}}{2^{e!}} \in ℝ) \to L - (\frac{H (e) 2^{e!}}{2^{e!}}) \in ℝ$
32	27 30 31	sylancr	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to L - (\frac{H (e) 2^{e!}}{2^{e!}}) \in ℝ$
33	32	recnd	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to L - (\frac{H (e) 2^{e!}}{2^{e!}}) \in ℂ$
34	33	abscld	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \|L - (\frac{H (e) 2^{e!}}{2^{e!}})\| \in ℝ$
35		simplr	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to b \in ℝ^{+}$
36		nnnn0	$⊢ a \in ℕ \to a \in ℕ_{0}$
37	36	ad2antrr	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to a \in ℕ_{0}$
38	14 37	nnexpcld	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to {(2^{e!})}^{a} \in ℕ$
39	38	nnrpd	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to {(2^{e!})}^{a} \in ℝ^{+}$
40	35 39	rpdivcld	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \frac{b}{{(2^{e!})}^{a}} \in ℝ^{+}$
41	40	rpred	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \frac{b}{{(2^{e!})}^{a}} \in ℝ$
42		2rp	$⊢ 2 \in ℝ^{+}$
43		peano2nn0	$⊢ e \in ℕ_{0} \to e + 1 \in ℕ_{0}$
44		faccl	$⊢ e + 1 \in ℕ_{0} \to (e + 1)! \in ℕ$
45	9 43 44	3syl	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to (e + 1)! \in ℕ$
46		nnz	$⊢ (e + 1)! \in ℕ \to (e + 1)! \in ℤ$
47		znegcl	$⊢ (e + 1)! \in ℤ \to - (e + 1)! \in ℤ$
48	45 46 47	3syl	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to - (e + 1)! \in ℤ$
49		rpexpcl	$⊢ (2 \in ℝ^{+} \land - (e + 1)! \in ℤ) \to 2^{- (e + 1)!} \in ℝ^{+}$
50	42 48 49	sylancr	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to 2^{- (e + 1)!} \in ℝ^{+}$
51		rpmulcl	$⊢ (2 \in ℝ^{+} \land 2^{- (e + 1)!} \in ℝ^{+}) \to 2 2^{- (e + 1)!} \in ℝ^{+}$
52	42 50 51	sylancr	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to 2 2^{- (e + 1)!} \in ℝ^{+}$
53	52	rpred	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to 2 2^{- (e + 1)!} \in ℝ$
54	20	oveq2d	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to L - (\frac{H (e) 2^{e!}}{2^{e!}}) = L - H (e)$
55	54	fveq2d	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \|L - (\frac{H (e) 2^{e!}}{2^{e!}})\| = \|L - H (e)\|$
56	21	simprd	$⊢ e \in ℕ \to \|L - H (e)\| \leq 2 2^{- (e + 1)!}$
57	56	ad2antrl	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \|L - H (e)\| \leq 2 2^{- (e + 1)!}$
58	55 57	eqbrtrd	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \|L - (\frac{H (e) 2^{e!}}{2^{e!}})\| \leq 2 2^{- (e + 1)!}$
59		simprr	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}}$
60	34 53 41 58 59	letrd	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \|L - (\frac{H (e) 2^{e!}}{2^{e!}})\| \leq \frac{b}{{(2^{e!})}^{a}}$
61	34 41 60	lensymd	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \neg \frac{b}{{(2^{e!})}^{a}} < \|L - (\frac{H (e) 2^{e!}}{2^{e!}})\|$
62		oveq1	$⊢ f = H (e) 2^{e!} \to \frac{f}{d} = \frac{H (e) 2^{e!}}{d}$
63	62	eqeq2d	$⊢ f = H (e) 2^{e!} \to (L = \frac{f}{d} \leftrightarrow L = \frac{H (e) 2^{e!}}{d})$
64	63	notbid	$⊢ f = H (e) 2^{e!} \to (\neg L = \frac{f}{d} \leftrightarrow \neg L = \frac{H (e) 2^{e!}}{d})$
65	62	oveq2d	$⊢ f = H (e) 2^{e!} \to L - (\frac{f}{d}) = L - (\frac{H (e) 2^{e!}}{d})$
66	65	fveq2d	$⊢ f = H (e) 2^{e!} \to \|L - (\frac{f}{d})\| = \|L - (\frac{H (e) 2^{e!}}{d})\|$
67	66	breq2d	$⊢ f = H (e) 2^{e!} \to (\frac{b}{d^{a}} < \|L - (\frac{f}{d})\| \leftrightarrow \frac{b}{d^{a}} < \|L - (\frac{H (e) 2^{e!}}{d})\|)$
68	67	notbid	$⊢ f = H (e) 2^{e!} \to (\neg \frac{b}{d^{a}} < \|L - (\frac{f}{d})\| \leftrightarrow \neg \frac{b}{d^{a}} < \|L - (\frac{H (e) 2^{e!}}{d})\|)$
69	64 68	anbi12d	$⊢ f = H (e) 2^{e!} \to ((\neg L = \frac{f}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|) \leftrightarrow (\neg L = \frac{H (e) 2^{e!}}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{H (e) 2^{e!}}{d})\|))$
70		oveq2	$⊢ d = 2^{e!} \to \frac{H (e) 2^{e!}}{d} = \frac{H (e) 2^{e!}}{2^{e!}}$
71	70	eqeq2d	$⊢ d = 2^{e!} \to (L = \frac{H (e) 2^{e!}}{d} \leftrightarrow L = \frac{H (e) 2^{e!}}{2^{e!}})$
72	71	notbid	$⊢ d = 2^{e!} \to (\neg L = \frac{H (e) 2^{e!}}{d} \leftrightarrow \neg L = \frac{H (e) 2^{e!}}{2^{e!}})$
73		oveq1	$⊢ d = 2^{e!} \to d^{a} = {(2^{e!})}^{a}$
74	73	oveq2d	$⊢ d = 2^{e!} \to \frac{b}{d^{a}} = \frac{b}{{(2^{e!})}^{a}}$
75	70	oveq2d	$⊢ d = 2^{e!} \to L - (\frac{H (e) 2^{e!}}{d}) = L - (\frac{H (e) 2^{e!}}{2^{e!}})$
76	75	fveq2d	$⊢ d = 2^{e!} \to \|L - (\frac{H (e) 2^{e!}}{d})\| = \|L - (\frac{H (e) 2^{e!}}{2^{e!}})\|$
77	74 76	breq12d	$⊢ d = 2^{e!} \to (\frac{b}{d^{a}} < \|L - (\frac{H (e) 2^{e!}}{d})\| \leftrightarrow \frac{b}{{(2^{e!})}^{a}} < \|L - (\frac{H (e) 2^{e!}}{2^{e!}})\|)$
78	77	notbid	$⊢ d = 2^{e!} \to (\neg \frac{b}{d^{a}} < \|L - (\frac{H (e) 2^{e!}}{d})\| \leftrightarrow \neg \frac{b}{{(2^{e!})}^{a}} < \|L - (\frac{H (e) 2^{e!}}{2^{e!}})\|)$
79	72 78	anbi12d	$⊢ d = 2^{e!} \to ((\neg L = \frac{H (e) 2^{e!}}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{H (e) 2^{e!}}{d})\|) \leftrightarrow (\neg L = \frac{H (e) 2^{e!}}{2^{e!}} \land \neg \frac{b}{{(2^{e!})}^{a}} < \|L - (\frac{H (e) 2^{e!}}{2^{e!}})\|))$
80	69 79	rspc2ev	$⊢ (H (e) 2^{e!} \in ℤ \land 2^{e!} \in ℕ \land (\neg L = \frac{H (e) 2^{e!}}{2^{e!}} \land \neg \frac{b}{{(2^{e!})}^{a}} < \|L - (\frac{H (e) 2^{e!}}{2^{e!}})\|)) \to \exists f \in ℤ \exists d \in ℕ (\neg L = \frac{f}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
81	6 14 26 61 80	syl112anc	$⊢ ((a \in ℕ \land b \in ℝ^{+}) \land (e \in ℕ \land 2 2^{- (e + 1)!} \leq \frac{b}{{(2^{e!})}^{a}})) \to \exists f \in ℤ \exists d \in ℕ (\neg L = \frac{f}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
82	4 81	rexlimddv	$⊢ (a \in ℕ \land b \in ℝ^{+}) \to \exists f \in ℤ \exists d \in ℕ (\neg L = \frac{f}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
83		pm4.56	$⊢ (\neg L = \frac{f}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|) \leftrightarrow \neg (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
84	83	rexbii	$⊢ \exists d \in ℕ (\neg L = \frac{f}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|) \leftrightarrow \exists d \in ℕ \neg (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
85		rexnal	$⊢ \exists d \in ℕ \neg (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|) \leftrightarrow \neg \forall d \in ℕ (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
86	84 85	bitri	$⊢ \exists d \in ℕ (\neg L = \frac{f}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|) \leftrightarrow \neg \forall d \in ℕ (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
87	86	rexbii	$⊢ \exists f \in ℤ \exists d \in ℕ (\neg L = \frac{f}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|) \leftrightarrow \exists f \in ℤ \neg \forall d \in ℕ (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
88		rexnal	$⊢ \exists f \in ℤ \neg \forall d \in ℕ (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|) \leftrightarrow \neg \forall f \in ℤ \forall d \in ℕ (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
89	87 88	bitri	$⊢ \exists f \in ℤ \exists d \in ℕ (\neg L = \frac{f}{d} \land \neg \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|) \leftrightarrow \neg \forall f \in ℤ \forall d \in ℕ (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
90	82 89	sylib	$⊢ (a \in ℕ \land b \in ℝ^{+}) \to \neg \forall f \in ℤ \forall d \in ℕ (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
91	90	nrexdv	$⊢ a \in ℕ \to \neg \exists b \in ℝ^{+} \forall f \in ℤ \forall d \in ℕ (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
92	91	nrex	$⊢ \neg \exists a \in ℕ \exists b \in ℝ^{+} \forall f \in ℤ \forall d \in ℕ (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
93		aaliou2b	$⊢ L \in 𝔸 \to \exists a \in ℕ \exists b \in ℝ^{+} \forall f \in ℤ \forall d \in ℕ (L = \frac{f}{d} \lor \frac{b}{d^{a}} < \|L - (\frac{f}{d})\|)$
94	92 93	mto	$⊢ \neg L \in 𝔸$

Metamath Proof Explorer

Theorem aaliou3lem9

Proof