Metamath Proof Explorer

Theorem aaliou3lem6

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

Ref Expression
Hypotheses aaliou3lem.c ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
aaliou3lem.d ⊢ 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 )
aaliou3lem.e ⊢ 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) )
Assertion aaliou3lem6 ( 𝐴 ∈ ℕ → ( ( 𝐻 ‘ 𝐴 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 aaliou3lem.c ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
2 aaliou3lem.d ⊢ 𝐿 = Σ 𝑏 ∈ ℕ ( 𝐹 ‘ 𝑏 )
3 aaliou3lem.e ⊢ 𝐻 = ( 𝑐 ∈ ℕ ↦ Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) )
4 oveq2 ⊢ ( 𝑐 = 𝐴 → ( 1 ... 𝑐 ) = ( 1 ... 𝐴 ) )
5 4 sumeq1d ⊢ ( 𝑐 = 𝐴 → Σ 𝑏 ∈ ( 1 ... 𝑐 ) ( 𝐹 ‘ 𝑏 ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) )
6 sumex ⊢ Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) ∈ V
7 5 3 6 fvmpt ⊢ ( 𝐴 ∈ ℕ → ( 𝐻 ‘ 𝐴 ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) )
8 7 oveq1d ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐻 ‘ 𝐴 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) = ( Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
9 fzfid ⊢ ( 𝐴 ∈ ℕ → ( 1 ... 𝐴 ) ∈ Fin )
10 2rp ⊢ 2 ∈ ℝ+
11 nnnn0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
12 11 faccld ⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) ∈ ℕ )
13 12 nnzd ⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) ∈ ℤ )
14 rpexpcl ⊢ ( ( 2 ∈ ℝ+ ∧ ( ! ‘ 𝐴 ) ∈ ℤ ) → ( 2 ↑ ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
15 10 13 14 sylancr ⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
16 15 rpcnd ⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ ( ! ‘ 𝐴 ) ) ∈ ℂ )
17 elfznn ⊢ ( 𝑏 ∈ ( 1 ... 𝐴 ) → 𝑏 ∈ ℕ )
18 fveq2 ⊢ ( 𝑎 = 𝑏 → ( ! ‘ 𝑎 ) = ( ! ‘ 𝑏 ) )
19 18 negeqd ⊢ ( 𝑎 = 𝑏 → - ( ! ‘ 𝑎 ) = - ( ! ‘ 𝑏 ) )
20 19 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 2 ↑ - ( ! ‘ 𝑎 ) ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
21 ovex ⊢ ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ V
22 20 1 21 fvmpt ⊢ ( 𝑏 ∈ ℕ → ( 𝐹 ‘ 𝑏 ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
23 17 22 syl ⊢ ( 𝑏 ∈ ( 1 ... 𝐴 ) → ( 𝐹 ‘ 𝑏 ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
24 23 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 2 ↑ - ( ! ‘ 𝑏 ) ) )
25 17 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → 𝑏 ∈ ℕ )
26 25 nnnn0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → 𝑏 ∈ ℕ0 )
27 26 faccld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝑏 ) ∈ ℕ )
28 27 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝑏 ) ∈ ℤ )
29 28 znegcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → - ( ! ‘ 𝑏 ) ∈ ℤ )
30 rpexpcl ⊢ ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ 𝑏 ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℝ+ )
31 10 29 30 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℝ+ )
32 31 rpcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 2 ↑ - ( ! ‘ 𝑏 ) ) ∈ ℂ )
33 24 32 eqeltrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℂ )
34 9 16 33 fsummulc1 ⊢ ( 𝐴 ∈ ℕ → ( Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) = Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
35 24 oveq1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑏 ) ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
36 13 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℤ )
37 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
38 expaddz ⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( - ( ! ‘ 𝑏 ) ∈ ℤ ∧ ( ! ‘ 𝐴 ) ∈ ℤ ) ) → ( 2 ↑ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑏 ) ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
39 37 38 mpan ⊢ ( ( - ( ! ‘ 𝑏 ) ∈ ℤ ∧ ( ! ‘ 𝐴 ) ∈ ℤ ) → ( 2 ↑ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑏 ) ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
40 29 36 39 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 2 ↑ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝑏 ) ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) )
41 2z ⊢ 2 ∈ ℤ
42 29 zcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → - ( ! ‘ 𝑏 ) ∈ ℂ )
43 36 zcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℂ )
44 42 43 addcomd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) = ( ( ! ‘ 𝐴 ) + - ( ! ‘ 𝑏 ) ) )
45 27 nncnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝑏 ) ∈ ℂ )
46 43 45 negsubd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( ! ‘ 𝐴 ) + - ( ! ‘ 𝑏 ) ) = ( ( ! ‘ 𝐴 ) − ( ! ‘ 𝑏 ) ) )
47 44 46 eqtrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) = ( ( ! ‘ 𝐴 ) − ( ! ‘ 𝑏 ) ) )
48 11 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → 𝐴 ∈ ℕ0 )
49 elfzle2 ⊢ ( 𝑏 ∈ ( 1 ... 𝐴 ) → 𝑏 ≤ 𝐴 )
50 49 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → 𝑏 ≤ 𝐴 )
51 facwordi ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝑏 ≤ 𝐴 ) → ( ! ‘ 𝑏 ) ≤ ( ! ‘ 𝐴 ) )
52 26 48 50 51 syl3anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝑏 ) ≤ ( ! ‘ 𝐴 ) )
53 27 nnnn0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝑏 ) ∈ ℕ0 )
54 48 faccld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℕ )
55 54 nnnn0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ! ‘ 𝐴 ) ∈ ℕ0 )
56 nn0sub ⊢ ( ( ( ! ‘ 𝑏 ) ∈ ℕ0 ∧ ( ! ‘ 𝐴 ) ∈ ℕ0 ) → ( ( ! ‘ 𝑏 ) ≤ ( ! ‘ 𝐴 ) ↔ ( ( ! ‘ 𝐴 ) − ( ! ‘ 𝑏 ) ) ∈ ℕ0 ) )
57 53 55 56 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( ! ‘ 𝑏 ) ≤ ( ! ‘ 𝐴 ) ↔ ( ( ! ‘ 𝐴 ) − ( ! ‘ 𝑏 ) ) ∈ ℕ0 ) )
58 52 57 mpbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( ! ‘ 𝐴 ) − ( ! ‘ 𝑏 ) ) ∈ ℕ0 )
59 47 58 eqeltrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ∈ ℕ0 )
60 zexpcl ⊢ ( ( 2 ∈ ℤ ∧ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ∈ ℕ0 ) → ( 2 ↑ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
61 41 59 60 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( 2 ↑ ( - ( ! ‘ 𝑏 ) + ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
62 40 61 eqeltrrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( 2 ↑ - ( ! ‘ 𝑏 ) ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
63 35 62 eqeltrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
64 9 63 fsumzcl ⊢ ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
65 34 64 eqeltrd ⊢ ( 𝐴 ∈ ℕ → ( Σ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝐹 ‘ 𝑏 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )
66 8 65 eqeltrd ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐻 ‘ 𝐴 ) · ( 2 ↑ ( ! ‘ 𝐴 ) ) ) ∈ ℤ )