Proof of Theorem aaliou3lem6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . 5
⊢ (𝑐 = 𝐴 → (1...𝑐) = (1...𝐴)) | 
| 2 | 1 | sumeq1d 15736 | . . . 4
⊢ (𝑐 = 𝐴 → Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏) = Σ𝑏 ∈ (1...𝐴)(𝐹‘𝑏)) | 
| 3 |  | aaliou3lem.e | . . . 4
⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) | 
| 4 |  | sumex 15724 | . . . 4
⊢
Σ𝑏 ∈
(1...𝐴)(𝐹‘𝑏) ∈ V | 
| 5 | 2, 3, 4 | fvmpt 7016 | . . 3
⊢ (𝐴 ∈ ℕ → (𝐻‘𝐴) = Σ𝑏 ∈ (1...𝐴)(𝐹‘𝑏)) | 
| 6 | 5 | oveq1d 7446 | . 2
⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) · (2↑(!‘𝐴))) = (Σ𝑏 ∈ (1...𝐴)(𝐹‘𝑏) · (2↑(!‘𝐴)))) | 
| 7 |  | fzfid 14014 | . . . 4
⊢ (𝐴 ∈ ℕ →
(1...𝐴) ∈
Fin) | 
| 8 |  | 2rp 13039 | . . . . . 6
⊢ 2 ∈
ℝ+ | 
| 9 |  | nnnn0 12533 | . . . . . . . 8
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) | 
| 10 | 9 | faccld 14323 | . . . . . . 7
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℕ) | 
| 11 | 10 | nnzd 12640 | . . . . . 6
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℤ) | 
| 12 |  | rpexpcl 14121 | . . . . . 6
⊢ ((2
∈ ℝ+ ∧ (!‘𝐴) ∈ ℤ) →
(2↑(!‘𝐴)) ∈
ℝ+) | 
| 13 | 8, 11, 12 | sylancr 587 | . . . . 5
⊢ (𝐴 ∈ ℕ →
(2↑(!‘𝐴)) ∈
ℝ+) | 
| 14 | 13 | rpcnd 13079 | . . . 4
⊢ (𝐴 ∈ ℕ →
(2↑(!‘𝐴)) ∈
ℂ) | 
| 15 |  | elfznn 13593 | . . . . . . 7
⊢ (𝑏 ∈ (1...𝐴) → 𝑏 ∈ ℕ) | 
| 16 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (!‘𝑎) = (!‘𝑏)) | 
| 17 | 16 | negeqd 11502 | . . . . . . . . 9
⊢ (𝑎 = 𝑏 → -(!‘𝑎) = -(!‘𝑏)) | 
| 18 | 17 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑎 = 𝑏 → (2↑-(!‘𝑎)) = (2↑-(!‘𝑏))) | 
| 19 |  | aaliou3lem.c | . . . . . . . 8
⊢ 𝐹 = (𝑎 ∈ ℕ ↦
(2↑-(!‘𝑎))) | 
| 20 |  | ovex 7464 | . . . . . . . 8
⊢
(2↑-(!‘𝑏)) ∈ V | 
| 21 | 18, 19, 20 | fvmpt 7016 | . . . . . . 7
⊢ (𝑏 ∈ ℕ → (𝐹‘𝑏) = (2↑-(!‘𝑏))) | 
| 22 | 15, 21 | syl 17 | . . . . . 6
⊢ (𝑏 ∈ (1...𝐴) → (𝐹‘𝑏) = (2↑-(!‘𝑏))) | 
| 23 | 22 | adantl 481 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (𝐹‘𝑏) = (2↑-(!‘𝑏))) | 
| 24 | 15 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → 𝑏 ∈ ℕ) | 
| 25 | 24 | nnnn0d 12587 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → 𝑏 ∈ ℕ0) | 
| 26 | 25 | faccld 14323 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝑏) ∈ ℕ) | 
| 27 | 26 | nnzd 12640 | . . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝑏) ∈ ℤ) | 
| 28 | 27 | znegcld 12724 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → -(!‘𝑏) ∈ ℤ) | 
| 29 |  | rpexpcl 14121 | . . . . . . 7
⊢ ((2
∈ ℝ+ ∧ -(!‘𝑏) ∈ ℤ) →
(2↑-(!‘𝑏))
∈ ℝ+) | 
| 30 | 8, 28, 29 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (2↑-(!‘𝑏)) ∈
ℝ+) | 
| 31 | 30 | rpcnd 13079 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (2↑-(!‘𝑏)) ∈
ℂ) | 
| 32 | 23, 31 | eqeltrd 2841 | . . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (𝐹‘𝑏) ∈ ℂ) | 
| 33 | 7, 14, 32 | fsummulc1 15821 | . . 3
⊢ (𝐴 ∈ ℕ →
(Σ𝑏 ∈ (1...𝐴)(𝐹‘𝑏) · (2↑(!‘𝐴))) = Σ𝑏 ∈ (1...𝐴)((𝐹‘𝑏) · (2↑(!‘𝐴)))) | 
| 34 | 23 | oveq1d 7446 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((𝐹‘𝑏) · (2↑(!‘𝐴))) = ((2↑-(!‘𝑏)) · (2↑(!‘𝐴)))) | 
| 35 | 11 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝐴) ∈ ℤ) | 
| 36 |  | 2cnne0 12476 | . . . . . . . 8
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 37 |  | expaddz 14147 | . . . . . . . 8
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (-(!‘𝑏) ∈ ℤ ∧ (!‘𝐴) ∈ ℤ)) →
(2↑(-(!‘𝑏) +
(!‘𝐴))) =
((2↑-(!‘𝑏))
· (2↑(!‘𝐴)))) | 
| 38 | 36, 37 | mpan 690 | . . . . . . 7
⊢
((-(!‘𝑏)
∈ ℤ ∧ (!‘𝐴) ∈ ℤ) →
(2↑(-(!‘𝑏) +
(!‘𝐴))) =
((2↑-(!‘𝑏))
· (2↑(!‘𝐴)))) | 
| 39 | 28, 35, 38 | syl2anc 584 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (2↑(-(!‘𝑏) + (!‘𝐴))) = ((2↑-(!‘𝑏)) · (2↑(!‘𝐴)))) | 
| 40 |  | 2z 12649 | . . . . . . 7
⊢ 2 ∈
ℤ | 
| 41 | 28 | zcnd 12723 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → -(!‘𝑏) ∈ ℂ) | 
| 42 | 35 | zcnd 12723 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝐴) ∈ ℂ) | 
| 43 | 41, 42 | addcomd 11463 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (-(!‘𝑏) + (!‘𝐴)) = ((!‘𝐴) + -(!‘𝑏))) | 
| 44 | 26 | nncnd 12282 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝑏) ∈ ℂ) | 
| 45 | 42, 44 | negsubd 11626 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((!‘𝐴) + -(!‘𝑏)) = ((!‘𝐴) − (!‘𝑏))) | 
| 46 | 43, 45 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (-(!‘𝑏) + (!‘𝐴)) = ((!‘𝐴) − (!‘𝑏))) | 
| 47 | 9 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → 𝐴 ∈
ℕ0) | 
| 48 |  | elfzle2 13568 | . . . . . . . . . . 11
⊢ (𝑏 ∈ (1...𝐴) → 𝑏 ≤ 𝐴) | 
| 49 | 48 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → 𝑏 ≤ 𝐴) | 
| 50 |  | facwordi 14328 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝑏
≤ 𝐴) →
(!‘𝑏) ≤
(!‘𝐴)) | 
| 51 | 25, 47, 49, 50 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝑏) ≤ (!‘𝐴)) | 
| 52 | 26 | nnnn0d 12587 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝑏) ∈
ℕ0) | 
| 53 | 47 | faccld 14323 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝐴) ∈ ℕ) | 
| 54 | 53 | nnnn0d 12587 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝐴) ∈
ℕ0) | 
| 55 |  | nn0sub 12576 | . . . . . . . . . 10
⊢
(((!‘𝑏) ∈
ℕ0 ∧ (!‘𝐴) ∈ ℕ0) →
((!‘𝑏) ≤
(!‘𝐴) ↔
((!‘𝐴) −
(!‘𝑏)) ∈
ℕ0)) | 
| 56 | 52, 54, 55 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((!‘𝑏) ≤ (!‘𝐴) ↔ ((!‘𝐴) − (!‘𝑏)) ∈
ℕ0)) | 
| 57 | 51, 56 | mpbid 232 | . . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((!‘𝐴) − (!‘𝑏)) ∈
ℕ0) | 
| 58 | 46, 57 | eqeltrd 2841 | . . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (-(!‘𝑏) + (!‘𝐴)) ∈
ℕ0) | 
| 59 |  | zexpcl 14117 | . . . . . . 7
⊢ ((2
∈ ℤ ∧ (-(!‘𝑏) + (!‘𝐴)) ∈ ℕ0) →
(2↑(-(!‘𝑏) +
(!‘𝐴))) ∈
ℤ) | 
| 60 | 40, 58, 59 | sylancr 587 | . . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (2↑(-(!‘𝑏) + (!‘𝐴))) ∈ ℤ) | 
| 61 | 39, 60 | eqeltrrd 2842 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((2↑-(!‘𝑏)) ·
(2↑(!‘𝐴)))
∈ ℤ) | 
| 62 | 34, 61 | eqeltrd 2841 | . . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((𝐹‘𝑏) · (2↑(!‘𝐴))) ∈ ℤ) | 
| 63 | 7, 62 | fsumzcl 15771 | . . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈ (1...𝐴)((𝐹‘𝑏) · (2↑(!‘𝐴))) ∈ ℤ) | 
| 64 | 33, 63 | eqeltrd 2841 | . 2
⊢ (𝐴 ∈ ℕ →
(Σ𝑏 ∈ (1...𝐴)(𝐹‘𝑏) · (2↑(!‘𝐴))) ∈ ℤ) | 
| 65 | 6, 64 | eqeltrd 2841 | 1
⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) · (2↑(!‘𝐴))) ∈
ℤ) |