Theorem aaliou3lem9 26513

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

Hypotheses

Ref	Expression
aaliou3lem.c	⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))
aaliou3lem.d	⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)
aaliou3lem.e	⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))

Assertion

Ref	Expression
aaliou3lem9	⊢ ¬ 𝐿 ∈ 𝔸

Distinct variable groups:   𝑎,𝑏,𝑐   𝐹,𝑏,𝑐   𝐿,𝑐,𝑎,𝑏

Allowed substitution hints:   𝐹(𝑎)   𝐻(𝑎,𝑏,𝑐)

Proof of Theorem aaliou3lem9

Dummy variables 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		aaliou3lem8 26508	. . . . . 6 ⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) → ∃𝑒 ∈ ℕ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))
2		aaliou3lem.c	. . . . . . . . 9 ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ (2↑-(!‘𝑎)))
3		aaliou3lem.d	. . . . . . . . 9 ⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏)
4		aaliou3lem.e	. . . . . . . . 9 ⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏))
5	2, 3, 4	aaliou3lem6 26511	. . . . . . . 8 ⊢ (𝑒 ∈ ℕ → ((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈ ℤ)
6	5	ad2antrl 740	. . . . . . 7 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈ ℤ)
7		2nn 12309	. . . . . . . 8 ⊢ 2 ∈ ℕ
8		nnnn0 12506	. . . . . . . . . 10 ⊢ (𝑒 ∈ ℕ → 𝑒 ∈ ℕ0)
9	8	ad2antrl 740	. . . . . . . . 9 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝑒 ∈ ℕ0)
10		faccl 14315	. . . . . . . . 9 ⊢ (𝑒 ∈ ℕ0 → (!‘𝑒) ∈ ℕ)
11		nnnn0 12506	. . . . . . . . 9 ⊢ ((!‘𝑒) ∈ ℕ → (!‘𝑒) ∈ ℕ0)
12	9, 10, 11	3syl 19	. . . . . . . 8 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (!‘𝑒) ∈ ℕ0)
13		nnexpcl 14106	. . . . . . . 8 ⊢ ((2 ∈ ℕ ∧ (!‘𝑒) ∈ ℕ0) → (2↑(!‘𝑒)) ∈ ℕ)
14	7, 12, 13	sylancr 598	. . . . . . 7 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ∈ ℕ)
15	2, 3, 4	aaliou3lem5 26510	. . . . . . . . . . . . 13 ⊢ (𝑒 ∈ ℕ → (𝐻‘𝑒) ∈ ℝ)
16	15	ad2antrl 740	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐻‘𝑒) ∈ ℝ)
17	16	recnd 11232	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐻‘𝑒) ∈ ℂ)
18	14	nncnd 12244	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ∈ ℂ)
19	14	nnne0d 12281	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ≠ 0)
20	17, 18, 19	divcan4d 11992	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) = (𝐻‘𝑒))
21	2, 3, 4	aaliou3lem7 26512	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ ℕ → ((𝐻‘𝑒) ≠ 𝐿 ∧ (abs‘(𝐿 − (𝐻‘𝑒))) ≤ (2 · (2↑-(!‘(𝑒 + 1))))))
22	21	simpld 499	. . . . . . . . . . 11 ⊢ (𝑒 ∈ ℕ → (𝐻‘𝑒) ≠ 𝐿)
23	22	ad2antrl 740	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐻‘𝑒) ≠ 𝐿)
24	20, 23	eqnetrd 3025	. . . . . . . . 9 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ≠ 𝐿)
25	24	necomd 3013	. . . . . . . 8 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝐿 ≠ (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))
26	25	neneqd 2963	. . . . . . 7 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))
27	2, 3, 4	aaliou3lem4 26509	. . . . . . . . . . 11 ⊢ 𝐿 ∈ ℝ
28	14	nnred 12243	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ∈ ℝ)
29	16, 28	remulcld 11234	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈ ℝ)
30	29, 14	nndivred 12285	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ∈ ℝ)
31		resubcl 11517	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ ℝ ∧ (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ∈ ℝ) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) ∈ ℝ)
32	27, 30, 31	sylancr 598	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) ∈ ℝ)
33	32	recnd 11232	. . . . . . . . 9 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) ∈ ℂ)
34	33	abscld 15486	. . . . . . . 8 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) ∈ ℝ)
35		simplr 780	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝑏 ∈ ℝ+)
36		nnnn0 12506	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℕ0)
37	36	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝑎 ∈ ℕ0)
38	14, 37	nnexpcld 14277	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((2↑(!‘𝑒))↑𝑎) ∈ ℕ)
39	38	nnrpd 13053	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((2↑(!‘𝑒))↑𝑎) ∈ ℝ+)
40	35, 39	rpdivcld 13072	. . . . . . . . 9 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝑏 / ((2↑(!‘𝑒))↑𝑎)) ∈ ℝ+)
41	40	rpred 13055	. . . . . . . 8 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝑏 / ((2↑(!‘𝑒))↑𝑎)) ∈ ℝ)
42		2rp 13016	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ+
43		peano2nn0 12539	. . . . . . . . . . . . . 14 ⊢ (𝑒 ∈ ℕ0 → (𝑒 + 1) ∈ ℕ0)
44		faccl 14315	. . . . . . . . . . . . . 14 ⊢ ((𝑒 + 1) ∈ ℕ0 → (!‘(𝑒 + 1)) ∈ ℕ)
45	9, 43, 44	3syl 19	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (!‘(𝑒 + 1)) ∈ ℕ)
46		nnz 12607	. . . . . . . . . . . . 13 ⊢ ((!‘(𝑒 + 1)) ∈ ℕ → (!‘(𝑒 + 1)) ∈ ℤ)
47		znegcl 12624	. . . . . . . . . . . . 13 ⊢ ((!‘(𝑒 + 1)) ∈ ℤ → -(!‘(𝑒 + 1)) ∈ ℤ)
48	45, 46, 47	3syl 19	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → -(!‘(𝑒 + 1)) ∈ ℤ)
49		rpexpcl 14112	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ+ ∧ -(!‘(𝑒 + 1)) ∈ ℤ) → (2↑-(!‘(𝑒 + 1))) ∈ ℝ+)
50	42, 48, 49	sylancr 598	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑-(!‘(𝑒 + 1))) ∈ ℝ+)
51		rpmulcl 13036	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ+ ∧ (2↑-(!‘(𝑒 + 1))) ∈ ℝ+) → (2 · (2↑-(!‘(𝑒 + 1)))) ∈ ℝ+)
52	42, 50, 51	sylancr 598	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2 · (2↑-(!‘(𝑒 + 1)))) ∈ ℝ+)
53	52	rpred 13055	. . . . . . . . 9 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2 · (2↑-(!‘(𝑒 + 1)))) ∈ ℝ)
54	20	oveq2d 7426	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) = (𝐿 − (𝐻‘𝑒)))
55	54	fveq2d 6885	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) = (abs‘(𝐿 − (𝐻‘𝑒))))
56	21	simprd 500	. . . . . . . . . . 11 ⊢ (𝑒 ∈ ℕ → (abs‘(𝐿 − (𝐻‘𝑒))) ≤ (2 · (2↑-(!‘(𝑒 + 1)))))
57	56	ad2antrl 740	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (𝐻‘𝑒))) ≤ (2 · (2↑-(!‘(𝑒 + 1)))))
58	55, 57	eqbrtrd 5133	. . . . . . . . 9 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) ≤ (2 · (2↑-(!‘(𝑒 + 1)))))
59		simprr 784	. . . . . . . . 9 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))
60	34, 53, 41, 58, 59	letrd 11362	. . . . . . . 8 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))
61	34, 41, 60	lensymd 11356	. . . . . . 7 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))
62		oveq1 7417	. . . . . . . . . . 11 ⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (𝑓 / 𝑑) = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))
63	62	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (𝐿 = (𝑓 / 𝑑) ↔ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))
64	63	notbid 321	. . . . . . . . 9 ⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (¬ 𝐿 = (𝑓 / 𝑑) ↔ ¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))
65	62	oveq2d 7426	. . . . . . . . . . . 12 ⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (𝐿 − (𝑓 / 𝑑)) = (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))
66	65	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (abs‘(𝐿 − (𝑓 / 𝑑))) = (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))))
67	66	breq2d 5121	. . . . . . . . . 10 ⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → ((𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))) ↔ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))))
68	67	notbid 321	. . . . . . . . 9 ⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))) ↔ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))))
69	64, 68	anbi12d 643	. . . . . . . 8 ⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → ((¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ (¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))))))
70		oveq2 7418	. . . . . . . . . . 11 ⊢ (𝑑 = (2↑(!‘𝑒)) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))
71	70	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑑 = (2↑(!‘𝑒)) → (𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ↔ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))
72	71	notbid 321	. . . . . . . . 9 ⊢ (𝑑 = (2↑(!‘𝑒)) → (¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ↔ ¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))
73		oveq1 7417	. . . . . . . . . . . 12 ⊢ (𝑑 = (2↑(!‘𝑒)) → (𝑑↑𝑎) = ((2↑(!‘𝑒))↑𝑎))
74	73	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝑑 = (2↑(!‘𝑒)) → (𝑏 / (𝑑↑𝑎)) = (𝑏 / ((2↑(!‘𝑒))↑𝑎)))
75	70	oveq2d 7426	. . . . . . . . . . . 12 ⊢ (𝑑 = (2↑(!‘𝑒)) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)) = (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))
76	75	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑑 = (2↑(!‘𝑒)) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) = (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))
77	74, 76	breq12d 5122	. . . . . . . . . 10 ⊢ (𝑑 = (2↑(!‘𝑒)) → ((𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) ↔ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))))
78	77	notbid 321	. . . . . . . . 9 ⊢ (𝑑 = (2↑(!‘𝑒)) → (¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) ↔ ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))))
79	72, 78	anbi12d 643	. . . . . . . 8 ⊢ (𝑑 = (2↑(!‘𝑒)) → ((¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))) ↔ (¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ∧ ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))))
80	69, 79	rspc2ev 3594	. . . . . . 7 ⊢ ((((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈ ℤ ∧ (2↑(!‘𝑒)) ∈ ℕ ∧ (¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ∧ ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))) → ∃𝑓 ∈ ℤ ∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
81	6, 14, 26, 61, 80	syl112anc 1401	. . . . . 6 ⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) ∧ (𝑒 ∈ ℕ ∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ∃𝑓 ∈ ℤ ∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
82	1, 81	rexlimddv 3172	. . . . 5 ⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) → ∃𝑓 ∈ ℤ ∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
83		pm4.56 1004	. . . . . . . . 9 ⊢ ((¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
84	83	rexbii 3112	. . . . . . . 8 ⊢ (∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ∃𝑑 ∈ ℕ ¬ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
85		rexnal 3117	. . . . . . . 8 ⊢ (∃𝑑 ∈ ℕ ¬ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
86	84, 85	bitri 278	. . . . . . 7 ⊢ (∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
87	86	rexbii 3112	. . . . . 6 ⊢ (∃𝑓 ∈ ℤ ∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ∃𝑓 ∈ ℤ ¬ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
88		rexnal 3117	. . . . . 6 ⊢ (∃𝑓 ∈ ℤ ¬ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
89	87, 88	bitri 278	. . . . 5 ⊢ (∃𝑓 ∈ ℤ ∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
90	82, 89	sylib 221	. . . 4 ⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+) → ¬ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
91	90	nrexdv 3160	. . 3 ⊢ (𝑎 ∈ ℕ → ¬ ∃𝑏 ∈ ℝ+ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
92	91	nrex 3093	. 2 ⊢ ¬ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℝ+ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))
93		aaliou2b 26504	. 2 ⊢ (𝐿 ∈ 𝔸 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℝ+ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))))
94	92, 93	mto 200	1 ⊢ ¬ 𝐿 ∈ 𝔸

Syntax hints:  ¬ wn 3   ∧ wa 400   ∨ wo 860   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089   class class class wbr 5109   ↦ cmpt 5192  ‘cfv 6536  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098   · cmul 11100   < clt 11238   ≤ cle 11239   − cmin 11436  -cneg 11437   / cdiv 11866  ℕcn 12228  2c2 12290  ℕ₀cn0 12499  ℤcz 12586  ℝ⁺crp 13011  ...cfz 13530  ↑cexp 14093  !cfa 14305  abscabs 15281  Σcsu 15733  𝔸caa 26475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-inf2 9606  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-pre-sup 11173  ax-addf 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7674  df-om 7859  df-1st 7982  df-2nd 7983  df-supp 8153  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-oadd 8453  df-er 8690  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9318  df-fi 9367  df-sup 9398  df-inf 9399  df-oi 9468  df-dju 9883  df-card 9921  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867  df-nn 12229  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304  df-9 12305  df-n0 12500  df-xnn0 12573  df-z 12587  df-dec 12707  df-uz 12858  df-q 12968  df-rp 13012  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13371  df-ioc 13372  df-ico 13373  df-icc 13374  df-fz 13531  df-fzo 13679  df-fl 13821  df-seq 14034  df-exp 14094  df-fac 14306  df-hash 14363  df-shft 15100  df-cj 15146  df-re 15147  df-im 15148  df-sqrt 15282  df-abs 15283  df-limsup 15518  df-clim 15535  df-rlim 15536  df-sum 15734  df-struct 17202  df-sets 17219  df-slot 17237  df-ndx 17249  df-base 17265  df-ress 17286  df-plusg 17318  df-mulr 17319  df-starv 17320  df-sca 17321  df-vsca 17322  df-ip 17323  df-tset 17324  df-ple 17325  df-ds 17327  df-unif 17328  df-hom 17329  df-cco 17330  df-rest 17470  df-topn 17471  df-0g 17489  df-gsum 17490  df-topgen 17491  df-pt 17492  df-prds 17495  df-xrs 17551  df-qtop 17556  df-imas 17557  df-xps 17559  df-mre 17633  df-mrc 17634  df-acs 17636  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-submnd 18837  df-grp 18998  df-minusg 18999  df-mulg 19129  df-subg 19184  df-cntz 19382  df-cmn 19847  df-abl 19848  df-mgp 20212  df-rng 20226  df-ur 20259  df-ring 20312  df-cring 20313  df-subrng 20645  df-subrg 20669  df-psmet 21514  df-xmet 21515  df-met 21516  df-bl 21517  df-mopn 21518  df-fbas 21519  df-fg 21520  df-cnfld 21523  df-top 23051  df-topon 23068  df-topsp 23090  df-bases 23103  df-cld 23176  df-ntr 23177  df-cls 23178  df-nei 23255  df-lp 23293  df-perf 23294  df-cn 23384  df-cnp 23385  df-haus 23472  df-cmp 23544  df-tx 23719  df-hmeo 23912  df-fil 24003  df-fm 24095  df-flim 24096  df-flf 24097  df-xms 24477  df-ms 24478  df-tms 24479  df-cncf 25037  df-0p 25829  df-limc 26025  df-dv 26026  df-dvn 26027  df-cpn 26028  df-ply 26345  df-idp 26346  df-coe 26347  df-dgr 26348  df-quot 26452  df-aa 26476

This theorem is referenced by:  aaliou3  26514