Proof of Theorem aaliou3lem6
Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . 5
⊢ (𝑐 = 𝐴 → (1...𝑐) = (1...𝐴)) |
2 | 1 | sumeq1d 14431 |
. . . 4
⊢ (𝑐 = 𝐴 → Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏) = Σ𝑏 ∈ (1...𝐴)(𝐹‘𝑏)) |
3 | | aaliou3lem.e |
. . . 4
⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) |
4 | | sumex 14418 |
. . . 4
⊢
Σ𝑏 ∈
(1...𝐴)(𝐹‘𝑏) ∈ V |
5 | 2, 3, 4 | fvmpt 6282 |
. . 3
⊢ (𝐴 ∈ ℕ → (𝐻‘𝐴) = Σ𝑏 ∈ (1...𝐴)(𝐹‘𝑏)) |
6 | 5 | oveq1d 6665 |
. 2
⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) · (2↑(!‘𝐴))) = (Σ𝑏 ∈ (1...𝐴)(𝐹‘𝑏) · (2↑(!‘𝐴)))) |
7 | | fzfid 12772 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(1...𝐴) ∈
Fin) |
8 | | 2rp 11837 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
9 | | nnnn0 11299 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
10 | | faccl 13070 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ0
→ (!‘𝐴) ∈
ℕ) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℕ) |
12 | 11 | nnzd 11481 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℤ) |
13 | | rpexpcl 12879 |
. . . . . 6
⊢ ((2
∈ ℝ+ ∧ (!‘𝐴) ∈ ℤ) →
(2↑(!‘𝐴)) ∈
ℝ+) |
14 | 8, 12, 13 | sylancr 695 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
(2↑(!‘𝐴)) ∈
ℝ+) |
15 | 14 | rpcnd 11874 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(2↑(!‘𝐴)) ∈
ℂ) |
16 | | elfznn 12370 |
. . . . . . 7
⊢ (𝑏 ∈ (1...𝐴) → 𝑏 ∈ ℕ) |
17 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (!‘𝑎) = (!‘𝑏)) |
18 | 17 | negeqd 10275 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → -(!‘𝑎) = -(!‘𝑏)) |
19 | 18 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (2↑-(!‘𝑎)) = (2↑-(!‘𝑏))) |
20 | | aaliou3lem.c |
. . . . . . . 8
⊢ 𝐹 = (𝑎 ∈ ℕ ↦
(2↑-(!‘𝑎))) |
21 | | ovex 6678 |
. . . . . . . 8
⊢
(2↑-(!‘𝑏)) ∈ V |
22 | 19, 20, 21 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑏 ∈ ℕ → (𝐹‘𝑏) = (2↑-(!‘𝑏))) |
23 | 16, 22 | syl 17 |
. . . . . 6
⊢ (𝑏 ∈ (1...𝐴) → (𝐹‘𝑏) = (2↑-(!‘𝑏))) |
24 | 23 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (𝐹‘𝑏) = (2↑-(!‘𝑏))) |
25 | 16 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → 𝑏 ∈ ℕ) |
26 | 25 | nnnn0d 11351 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → 𝑏 ∈ ℕ0) |
27 | | faccl 13070 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ℕ0
→ (!‘𝑏) ∈
ℕ) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝑏) ∈ ℕ) |
29 | 28 | nnzd 11481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝑏) ∈ ℤ) |
30 | 29 | znegcld 11484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → -(!‘𝑏) ∈ ℤ) |
31 | | rpexpcl 12879 |
. . . . . . 7
⊢ ((2
∈ ℝ+ ∧ -(!‘𝑏) ∈ ℤ) →
(2↑-(!‘𝑏))
∈ ℝ+) |
32 | 8, 30, 31 | sylancr 695 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (2↑-(!‘𝑏)) ∈
ℝ+) |
33 | 32 | rpcnd 11874 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (2↑-(!‘𝑏)) ∈
ℂ) |
34 | 24, 33 | eqeltrd 2701 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (𝐹‘𝑏) ∈ ℂ) |
35 | 7, 15, 34 | fsummulc1 14517 |
. . 3
⊢ (𝐴 ∈ ℕ →
(Σ𝑏 ∈ (1...𝐴)(𝐹‘𝑏) · (2↑(!‘𝐴))) = Σ𝑏 ∈ (1...𝐴)((𝐹‘𝑏) · (2↑(!‘𝐴)))) |
36 | 24 | oveq1d 6665 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((𝐹‘𝑏) · (2↑(!‘𝐴))) = ((2↑-(!‘𝑏)) · (2↑(!‘𝐴)))) |
37 | 12 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝐴) ∈ ℤ) |
38 | | 2cnne0 11242 |
. . . . . . . 8
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
39 | | expaddz 12904 |
. . . . . . . 8
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ (-(!‘𝑏) ∈ ℤ ∧ (!‘𝐴) ∈ ℤ)) →
(2↑(-(!‘𝑏) +
(!‘𝐴))) =
((2↑-(!‘𝑏))
· (2↑(!‘𝐴)))) |
40 | 38, 39 | mpan 706 |
. . . . . . 7
⊢
((-(!‘𝑏)
∈ ℤ ∧ (!‘𝐴) ∈ ℤ) →
(2↑(-(!‘𝑏) +
(!‘𝐴))) =
((2↑-(!‘𝑏))
· (2↑(!‘𝐴)))) |
41 | 30, 37, 40 | syl2anc 693 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (2↑(-(!‘𝑏) + (!‘𝐴))) = ((2↑-(!‘𝑏)) · (2↑(!‘𝐴)))) |
42 | | 2z 11409 |
. . . . . . 7
⊢ 2 ∈
ℤ |
43 | 30 | zcnd 11483 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → -(!‘𝑏) ∈ ℂ) |
44 | 37 | zcnd 11483 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝐴) ∈ ℂ) |
45 | 43, 44 | addcomd 10238 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (-(!‘𝑏) + (!‘𝐴)) = ((!‘𝐴) + -(!‘𝑏))) |
46 | 28 | nncnd 11036 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝑏) ∈ ℂ) |
47 | 44, 46 | negsubd 10398 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((!‘𝐴) + -(!‘𝑏)) = ((!‘𝐴) − (!‘𝑏))) |
48 | 45, 47 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (-(!‘𝑏) + (!‘𝐴)) = ((!‘𝐴) − (!‘𝑏))) |
49 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → 𝐴 ∈
ℕ0) |
50 | | elfzle2 12345 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (1...𝐴) → 𝑏 ≤ 𝐴) |
51 | 50 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → 𝑏 ≤ 𝐴) |
52 | | facwordi 13076 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝑏
≤ 𝐴) →
(!‘𝑏) ≤
(!‘𝐴)) |
53 | 26, 49, 51, 52 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝑏) ≤ (!‘𝐴)) |
54 | 28 | nnnn0d 11351 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝑏) ∈
ℕ0) |
55 | 49, 10 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝐴) ∈ ℕ) |
56 | 55 | nnnn0d 11351 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (!‘𝐴) ∈
ℕ0) |
57 | | nn0sub 11343 |
. . . . . . . . . 10
⊢
(((!‘𝑏) ∈
ℕ0 ∧ (!‘𝐴) ∈ ℕ0) →
((!‘𝑏) ≤
(!‘𝐴) ↔
((!‘𝐴) −
(!‘𝑏)) ∈
ℕ0)) |
58 | 54, 56, 57 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((!‘𝑏) ≤ (!‘𝐴) ↔ ((!‘𝐴) − (!‘𝑏)) ∈
ℕ0)) |
59 | 53, 58 | mpbid 222 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((!‘𝐴) − (!‘𝑏)) ∈
ℕ0) |
60 | 48, 59 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (-(!‘𝑏) + (!‘𝐴)) ∈
ℕ0) |
61 | | zexpcl 12875 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ (-(!‘𝑏) + (!‘𝐴)) ∈ ℕ0) →
(2↑(-(!‘𝑏) +
(!‘𝐴))) ∈
ℤ) |
62 | 42, 60, 61 | sylancr 695 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → (2↑(-(!‘𝑏) + (!‘𝐴))) ∈ ℤ) |
63 | 41, 62 | eqeltrrd 2702 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((2↑-(!‘𝑏)) ·
(2↑(!‘𝐴)))
∈ ℤ) |
64 | 36, 63 | eqeltrd 2701 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈ (1...𝐴)) → ((𝐹‘𝑏) · (2↑(!‘𝐴))) ∈ ℤ) |
65 | 7, 64 | fsumzcl 14466 |
. . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈ (1...𝐴)((𝐹‘𝑏) · (2↑(!‘𝐴))) ∈ ℤ) |
66 | 35, 65 | eqeltrd 2701 |
. 2
⊢ (𝐴 ∈ ℕ →
(Σ𝑏 ∈ (1...𝐴)(𝐹‘𝑏) · (2↑(!‘𝐴))) ∈ ℤ) |
67 | 6, 66 | eqeltrd 2701 |
1
⊢ (𝐴 ∈ ℕ → ((𝐻‘𝐴) · (2↑(!‘𝐴))) ∈
ℤ) |