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 ffvelrnd
 |-  ( 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 ffvelrnd
 |-  ( 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 ) )