Metamath Proof Explorer


Theorem dchrisum0flblem1

Description: Lemma for dchrisum0flb . Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypotheses rpvmasum.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ( 𝜑𝑁 ∈ ℕ )
rpvmasum2.g 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum2.d 𝐷 = ( Base ‘ 𝐺 )
rpvmasum2.1 1 = ( 0g𝐺 )
dchrisum0f.f 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑏 } ( 𝑋 ‘ ( 𝐿𝑣 ) ) )
dchrisum0f.x ( 𝜑𝑋𝐷 )
dchrisum0flb.r ( 𝜑𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
dchrisum0flblem1.1 ( 𝜑𝑃 ∈ ℙ )
dchrisum0flblem1.2 ( 𝜑𝐴 ∈ ℕ0 )
Assertion dchrisum0flblem1 ( 𝜑 → if ( ( √ ‘ ( 𝑃𝐴 ) ) ∈ ℕ , 1 , 0 ) ≤ ( 𝐹 ‘ ( 𝑃𝐴 ) ) )

Proof

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 ) ≤ ( 𝐹 ‘ ( 𝑃𝐴 ) ) )