Metamath Proof Explorer

Theorem aaliou3lem1

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

Ref Expression
Hypothesis aaliou3lem.a ⊢ 𝐺 = ( 𝑐 ∈ ( ℤ≥ ‘ 𝐴 ) ↦ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) ) )
Assertion aaliou3lem1 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 aaliou3lem.a ⊢ 𝐺 = ( 𝑐 ∈ ( ℤ≥ ‘ 𝐴 ) ↦ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) ) )
2 oveq1 ⊢ ( 𝑐 = 𝐵 → ( 𝑐 − 𝐴 ) = ( 𝐵 − 𝐴 ) )
3 2 oveq2d ⊢ ( 𝑐 = 𝐵 → ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) = ( ( 1 / 2 ) ↑ ( 𝐵 − 𝐴 ) ) )
4 3 oveq2d ⊢ ( 𝑐 = 𝐵 → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐵 − 𝐴 ) ) ) )
5 ovex ⊢ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐵 − 𝐴 ) ) ) ∈ V
6 4 1 5 fvmpt ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐺 ‘ 𝐵 ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐵 − 𝐴 ) ) ) )
7 6 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐺 ‘ 𝐵 ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐵 − 𝐴 ) ) ) )
8 2rp ⊢ 2 ∈ ℝ+
9 simpl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐴 ∈ ℕ )
10 9 nnnn0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐴 ∈ ℕ0 )
11 10 faccld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℕ )
12 11 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℤ )
13 12 znegcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → - ( ! ‘ 𝐴 ) ∈ ℤ )
14 rpexpcl ⊢ ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ 𝐴 ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
15 8 13 14 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
16 halfre ⊢ ( 1 / 2 ) ∈ ℝ
17 halfgt0 ⊢ 0 < ( 1 / 2 )
18 16 17 elrpii ⊢ ( 1 / 2 ) ∈ ℝ+
19 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℤ )
20 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
21 zsubcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐵 − 𝐴 ) ∈ ℤ )
22 19 20 21 syl2anr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐵 − 𝐴 ) ∈ ℤ )
23 rpexpcl ⊢ ( ( ( 1 / 2 ) ∈ ℝ+ ∧ ( 𝐵 − 𝐴 ) ∈ ℤ ) → ( ( 1 / 2 ) ↑ ( 𝐵 − 𝐴 ) ) ∈ ℝ+ )
24 18 22 23 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 1 / 2 ) ↑ ( 𝐵 − 𝐴 ) ) ∈ ℝ+ )
25 15 24 rpmulcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐵 − 𝐴 ) ) ) ∈ ℝ+ )
26 25 rpred ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝐵 − 𝐴 ) ) ) ∈ ℝ )
27 7 26 eqeltrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )