Step | Hyp | Ref
| Expression |
1 | | 1red 10055 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → 1 ∈
ℝ) |
2 | | 0red 10041 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) ∧ ¬ (√‘(𝑃↑𝐴)) ∈ ℕ) → 0 ∈
ℝ) |
3 | 1, 2 | ifclda 4120 |
. . . 4
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ∈
ℝ) |
4 | | 1red 10055 |
. . . 4
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → 1 ∈
ℝ) |
5 | | fzfid 12772 |
. . . . . 6
⊢ (𝜑 → (0...𝐴) ∈ Fin) |
6 | | dchrisum0flb.r |
. . . . . . . 8
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) |
7 | | rpvmasum.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
8 | 7 | nnnn0d 11351 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
9 | | rpvmasum.z |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
10 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘𝑍) =
(Base‘𝑍) |
11 | | rpvmasum.l |
. . . . . . . . . . 11
⊢ 𝐿 = (ℤRHom‘𝑍) |
12 | 9, 10, 11 | znzrhfo 19896 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
13 | | fof 6115 |
. . . . . . . . . 10
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
14 | 8, 12, 13 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
15 | | dchrisum0flblem1.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℙ) |
16 | | prmz 15389 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℤ) |
18 | 14, 17 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (𝜑 → (𝐿‘𝑃) ∈ (Base‘𝑍)) |
19 | 6, 18 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝑋‘(𝐿‘𝑃)) ∈ ℝ) |
20 | | elfznn0 12433 |
. . . . . . 7
⊢ (𝑖 ∈ (0...𝐴) → 𝑖 ∈ ℕ0) |
21 | | reexpcl 12877 |
. . . . . . 7
⊢ (((𝑋‘(𝐿‘𝑃)) ∈ ℝ ∧ 𝑖 ∈ ℕ0) → ((𝑋‘(𝐿‘𝑃))↑𝑖) ∈ ℝ) |
22 | 19, 20, 21 | syl2an 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → ((𝑋‘(𝐿‘𝑃))↑𝑖) ∈ ℝ) |
23 | 5, 22 | fsumrecl 14465 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖) ∈ ℝ) |
24 | 23 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖) ∈ ℝ) |
25 | | breq1 4656 |
. . . . . 6
⊢ (1 =
if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) → (1 ≤ 1
↔ if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤
1)) |
26 | | breq1 4656 |
. . . . . 6
⊢ (0 =
if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) → (0 ≤ 1
↔ if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤
1)) |
27 | | 1le1 10655 |
. . . . . 6
⊢ 1 ≤
1 |
28 | | 0le1 10551 |
. . . . . 6
⊢ 0 ≤
1 |
29 | 25, 26, 27, 28 | keephyp 4152 |
. . . . 5
⊢
if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤
1 |
30 | 29 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤
1) |
31 | | dchrisum0flblem1.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℕ0) |
32 | | nn0uz 11722 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
33 | 31, 32 | syl6eleq 2711 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘0)) |
34 | | fzn0 12355 |
. . . . . . . . 9
⊢
((0...𝐴) ≠
∅ ↔ 𝐴 ∈
(ℤ≥‘0)) |
35 | 33, 34 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → (0...𝐴) ≠ ∅) |
36 | | hashnncl 13157 |
. . . . . . . . 9
⊢
((0...𝐴) ∈ Fin
→ ((#‘(0...𝐴))
∈ ℕ ↔ (0...𝐴) ≠ ∅)) |
37 | 5, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((#‘(0...𝐴)) ∈ ℕ ↔
(0...𝐴) ≠
∅)) |
38 | 35, 37 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → (#‘(0...𝐴)) ∈
ℕ) |
39 | 38 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → (#‘(0...𝐴)) ∈
ℕ) |
40 | 39 | nnge1d 11063 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → 1 ≤ (#‘(0...𝐴))) |
41 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → (𝑋‘(𝐿‘𝑃)) = 1) |
42 | 41 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → ((𝑋‘(𝐿‘𝑃))↑𝑖) = (1↑𝑖)) |
43 | | elfzelz 12342 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0...𝐴) → 𝑖 ∈ ℤ) |
44 | | 1exp 12889 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℤ →
(1↑𝑖) =
1) |
45 | 43, 44 | syl 17 |
. . . . . . . 8
⊢ (𝑖 ∈ (0...𝐴) → (1↑𝑖) = 1) |
46 | 42, 45 | sylan9eq 2676 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) ∧ 𝑖 ∈ (0...𝐴)) → ((𝑋‘(𝐿‘𝑃))↑𝑖) = 1) |
47 | 46 | sumeq2dv 14433 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖) = Σ𝑖 ∈ (0...𝐴)1) |
48 | | fzfid 12772 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → (0...𝐴) ∈ Fin) |
49 | | ax-1cn 9994 |
. . . . . . 7
⊢ 1 ∈
ℂ |
50 | | fsumconst 14522 |
. . . . . . 7
⊢
(((0...𝐴) ∈ Fin
∧ 1 ∈ ℂ) → Σ𝑖 ∈ (0...𝐴)1 = ((#‘(0...𝐴)) · 1)) |
51 | 48, 49, 50 | sylancl 694 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → Σ𝑖 ∈ (0...𝐴)1 = ((#‘(0...𝐴)) · 1)) |
52 | 39 | nncnd 11036 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → (#‘(0...𝐴)) ∈
ℂ) |
53 | 52 | mulid1d 10057 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → ((#‘(0...𝐴)) · 1) =
(#‘(0...𝐴))) |
54 | 47, 51, 53 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖) = (#‘(0...𝐴))) |
55 | 40, 54 | breqtrrd 4681 |
. . . 4
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → 1 ≤ Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖)) |
56 | 3, 4, 24, 30, 55 | letrd 10194 |
. . 3
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) = 1) → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖)) |
57 | | oveq1 6657 |
. . . . . . 7
⊢ (1 =
if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) → (1 ·
(1 − (𝑋‘(𝐿‘𝑃)))) = (if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) · (1 −
(𝑋‘(𝐿‘𝑃))))) |
58 | 57 | breq1d 4663 |
. . . . . 6
⊢ (1 =
if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) → ((1 ·
(1 − (𝑋‘(𝐿‘𝑃)))) ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ↔ (if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) · (1 −
(𝑋‘(𝐿‘𝑃)))) ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))))) |
59 | | oveq1 6657 |
. . . . . . 7
⊢ (0 =
if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) → (0 ·
(1 − (𝑋‘(𝐿‘𝑃)))) = (if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) · (1 −
(𝑋‘(𝐿‘𝑃))))) |
60 | 59 | breq1d 4663 |
. . . . . 6
⊢ (0 =
if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) → ((0 ·
(1 − (𝑋‘(𝐿‘𝑃)))) ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ↔ (if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) · (1 −
(𝑋‘(𝐿‘𝑃)))) ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))))) |
61 | | 1re 10039 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
62 | 19 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (𝑋‘(𝐿‘𝑃)) ∈ ℝ) |
63 | | resubcl 10345 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (𝑋‘(𝐿‘𝑃)) ∈ ℝ) → (1 − (𝑋‘(𝐿‘𝑃))) ∈ ℝ) |
64 | 61, 62, 63 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (1 − (𝑋‘(𝐿‘𝑃))) ∈ ℝ) |
65 | 64 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (1 − (𝑋‘(𝐿‘𝑃))) ∈ ℝ) |
66 | 65 | leidd 10594 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (1 − (𝑋‘(𝐿‘𝑃))) ≤ (1 − (𝑋‘(𝐿‘𝑃)))) |
67 | 64 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (1 − (𝑋‘(𝐿‘𝑃))) ∈ ℂ) |
68 | 67 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (1 − (𝑋‘(𝐿‘𝑃))) ∈ ℂ) |
69 | 68 | mulid2d 10058 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (1 · (1
− (𝑋‘(𝐿‘𝑃)))) = (1 − (𝑋‘(𝐿‘𝑃)))) |
70 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ0
→ (𝐴 + 1) ∈
ℕ) |
71 | 31, 70 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + 1) ∈ ℕ) |
72 | 71 | ad3antrrr 766 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) = 0) → (𝐴 + 1) ∈ ℕ) |
73 | 72 | 0expd 13024 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) = 0) → (0↑(𝐴 + 1)) = 0) |
74 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) = 0) → (𝑋‘(𝐿‘𝑃)) = 0) |
75 | 74 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) = 0) → ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) = (0↑(𝐴 + 1))) |
76 | 73, 75, 74 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) = 0) → ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) = (𝑋‘(𝐿‘𝑃))) |
77 | | neg1cn 11124 |
. . . . . . . . . . . . 13
⊢ -1 ∈
ℂ |
78 | 31 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → 𝐴 ∈
ℕ0) |
79 | | expp1 12867 |
. . . . . . . . . . . . 13
⊢ ((-1
∈ ℂ ∧ 𝐴
∈ ℕ0) → (-1↑(𝐴 + 1)) = ((-1↑𝐴) · -1)) |
80 | 77, 78, 79 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (-1↑(𝐴 + 1)) = ((-1↑𝐴) · -1)) |
81 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
82 | 15, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑃 ∈ ℕ) |
83 | 82, 31 | nnexpcld 13030 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑃↑𝐴) ∈ ℕ) |
84 | 83 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑃↑𝐴) ∈ ℂ) |
85 | 84 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (𝑃↑𝐴) ∈ ℂ) |
86 | 85 | sqsqrtd 14178 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) →
((√‘(𝑃↑𝐴))↑2) = (𝑃↑𝐴)) |
87 | 86 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (𝑃 pCnt ((√‘(𝑃↑𝐴))↑2)) = (𝑃 pCnt (𝑃↑𝐴))) |
88 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → 𝑃 ∈ ℙ) |
89 | | nnq 11801 |
. . . . . . . . . . . . . . . . . . 19
⊢
((√‘(𝑃↑𝐴)) ∈ ℕ →
(√‘(𝑃↑𝐴)) ∈ ℚ) |
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) →
(√‘(𝑃↑𝐴)) ∈ ℚ) |
91 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . 19
⊢
((√‘(𝑃↑𝐴)) ∈ ℕ →
(√‘(𝑃↑𝐴)) ≠ 0) |
92 | 91 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) →
(√‘(𝑃↑𝐴)) ≠ 0) |
93 | | 2z 11409 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℤ |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → 2 ∈
ℤ) |
95 | | pcexp 15564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧
((√‘(𝑃↑𝐴)) ∈ ℚ ∧
(√‘(𝑃↑𝐴)) ≠ 0) ∧ 2 ∈ ℤ) →
(𝑃 pCnt
((√‘(𝑃↑𝐴))↑2)) = (2 · (𝑃 pCnt (√‘(𝑃↑𝐴))))) |
96 | 88, 90, 92, 94, 95 | syl121anc 1331 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (𝑃 pCnt ((√‘(𝑃↑𝐴))↑2)) = (2 · (𝑃 pCnt (√‘(𝑃↑𝐴))))) |
97 | 78 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → 𝐴 ∈ ℤ) |
98 | | pcid 15577 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) |
99 | 88, 97, 98 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) |
100 | 87, 96, 99 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → 𝐴 = (2 · (𝑃 pCnt (√‘(𝑃↑𝐴))))) |
101 | 100 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (-1↑𝐴) = (-1↑(2 · (𝑃 pCnt (√‘(𝑃↑𝐴)))))) |
102 | 77 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → -1 ∈
ℂ) |
103 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) →
(√‘(𝑃↑𝐴)) ∈ ℕ) |
104 | 88, 103 | pccld 15555 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (𝑃 pCnt (√‘(𝑃↑𝐴))) ∈
ℕ0) |
105 | | 2nn0 11309 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ0 |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → 2 ∈
ℕ0) |
107 | 102, 104,
106 | expmuld 13011 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (-1↑(2
· (𝑃 pCnt
(√‘(𝑃↑𝐴))))) = ((-1↑2)↑(𝑃 pCnt (√‘(𝑃↑𝐴))))) |
108 | | neg1sqe1 12959 |
. . . . . . . . . . . . . . . . 17
⊢
(-1↑2) = 1 |
109 | 108 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
⊢
((-1↑2)↑(𝑃
pCnt (√‘(𝑃↑𝐴)))) = (1↑(𝑃 pCnt (√‘(𝑃↑𝐴)))) |
110 | 104 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (𝑃 pCnt (√‘(𝑃↑𝐴))) ∈ ℤ) |
111 | | 1exp 12889 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 pCnt (√‘(𝑃↑𝐴))) ∈ ℤ → (1↑(𝑃 pCnt (√‘(𝑃↑𝐴)))) = 1) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (1↑(𝑃 pCnt (√‘(𝑃↑𝐴)))) = 1) |
113 | 109, 112 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) →
((-1↑2)↑(𝑃 pCnt
(√‘(𝑃↑𝐴)))) = 1) |
114 | 101, 107,
113 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (-1↑𝐴) = 1) |
115 | 114 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → ((-1↑𝐴) · -1) = (1 ·
-1)) |
116 | 77 | mulid2i 10043 |
. . . . . . . . . . . . 13
⊢ (1
· -1) = -1 |
117 | 115, 116 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → ((-1↑𝐴) · -1) =
-1) |
118 | 80, 117 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (-1↑(𝐴 + 1)) = -1) |
119 | 118 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → (-1↑(𝐴 + 1)) = -1) |
120 | 19 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋‘(𝐿‘𝑃)) ∈ ℂ) |
121 | 120 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (𝑋‘(𝐿‘𝑃)) ∈ ℂ) |
122 | 121 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → (𝑋‘(𝐿‘𝑃)) ∈ ℂ) |
123 | 122 | negnegd 10383 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → --(𝑋‘(𝐿‘𝑃)) = (𝑋‘(𝐿‘𝑃))) |
124 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (𝑋‘(𝐿‘𝑃)) ≠ 1) |
125 | 124 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → (𝑋‘(𝐿‘𝑃)) ≠ 1) |
126 | | rpvmasum2.g |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐺 = (DChr‘𝑁) |
127 | | rpvmasum2.d |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐷 = (Base‘𝐺) |
128 | | dchrisum0f.x |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
129 | 128 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → 𝑋 ∈ 𝐷) |
130 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Unit‘𝑍) =
(Unit‘𝑍) |
131 | 126, 9, 127, 10, 130, 128, 18 | dchrn0 24975 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑋‘(𝐿‘𝑃)) ≠ 0 ↔ (𝐿‘𝑃) ∈ (Unit‘𝑍))) |
132 | 131 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → ((𝑋‘(𝐿‘𝑃)) ≠ 0 ↔ (𝐿‘𝑃) ∈ (Unit‘𝑍))) |
133 | 132 | biimpa 501 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → (𝐿‘𝑃) ∈ (Unit‘𝑍)) |
134 | 126, 127,
129, 9, 130, 133 | dchrabs 24985 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → (abs‘(𝑋‘(𝐿‘𝑃))) = 1) |
135 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . 18
⊢
((abs‘(𝑋‘(𝐿‘𝑃))) = (𝑋‘(𝐿‘𝑃)) → ((abs‘(𝑋‘(𝐿‘𝑃))) = 1 ↔ (𝑋‘(𝐿‘𝑃)) = 1)) |
136 | 134, 135 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → ((abs‘(𝑋‘(𝐿‘𝑃))) = (𝑋‘(𝐿‘𝑃)) → (𝑋‘(𝐿‘𝑃)) = 1)) |
137 | 136 | necon3ad 2807 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → ((𝑋‘(𝐿‘𝑃)) ≠ 1 → ¬ (abs‘(𝑋‘(𝐿‘𝑃))) = (𝑋‘(𝐿‘𝑃)))) |
138 | 125, 137 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → ¬ (abs‘(𝑋‘(𝐿‘𝑃))) = (𝑋‘(𝐿‘𝑃))) |
139 | 62 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → (𝑋‘(𝐿‘𝑃)) ∈ ℝ) |
140 | 139 | absord 14154 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → ((abs‘(𝑋‘(𝐿‘𝑃))) = (𝑋‘(𝐿‘𝑃)) ∨ (abs‘(𝑋‘(𝐿‘𝑃))) = -(𝑋‘(𝐿‘𝑃)))) |
141 | 140 | ord 392 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → (¬ (abs‘(𝑋‘(𝐿‘𝑃))) = (𝑋‘(𝐿‘𝑃)) → (abs‘(𝑋‘(𝐿‘𝑃))) = -(𝑋‘(𝐿‘𝑃)))) |
142 | 138, 141 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → (abs‘(𝑋‘(𝐿‘𝑃))) = -(𝑋‘(𝐿‘𝑃))) |
143 | 142, 134 | eqtr3d 2658 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → -(𝑋‘(𝐿‘𝑃)) = 1) |
144 | 143 | negeqd 10275 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → --(𝑋‘(𝐿‘𝑃)) = -1) |
145 | 123, 144 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → (𝑋‘(𝐿‘𝑃)) = -1) |
146 | 145 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) = (-1↑(𝐴 + 1))) |
147 | 119, 146,
145 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) ∧ (𝑋‘(𝐿‘𝑃)) ≠ 0) → ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) = (𝑋‘(𝐿‘𝑃))) |
148 | 76, 147 | pm2.61dane 2881 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) = (𝑋‘(𝐿‘𝑃))) |
149 | 148 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) = (1 − (𝑋‘(𝐿‘𝑃)))) |
150 | 66, 69, 149 | 3brtr4d 4685 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ (√‘(𝑃↑𝐴)) ∈ ℕ) → (1 · (1
− (𝑋‘(𝐿‘𝑃)))) ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)))) |
151 | 67 | mul02d 10234 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (0 · (1 −
(𝑋‘(𝐿‘𝑃)))) = 0) |
152 | | peano2nn0 11333 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ0
→ (𝐴 + 1) ∈
ℕ0) |
153 | 31, 152 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + 1) ∈
ℕ0) |
154 | 19, 153 | reexpcld 13025 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) ∈ ℝ) |
155 | 154 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) ∈ ℝ) |
156 | 155 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) ∈ ℂ) |
157 | 156 | abscld 14175 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (abs‘((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ∈ ℝ) |
158 | | 1red 10055 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → 1 ∈
ℝ) |
159 | 155 | leabsd 14153 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) ≤ (abs‘((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)))) |
160 | 153 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (𝐴 + 1) ∈
ℕ0) |
161 | 121, 160 | absexpd 14191 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (abs‘((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) = ((abs‘(𝑋‘(𝐿‘𝑃)))↑(𝐴 + 1))) |
162 | 121 | abscld 14175 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (abs‘(𝑋‘(𝐿‘𝑃))) ∈ ℝ) |
163 | 121 | absge0d 14183 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → 0 ≤ (abs‘(𝑋‘(𝐿‘𝑃)))) |
164 | 126, 127,
9, 10, 128, 18 | dchrabs2 24987 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘(𝑋‘(𝐿‘𝑃))) ≤ 1) |
165 | 164 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (abs‘(𝑋‘(𝐿‘𝑃))) ≤ 1) |
166 | | exple1 12920 |
. . . . . . . . . . . 12
⊢
((((abs‘(𝑋‘(𝐿‘𝑃))) ∈ ℝ ∧ 0 ≤
(abs‘(𝑋‘(𝐿‘𝑃))) ∧ (abs‘(𝑋‘(𝐿‘𝑃))) ≤ 1) ∧ (𝐴 + 1) ∈ ℕ0) →
((abs‘(𝑋‘(𝐿‘𝑃)))↑(𝐴 + 1)) ≤ 1) |
167 | 162, 163,
165, 160, 166 | syl31anc 1329 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → ((abs‘(𝑋‘(𝐿‘𝑃)))↑(𝐴 + 1)) ≤ 1) |
168 | 161, 167 | eqbrtrd 4675 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (abs‘((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ≤ 1) |
169 | 155, 157,
158, 159, 168 | letrd 10194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) ≤ 1) |
170 | | subge0 10541 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) ∈ ℝ) → (0 ≤ (1
− ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ↔ ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) ≤ 1)) |
171 | 61, 155, 170 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (0 ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ↔ ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) ≤ 1)) |
172 | 169, 171 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → 0 ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)))) |
173 | 151, 172 | eqbrtrd 4675 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (0 · (1 −
(𝑋‘(𝐿‘𝑃)))) ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)))) |
174 | 173 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) ∧ ¬ (√‘(𝑃↑𝐴)) ∈ ℕ) → (0 · (1
− (𝑋‘(𝐿‘𝑃)))) ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)))) |
175 | 58, 60, 150, 174 | ifbothda 4123 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) · (1 −
(𝑋‘(𝐿‘𝑃)))) ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)))) |
176 | | 0re 10040 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
177 | 61, 176 | keepel 4155 |
. . . . . . 7
⊢
if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ∈
ℝ |
178 | 177 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ∈
ℝ) |
179 | | resubcl 10345 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)) ∈ ℝ) → (1 −
((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ∈ ℝ) |
180 | 61, 155, 179 | sylancr 695 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ∈ ℝ) |
181 | 124 | necomd 2849 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → 1 ≠ (𝑋‘(𝐿‘𝑃))) |
182 | 62 | leabsd 14153 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (𝑋‘(𝐿‘𝑃)) ≤ (abs‘(𝑋‘(𝐿‘𝑃)))) |
183 | 62, 162, 158, 182, 165 | letrd 10194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (𝑋‘(𝐿‘𝑃)) ≤ 1) |
184 | 62, 158, 183 | leltned 10190 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → ((𝑋‘(𝐿‘𝑃)) < 1 ↔ 1 ≠ (𝑋‘(𝐿‘𝑃)))) |
185 | 181, 184 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (𝑋‘(𝐿‘𝑃)) < 1) |
186 | | posdif 10521 |
. . . . . . . 8
⊢ (((𝑋‘(𝐿‘𝑃)) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝑋‘(𝐿‘𝑃)) < 1 ↔ 0 < (1 − (𝑋‘(𝐿‘𝑃))))) |
187 | 62, 61, 186 | sylancl 694 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → ((𝑋‘(𝐿‘𝑃)) < 1 ↔ 0 < (1 − (𝑋‘(𝐿‘𝑃))))) |
188 | 185, 187 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → 0 < (1 − (𝑋‘(𝐿‘𝑃)))) |
189 | | lemuldiv 10903 |
. . . . . 6
⊢
((if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ∈ ℝ
∧ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ∈ ℝ ∧ ((1 −
(𝑋‘(𝐿‘𝑃))) ∈ ℝ ∧ 0 < (1 −
(𝑋‘(𝐿‘𝑃))))) → ((if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) · (1 −
(𝑋‘(𝐿‘𝑃)))) ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ↔ if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ ((1 −
((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) / (1 − (𝑋‘(𝐿‘𝑃)))))) |
190 | 178, 180,
64, 188, 189 | syl112anc 1330 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → ((if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) · (1 −
(𝑋‘(𝐿‘𝑃)))) ≤ (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) ↔ if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ ((1 −
((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) / (1 − (𝑋‘(𝐿‘𝑃)))))) |
191 | 175, 190 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ ((1 −
((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) / (1 − (𝑋‘(𝐿‘𝑃))))) |
192 | 31 | nn0zd 11480 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℤ) |
193 | | fzval3 12536 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ →
(0...𝐴) = (0..^(𝐴 + 1))) |
194 | 192, 193 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0...𝐴) = (0..^(𝐴 + 1))) |
195 | 194 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (0...𝐴) = (0..^(𝐴 + 1))) |
196 | 195 | sumeq1d 14431 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖) = Σ𝑖 ∈ (0..^(𝐴 + 1))((𝑋‘(𝐿‘𝑃))↑𝑖)) |
197 | | 0nn0 11307 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
198 | 197 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → 0 ∈
ℕ0) |
199 | 153, 32 | syl6eleq 2711 |
. . . . . . 7
⊢ (𝜑 → (𝐴 + 1) ∈
(ℤ≥‘0)) |
200 | 199 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (𝐴 + 1) ∈
(ℤ≥‘0)) |
201 | 121, 124,
198, 200 | geoserg 14598 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → Σ𝑖 ∈ (0..^(𝐴 + 1))((𝑋‘(𝐿‘𝑃))↑𝑖) = ((((𝑋‘(𝐿‘𝑃))↑0) − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) / (1 − (𝑋‘(𝐿‘𝑃))))) |
202 | 121 | exp0d 13002 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → ((𝑋‘(𝐿‘𝑃))↑0) = 1) |
203 | 202 | oveq1d 6665 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → (((𝑋‘(𝐿‘𝑃))↑0) − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) = (1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1)))) |
204 | 203 | oveq1d 6665 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → ((((𝑋‘(𝐿‘𝑃))↑0) − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) / (1 − (𝑋‘(𝐿‘𝑃)))) = ((1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) / (1 − (𝑋‘(𝐿‘𝑃))))) |
205 | 196, 201,
204 | 3eqtrd 2660 |
. . . 4
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖) = ((1 − ((𝑋‘(𝐿‘𝑃))↑(𝐴 + 1))) / (1 − (𝑋‘(𝐿‘𝑃))))) |
206 | 191, 205 | breqtrrd 4681 |
. . 3
⊢ ((𝜑 ∧ (𝑋‘(𝐿‘𝑃)) ≠ 1) → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖)) |
207 | 56, 206 | pm2.61dane 2881 |
. 2
⊢ (𝜑 → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖)) |
208 | | rpvmasum2.1 |
. . . . 5
⊢ 1 =
(0g‘𝐺) |
209 | | dchrisum0f.f |
. . . . 5
⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) |
210 | 9, 11, 7, 126, 127, 208, 209 | dchrisum0fval 25194 |
. . . 4
⊢ ((𝑃↑𝐴) ∈ ℕ → (𝐹‘(𝑃↑𝐴)) = Σ𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)} (𝑋‘(𝐿‘𝑘))) |
211 | 83, 210 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹‘(𝑃↑𝐴)) = Σ𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)} (𝑋‘(𝐿‘𝑘))) |
212 | | fveq2 6191 |
. . . . 5
⊢ (𝑘 = (𝑃↑𝑖) → (𝐿‘𝑘) = (𝐿‘(𝑃↑𝑖))) |
213 | 212 | fveq2d 6195 |
. . . 4
⊢ (𝑘 = (𝑃↑𝑖) → (𝑋‘(𝐿‘𝑘)) = (𝑋‘(𝐿‘(𝑃↑𝑖)))) |
214 | | eqid 2622 |
. . . . . 6
⊢ (𝑏 ∈ (0...𝐴) ↦ (𝑃↑𝑏)) = (𝑏 ∈ (0...𝐴) ↦ (𝑃↑𝑏)) |
215 | 214 | dvdsppwf1o 24912 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
→ (𝑏 ∈ (0...𝐴) ↦ (𝑃↑𝑏)):(0...𝐴)–1-1-onto→{𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)}) |
216 | 15, 31, 215 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ (0...𝐴) ↦ (𝑃↑𝑏)):(0...𝐴)–1-1-onto→{𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)}) |
217 | | oveq2 6658 |
. . . . . 6
⊢ (𝑏 = 𝑖 → (𝑃↑𝑏) = (𝑃↑𝑖)) |
218 | | ovex 6678 |
. . . . . 6
⊢ (𝑃↑𝑏) ∈ V |
219 | 217, 214,
218 | fvmpt3i 6287 |
. . . . 5
⊢ (𝑖 ∈ (0...𝐴) → ((𝑏 ∈ (0...𝐴) ↦ (𝑃↑𝑏))‘𝑖) = (𝑃↑𝑖)) |
220 | 219 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → ((𝑏 ∈ (0...𝐴) ↦ (𝑃↑𝑏))‘𝑖) = (𝑃↑𝑖)) |
221 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)}) → 𝑋:(Base‘𝑍)⟶ℝ) |
222 | | elrabi 3359 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)} → 𝑘 ∈ ℕ) |
223 | 222 | nnzd 11481 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)} → 𝑘 ∈ ℤ) |
224 | | ffvelrn 6357 |
. . . . . . 7
⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑘 ∈ ℤ) → (𝐿‘𝑘) ∈ (Base‘𝑍)) |
225 | 14, 223, 224 | syl2an 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)}) → (𝐿‘𝑘) ∈ (Base‘𝑍)) |
226 | 221, 225 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)}) → (𝑋‘(𝐿‘𝑘)) ∈ ℝ) |
227 | 226 | recnd 10068 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)}) → (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
228 | 213, 5, 216, 220, 227 | fsumf1o 14454 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝑃↑𝐴)} (𝑋‘(𝐿‘𝑘)) = Σ𝑖 ∈ (0...𝐴)(𝑋‘(𝐿‘(𝑃↑𝑖)))) |
229 | | zsubrg 19799 |
. . . . . . . . . . 11
⊢ ℤ
∈ (SubRing‘ℂfld) |
230 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
231 | 230 | subrgsubm 18793 |
. . . . . . . . . . 11
⊢ (ℤ
∈ (SubRing‘ℂfld) → ℤ ∈
(SubMnd‘(mulGrp‘ℂfld))) |
232 | 229, 231 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → ℤ ∈
(SubMnd‘(mulGrp‘ℂfld))) |
233 | 20 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → 𝑖 ∈ ℕ0) |
234 | 17 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → 𝑃 ∈ ℤ) |
235 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
236 | | zringmpg 19840 |
. . . . . . . . . . . 12
⊢
((mulGrp‘ℂfld) ↾s ℤ) =
(mulGrp‘ℤring) |
237 | 236 | eqcomi 2631 |
. . . . . . . . . . 11
⊢
(mulGrp‘ℤring) =
((mulGrp‘ℂfld) ↾s
ℤ) |
238 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(.g‘(mulGrp‘ℤring)) =
(.g‘(mulGrp‘ℤring)) |
239 | 235, 237,
238 | submmulg 17586 |
. . . . . . . . . 10
⊢ ((ℤ
∈ (SubMnd‘(mulGrp‘ℂfld)) ∧ 𝑖 ∈ ℕ0
∧ 𝑃 ∈ ℤ)
→ (𝑖(.g‘(mulGrp‘ℂfld))𝑃) = (𝑖(.g‘(mulGrp‘ℤring))𝑃)) |
240 | 232, 233,
234, 239 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝑖(.g‘(mulGrp‘ℂfld))𝑃) = (𝑖(.g‘(mulGrp‘ℤring))𝑃)) |
241 | 82 | nncnd 11036 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℂ) |
242 | | cnfldexp 19779 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℂ ∧ 𝑖 ∈ ℕ0)
→ (𝑖(.g‘(mulGrp‘ℂfld))𝑃) = (𝑃↑𝑖)) |
243 | 241, 20, 242 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝑖(.g‘(mulGrp‘ℂfld))𝑃) = (𝑃↑𝑖)) |
244 | 240, 243 | eqtr3d 2658 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝑖(.g‘(mulGrp‘ℤring))𝑃) = (𝑃↑𝑖)) |
245 | 244 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝐿‘(𝑖(.g‘(mulGrp‘ℤring))𝑃)) = (𝐿‘(𝑃↑𝑖))) |
246 | 9 | zncrng 19893 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
247 | | crngring 18558 |
. . . . . . . . . . 11
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
248 | 8, 246, 247 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ Ring) |
249 | 11 | zrhrhm 19860 |
. . . . . . . . . 10
⊢ (𝑍 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑍)) |
250 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(mulGrp‘ℤring) =
(mulGrp‘ℤring) |
251 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
252 | 250, 251 | rhmmhm 18722 |
. . . . . . . . . 10
⊢ (𝐿 ∈ (ℤring
RingHom 𝑍) → 𝐿 ∈
((mulGrp‘ℤring) MndHom (mulGrp‘𝑍))) |
253 | 248, 249,
252 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈
((mulGrp‘ℤring) MndHom (mulGrp‘𝑍))) |
254 | 253 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → 𝐿 ∈
((mulGrp‘ℤring) MndHom (mulGrp‘𝑍))) |
255 | | zringbas 19824 |
. . . . . . . . . 10
⊢ ℤ =
(Base‘ℤring) |
256 | 250, 255 | mgpbas 18495 |
. . . . . . . . 9
⊢ ℤ =
(Base‘(mulGrp‘ℤring)) |
257 | | eqid 2622 |
. . . . . . . . 9
⊢
(.g‘(mulGrp‘𝑍)) =
(.g‘(mulGrp‘𝑍)) |
258 | 256, 238,
257 | mhmmulg 17583 |
. . . . . . . 8
⊢ ((𝐿 ∈
((mulGrp‘ℤring) MndHom (mulGrp‘𝑍)) ∧ 𝑖 ∈ ℕ0 ∧ 𝑃 ∈ ℤ) → (𝐿‘(𝑖(.g‘(mulGrp‘ℤring))𝑃)) = (𝑖(.g‘(mulGrp‘𝑍))(𝐿‘𝑃))) |
259 | 254, 233,
234, 258 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝐿‘(𝑖(.g‘(mulGrp‘ℤring))𝑃)) = (𝑖(.g‘(mulGrp‘𝑍))(𝐿‘𝑃))) |
260 | 245, 259 | eqtr3d 2658 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝐿‘(𝑃↑𝑖)) = (𝑖(.g‘(mulGrp‘𝑍))(𝐿‘𝑃))) |
261 | 260 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝑋‘(𝐿‘(𝑃↑𝑖))) = (𝑋‘(𝑖(.g‘(mulGrp‘𝑍))(𝐿‘𝑃)))) |
262 | 126, 9, 127 | dchrmhm 24966 |
. . . . . . . 8
⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) |
263 | 262, 128 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
264 | 263 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
265 | 18 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝐿‘𝑃) ∈ (Base‘𝑍)) |
266 | 251, 10 | mgpbas 18495 |
. . . . . . 7
⊢
(Base‘𝑍) =
(Base‘(mulGrp‘𝑍)) |
267 | 266, 257,
235 | mhmmulg 17583 |
. . . . . 6
⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ 𝑖 ∈ ℕ0 ∧ (𝐿‘𝑃) ∈ (Base‘𝑍)) → (𝑋‘(𝑖(.g‘(mulGrp‘𝑍))(𝐿‘𝑃))) = (𝑖(.g‘(mulGrp‘ℂfld))(𝑋‘(𝐿‘𝑃)))) |
268 | 264, 233,
265, 267 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝑋‘(𝑖(.g‘(mulGrp‘𝑍))(𝐿‘𝑃))) = (𝑖(.g‘(mulGrp‘ℂfld))(𝑋‘(𝐿‘𝑃)))) |
269 | | cnfldexp 19779 |
. . . . . 6
⊢ (((𝑋‘(𝐿‘𝑃)) ∈ ℂ ∧ 𝑖 ∈ ℕ0) → (𝑖(.g‘(mulGrp‘ℂfld))(𝑋‘(𝐿‘𝑃)))
= ((𝑋‘(𝐿‘𝑃))↑𝑖)) |
270 | 120, 20, 269 | syl2an 494 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝑖(.g‘(mulGrp‘ℂfld))(𝑋‘(𝐿‘𝑃)))
= ((𝑋‘(𝐿‘𝑃))↑𝑖)) |
271 | 261, 268,
270 | 3eqtrd 2660 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐴)) → (𝑋‘(𝐿‘(𝑃↑𝑖))) = ((𝑋‘(𝐿‘𝑃))↑𝑖)) |
272 | 271 | sumeq2dv 14433 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ (0...𝐴)(𝑋‘(𝐿‘(𝑃↑𝑖))) = Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖)) |
273 | 211, 228,
272 | 3eqtrd 2660 |
. 2
⊢ (𝜑 → (𝐹‘(𝑃↑𝐴)) = Σ𝑖 ∈ (0...𝐴)((𝑋‘(𝐿‘𝑃))↑𝑖)) |
274 | 207, 273 | breqtrrd 4681 |
1
⊢ (𝜑 → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑𝐴))) |