Metamath Proof Explorer

Theorem 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 ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
aaliou3lem.d ⊢ 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 )
aaliou3lem.e ⊢ 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) )
Assertion aaliou3lem9 ¬ 𝐿 ∈ 𝔸

Proof

Step Hyp Ref Expression
1 aaliou3lem.c ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
2 aaliou3lem.d ⊢ 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 )
3 aaliou3lem.e ⊢ 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) )
4 aaliou3lem8 ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) → ∃ 𝑒 ∈ ℕ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) )
5 1 2 3 aaliou3lem6 ⊢ ( 𝑒 ∈ ℕ → ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ∈ ℤ )
6 5 ad2antrl ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ∈ ℤ )
7 2nn ⊢ 2 ∈ ℕ
8 nnnn0 ⊢ ( 𝑒 ∈ ℕ → 𝑒 ∈ ℕ0 )
9 8 ad2antrl ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → 𝑒 ∈ ℕ0 )
10 faccl ⊢ ( 𝑒 ∈ ℕ0 → ( ! ‘ 𝑒 ) ∈ ℕ )
11 nnnn0 ⊢ ( ( ! ‘ 𝑒 ) ∈ ℕ → ( ! ‘ 𝑒 ) ∈ ℕ0 )
12 9 10 11 3syl ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( ! ‘ 𝑒 ) ∈ ℕ0 )
13 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ ( ! ‘ 𝑒 ) ∈ ℕ0 ) → ( 2 ↑ ( ! ‘ 𝑒 ) ) ∈ ℕ )
14 7 12 13 sylancr ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 2 ↑ ( ! ‘ 𝑒 ) ) ∈ ℕ )
15 1 2 3 aaliou3lem5 ⊢ ( 𝑒 ∈ ℕ → ( 𝐻 ‘ 𝑒 ) ∈ ℝ )
16 15 ad2antrl ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 𝐻 ‘ 𝑒 ) ∈ ℝ )
17 16 recnd ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 𝐻 ‘ 𝑒 ) ∈ ℂ )
18 14 nncnd ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 2 ↑ ( ! ‘ 𝑒 ) ) ∈ ℂ )
19 14 nnne0d ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 2 ↑ ( ! ‘ 𝑒 ) ) ≠ 0 )
20 17 18 19 divcan4d ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) = ( 𝐻 ‘ 𝑒 ) )
21 1 2 3 aaliou3lem7 ⊢ ( 𝑒 ∈ ℕ → ( ( 𝐻 ‘ 𝑒 ) ≠ 𝐿 ∧ ( abs ‘ ( 𝐿 − ( 𝐻 ‘ 𝑒 ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ) )
22 21 simpld ⊢ ( 𝑒 ∈ ℕ → ( 𝐻 ‘ 𝑒 ) ≠ 𝐿 )
23 22 ad2antrl ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 𝐻 ‘ 𝑒 ) ≠ 𝐿 )
24 20 23 eqnetrd ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ≠ 𝐿 )
25 24 necomd ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → 𝐿 ≠ ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) )
26 25 neneqd ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ¬ 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) )
27 1 2 3 aaliou3lem4 ⊢ 𝐿 ∈ ℝ
28 14 nnred ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 2 ↑ ( ! ‘ 𝑒 ) ) ∈ ℝ )
29 16 28 remulcld ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ∈ ℝ )
30 29 14 nndivred ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ∈ ℝ )
31 resubcl ⊢ ( ( 𝐿 ∈ ℝ ∧ ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ∈ ℝ ) → ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ∈ ℝ )
32 27 30 31 sylancr ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ∈ ℝ )
33 32 recnd ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ∈ ℂ )
34 33 abscld ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ) ∈ ℝ )
35 simplr ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → 𝑏 ∈ ℝ+ )
36 nnnn0 ⊢ ( 𝑎 ∈ ℕ → 𝑎 ∈ ℕ0 )
37 36 ad2antrr ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → 𝑎 ∈ ℕ0 )
38 14 37 nnexpcld ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ∈ ℕ )
39 38 nnrpd ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ∈ ℝ+ )
40 35 39 rpdivcld ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ∈ ℝ+ )
41 40 rpred ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ∈ ℝ )
42 2rp ⊢ 2 ∈ ℝ+
43 peano2nn0 ⊢ ( 𝑒 ∈ ℕ0 → ( 𝑒 + 1 ) ∈ ℕ0 )
44 faccl ⊢ ( ( 𝑒 + 1 ) ∈ ℕ0 → ( ! ‘ ( 𝑒 + 1 ) ) ∈ ℕ )
45 9 43 44 3syl ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( ! ‘ ( 𝑒 + 1 ) ) ∈ ℕ )
46 nnz ⊢ ( ( ! ‘ ( 𝑒 + 1 ) ) ∈ ℕ → ( ! ‘ ( 𝑒 + 1 ) ) ∈ ℤ )
47 znegcl ⊢ ( ( ! ‘ ( 𝑒 + 1 ) ) ∈ ℤ → - ( ! ‘ ( 𝑒 + 1 ) ) ∈ ℤ )
48 45 46 47 3syl ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → - ( ! ‘ ( 𝑒 + 1 ) ) ∈ ℤ )
49 rpexpcl ⊢ ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ ( 𝑒 + 1 ) ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ∈ ℝ+ )
50 42 48 49 sylancr ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ∈ ℝ+ )
51 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ∈ ℝ+ ) → ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ∈ ℝ+ )
52 42 50 51 sylancr ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ∈ ℝ+ )
53 52 rpred ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ∈ ℝ )
54 20 oveq2d ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) = ( 𝐿 − ( 𝐻 ‘ 𝑒 ) ) )
55 54 fveq2d ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ) = ( abs ‘ ( 𝐿 − ( 𝐻 ‘ 𝑒 ) ) ) )
56 21 simprd ⊢ ( 𝑒 ∈ ℕ → ( abs ‘ ( 𝐿 − ( 𝐻 ‘ 𝑒 ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) )
57 56 ad2antrl ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( abs ‘ ( 𝐿 − ( 𝐻 ‘ 𝑒 ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) )
58 55 57 eqbrtrd ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) )
59 simprr ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) )
60 34 53 41 58 59 letrd ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) )
61 34 41 60 lensymd ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ¬ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ) )
62 oveq1 ⊢ ( 𝑓 = ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) → ( 𝑓 / 𝑑 ) = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) )
63 62 eqeq2d ⊢ ( 𝑓 = ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) → ( 𝐿 = ( 𝑓 / 𝑑 ) ↔ 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) )
64 63 notbid ⊢ ( 𝑓 = ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) → ( ¬ 𝐿 = ( 𝑓 / 𝑑 ) ↔ ¬ 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) )
65 62 oveq2d ⊢ ( 𝑓 = ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) → ( 𝐿 − ( 𝑓 / 𝑑 ) ) = ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) )
66 65 fveq2d ⊢ ( 𝑓 = ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) → ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) = ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) ) )
67 66 breq2d ⊢ ( 𝑓 = ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) → ( ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ↔ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) ) ) )
68 67 notbid ⊢ ( 𝑓 = ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) → ( ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ↔ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) ) ) )
69 64 68 anbi12d ⊢ ( 𝑓 = ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) → ( ( ¬ 𝐿 = ( 𝑓 / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) ↔ ( ¬ 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) ) ) ) )
70 oveq2 ⊢ ( 𝑑 = ( 2 ↑ ( ! ‘ 𝑒 ) ) → ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) )
71 70 eqeq2d ⊢ ( 𝑑 = ( 2 ↑ ( ! ‘ 𝑒 ) ) → ( 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ↔ 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) )
72 71 notbid ⊢ ( 𝑑 = ( 2 ↑ ( ! ‘ 𝑒 ) ) → ( ¬ 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ↔ ¬ 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) )
73 oveq1 ⊢ ( 𝑑 = ( 2 ↑ ( ! ‘ 𝑒 ) ) → ( 𝑑 ↑ 𝑎 ) = ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) )
74 73 oveq2d ⊢ ( 𝑑 = ( 2 ↑ ( ! ‘ 𝑒 ) ) → ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) = ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) )
75 70 oveq2d ⊢ ( 𝑑 = ( 2 ↑ ( ! ‘ 𝑒 ) ) → ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) = ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) )
76 75 fveq2d ⊢ ( 𝑑 = ( 2 ↑ ( ! ‘ 𝑒 ) ) → ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) ) = ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ) )
77 74 76 breq12d ⊢ ( 𝑑 = ( 2 ↑ ( ! ‘ 𝑒 ) ) → ( ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) ) ↔ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ) ) )
78 77 notbid ⊢ ( 𝑑 = ( 2 ↑ ( ! ‘ 𝑒 ) ) → ( ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) ) ↔ ¬ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ) ) )
79 72 78 anbi12d ⊢ ( 𝑑 = ( 2 ↑ ( ! ‘ 𝑒 ) ) → ( ( ¬ 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / 𝑑 ) ) ) ) ↔ ( ¬ 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ∧ ¬ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ) ) ) )
80 69 79 rspc2ev ⊢ ( ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ∈ ℤ ∧ ( 2 ↑ ( ! ‘ 𝑒 ) ) ∈ ℕ ∧ ( ¬ 𝐿 = ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ∧ ¬ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( ( ( 𝐻 ‘ 𝑒 ) · ( 2 ↑ ( ! ‘ 𝑒 ) ) ) / ( 2 ↑ ( ! ‘ 𝑒 ) ) ) ) ) ) ) → ∃ 𝑓 ∈ ℤ ∃ 𝑑 ∈ ℕ ( ¬ 𝐿 = ( 𝑓 / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
81 6 14 26 61 80 syl112anc ⊢ ( ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑒 + 1 ) ) ) ) ≤ ( 𝑏 / ( ( 2 ↑ ( ! ‘ 𝑒 ) ) ↑ 𝑎 ) ) ) ) → ∃ 𝑓 ∈ ℤ ∃ 𝑑 ∈ ℕ ( ¬ 𝐿 = ( 𝑓 / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
82 4 81 rexlimddv ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) → ∃ 𝑓 ∈ ℤ ∃ 𝑑 ∈ ℕ ( ¬ 𝐿 = ( 𝑓 / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
83 pm4.56 ⊢ ( ( ¬ 𝐿 = ( 𝑓 / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) ↔ ¬ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
84 83 rexbii ⊢ ( ∃ 𝑑 ∈ ℕ ( ¬ 𝐿 = ( 𝑓 / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) ↔ ∃ 𝑑 ∈ ℕ ¬ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
85 rexnal ⊢ ( ∃ 𝑑 ∈ ℕ ¬ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) ↔ ¬ ∀ 𝑑 ∈ ℕ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
86 84 85 bitri ⊢ ( ∃ 𝑑 ∈ ℕ ( ¬ 𝐿 = ( 𝑓 / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) ↔ ¬ ∀ 𝑑 ∈ ℕ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
87 86 rexbii ⊢ ( ∃ 𝑓 ∈ ℤ ∃ 𝑑 ∈ ℕ ( ¬ 𝐿 = ( 𝑓 / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) ↔ ∃ 𝑓 ∈ ℤ ¬ ∀ 𝑑 ∈ ℕ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
88 rexnal ⊢ ( ∃ 𝑓 ∈ ℤ ¬ ∀ 𝑑 ∈ ℕ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) ↔ ¬ ∀ 𝑓 ∈ ℤ ∀ 𝑑 ∈ ℕ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
89 87 88 bitri ⊢ ( ∃ 𝑓 ∈ ℤ ∃ 𝑑 ∈ ℕ ( ¬ 𝐿 = ( 𝑓 / 𝑑 ) ∧ ¬ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) ↔ ¬ ∀ 𝑓 ∈ ℤ ∀ 𝑑 ∈ ℕ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
90 82 89 sylib ⊢ ( ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+ ) → ¬ ∀ 𝑓 ∈ ℤ ∀ 𝑑 ∈ ℕ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
91 90 nrexdv ⊢ ( 𝑎 ∈ ℕ → ¬ ∃ 𝑏 ∈ ℝ+ ∀ 𝑓 ∈ ℤ ∀ 𝑑 ∈ ℕ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
92 91 nrex ⊢ ¬ ∃ 𝑎 ∈ ℕ ∃ 𝑏 ∈ ℝ+ ∀ 𝑓 ∈ ℤ ∀ 𝑑 ∈ ℕ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) )
93 aaliou2b ⊢ ( 𝐿 ∈ 𝔸 → ∃ 𝑎 ∈ ℕ ∃ 𝑏 ∈ ℝ+ ∀ 𝑓 ∈ ℤ ∀ 𝑑 ∈ ℕ ( 𝐿 = ( 𝑓 / 𝑑 ) ∨ ( 𝑏 / ( 𝑑 ↑ 𝑎 ) ) < ( abs ‘ ( 𝐿 − ( 𝑓 / 𝑑 ) ) ) ) )
94 92 93 mto ⊢ ¬ 𝐿 ∈ 𝔸