Metamath Proof Explorer

Theorem aaliou3lem2

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

Ref Expression
Hypotheses aaliou3lem.a ⊢ 𝐺 = ( 𝑐 ∈ ( ℤ≥ ‘ 𝐴 ) ↦ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) ) )
aaliou3lem.b ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
Assertion aaliou3lem2 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 0 (,] ( 𝐺 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 aaliou3lem.a ⊢ 𝐺 = ( 𝑐 ∈ ( ℤ≥ ‘ 𝐴 ) ↦ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) ) )
2 aaliou3lem.b ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
3 eluznn ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐵 ∈ ℕ )
4 fveq2 ⊢ ( 𝑎 = 𝐵 → ( ! ‘ 𝑎 ) = ( ! ‘ 𝐵 ) )
5 4 negeqd ⊢ ( 𝑎 = 𝐵 → - ( ! ‘ 𝑎 ) = - ( ! ‘ 𝐵 ) )
6 5 oveq2d ⊢ ( 𝑎 = 𝐵 → ( 2 ↑ - ( ! ‘ 𝑎 ) ) = ( 2 ↑ - ( ! ‘ 𝐵 ) ) )
7 ovex ⊢ ( 2 ↑ - ( ! ‘ 𝐵 ) ) ∈ V
8 6 2 7 fvmpt ⊢ ( 𝐵 ∈ ℕ → ( 𝐹 ‘ 𝐵 ) = ( 2 ↑ - ( ! ‘ 𝐵 ) ) )
9 3 8 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐵 ) = ( 2 ↑ - ( ! ‘ 𝐵 ) ) )
10 2rp ⊢ 2 ∈ ℝ+
11 3 nnnn0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐵 ∈ ℕ0 )
12 11 faccld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ! ‘ 𝐵 ) ∈ ℕ )
13 12 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ! ‘ 𝐵 ) ∈ ℤ )
14 13 znegcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → - ( ! ‘ 𝐵 ) ∈ ℤ )
15 rpexpcl ⊢ ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ 𝐵 ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ 𝐵 ) ) ∈ ℝ+ )
16 10 14 15 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ - ( ! ‘ 𝐵 ) ) ∈ ℝ+ )
17 9 16 eqeltrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ+ )
18 17 rpred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
19 17 rpgt0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 0 < ( 𝐹 ‘ 𝐵 ) )
20 fveq2 ⊢ ( 𝑏 = 𝐴 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝐴 ) )
21 fveq2 ⊢ ( 𝑏 = 𝐴 → ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝐴 ) )
22 20 21 breq12d ⊢ ( 𝑏 = 𝐴 → ( ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝐴 ) ) )
23 22 imbi2d ⊢ ( 𝑏 = 𝐴 → ( ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ) ↔ ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝐴 ) ) ) )
24 fveq2 ⊢ ( 𝑏 = 𝑑 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑑 ) )
25 fveq2 ⊢ ( 𝑏 = 𝑑 → ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑑 ) )
26 24 25 breq12d ⊢ ( 𝑏 = 𝑑 → ( ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑑 ) ≤ ( 𝐺 ‘ 𝑑 ) ) )
27 26 imbi2d ⊢ ( 𝑏 = 𝑑 → ( ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ) ↔ ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝑑 ) ≤ ( 𝐺 ‘ 𝑑 ) ) ) )
28 fveq2 ⊢ ( 𝑏 = ( 𝑑 + 1 ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ ( 𝑑 + 1 ) ) )
29 fveq2 ⊢ ( 𝑏 = ( 𝑑 + 1 ) → ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ ( 𝑑 + 1 ) ) )
30 28 29 breq12d ⊢ ( 𝑏 = ( 𝑑 + 1 ) → ( ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ↔ ( 𝐹 ‘ ( 𝑑 + 1 ) ) ≤ ( 𝐺 ‘ ( 𝑑 + 1 ) ) ) )
31 30 imbi2d ⊢ ( 𝑏 = ( 𝑑 + 1 ) → ( ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ) ↔ ( 𝐴 ∈ ℕ → ( 𝐹 ‘ ( 𝑑 + 1 ) ) ≤ ( 𝐺 ‘ ( 𝑑 + 1 ) ) ) ) )
32 fveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝐵 ) )
33 fveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝐵 ) )
34 32 33 breq12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐵 ) ) )
35 34 imbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ) ↔ ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐵 ) ) ) )
36 nnnn0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
37 36 faccld ⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) ∈ ℕ )
38 37 nnzd ⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) ∈ ℤ )
39 38 znegcld ⊢ ( 𝐴 ∈ ℕ → - ( ! ‘ 𝐴 ) ∈ ℤ )
40 rpexpcl ⊢ ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ 𝐴 ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
41 10 39 40 sylancr ⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
42 41 rpred ⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℝ )
43 42 leidd ⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ≤ ( 2 ↑ - ( ! ‘ 𝐴 ) ) )
44 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
45 44 subidd ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 − 𝐴 ) = 0 )
46 45 oveq2d ⊢ ( 𝐴 ∈ ℕ → ( ( 1 / 2 ) ↑ ( 𝐴 − 𝐴 ) ) = ( ( 1 / 2 ) ↑ 0 ) )
47 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
48 exp0 ⊢ ( ( 1 / 2 ) ∈ ℂ → ( ( 1 / 2 ) ↑ 0 ) = 1 )
49 47 48 ax-mp ⊢ ( ( 1 / 2 ) ↑ 0 ) = 1
50 46 49 eqtrdi ⊢ ( 𝐴 ∈ ℕ → ( ( 1 / 2 ) ↑ ( 𝐴 − 𝐴 ) ) = 1 )
51 50 oveq2d ⊢ ( 𝐴 ∈ ℕ → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐴 − 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 1 ) )
52 41 rpcnd ⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℂ )
53 52 mulid1d ⊢ ( 𝐴 ∈ ℕ → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 1 ) = ( 2 ↑ - ( ! ‘ 𝐴 ) ) )
54 51 53 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐴 − 𝐴 ) ) ) = ( 2 ↑ - ( ! ‘ 𝐴 ) ) )
55 43 54 breqtrrd ⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐴 − 𝐴 ) ) ) )
56 fveq2 ⊢ ( 𝑎 = 𝐴 → ( ! ‘ 𝑎 ) = ( ! ‘ 𝐴 ) )
57 56 negeqd ⊢ ( 𝑎 = 𝐴 → - ( ! ‘ 𝑎 ) = - ( ! ‘ 𝐴 ) )
58 57 oveq2d ⊢ ( 𝑎 = 𝐴 → ( 2 ↑ - ( ! ‘ 𝑎 ) ) = ( 2 ↑ - ( ! ‘ 𝐴 ) ) )
59 ovex ⊢ ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ V
60 58 2 59 fvmpt ⊢ ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝐴 ) = ( 2 ↑ - ( ! ‘ 𝐴 ) ) )
61 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
62 uzid ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) )
63 oveq1 ⊢ ( 𝑐 = 𝐴 → ( 𝑐 − 𝐴 ) = ( 𝐴 − 𝐴 ) )
64 63 oveq2d ⊢ ( 𝑐 = 𝐴 → ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) = ( ( 1 / 2 ) ↑ ( 𝐴 − 𝐴 ) ) )
65 64 oveq2d ⊢ ( 𝑐 = 𝐴 → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐴 − 𝐴 ) ) ) )
66 ovex ⊢ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐴 − 𝐴 ) ) ) ∈ V
67 65 1 66 fvmpt ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐺 ‘ 𝐴 ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐴 − 𝐴 ) ) ) )
68 61 62 67 3syl ⊢ ( 𝐴 ∈ ℕ → ( 𝐺 ‘ 𝐴 ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐴 − 𝐴 ) ) ) )
69 55 60 68 3brtr4d ⊢ ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝐴 ) )
70 eluznn ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝑑 ∈ ℕ )
71 70 nnnn0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝑑 ∈ ℕ0 )
72 71 faccld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ! ‘ 𝑑 ) ∈ ℕ )
73 72 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ! ‘ 𝑑 ) ∈ ℤ )
74 73 znegcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → - ( ! ‘ 𝑑 ) ∈ ℤ )
75 rpexpcl ⊢ ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ 𝑑 ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ 𝑑 ) ) ∈ ℝ+ )
76 10 74 75 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ - ( ! ‘ 𝑑 ) ) ∈ ℝ+ )
77 76 rpred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ - ( ! ‘ 𝑑 ) ) ∈ ℝ )
78 76 rpge0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 0 ≤ ( 2 ↑ - ( ! ‘ 𝑑 ) ) )
79 simpl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐴 ∈ ℕ )
80 79 nnnn0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐴 ∈ ℕ0 )
81 80 faccld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℕ )
82 81 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℤ )
83 82 znegcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → - ( ! ‘ 𝐴 ) ∈ ℤ )
84 10 83 40 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
85 halfre ⊢ ( 1 / 2 ) ∈ ℝ
86 halfgt0 ⊢ 0 < ( 1 / 2 )
87 85 86 elrpii ⊢ ( 1 / 2 ) ∈ ℝ+
88 eluzelz ⊢ ( 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑑 ∈ ℤ )
89 zsubcl ⊢ ( ( 𝑑 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑑 − 𝐴 ) ∈ ℤ )
90 88 61 89 syl2anr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑑 − 𝐴 ) ∈ ℤ )
91 rpexpcl ⊢ ( ( ( 1 / 2 ) ∈ ℝ+ ∧ ( 𝑑 − 𝐴 ) ∈ ℤ ) → ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ∈ ℝ+ )
92 87 90 91 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ∈ ℝ+ )
93 84 92 rpmulcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ∈ ℝ+ )
94 93 rpred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ∈ ℝ )
95 77 78 94 jca31 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ) ∧ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ∈ ℝ ) )
96 95 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ) → ( ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ) ∧ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ∈ ℝ ) )
97 88 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝑑 ∈ ℤ )
98 74 97 zmulcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( - ( ! ‘ 𝑑 ) · 𝑑 ) ∈ ℤ )
99 rpexpcl ⊢ ( ( 2 ∈ ℝ+ ∧ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ∈ ℤ ) → ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ∈ ℝ+ )
100 10 98 99 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ∈ ℝ+ )
101 100 rpred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ∈ ℝ )
102 100 rpge0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 0 ≤ ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) )
103 85 a1i ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 1 / 2 ) ∈ ℝ )
104 101 102 103 jca31 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) ∧ ( 1 / 2 ) ∈ ℝ ) )
105 104 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ) → ( ( ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) ∧ ( 1 / 2 ) ∈ ℝ ) )
106 simpr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ) → ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) )
107 2re ⊢ 2 ∈ ℝ
108 1le2 ⊢ 1 ≤ 2
109 72 nncnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ! ‘ 𝑑 ) ∈ ℂ )
110 97 zcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝑑 ∈ ℂ )
111 109 110 mulneg1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( - ( ! ‘ 𝑑 ) · 𝑑 ) = - ( ( ! ‘ 𝑑 ) · 𝑑 ) )
112 72 70 nnmulcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( ! ‘ 𝑑 ) · 𝑑 ) ∈ ℕ )
113 112 nnge1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 1 ≤ ( ( ! ‘ 𝑑 ) · 𝑑 ) )
114 1re ⊢ 1 ∈ ℝ
115 112 nnred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( ! ‘ 𝑑 ) · 𝑑 ) ∈ ℝ )
116 leneg ⊢ ( ( 1 ∈ ℝ ∧ ( ( ! ‘ 𝑑 ) · 𝑑 ) ∈ ℝ ) → ( 1 ≤ ( ( ! ‘ 𝑑 ) · 𝑑 ) ↔ - ( ( ! ‘ 𝑑 ) · 𝑑 ) ≤ - 1 ) )
117 114 115 116 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 1 ≤ ( ( ! ‘ 𝑑 ) · 𝑑 ) ↔ - ( ( ! ‘ 𝑑 ) · 𝑑 ) ≤ - 1 ) )
118 113 117 mpbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → - ( ( ! ‘ 𝑑 ) · 𝑑 ) ≤ - 1 )
119 111 118 eqbrtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( - ( ! ‘ 𝑑 ) · 𝑑 ) ≤ - 1 )
120 neg1z ⊢ - 1 ∈ ℤ
121 eluz ⊢ ( ( ( - ( ! ‘ 𝑑 ) · 𝑑 ) ∈ ℤ ∧ - 1 ∈ ℤ ) → ( - 1 ∈ ( ℤ≥ ‘ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ↔ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ≤ - 1 ) )
122 98 120 121 sylancl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( - 1 ∈ ( ℤ≥ ‘ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ↔ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ≤ - 1 ) )
123 119 122 mpbird ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → - 1 ∈ ( ℤ≥ ‘ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) )
124 leexp2a ⊢ ( ( 2 ∈ ℝ ∧ 1 ≤ 2 ∧ - 1 ∈ ( ℤ≥ ‘ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) → ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ≤ ( 2 ↑ - 1 ) )
125 107 108 123 124 mp3an12i ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ≤ ( 2 ↑ - 1 ) )
126 2cn ⊢ 2 ∈ ℂ
127 expn1 ⊢ ( 2 ∈ ℂ → ( 2 ↑ - 1 ) = ( 1 / 2 ) )
128 126 127 ax-mp ⊢ ( 2 ↑ - 1 ) = ( 1 / 2 )
129 125 128 breqtrdi ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ≤ ( 1 / 2 ) )
130 129 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ) → ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ≤ ( 1 / 2 ) )
131 lemul12a ⊢ ( ( ( ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ) ∧ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ∈ ℝ ) ∧ ( ( ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) ∧ ( 1 / 2 ) ∈ ℝ ) ) → ( ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ∧ ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ≤ ( 1 / 2 ) ) → ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) · ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) ≤ ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) · ( 1 / 2 ) ) ) )
132 131 3impia ⊢ ( ( ( ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ) ∧ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ∈ ℝ ) ∧ ( ( ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) ∧ ( 1 / 2 ) ∈ ℝ ) ∧ ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ∧ ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ≤ ( 1 / 2 ) ) ) → ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) · ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) ≤ ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) · ( 1 / 2 ) ) )
133 96 105 106 130 132 syl112anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) ∧ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ) → ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) · ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) ≤ ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) · ( 1 / 2 ) ) )
134 133 ex ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) → ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) · ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) ≤ ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) · ( 1 / 2 ) ) ) )
135 facp1 ⊢ ( 𝑑 ∈ ℕ0 → ( ! ‘ ( 𝑑 + 1 ) ) = ( ( ! ‘ 𝑑 ) · ( 𝑑 + 1 ) ) )
136 71 135 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ! ‘ ( 𝑑 + 1 ) ) = ( ( ! ‘ 𝑑 ) · ( 𝑑 + 1 ) ) )
137 136 negeqd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → - ( ! ‘ ( 𝑑 + 1 ) ) = - ( ( ! ‘ 𝑑 ) · ( 𝑑 + 1 ) ) )
138 ax-1cn ⊢ 1 ∈ ℂ
139 addcom ⊢ ( ( 𝑑 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑑 + 1 ) = ( 1 + 𝑑 ) )
140 110 138 139 sylancl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑑 + 1 ) = ( 1 + 𝑑 ) )
141 140 oveq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( - ( ! ‘ 𝑑 ) · ( 𝑑 + 1 ) ) = ( - ( ! ‘ 𝑑 ) · ( 1 + 𝑑 ) ) )
142 peano2cn ⊢ ( 𝑑 ∈ ℂ → ( 𝑑 + 1 ) ∈ ℂ )
143 110 142 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑑 + 1 ) ∈ ℂ )
144 109 143 mulneg1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( - ( ! ‘ 𝑑 ) · ( 𝑑 + 1 ) ) = - ( ( ! ‘ 𝑑 ) · ( 𝑑 + 1 ) ) )
145 74 zcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → - ( ! ‘ 𝑑 ) ∈ ℂ )
146 1cnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 1 ∈ ℂ )
147 145 146 110 adddid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( - ( ! ‘ 𝑑 ) · ( 1 + 𝑑 ) ) = ( ( - ( ! ‘ 𝑑 ) · 1 ) + ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) )
148 145 mulid1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( - ( ! ‘ 𝑑 ) · 1 ) = - ( ! ‘ 𝑑 ) )
149 148 oveq1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( - ( ! ‘ 𝑑 ) · 1 ) + ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) = ( - ( ! ‘ 𝑑 ) + ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) )
150 147 149 eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( - ( ! ‘ 𝑑 ) · ( 1 + 𝑑 ) ) = ( - ( ! ‘ 𝑑 ) + ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) )
151 141 144 150 3eqtr3d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → - ( ( ! ‘ 𝑑 ) · ( 𝑑 + 1 ) ) = ( - ( ! ‘ 𝑑 ) + ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) )
152 137 151 eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → - ( ! ‘ ( 𝑑 + 1 ) ) = ( - ( ! ‘ 𝑑 ) + ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) )
153 152 oveq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ - ( ! ‘ ( 𝑑 + 1 ) ) ) = ( 2 ↑ ( - ( ! ‘ 𝑑 ) + ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) )
154 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
155 expaddz ⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( - ( ! ‘ 𝑑 ) ∈ ℤ ∧ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ∈ ℤ ) ) → ( 2 ↑ ( - ( ! ‘ 𝑑 ) + ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) · ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) )
156 154 155 mpan ⊢ ( ( - ( ! ‘ 𝑑 ) ∈ ℤ ∧ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ∈ ℤ ) → ( 2 ↑ ( - ( ! ‘ 𝑑 ) + ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) · ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) )
157 74 98 156 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ ( - ( ! ‘ 𝑑 ) + ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) · ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) )
158 153 157 eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ - ( ! ‘ ( 𝑑 + 1 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) · ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) )
159 44 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐴 ∈ ℂ )
160 110 146 159 addsubd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝑑 + 1 ) − 𝐴 ) = ( ( 𝑑 − 𝐴 ) + 1 ) )
161 160 oveq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) = ( ( 1 / 2 ) ↑ ( ( 𝑑 − 𝐴 ) + 1 ) ) )
162 uznn0sub ⊢ ( 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑑 − 𝐴 ) ∈ ℕ0 )
163 162 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑑 − 𝐴 ) ∈ ℕ0 )
164 expp1 ⊢ ( ( ( 1 / 2 ) ∈ ℂ ∧ ( 𝑑 − 𝐴 ) ∈ ℕ0 ) → ( ( 1 / 2 ) ↑ ( ( 𝑑 − 𝐴 ) + 1 ) ) = ( ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) · ( 1 / 2 ) ) )
165 47 163 164 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 1 / 2 ) ↑ ( ( 𝑑 − 𝐴 ) + 1 ) ) = ( ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) · ( 1 / 2 ) ) )
166 161 165 eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) = ( ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) · ( 1 / 2 ) ) )
167 166 oveq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) · ( 1 / 2 ) ) ) )
168 84 rpcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℂ )
169 92 rpcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ∈ ℂ )
170 47 a1i ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 1 / 2 ) ∈ ℂ )
171 168 169 170 mulassd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) · ( 1 / 2 ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) · ( 1 / 2 ) ) ) )
172 167 171 eqtr4d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) ) = ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) · ( 1 / 2 ) ) )
173 158 172 breq12d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ ( 𝑑 + 1 ) ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) ) ↔ ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) · ( 2 ↑ ( - ( ! ‘ 𝑑 ) · 𝑑 ) ) ) ≤ ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) · ( 1 / 2 ) ) ) )
174 134 173 sylibrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) → ( 2 ↑ - ( ! ‘ ( 𝑑 + 1 ) ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) ) ) )
175 fveq2 ⊢ ( 𝑎 = 𝑑 → ( ! ‘ 𝑎 ) = ( ! ‘ 𝑑 ) )
176 175 negeqd ⊢ ( 𝑎 = 𝑑 → - ( ! ‘ 𝑎 ) = - ( ! ‘ 𝑑 ) )
177 176 oveq2d ⊢ ( 𝑎 = 𝑑 → ( 2 ↑ - ( ! ‘ 𝑎 ) ) = ( 2 ↑ - ( ! ‘ 𝑑 ) ) )
178 ovex ⊢ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ∈ V
179 177 2 178 fvmpt ⊢ ( 𝑑 ∈ ℕ → ( 𝐹 ‘ 𝑑 ) = ( 2 ↑ - ( ! ‘ 𝑑 ) ) )
180 70 179 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑑 ) = ( 2 ↑ - ( ! ‘ 𝑑 ) ) )
181 oveq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 − 𝐴 ) = ( 𝑑 − 𝐴 ) )
182 181 oveq2d ⊢ ( 𝑐 = 𝑑 → ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) = ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) )
183 182 oveq2d ⊢ ( 𝑐 = 𝑑 → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) )
184 ovex ⊢ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ∈ V
185 183 1 184 fvmpt ⊢ ( 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐺 ‘ 𝑑 ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) )
186 185 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐺 ‘ 𝑑 ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) )
187 180 186 breq12d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑑 ) ≤ ( 𝐺 ‘ 𝑑 ) ↔ ( 2 ↑ - ( ! ‘ 𝑑 ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑑 − 𝐴 ) ) ) ) )
188 70 peano2nnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑑 + 1 ) ∈ ℕ )
189 fveq2 ⊢ ( 𝑎 = ( 𝑑 + 1 ) → ( ! ‘ 𝑎 ) = ( ! ‘ ( 𝑑 + 1 ) ) )
190 189 negeqd ⊢ ( 𝑎 = ( 𝑑 + 1 ) → - ( ! ‘ 𝑎 ) = - ( ! ‘ ( 𝑑 + 1 ) ) )
191 190 oveq2d ⊢ ( 𝑎 = ( 𝑑 + 1 ) → ( 2 ↑ - ( ! ‘ 𝑎 ) ) = ( 2 ↑ - ( ! ‘ ( 𝑑 + 1 ) ) ) )
192 ovex ⊢ ( 2 ↑ - ( ! ‘ ( 𝑑 + 1 ) ) ) ∈ V
193 191 2 192 fvmpt ⊢ ( ( 𝑑 + 1 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑑 + 1 ) ) = ( 2 ↑ - ( ! ‘ ( 𝑑 + 1 ) ) ) )
194 188 193 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ ( 𝑑 + 1 ) ) = ( 2 ↑ - ( ! ‘ ( 𝑑 + 1 ) ) ) )
195 peano2uz ⊢ ( 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑑 + 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) )
196 oveq1 ⊢ ( 𝑐 = ( 𝑑 + 1 ) → ( 𝑐 − 𝐴 ) = ( ( 𝑑 + 1 ) − 𝐴 ) )
197 196 oveq2d ⊢ ( 𝑐 = ( 𝑑 + 1 ) → ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) = ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) )
198 197 oveq2d ⊢ ( 𝑐 = ( 𝑑 + 1 ) → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) ) )
199 ovex ⊢ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) ) ∈ V
200 198 1 199 fvmpt ⊢ ( ( 𝑑 + 1 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐺 ‘ ( 𝑑 + 1 ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) ) )
201 195 200 syl ⊢ ( 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐺 ‘ ( 𝑑 + 1 ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) ) )
202 201 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐺 ‘ ( 𝑑 + 1 ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) ) )
203 194 202 breq12d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝐹 ‘ ( 𝑑 + 1 ) ) ≤ ( 𝐺 ‘ ( 𝑑 + 1 ) ) ↔ ( 2 ↑ - ( ! ‘ ( 𝑑 + 1 ) ) ) ≤ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( ( 𝑑 + 1 ) − 𝐴 ) ) ) ) )
204 174 187 203 3imtr4d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑑 ) ≤ ( 𝐺 ‘ 𝑑 ) → ( 𝐹 ‘ ( 𝑑 + 1 ) ) ≤ ( 𝐺 ‘ ( 𝑑 + 1 ) ) ) )
205 204 expcom ⊢ ( 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ∈ ℕ → ( ( 𝐹 ‘ 𝑑 ) ≤ ( 𝐺 ‘ 𝑑 ) → ( 𝐹 ‘ ( 𝑑 + 1 ) ) ≤ ( 𝐺 ‘ ( 𝑑 + 1 ) ) ) ) )
206 205 a2d ⊢ ( 𝑑 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝑑 ) ≤ ( 𝐺 ‘ 𝑑 ) ) → ( 𝐴 ∈ ℕ → ( 𝐹 ‘ ( 𝑑 + 1 ) ) ≤ ( 𝐺 ‘ ( 𝑑 + 1 ) ) ) ) )
207 23 27 31 35 69 206 uzind4i ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐵 ) ) )
208 207 impcom ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐵 ) )
209 0xr ⊢ 0 ∈ ℝ*
210 1 aaliou3lem1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )
211 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ ( 𝐺 ‘ 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 (,] ( 𝐺 ‘ 𝐵 ) ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐵 ) ) ) )
212 209 210 211 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 (,] ( 𝐺 ‘ 𝐵 ) ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐵 ) ) ) )
213 18 19 208 212 mpbir3and ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 0 (,] ( 𝐺 ‘ 𝐵 ) ) )