Step |
Hyp |
Ref |
Expression |
1 |
|
rpvmasum.z |
⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) |
2 |
|
rpvmasum.l |
⊢ 𝐿 = ( ℤRHom ‘ 𝑍 ) |
3 |
|
rpvmasum.a |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
4 |
|
rpvmasum2.g |
⊢ 𝐺 = ( DChr ‘ 𝑁 ) |
5 |
|
rpvmasum2.d |
⊢ 𝐷 = ( Base ‘ 𝐺 ) |
6 |
|
rpvmasum2.1 |
⊢ 1 = ( 0g ‘ 𝐺 ) |
7 |
|
dchrisum0f.f |
⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) ) |
8 |
|
dchrisum0f.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐷 ) |
9 |
|
dchrisum0flb.r |
⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ ) |
10 |
|
dchrisum0flblem1.1 |
⊢ ( 𝜑 → 𝑃 ∈ ℙ ) |
11 |
|
dchrisum0flblem1.2 |
⊢ ( 𝜑 → 𝐴 ∈ ℕ0 ) |
12 |
|
1red |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 1 ∈ ℝ ) |
13 |
|
0red |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) ∧ ¬ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 0 ∈ ℝ ) |
14 |
12 13
|
ifclda |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ ) |
15 |
|
1red |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → 1 ∈ ℝ ) |
16 |
|
fzfid |
⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ Fin ) |
17 |
3
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
18 |
|
eqid |
⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 ) |
19 |
1 18 2
|
znzrhfo |
⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) ) |
20 |
|
fof |
⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ) |
21 |
17 19 20
|
3syl |
⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ) |
22 |
|
prmz |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ ) |
23 |
10 22
|
syl |
⊢ ( 𝜑 → 𝑃 ∈ ℤ ) |
24 |
21 23
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝐿 ‘ 𝑃 ) ∈ ( Base ‘ 𝑍 ) ) |
25 |
9 24
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ ) |
26 |
|
elfznn0 |
⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → 𝑖 ∈ ℕ0 ) |
27 |
|
reexpcl |
⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ∈ ℝ ) |
28 |
25 26 27
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ∈ ℝ ) |
29 |
16 28
|
fsumrecl |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ∈ ℝ ) |
30 |
29
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ∈ ℝ ) |
31 |
|
breq1 |
⊢ ( 1 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( 1 ≤ 1 ↔ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ 1 ) ) |
32 |
|
breq1 |
⊢ ( 0 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( 0 ≤ 1 ↔ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ 1 ) ) |
33 |
|
1le1 |
⊢ 1 ≤ 1 |
34 |
|
0le1 |
⊢ 0 ≤ 1 |
35 |
31 32 33 34
|
keephyp |
⊢ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ 1 |
36 |
35
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ 1 ) |
37 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
38 |
11 37
|
eleqtrdi |
⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 0 ) ) |
39 |
|
fzn0 |
⊢ ( ( 0 ... 𝐴 ) ≠ ∅ ↔ 𝐴 ∈ ( ℤ≥ ‘ 0 ) ) |
40 |
38 39
|
sylibr |
⊢ ( 𝜑 → ( 0 ... 𝐴 ) ≠ ∅ ) |
41 |
|
hashnncl |
⊢ ( ( 0 ... 𝐴 ) ∈ Fin → ( ( ♯ ‘ ( 0 ... 𝐴 ) ) ∈ ℕ ↔ ( 0 ... 𝐴 ) ≠ ∅ ) ) |
42 |
16 41
|
syl |
⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ... 𝐴 ) ) ∈ ℕ ↔ ( 0 ... 𝐴 ) ≠ ∅ ) ) |
43 |
40 42
|
mpbird |
⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... 𝐴 ) ) ∈ ℕ ) |
44 |
43
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( ♯ ‘ ( 0 ... 𝐴 ) ) ∈ ℕ ) |
45 |
44
|
nnge1d |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → 1 ≤ ( ♯ ‘ ( 0 ... 𝐴 ) ) ) |
46 |
|
simpr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) |
47 |
46
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = ( 1 ↑ 𝑖 ) ) |
48 |
|
elfzelz |
⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → 𝑖 ∈ ℤ ) |
49 |
|
1exp |
⊢ ( 𝑖 ∈ ℤ → ( 1 ↑ 𝑖 ) = 1 ) |
50 |
48 49
|
syl |
⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → ( 1 ↑ 𝑖 ) = 1 ) |
51 |
47 50
|
sylan9eq |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = 1 ) |
52 |
51
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = Σ 𝑖 ∈ ( 0 ... 𝐴 ) 1 ) |
53 |
|
fzfid |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( 0 ... 𝐴 ) ∈ Fin ) |
54 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
55 |
|
fsumconst |
⊢ ( ( ( 0 ... 𝐴 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) 1 = ( ( ♯ ‘ ( 0 ... 𝐴 ) ) · 1 ) ) |
56 |
53 54 55
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) 1 = ( ( ♯ ‘ ( 0 ... 𝐴 ) ) · 1 ) ) |
57 |
44
|
nncnd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( ♯ ‘ ( 0 ... 𝐴 ) ) ∈ ℂ ) |
58 |
57
|
mulid1d |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → ( ( ♯ ‘ ( 0 ... 𝐴 ) ) · 1 ) = ( ♯ ‘ ( 0 ... 𝐴 ) ) ) |
59 |
52 56 58
|
3eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = ( ♯ ‘ ( 0 ... 𝐴 ) ) ) |
60 |
45 59
|
breqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → 1 ≤ Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ) |
61 |
14 15 30 36 60
|
letrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ) |
62 |
|
oveq1 |
⊢ ( 1 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( 1 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) = ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) |
63 |
62
|
breq1d |
⊢ ( 1 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( ( 1 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) ) |
64 |
|
oveq1 |
⊢ ( 0 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( 0 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) = ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) |
65 |
64
|
breq1d |
⊢ ( 0 = if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) → ( ( 0 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) ) |
66 |
|
1re |
⊢ 1 ∈ ℝ |
67 |
25
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ ) |
68 |
|
resubcl |
⊢ ( ( 1 ∈ ℝ ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ ) |
69 |
66 67 68
|
sylancr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ ) |
70 |
69
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ ) |
71 |
70
|
leidd |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ≤ ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
72 |
69
|
recnd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℂ ) |
73 |
72
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℂ ) |
74 |
73
|
mulid2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) = ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
75 |
|
nn0p1nn |
⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 + 1 ) ∈ ℕ ) |
76 |
11 75
|
syl |
⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℕ ) |
77 |
76
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) → ( 𝐴 + 1 ) ∈ ℕ ) |
78 |
77
|
0expd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) → ( 0 ↑ ( 𝐴 + 1 ) ) = 0 ) |
79 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) |
80 |
79
|
oveq1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) = ( 0 ↑ ( 𝐴 + 1 ) ) ) |
81 |
78 80 79
|
3eqtr4d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) |
82 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
83 |
11
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 𝐴 ∈ ℕ0 ) |
84 |
|
expp1 |
⊢ ( ( - 1 ∈ ℂ ∧ 𝐴 ∈ ℕ0 ) → ( - 1 ↑ ( 𝐴 + 1 ) ) = ( ( - 1 ↑ 𝐴 ) · - 1 ) ) |
85 |
82 83 84
|
sylancr |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ ( 𝐴 + 1 ) ) = ( ( - 1 ↑ 𝐴 ) · - 1 ) ) |
86 |
|
prmnn |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ ) |
87 |
10 86
|
syl |
⊢ ( 𝜑 → 𝑃 ∈ ℕ ) |
88 |
87 11
|
nnexpcld |
⊢ ( 𝜑 → ( 𝑃 ↑ 𝐴 ) ∈ ℕ ) |
89 |
88
|
nncnd |
⊢ ( 𝜑 → ( 𝑃 ↑ 𝐴 ) ∈ ℂ ) |
90 |
89
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 ↑ 𝐴 ) ∈ ℂ ) |
91 |
90
|
sqsqrtd |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ↑ 2 ) = ( 𝑃 ↑ 𝐴 ) ) |
92 |
91
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ↑ 2 ) ) = ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) ) |
93 |
10
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 𝑃 ∈ ℙ ) |
94 |
|
nnq |
⊢ ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ → ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℚ ) |
95 |
94
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℚ ) |
96 |
|
nnne0 |
⊢ ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ → ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ≠ 0 ) |
97 |
96
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ≠ 0 ) |
98 |
|
2z |
⊢ 2 ∈ ℤ |
99 |
98
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 2 ∈ ℤ ) |
100 |
|
pcexp |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℚ ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ≠ 0 ) ∧ 2 ∈ ℤ ) → ( 𝑃 pCnt ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ↑ 2 ) ) = ( 2 · ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) ) |
101 |
93 95 97 99 100
|
syl121anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ↑ 2 ) ) = ( 2 · ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) ) |
102 |
83
|
nn0zd |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 𝐴 ∈ ℤ ) |
103 |
|
pcid |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) = 𝐴 ) |
104 |
93 102 103
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( 𝑃 ↑ 𝐴 ) ) = 𝐴 ) |
105 |
92 101 104
|
3eqtr3rd |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 𝐴 = ( 2 · ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) ) |
106 |
105
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ 𝐴 ) = ( - 1 ↑ ( 2 · ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) ) ) |
107 |
82
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → - 1 ∈ ℂ ) |
108 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) |
109 |
93 108
|
pccld |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ∈ ℕ0 ) |
110 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
111 |
110
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → 2 ∈ ℕ0 ) |
112 |
107 109 111
|
expmuld |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ ( 2 · ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) ) |
113 |
|
neg1sqe1 |
⊢ ( - 1 ↑ 2 ) = 1 |
114 |
113
|
oveq1i |
⊢ ( ( - 1 ↑ 2 ) ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) = ( 1 ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) |
115 |
109
|
nn0zd |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ∈ ℤ ) |
116 |
|
1exp |
⊢ ( ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ∈ ℤ → ( 1 ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) = 1 ) |
117 |
115 116
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) = 1 ) |
118 |
114 117
|
syl5eq |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( - 1 ↑ 2 ) ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) = 1 ) |
119 |
106 112 118
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ 𝐴 ) = 1 ) |
120 |
119
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( - 1 ↑ 𝐴 ) · - 1 ) = ( 1 · - 1 ) ) |
121 |
82
|
mulid2i |
⊢ ( 1 · - 1 ) = - 1 |
122 |
120 121
|
eqtrdi |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( - 1 ↑ 𝐴 ) · - 1 ) = - 1 ) |
123 |
85 122
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ ( 𝐴 + 1 ) ) = - 1 ) |
124 |
123
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( - 1 ↑ ( 𝐴 + 1 ) ) = - 1 ) |
125 |
25
|
recnd |
⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℂ ) |
126 |
125
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℂ ) |
127 |
126
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℂ ) |
128 |
127
|
negnegd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → - - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) |
129 |
|
simpr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) |
130 |
129
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) |
131 |
8
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → 𝑋 ∈ 𝐷 ) |
132 |
|
eqid |
⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 ) |
133 |
4 1 5 18 132 8 24
|
dchrn0 |
⊢ ( 𝜑 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ↔ ( 𝐿 ‘ 𝑃 ) ∈ ( Unit ‘ 𝑍 ) ) ) |
134 |
133
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ↔ ( 𝐿 ‘ 𝑃 ) ∈ ( Unit ‘ 𝑍 ) ) ) |
135 |
134
|
biimpa |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( 𝐿 ‘ 𝑃 ) ∈ ( Unit ‘ 𝑍 ) ) |
136 |
4 5 131 1 132 135
|
dchrabs |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = 1 ) |
137 |
|
eqeq1 |
⊢ ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = 1 ↔ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) ) |
138 |
136 137
|
syl5ibcom |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) ) |
139 |
138
|
necon3ad |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 → ¬ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
140 |
130 139
|
mpd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ¬ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) |
141 |
67
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ ) |
142 |
141
|
absord |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∨ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
143 |
142
|
ord |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ¬ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
144 |
140 143
|
mpd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) |
145 |
144 136
|
eqtr3d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 1 ) |
146 |
145
|
negeqd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → - - ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = - 1 ) |
147 |
128 146
|
eqtr3d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = - 1 ) |
148 |
147
|
oveq1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) = ( - 1 ↑ ( 𝐴 + 1 ) ) ) |
149 |
124 148 147
|
3eqtr4d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 0 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) |
150 |
81 149
|
pm2.61dane |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) |
151 |
150
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) = ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
152 |
71 74 151
|
3brtr4d |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 1 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) |
153 |
72
|
mul02d |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 0 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) = 0 ) |
154 |
|
peano2nn0 |
⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 + 1 ) ∈ ℕ0 ) |
155 |
11 154
|
syl |
⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℕ0 ) |
156 |
25 155
|
reexpcld |
⊢ ( 𝜑 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ∈ ℝ ) |
157 |
156
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ∈ ℝ ) |
158 |
157
|
recnd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ∈ ℂ ) |
159 |
158
|
abscld |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ ) |
160 |
|
1red |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 1 ∈ ℝ ) |
161 |
157
|
leabsd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ≤ ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) |
162 |
155
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝐴 + 1 ) ∈ ℕ0 ) |
163 |
126 162
|
absexpd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ↑ ( 𝐴 + 1 ) ) ) |
164 |
126
|
abscld |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ ) |
165 |
126
|
absge0d |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
166 |
4 5 1 18 8 24
|
dchrabs2 |
⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ≤ 1 ) |
167 |
166
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ≤ 1 ) |
168 |
|
exple1 |
⊢ ( ( ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∧ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ≤ 1 ) ∧ ( 𝐴 + 1 ) ∈ ℕ0 ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ↑ ( 𝐴 + 1 ) ) ≤ 1 ) |
169 |
164 165 167 162 168
|
syl31anc |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ↑ ( 𝐴 + 1 ) ) ≤ 1 ) |
170 |
163 169
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ≤ 1 ) |
171 |
157 159 160 161 170
|
letrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ≤ 1 ) |
172 |
|
subge0 |
⊢ ( ( 1 ∈ ℝ ∧ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ∈ ℝ ) → ( 0 ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ≤ 1 ) ) |
173 |
66 157 172
|
sylancr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 0 ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ≤ 1 ) ) |
174 |
171 173
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 0 ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) |
175 |
153 174
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 0 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) |
176 |
175
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ¬ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( 0 · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) |
177 |
63 65 152 176
|
ifbothda |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) |
178 |
|
0re |
⊢ 0 ∈ ℝ |
179 |
66 178
|
ifcli |
⊢ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ |
180 |
179
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ ) |
181 |
|
resubcl |
⊢ ( ( 1 ∈ ℝ ∧ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ∈ ℝ ) → ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ ) |
182 |
66 157 181
|
sylancr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ ) |
183 |
67
|
leabsd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
184 |
67 164 160 183 167
|
letrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≤ 1 ) |
185 |
129
|
necomd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 1 ≠ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) |
186 |
67 160 184 185
|
leneltd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) < 1 ) |
187 |
|
posdif |
⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) < 1 ↔ 0 < ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) |
188 |
67 66 187
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) < 1 ↔ 0 < ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) |
189 |
186 188
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 0 < ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
190 |
|
lemuldiv |
⊢ ( ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ∈ ℝ ∧ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ ∧ ( ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ∈ ℝ ∧ 0 < ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) → ( ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ ( ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) ) |
191 |
180 182 69 189 190
|
syl112anc |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) · ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ≤ ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ↔ if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ ( ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) ) |
192 |
177 191
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ ( ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) |
193 |
11
|
nn0zd |
⊢ ( 𝜑 → 𝐴 ∈ ℤ ) |
194 |
|
fzval3 |
⊢ ( 𝐴 ∈ ℤ → ( 0 ... 𝐴 ) = ( 0 ..^ ( 𝐴 + 1 ) ) ) |
195 |
193 194
|
syl |
⊢ ( 𝜑 → ( 0 ... 𝐴 ) = ( 0 ..^ ( 𝐴 + 1 ) ) ) |
196 |
195
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 0 ... 𝐴 ) = ( 0 ..^ ( 𝐴 + 1 ) ) ) |
197 |
196
|
sumeq1d |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = Σ 𝑖 ∈ ( 0 ..^ ( 𝐴 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ) |
198 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
199 |
198
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → 0 ∈ ℕ0 ) |
200 |
155 37
|
eleqtrdi |
⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 0 ) ) |
201 |
200
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( 𝐴 + 1 ) ∈ ( ℤ≥ ‘ 0 ) ) |
202 |
126 129 199 201
|
geoserg |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → Σ 𝑖 ∈ ( 0 ..^ ( 𝐴 + 1 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 0 ) − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) |
203 |
126
|
exp0d |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 0 ) = 1 ) |
204 |
203
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 0 ) − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) = ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) ) |
205 |
204
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 0 ) − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) = ( ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) |
206 |
197 202 205
|
3eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) = ( ( 1 − ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ ( 𝐴 + 1 ) ) ) / ( 1 − ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) ) |
207 |
192 206
|
breqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ) |
208 |
61 207
|
pm2.61dane |
⊢ ( 𝜑 → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ) |
209 |
1 2 3 4 5 6 7
|
dchrisum0fval |
⊢ ( ( 𝑃 ↑ 𝐴 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑃 ↑ 𝐴 ) ) = Σ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) |
210 |
88 209
|
syl |
⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑃 ↑ 𝐴 ) ) = Σ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) |
211 |
|
2fveq3 |
⊢ ( 𝑘 = ( 𝑃 ↑ 𝑖 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) ) |
212 |
|
eqid |
⊢ ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) = ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) |
213 |
212
|
dvdsppwf1o |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) : ( 0 ... 𝐴 ) –1-1-onto→ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) |
214 |
10 11 213
|
syl2anc |
⊢ ( 𝜑 → ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) : ( 0 ... 𝐴 ) –1-1-onto→ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) |
215 |
|
oveq2 |
⊢ ( 𝑏 = 𝑖 → ( 𝑃 ↑ 𝑏 ) = ( 𝑃 ↑ 𝑖 ) ) |
216 |
|
ovex |
⊢ ( 𝑃 ↑ 𝑏 ) ∈ V |
217 |
215 212 216
|
fvmpt3i |
⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → ( ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) ‘ 𝑖 ) = ( 𝑃 ↑ 𝑖 ) ) |
218 |
217
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑏 ∈ ( 0 ... 𝐴 ) ↦ ( 𝑃 ↑ 𝑏 ) ) ‘ 𝑖 ) = ( 𝑃 ↑ 𝑖 ) ) |
219 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ ) |
220 |
|
elrabi |
⊢ ( 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } → 𝑘 ∈ ℕ ) |
221 |
220
|
nnzd |
⊢ ( 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } → 𝑘 ∈ ℤ ) |
222 |
|
ffvelrn |
⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐿 ‘ 𝑘 ) ∈ ( Base ‘ 𝑍 ) ) |
223 |
21 221 222
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝐿 ‘ 𝑘 ) ∈ ( Base ‘ 𝑍 ) ) |
224 |
219 223
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℝ ) |
225 |
224
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℂ ) |
226 |
211 16 214 218 225
|
fsumf1o |
⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) = Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) ) |
227 |
|
zsubrg |
⊢ ℤ ∈ ( SubRing ‘ ℂfld ) |
228 |
|
eqid |
⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld ) |
229 |
228
|
subrgsubm |
⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ) |
230 |
227 229
|
mp1i |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ℤ ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ) |
231 |
26
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑖 ∈ ℕ0 ) |
232 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑃 ∈ ℤ ) |
233 |
|
eqid |
⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) ) |
234 |
|
zringmpg |
⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) = ( mulGrp ‘ ℤring ) |
235 |
234
|
eqcomi |
⊢ ( mulGrp ‘ ℤring ) = ( ( mulGrp ‘ ℂfld ) ↾s ℤ ) |
236 |
|
eqid |
⊢ ( .g ‘ ( mulGrp ‘ ℤring ) ) = ( .g ‘ ( mulGrp ‘ ℤring ) ) |
237 |
233 235 236
|
submmulg |
⊢ ( ( ℤ ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ 𝑖 ∈ ℕ0 ∧ 𝑃 ∈ ℤ ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑃 ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) ) |
238 |
230 231 232 237
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑃 ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) ) |
239 |
87
|
nncnd |
⊢ ( 𝜑 → 𝑃 ∈ ℂ ) |
240 |
|
cnfldexp |
⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑃 ) = ( 𝑃 ↑ 𝑖 ) ) |
241 |
239 26 240
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑃 ) = ( 𝑃 ↑ 𝑖 ) ) |
242 |
238 241
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) = ( 𝑃 ↑ 𝑖 ) ) |
243 |
242
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝐿 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) ) = ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) |
244 |
1
|
zncrng |
⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing ) |
245 |
|
crngring |
⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring ) |
246 |
17 244 245
|
3syl |
⊢ ( 𝜑 → 𝑍 ∈ Ring ) |
247 |
2
|
zrhrhm |
⊢ ( 𝑍 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑍 ) ) |
248 |
|
eqid |
⊢ ( mulGrp ‘ ℤring ) = ( mulGrp ‘ ℤring ) |
249 |
|
eqid |
⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 ) |
250 |
248 249
|
rhmmhm |
⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑍 ) → 𝐿 ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑍 ) ) ) |
251 |
246 247 250
|
3syl |
⊢ ( 𝜑 → 𝐿 ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑍 ) ) ) |
252 |
251
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝐿 ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑍 ) ) ) |
253 |
|
zringbas |
⊢ ℤ = ( Base ‘ ℤring ) |
254 |
248 253
|
mgpbas |
⊢ ℤ = ( Base ‘ ( mulGrp ‘ ℤring ) ) |
255 |
|
eqid |
⊢ ( .g ‘ ( mulGrp ‘ 𝑍 ) ) = ( .g ‘ ( mulGrp ‘ 𝑍 ) ) |
256 |
254 236 255
|
mhmmulg |
⊢ ( ( 𝐿 ∈ ( ( mulGrp ‘ ℤring ) MndHom ( mulGrp ‘ 𝑍 ) ) ∧ 𝑖 ∈ ℕ0 ∧ 𝑃 ∈ ℤ ) → ( 𝐿 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) ) |
257 |
252 231 232 256
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝐿 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ ℤring ) ) 𝑃 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) ) |
258 |
243 257
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) ) |
259 |
258
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) = ( 𝑋 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) ) ) |
260 |
4 1 5
|
dchrmhm |
⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) |
261 |
260 8
|
sselid |
⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) |
262 |
261
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) |
263 |
24
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝐿 ‘ 𝑃 ) ∈ ( Base ‘ 𝑍 ) ) |
264 |
249 18
|
mgpbas |
⊢ ( Base ‘ 𝑍 ) = ( Base ‘ ( mulGrp ‘ 𝑍 ) ) |
265 |
264 255 233
|
mhmmulg |
⊢ ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝑖 ∈ ℕ0 ∧ ( 𝐿 ‘ 𝑃 ) ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
266 |
262 231 263 265
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ‘ ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑍 ) ) ( 𝐿 ‘ 𝑃 ) ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) ) |
267 |
|
cnfldexp |
⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℂ ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ) |
268 |
125 26 267
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ) |
269 |
259 266 268
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ) |
270 |
269
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑃 ↑ 𝑖 ) ) ) = Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ) |
271 |
210 226 270
|
3eqtrd |
⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑃 ↑ 𝐴 ) ) = Σ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ↑ 𝑖 ) ) |
272 |
208 271
|
breqtrrd |
⊢ ( 𝜑 → if ( ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑃 ↑ 𝐴 ) ) ) |