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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐿 ‘ 𝑃 ) ∈ ( Base ‘ 𝑍 ) )
25 9 24 ffvelcdmd ⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ∈ ℝ )
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 mulridd ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) = 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 mullidd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 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 eqtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( - 1 ↑ 2 ) ↑ ( 𝑃 pCnt ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ) ) = 1 )
119 106 112 118 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( - 1 ↑ 𝐴 ) = 1 )
120 119 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑃 ) ) ≠ 1 ) ∧ ( √ ‘ ( 𝑃 ↑ 𝐴 ) ) ∈ ℕ ) → ( ( - 1 ↑ 𝐴 ) · - 1 ) = ( 1 · - 1 ) )
121 82 mullidi ⊢ ( 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 ffvelcdm ⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐿 ‘ 𝑘 ) ∈ ( Base ‘ 𝑍 ) )
223 21 221 222 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝐿 ‘ 𝑘 ) ∈ ( Base ‘ 𝑍 ) )
224 219 223 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝑃 ↑ 𝐴 ) } ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℝ )
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 ) ≤ ( 𝐹 ‘ ( 𝑃 ↑ 𝐴 ) ) )