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 ) ) ) ) ) )