This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum2.g 
|- G = ( DChr ` N )
rpvmasum2.d 
|- D = ( Base ` G )
rpvmasum2.1 
|- .1. = ( 0g ` G )
dchrisum0f.f 
|- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )
dchrisum0f.x 
|- ( ph -> X e. D )
dchrisum0flb.r 
|- ( ph -> X : ( Base ` Z ) --> RR )
dchrisum0flblem1.1 
|- ( ph -> P e. Prime )
dchrisum0flblem1.2 
|- ( ph -> A e. NN0 )
Assertion dchrisum0flblem1 
|- ( ph -> if ( ( sqrt ` ( P ^ A ) ) e. NN , 1 , 0 ) <_ ( F ` ( P ^ A ) ) )

Proof

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