Metamath Proof Explorer


Theorem aaliou3lem7

Description: Lemma for aaliou3 . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypotheses aaliou3lem.c 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
aaliou3lem.d 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹𝑏 )
aaliou3lem.e 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹𝑏 ) )
Assertion aaliou3lem7 ( 𝐴 ∈ ℕ → ( ( 𝐻𝐴 ) ≠ 𝐿 ∧ ( abs ‘ ( 𝐿 − ( 𝐻𝐴 ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 aaliou3lem.c 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
2 aaliou3lem.d 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹𝑏 )
3 aaliou3lem.e 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹𝑏 ) )
4 peano2nn ( 𝐴 ∈ ℕ → ( 𝐴 + 1 ) ∈ ℕ )
5 eqid ( 𝑐 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ↦ ( ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − ( 𝐴 + 1 ) ) ) ) ) = ( 𝑐 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ↦ ( ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − ( 𝐴 + 1 ) ) ) ) )
6 5 1 aaliou3lem3 ( ( 𝐴 + 1 ) ∈ ℕ → ( seq ( 𝐴 + 1 ) ( + , 𝐹 ) ∈ dom ⇝ ∧ Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) )
7 3simpc ( ( seq ( 𝐴 + 1 ) ( + , 𝐹 ) ∈ dom ⇝ ∧ Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) → ( Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) )
8 4 6 7 3syl ( 𝐴 ∈ ℕ → ( Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) )
9 nncn ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
10 ax-1cn 1 ∈ ℂ
11 pncan ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
12 9 10 11 sylancl ( 𝐴 ∈ ℕ → ( ( 𝐴 + 1 ) − 1 ) = 𝐴 )
13 12 oveq2d ( 𝐴 ∈ ℕ → ( 1 ... ( ( 𝐴 + 1 ) − 1 ) ) = ( 1 ... 𝐴 ) )
14 13 sumeq1d ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( 1 ... ( ( 𝐴 + 1 ) − 1 ) ) ( 𝐹𝑏 ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹𝑏 ) )
15 14 oveq1d ( 𝐴 ∈ ℕ → ( Σ 𝑏 ∈ ( 1 ... ( ( 𝐴 + 1 ) − 1 ) ) ( 𝐹𝑏 ) + Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ) = ( Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹𝑏 ) + Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ) )
16 nnuz ℕ = ( ℤ ‘ 1 )
17 eqid ( ℤ ‘ ( 𝐴 + 1 ) ) = ( ℤ ‘ ( 𝐴 + 1 ) )
18 eqidd ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ℕ ) → ( 𝐹𝑏 ) = ( 𝐹𝑏 ) )
19 fveq2 ( 𝑎 = 𝑏 → ( ! ‘ 𝑎 ) = ( ! ‘ 𝑏 ) )
20 19 negeqd ( 𝑎 = 𝑏 → - ( ! ‘ 𝑎 ) = - ( ! ‘ 𝑏 ) )
21 20 oveq2d ( 𝑎 = 𝑏 → ( 2 ↑ - ( ! ‘ 𝑎 ) ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
22 ovex ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ V
23 21 1 22 fvmpt ( 𝑏 ∈ ℕ → ( 𝐹𝑏 ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
24 2rp 2 ∈ ℝ+
25 nnnn0 ( 𝑏 ∈ ℕ → 𝑏 ∈ ℕ0 )
26 faccl ( 𝑏 ∈ ℕ0 → ( ! ‘ 𝑏 ) ∈ ℕ )
27 25 26 syl ( 𝑏 ∈ ℕ → ( ! ‘ 𝑏 ) ∈ ℕ )
28 27 nnzd ( 𝑏 ∈ ℕ → ( ! ‘ 𝑏 ) ∈ ℤ )
29 28 znegcld ( 𝑏 ∈ ℕ → - ( ! ‘ 𝑏 ) ∈ ℤ )
30 rpexpcl ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ 𝑏 ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℝ+ )
31 24 29 30 sylancr ( 𝑏 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℝ+ )
32 31 rpcnd ( 𝑏 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℂ )
33 23 32 eqeltrd ( 𝑏 ∈ ℕ → ( 𝐹𝑏 ) ∈ ℂ )
34 33 adantl ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ℕ ) → ( 𝐹𝑏 ) ∈ ℂ )
35 1nn 1 ∈ ℕ
36 eqid ( 𝑐 ∈ ( ℤ ‘ 1 ) ↦ ( ( 2 ↑ - ( ! ‘ 1 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 1 ) ) ) ) = ( 𝑐 ∈ ( ℤ ‘ 1 ) ↦ ( ( 2 ↑ - ( ! ‘ 1 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 1 ) ) ) )
37 36 1 aaliou3lem3 ( 1 ∈ ℕ → ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ Σ 𝑏 ∈ ( ℤ ‘ 1 ) ( 𝐹𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ ‘ 1 ) ( 𝐹𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ 1 ) ) ) ) )
38 37 simp1d ( 1 ∈ ℕ → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
39 35 38 mp1i ( 𝐴 ∈ ℕ → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
40 16 17 4 18 34 39 isumsplit ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ℕ ( 𝐹𝑏 ) = ( Σ 𝑏 ∈ ( 1 ... ( ( 𝐴 + 1 ) − 1 ) ) ( 𝐹𝑏 ) + Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ) )
41 oveq2 ( 𝑐 = 𝐴 → ( 1 ... 𝑐 ) = ( 1 ... 𝐴 ) )
42 41 sumeq1d ( 𝑐 = 𝐴 → Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹𝑏 ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹𝑏 ) )
43 sumex Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹𝑏 ) ∈ V
44 42 3 43 fvmpt ( 𝐴 ∈ ℕ → ( 𝐻𝐴 ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹𝑏 ) )
45 44 oveq1d ( 𝐴 ∈ ℕ → ( ( 𝐻𝐴 ) + Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ) = ( Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹𝑏 ) + Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ) )
46 15 40 45 3eqtr4rd ( 𝐴 ∈ ℕ → ( ( 𝐻𝐴 ) + Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ) = Σ 𝑏 ∈ ℕ ( 𝐹𝑏 ) )
47 46 2 eqtr4di ( 𝐴 ∈ ℕ → ( ( 𝐻𝐴 ) + Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ) = 𝐿 )
48 1 2 3 aaliou3lem4 𝐿 ∈ ℝ
49 48 recni 𝐿 ∈ ℂ
50 49 a1i ( 𝐴 ∈ ℕ → 𝐿 ∈ ℂ )
51 1 2 3 aaliou3lem5 ( 𝐴 ∈ ℕ → ( 𝐻𝐴 ) ∈ ℝ )
52 51 recnd ( 𝐴 ∈ ℕ → ( 𝐻𝐴 ) ∈ ℂ )
53 6 simp2d ( ( 𝐴 + 1 ) ∈ ℕ → Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℝ+ )
54 4 53 syl ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℝ+ )
55 54 rpcnd ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℂ )
56 50 52 55 subaddd ( 𝐴 ∈ ℕ → ( ( 𝐿 − ( 𝐻𝐴 ) ) = Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ↔ ( ( 𝐻𝐴 ) + Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ) = 𝐿 ) )
57 47 56 mpbird ( 𝐴 ∈ ℕ → ( 𝐿 − ( 𝐻𝐴 ) ) = Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) )
58 57 eqcomd ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) = ( 𝐿 − ( 𝐻𝐴 ) ) )
59 eleq1 ( Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) = ( 𝐿 − ( 𝐻𝐴 ) ) → ( Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℝ+ ↔ ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ) )
60 breq1 ( Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) = ( 𝐿 − ( 𝐻𝐴 ) ) → ( Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ↔ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) )
61 59 60 anbi12d ( Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) = ( 𝐿 − ( 𝐻𝐴 ) ) → ( ( Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ↔ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) )
62 58 61 syl ( 𝐴 ∈ ℕ → ( ( Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ↔ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) )
63 51 adantr ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( 𝐻𝐴 ) ∈ ℝ )
64 simprl ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ )
65 difrp ( ( ( 𝐻𝐴 ) ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 𝐻𝐴 ) < 𝐿 ↔ ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ) )
66 63 48 65 sylancl ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( ( 𝐻𝐴 ) < 𝐿 ↔ ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ) )
67 64 66 mpbird ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( 𝐻𝐴 ) < 𝐿 )
68 63 67 ltned ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( 𝐻𝐴 ) ≠ 𝐿 )
69 nnnn0 ( ( 𝐴 + 1 ) ∈ ℕ → ( 𝐴 + 1 ) ∈ ℕ0 )
70 faccl ( ( 𝐴 + 1 ) ∈ ℕ0 → ( ! ‘ ( 𝐴 + 1 ) ) ∈ ℕ )
71 4 69 70 3syl ( 𝐴 ∈ ℕ → ( ! ‘ ( 𝐴 + 1 ) ) ∈ ℕ )
72 71 nnzd ( 𝐴 ∈ ℕ → ( ! ‘ ( 𝐴 + 1 ) ) ∈ ℤ )
73 72 znegcld ( 𝐴 ∈ ℕ → - ( ! ‘ ( 𝐴 + 1 ) ) ∈ ℤ )
74 rpexpcl ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ ( 𝐴 + 1 ) ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ∈ ℝ+ )
75 24 73 74 sylancr ( 𝐴 ∈ ℕ → ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ∈ ℝ+ )
76 rpmulcl ( ( 2 ∈ ℝ+ ∧ ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ∈ ℝ+ ) → ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ∈ ℝ+ )
77 24 75 76 sylancr ( 𝐴 ∈ ℕ → ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ∈ ℝ+ )
78 77 adantr ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ∈ ℝ+ )
79 78 rpred ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ∈ ℝ )
80 63 79 resubcld ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( ( 𝐻𝐴 ) − ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ∈ ℝ )
81 48 a1i ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → 𝐿 ∈ ℝ )
82 63 78 ltsubrpd ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( ( 𝐻𝐴 ) − ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) < ( 𝐻𝐴 ) )
83 80 63 81 82 67 lttrd ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( ( 𝐻𝐴 ) − ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) < 𝐿 )
84 80 81 83 ltled ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( ( 𝐻𝐴 ) − ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ≤ 𝐿 )
85 simprr ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) )
86 81 63 79 lesubadd2d ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ↔ 𝐿 ≤ ( ( 𝐻𝐴 ) + ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) )
87 85 86 mpbid ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → 𝐿 ≤ ( ( 𝐻𝐴 ) + ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) )
88 81 63 79 absdifled ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( ( abs ‘ ( 𝐿 − ( 𝐻𝐴 ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ↔ ( ( ( 𝐻𝐴 ) − ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ≤ 𝐿𝐿 ≤ ( ( 𝐻𝐴 ) + ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) ) )
89 84 87 88 mpbir2and ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( abs ‘ ( 𝐿 − ( 𝐻𝐴 ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) )
90 68 89 jca ( ( 𝐴 ∈ ℕ ∧ ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) → ( ( 𝐻𝐴 ) ≠ 𝐿 ∧ ( abs ‘ ( 𝐿 − ( 𝐻𝐴 ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) )
91 90 ex ( 𝐴 ∈ ℕ → ( ( ( 𝐿 − ( 𝐻𝐴 ) ) ∈ ℝ+ ∧ ( 𝐿 − ( 𝐻𝐴 ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) → ( ( 𝐻𝐴 ) ≠ 𝐿 ∧ ( abs ‘ ( 𝐿 − ( 𝐻𝐴 ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) )
92 62 91 sylbid ( 𝐴 ∈ ℕ → ( ( Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ ‘ ( 𝐴 + 1 ) ) ( 𝐹𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) → ( ( 𝐻𝐴 ) ≠ 𝐿 ∧ ( abs ‘ ( 𝐿 − ( 𝐻𝐴 ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) ) )
93 8 92 mpd ( 𝐴 ∈ ℕ → ( ( 𝐻𝐴 ) ≠ 𝐿 ∧ ( abs ‘ ( 𝐿 − ( 𝐻𝐴 ) ) ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝐴 + 1 ) ) ) ) ) )