Metamath Proof Explorer

Theorem dchrisum0flblem2

Description: Lemma for dchrisum0flb . Induction over relatively prime factors, with the prime power case handled in dchrisum0flblem1 . (Contributed by Mario Carneiro, 5-May-2016) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020)

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 )
dchrisum0flb.1 
|- ( ph -> A e. ( ZZ>= ` 2 ) )
dchrisum0flb.2 
|- ( ph -> P e. Prime )
dchrisum0flb.3 
|- ( ph -> P || A )
dchrisum0flb.4 
|- ( ph -> A. y e. ( 1 ..^ A ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) )
Assertion dchrisum0flblem2 
|- ( ph -> if ( ( sqrt ` A ) e. NN , 1 , 0 ) <_ ( F ` 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 dchrisum0flb.1 
 |-  ( ph -> A e. ( ZZ>= ` 2 ) )
11 dchrisum0flb.2 
 |-  ( ph -> P e. Prime )
12 dchrisum0flb.3 
 |-  ( ph -> P || A )
13 dchrisum0flb.4 
 |-  ( ph -> A. y e. ( 1 ..^ A ) if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) )
14 breq1 
 |-  ( 1 = if ( ( sqrt ` A ) e. NN , 1 , 0 ) -> ( 1 <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) <-> if ( ( sqrt ` A ) e. NN , 1 , 0 ) <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) ) )
15 breq1 
 |-  ( 0 = if ( ( sqrt ` A ) e. NN , 1 , 0 ) -> ( 0 <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) <-> if ( ( sqrt ` A ) e. NN , 1 , 0 ) <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) ) )
16 1t1e1 
 |-  ( 1 x. 1 ) = 1
17 11 adantr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> P e. Prime )
18 nnq 
 |-  ( ( sqrt ` A ) e. NN -> ( sqrt ` A ) e. QQ )
19 18 adantl 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` A ) e. QQ )
20 nnne0 
 |-  ( ( sqrt ` A ) e. NN -> ( sqrt ` A ) =/= 0 )
21 20 adantl 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` A ) =/= 0 )
22 2z 
 |-  2 e. ZZ
23 22 a1i 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> 2 e. ZZ )
24 pcexp 
 |-  ( ( P e. Prime /\ ( ( sqrt ` A ) e. QQ /\ ( sqrt ` A ) =/= 0 ) /\ 2 e. ZZ ) -> ( P pCnt ( ( sqrt ` A ) ^ 2 ) ) = ( 2 x. ( P pCnt ( sqrt ` A ) ) ) )
25 17 19 21 23 24 syl121anc 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P pCnt ( ( sqrt ` A ) ^ 2 ) ) = ( 2 x. ( P pCnt ( sqrt ` A ) ) ) )
26 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
27 10 26 syl 
 |-  ( ph -> A e. NN )
28 27 nncnd 
 |-  ( ph -> A e. CC )
29 28 adantr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> A e. CC )
30 29 sqsqrtd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( ( sqrt ` A ) ^ 2 ) = A )
31 30 oveq2d 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P pCnt ( ( sqrt ` A ) ^ 2 ) ) = ( P pCnt A ) )
32 2cnd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> 2 e. CC )
33 simpr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` A ) e. NN )
34 17 33 pccld 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P pCnt ( sqrt ` A ) ) e. NN0 )
35 34 nn0cnd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P pCnt ( sqrt ` A ) ) e. CC )
36 32 35 mulcomd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( 2 x. ( P pCnt ( sqrt ` A ) ) ) = ( ( P pCnt ( sqrt ` A ) ) x. 2 ) )
37 25 31 36 3eqtr3rd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( ( P pCnt ( sqrt ` A ) ) x. 2 ) = ( P pCnt A ) )
38 37 oveq2d 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P ^ ( ( P pCnt ( sqrt ` A ) ) x. 2 ) ) = ( P ^ ( P pCnt A ) ) )
39 prmnn 
 |-  ( P e. Prime -> P e. NN )
40 17 39 syl 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> P e. NN )
41 40 nncnd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> P e. CC )
42 2nn0 
 |-  2 e. NN0
43 42 a1i 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> 2 e. NN0 )
44 41 43 34 expmuld 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P ^ ( ( P pCnt ( sqrt ` A ) ) x. 2 ) ) = ( ( P ^ ( P pCnt ( sqrt ` A ) ) ) ^ 2 ) )
45 38 44 eqtr3d 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P ^ ( P pCnt A ) ) = ( ( P ^ ( P pCnt ( sqrt ` A ) ) ) ^ 2 ) )
46 45 fveq2d 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` ( P ^ ( P pCnt A ) ) ) = ( sqrt ` ( ( P ^ ( P pCnt ( sqrt ` A ) ) ) ^ 2 ) ) )
47 40 34 nnexpcld 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P ^ ( P pCnt ( sqrt ` A ) ) ) e. NN )
48 47 nnrpd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P ^ ( P pCnt ( sqrt ` A ) ) ) e. RR+ )
49 48 rprege0d 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( ( P ^ ( P pCnt ( sqrt ` A ) ) ) e. RR /\ 0 <_ ( P ^ ( P pCnt ( sqrt ` A ) ) ) ) )
50 sqrtsq 
 |-  ( ( ( P ^ ( P pCnt ( sqrt ` A ) ) ) e. RR /\ 0 <_ ( P ^ ( P pCnt ( sqrt ` A ) ) ) ) -> ( sqrt ` ( ( P ^ ( P pCnt ( sqrt ` A ) ) ) ^ 2 ) ) = ( P ^ ( P pCnt ( sqrt ` A ) ) ) )
51 49 50 syl 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` ( ( P ^ ( P pCnt ( sqrt ` A ) ) ) ^ 2 ) ) = ( P ^ ( P pCnt ( sqrt ` A ) ) ) )
52 46 51 eqtrd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` ( P ^ ( P pCnt A ) ) ) = ( P ^ ( P pCnt ( sqrt ` A ) ) ) )
53 52 47 eqeltrd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN )
54 53 iftrued 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 ) = 1 )
55 11 27 pccld 
 |-  ( ph -> ( P pCnt A ) e. NN0 )
56 1 2 3 4 5 6 7 8 9 11 55 dchrisum0flblem1 
 |-  ( ph -> if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 ) <_ ( F ` ( P ^ ( P pCnt A ) ) ) )
57 56 adantr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 ) <_ ( F ` ( P ^ ( P pCnt A ) ) ) )
58 54 57 eqbrtrrd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> 1 <_ ( F ` ( P ^ ( P pCnt A ) ) ) )
59 pcdvds 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( P ^ ( P pCnt A ) ) || A )
60 11 27 59 syl2anc 
 |-  ( ph -> ( P ^ ( P pCnt A ) ) || A )
61 11 39 syl 
 |-  ( ph -> P e. NN )
62 61 55 nnexpcld 
 |-  ( ph -> ( P ^ ( P pCnt A ) ) e. NN )
63 nndivdvds 
 |-  ( ( A e. NN /\ ( P ^ ( P pCnt A ) ) e. NN ) -> ( ( P ^ ( P pCnt A ) ) || A <-> ( A / ( P ^ ( P pCnt A ) ) ) e. NN ) )
64 27 62 63 syl2anc 
 |-  ( ph -> ( ( P ^ ( P pCnt A ) ) || A <-> ( A / ( P ^ ( P pCnt A ) ) ) e. NN ) )
65 60 64 mpbid 
 |-  ( ph -> ( A / ( P ^ ( P pCnt A ) ) ) e. NN )
66 65 nnzd 
 |-  ( ph -> ( A / ( P ^ ( P pCnt A ) ) ) e. ZZ )
67 66 adantr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( A / ( P ^ ( P pCnt A ) ) ) e. ZZ )
68 27 adantr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> A e. NN )
69 68 nnrpd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> A e. RR+ )
70 69 rprege0d 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( A e. RR /\ 0 <_ A ) )
71 62 adantr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P ^ ( P pCnt A ) ) e. NN )
72 71 nnrpd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( P ^ ( P pCnt A ) ) e. RR+ )
73 sqrtdiv 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( P ^ ( P pCnt A ) ) e. RR+ ) -> ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) = ( ( sqrt ` A ) / ( sqrt ` ( P ^ ( P pCnt A ) ) ) ) )
74 70 72 73 syl2anc 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) = ( ( sqrt ` A ) / ( sqrt ` ( P ^ ( P pCnt A ) ) ) ) )
75 nnz 
 |-  ( ( sqrt ` A ) e. NN -> ( sqrt ` A ) e. ZZ )
76 znq 
 |-  ( ( ( sqrt ` A ) e. ZZ /\ ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN ) -> ( ( sqrt ` A ) / ( sqrt ` ( P ^ ( P pCnt A ) ) ) ) e. QQ )
77 75 53 76 syl2an2 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( ( sqrt ` A ) / ( sqrt ` ( P ^ ( P pCnt A ) ) ) ) e. QQ )
78 74 77 eqeltrd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. QQ )
79 zsqrtelqelz 
 |-  ( ( ( A / ( P ^ ( P pCnt A ) ) ) e. ZZ /\ ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. QQ ) -> ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. ZZ )
80 67 78 79 syl2anc 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. ZZ )
81 65 adantr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( A / ( P ^ ( P pCnt A ) ) ) e. NN )
82 81 nnrpd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( A / ( P ^ ( P pCnt A ) ) ) e. RR+ )
83 82 sqrtgt0d 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> 0 < ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) )
84 elnnz 
 |-  ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN <-> ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. ZZ /\ 0 < ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) )
85 80 83 84 sylanbrc 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN )
86 85 iftrued 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) = 1 )
87 fveq2 
 |-  ( y = ( A / ( P ^ ( P pCnt A ) ) ) -> ( sqrt ` y ) = ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) )
88 87 eleq1d 
 |-  ( y = ( A / ( P ^ ( P pCnt A ) ) ) -> ( ( sqrt ` y ) e. NN <-> ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN ) )
89 88 ifbid 
 |-  ( y = ( A / ( P ^ ( P pCnt A ) ) ) -> if ( ( sqrt ` y ) e. NN , 1 , 0 ) = if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) )
90 fveq2 
 |-  ( y = ( A / ( P ^ ( P pCnt A ) ) ) -> ( F ` y ) = ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) )
91 89 90 breq12d 
 |-  ( y = ( A / ( P ^ ( P pCnt A ) ) ) -> ( if ( ( sqrt ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) <-> if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) <_ ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) )
92 nnuz 
 |-  NN = ( ZZ>= ` 1 )
93 65 92 eleqtrdi 
 |-  ( ph -> ( A / ( P ^ ( P pCnt A ) ) ) e. ( ZZ>= ` 1 ) )
94 27 nnzd 
 |-  ( ph -> A e. ZZ )
95 61 nnred 
 |-  ( ph -> P e. RR )
96 pcelnn 
 |-  ( ( P e. Prime /\ A e. NN ) -> ( ( P pCnt A ) e. NN <-> P || A ) )
97 11 27 96 syl2anc 
 |-  ( ph -> ( ( P pCnt A ) e. NN <-> P || A ) )
98 12 97 mpbird 
 |-  ( ph -> ( P pCnt A ) e. NN )
99 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
100 eluz2gt1 
 |-  ( P e. ( ZZ>= ` 2 ) -> 1 < P )
101 11 99 100 3syl 
 |-  ( ph -> 1 < P )
102 expgt1 
 |-  ( ( P e. RR /\ ( P pCnt A ) e. NN /\ 1 < P ) -> 1 < ( P ^ ( P pCnt A ) ) )
103 95 98 101 102 syl3anc 
 |-  ( ph -> 1 < ( P ^ ( P pCnt A ) ) )
104 1red 
 |-  ( ph -> 1 e. RR )
105 0lt1 
 |-  0 < 1
106 105 a1i 
 |-  ( ph -> 0 < 1 )
107 62 nnred 
 |-  ( ph -> ( P ^ ( P pCnt A ) ) e. RR )
108 62 nngt0d 
 |-  ( ph -> 0 < ( P ^ ( P pCnt A ) ) )
109 27 nnred 
 |-  ( ph -> A e. RR )
110 27 nngt0d 
 |-  ( ph -> 0 < A )
111 ltdiv2 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( ( P ^ ( P pCnt A ) ) e. RR /\ 0 < ( P ^ ( P pCnt A ) ) ) /\ ( A e. RR /\ 0 < A ) ) -> ( 1 < ( P ^ ( P pCnt A ) ) <-> ( A / ( P ^ ( P pCnt A ) ) ) < ( A / 1 ) ) )
112 104 106 107 108 109 110 111 syl222anc 
 |-  ( ph -> ( 1 < ( P ^ ( P pCnt A ) ) <-> ( A / ( P ^ ( P pCnt A ) ) ) < ( A / 1 ) ) )
113 103 112 mpbid 
 |-  ( ph -> ( A / ( P ^ ( P pCnt A ) ) ) < ( A / 1 ) )
114 28 div1d 
 |-  ( ph -> ( A / 1 ) = A )
115 113 114 breqtrd 
 |-  ( ph -> ( A / ( P ^ ( P pCnt A ) ) ) < A )
116 elfzo2 
 |-  ( ( A / ( P ^ ( P pCnt A ) ) ) e. ( 1 ..^ A ) <-> ( ( A / ( P ^ ( P pCnt A ) ) ) e. ( ZZ>= ` 1 ) /\ A e. ZZ /\ ( A / ( P ^ ( P pCnt A ) ) ) < A ) )
117 93 94 115 116 syl3anbrc 
 |-  ( ph -> ( A / ( P ^ ( P pCnt A ) ) ) e. ( 1 ..^ A ) )
118 91 13 117 rspcdva 
 |-  ( ph -> if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) <_ ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) )
119 118 adantr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) <_ ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) )
120 86 119 eqbrtrrd 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> 1 <_ ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) )
121 1re 
 |-  1 e. RR
122 0le1 
 |-  0 <_ 1
123 121 122 pm3.2i 
 |-  ( 1 e. RR /\ 0 <_ 1 )
124 123 a1i 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( 1 e. RR /\ 0 <_ 1 ) )
125 1 2 3 4 5 6 7 8 9 dchrisum0ff 
 |-  ( ph -> F : NN --> RR )
126 125 62 ffvelcdmd 
 |-  ( ph -> ( F ` ( P ^ ( P pCnt A ) ) ) e. RR )
127 126 adantr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( F ` ( P ^ ( P pCnt A ) ) ) e. RR )
128 125 65 ffvelcdmd 
 |-  ( ph -> ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. RR )
129 128 adantr 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. RR )
130 lemul12a 
 |-  ( ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( F ` ( P ^ ( P pCnt A ) ) ) e. RR ) /\ ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. RR ) ) -> ( ( 1 <_ ( F ` ( P ^ ( P pCnt A ) ) ) /\ 1 <_ ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) -> ( 1 x. 1 ) <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) ) )
131 124 127 124 129 130 syl22anc 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( ( 1 <_ ( F ` ( P ^ ( P pCnt A ) ) ) /\ 1 <_ ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) -> ( 1 x. 1 ) <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) ) )
132 58 120 131 mp2and 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> ( 1 x. 1 ) <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) )
133 16 132 eqbrtrrid 
 |-  ( ( ph /\ ( sqrt ` A ) e. NN ) -> 1 <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) )
134 0red 
 |-  ( ph -> 0 e. RR )
135 0re 
 |-  0 e. RR
136 121 135 ifcli 
 |-  if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 ) e. RR
137 136 a1i 
 |-  ( ph -> if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 ) e. RR )
138 breq2 
 |-  ( 1 = if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 ) -> ( 0 <_ 1 <-> 0 <_ if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 ) ) )
139 breq2 
 |-  ( 0 = if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 ) ) )
140 0le0 
 |-  0 <_ 0
141 138 139 122 140 keephyp 
 |-  0 <_ if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 )
142 141 a1i 
 |-  ( ph -> 0 <_ if ( ( sqrt ` ( P ^ ( P pCnt A ) ) ) e. NN , 1 , 0 ) )
143 134 137 126 142 56 letrd 
 |-  ( ph -> 0 <_ ( F ` ( P ^ ( P pCnt A ) ) ) )
144 121 135 ifcli 
 |-  if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) e. RR
145 144 a1i 
 |-  ( ph -> if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) e. RR )
146 breq2 
 |-  ( 1 = if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) -> ( 0 <_ 1 <-> 0 <_ if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) ) )
147 breq2 
 |-  ( 0 = if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) ) )
148 146 147 122 140 keephyp 
 |-  0 <_ if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 )
149 148 a1i 
 |-  ( ph -> 0 <_ if ( ( sqrt ` ( A / ( P ^ ( P pCnt A ) ) ) ) e. NN , 1 , 0 ) )
150 134 145 128 149 118 letrd 
 |-  ( ph -> 0 <_ ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) )
151 126 128 143 150 mulge0d 
 |-  ( ph -> 0 <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) )
152 151 adantr 
 |-  ( ( ph /\ -. ( sqrt ` A ) e. NN ) -> 0 <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) )
153 14 15 133 152 ifbothda 
 |-  ( ph -> if ( ( sqrt ` A ) e. NN , 1 , 0 ) <_ ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) )
154 62 nncnd 
 |-  ( ph -> ( P ^ ( P pCnt A ) ) e. CC )
155 62 nnne0d 
 |-  ( ph -> ( P ^ ( P pCnt A ) ) =/= 0 )
156 28 154 155 divcan2d 
 |-  ( ph -> ( ( P ^ ( P pCnt A ) ) x. ( A / ( P ^ ( P pCnt A ) ) ) ) = A )
157 156 fveq2d 
 |-  ( ph -> ( F ` ( ( P ^ ( P pCnt A ) ) x. ( A / ( P ^ ( P pCnt A ) ) ) ) ) = ( F ` A ) )
158 pcndvds2 
 |-  ( ( P e. Prime /\ A e. NN ) -> -. P || ( A / ( P ^ ( P pCnt A ) ) ) )
159 11 27 158 syl2anc 
 |-  ( ph -> -. P || ( A / ( P ^ ( P pCnt A ) ) ) )
160 coprm 
 |-  ( ( P e. Prime /\ ( A / ( P ^ ( P pCnt A ) ) ) e. ZZ ) -> ( -. P || ( A / ( P ^ ( P pCnt A ) ) ) <-> ( P gcd ( A / ( P ^ ( P pCnt A ) ) ) ) = 1 ) )
161 11 66 160 syl2anc 
 |-  ( ph -> ( -. P || ( A / ( P ^ ( P pCnt A ) ) ) <-> ( P gcd ( A / ( P ^ ( P pCnt A ) ) ) ) = 1 ) )
162 159 161 mpbid 
 |-  ( ph -> ( P gcd ( A / ( P ^ ( P pCnt A ) ) ) ) = 1 )
163 prmz 
 |-  ( P e. Prime -> P e. ZZ )
164 11 163 syl 
 |-  ( ph -> P e. ZZ )
165 rpexp1i 
 |-  ( ( P e. ZZ /\ ( A / ( P ^ ( P pCnt A ) ) ) e. ZZ /\ ( P pCnt A ) e. NN0 ) -> ( ( P gcd ( A / ( P ^ ( P pCnt A ) ) ) ) = 1 -> ( ( P ^ ( P pCnt A ) ) gcd ( A / ( P ^ ( P pCnt A ) ) ) ) = 1 ) )
166 164 66 55 165 syl3anc 
 |-  ( ph -> ( ( P gcd ( A / ( P ^ ( P pCnt A ) ) ) ) = 1 -> ( ( P ^ ( P pCnt A ) ) gcd ( A / ( P ^ ( P pCnt A ) ) ) ) = 1 ) )
167 162 166 mpd 
 |-  ( ph -> ( ( P ^ ( P pCnt A ) ) gcd ( A / ( P ^ ( P pCnt A ) ) ) ) = 1 )
168 1 2 3 4 5 6 7 8 62 65 167 dchrisum0fmul 
 |-  ( ph -> ( F ` ( ( P ^ ( P pCnt A ) ) x. ( A / ( P ^ ( P pCnt A ) ) ) ) ) = ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) )
169 157 168 eqtr3d 
 |-  ( ph -> ( F ` A ) = ( ( F ` ( P ^ ( P pCnt A ) ) ) x. ( F ` ( A / ( P ^ ( P pCnt A ) ) ) ) ) )
170 153 169 breqtrrd 
 |-  ( ph -> if ( ( sqrt ` A ) e. NN , 1 , 0 ) <_ ( F ` A ) )