Metamath Proof Explorer

Theorem aks6d1c4

Description: Claim 4 of Theorem 6.1 of the AKS inequality lemma. https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 12-May-2025)

Ref Expression
Hypotheses aks6d1c4.1 
|- ( ph -> N e. NN )
aks6d1c4.2 
|- ( ph -> P e. Prime )
aks6d1c4.3 
|- ( ph -> P || N )
aks6d1c4.4 
|- ( ph -> R e. NN )
aks6d1c4.5 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c4.6 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
aks6d1c4.7 
|- L = ( ZRHom ` ( Z/nZ ` R ) )
Assertion aks6d1c4 
|- ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( phi ` R ) )

Proof

Step Hyp Ref Expression
1 aks6d1c4.1 
 |-  ( ph -> N e. NN )
2 aks6d1c4.2 
 |-  ( ph -> P e. Prime )
3 aks6d1c4.3 
 |-  ( ph -> P || N )
4 aks6d1c4.4 
 |-  ( ph -> R e. NN )
5 aks6d1c4.5 
 |-  ( ph -> ( N gcd R ) = 1 )
6 aks6d1c4.6 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
7 aks6d1c4.7 
 |-  L = ( ZRHom ` ( Z/nZ ` R ) )
8 fvexd 
 |-  ( ph -> ( Unit ` ( Z/nZ ` R ) ) e. _V )
9 4 nnnn0d 
 |-  ( ph -> R e. NN0 )
10 eqid 
 |-  ( Z/nZ ` R ) = ( Z/nZ ` R )
11 10 zncrng 
 |-  ( R e. NN0 -> ( Z/nZ ` R ) e. CRing )
12 9 11 syl 
 |-  ( ph -> ( Z/nZ ` R ) e. CRing )
13 crngring 
 |-  ( ( Z/nZ ` R ) e. CRing -> ( Z/nZ ` R ) e. Ring )
14 7 zrhrhm 
 |-  ( ( Z/nZ ` R ) e. Ring -> L e. ( ZZring RingHom ( Z/nZ ` R ) ) )
15 zringbas 
 |-  ZZ = ( Base ` ZZring )
16 eqid 
 |-  ( Base ` ( Z/nZ ` R ) ) = ( Base ` ( Z/nZ ` R ) )
17 15 16 rhmf 
 |-  ( L e. ( ZZring RingHom ( Z/nZ ` R ) ) -> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) )
18 12 13 14 17 4syl 
 |-  ( ph -> L : ZZ --> ( Base ` ( Z/nZ ` R ) ) )
19 18 ffund 
 |-  ( ph -> Fun L )
20 19 adantr 
 |-  ( ( ph /\ a e. ( L " ( E " ( NN0 X. NN0 ) ) ) ) -> Fun L )
21 simpr 
 |-  ( ( ph /\ a e. ( L " ( E " ( NN0 X. NN0 ) ) ) ) -> a e. ( L " ( E " ( NN0 X. NN0 ) ) ) )
22 fvelima 
 |-  ( ( Fun L /\ a e. ( L " ( E " ( NN0 X. NN0 ) ) ) ) -> E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a )
23 20 21 22 syl2anc 
 |-  ( ( ph /\ a e. ( L " ( E " ( NN0 X. NN0 ) ) ) ) -> E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a )
24 simpr 
 |-  ( ( ( ( ph /\ E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a ) /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ ( L ` c ) = a ) -> ( L ` c ) = a )
25 24 eqcomd 
 |-  ( ( ( ( ph /\ E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a ) /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ ( L ` c ) = a ) -> a = ( L ` c ) )
26 simpll 
 |-  ( ( ( ph /\ E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a ) /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> ph )
27 simpr 
 |-  ( ( ( ph /\ E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a ) /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> c e. ( E " ( NN0 X. NN0 ) ) )
28 26 27 jca 
 |-  ( ( ( ph /\ E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a ) /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) )
29 ovexd 
 |-  ( ( ph /\ m e. ( NN0 X. NN0 ) ) -> ( ( P ^ ( 1st ` m ) ) x. ( ( N / P ) ^ ( 2nd ` m ) ) ) e. _V )
30 vex 
 |-  k e. _V
31 vex 
 |-  l e. _V
32 30 31 op1std 
 |-  ( m = <. k , l >. -> ( 1st ` m ) = k )
33 32 oveq2d 
 |-  ( m = <. k , l >. -> ( P ^ ( 1st ` m ) ) = ( P ^ k ) )
34 30 31 op2ndd 
 |-  ( m = <. k , l >. -> ( 2nd ` m ) = l )
35 34 oveq2d 
 |-  ( m = <. k , l >. -> ( ( N / P ) ^ ( 2nd ` m ) ) = ( ( N / P ) ^ l ) )
36 33 35 oveq12d 
 |-  ( m = <. k , l >. -> ( ( P ^ ( 1st ` m ) ) x. ( ( N / P ) ^ ( 2nd ` m ) ) ) = ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
37 36 mpompt 
 |-  ( m e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` m ) ) x. ( ( N / P ) ^ ( 2nd ` m ) ) ) ) = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
38 37 eqcomi 
 |-  ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) = ( m e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` m ) ) x. ( ( N / P ) ^ ( 2nd ` m ) ) ) )
39 6 38 eqtri 
 |-  E = ( m e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` m ) ) x. ( ( N / P ) ^ ( 2nd ` m ) ) ) )
40 29 39 fmptd 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> _V )
41 40 ffund 
 |-  ( ph -> Fun E )
42 41 adantr 
 |-  ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> Fun E )
43 simpr 
 |-  ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> c e. ( E " ( NN0 X. NN0 ) ) )
44 fvelima 
 |-  ( ( Fun E /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> E. d e. ( NN0 X. NN0 ) ( E ` d ) = c )
45 42 43 44 syl2anc 
 |-  ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> E. d e. ( NN0 X. NN0 ) ( E ` d ) = c )
46 simpr 
 |-  ( ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) /\ ( E ` e ) = c ) -> ( E ` e ) = c )
47 46 eqcomd 
 |-  ( ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) /\ ( E ` e ) = c ) -> c = ( E ` e ) )
48 47 oveq1d 
 |-  ( ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) /\ ( E ` e ) = c ) -> ( c gcd R ) = ( ( E ` e ) gcd R ) )
49 simplll 
 |-  ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) -> ph )
50 simpr 
 |-  ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) -> e e. ( NN0 X. NN0 ) )
51 49 50 jca 
 |-  ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) -> ( ph /\ e e. ( NN0 X. NN0 ) ) )
52 39 a1i 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> E = ( m e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` m ) ) x. ( ( N / P ) ^ ( 2nd ` m ) ) ) ) )
53 simpr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ m = e ) -> m = e )
54 53 fveq2d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ m = e ) -> ( 1st ` m ) = ( 1st ` e ) )
55 54 oveq2d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ m = e ) -> ( P ^ ( 1st ` m ) ) = ( P ^ ( 1st ` e ) ) )
56 53 fveq2d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ m = e ) -> ( 2nd ` m ) = ( 2nd ` e ) )
57 56 oveq2d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ m = e ) -> ( ( N / P ) ^ ( 2nd ` m ) ) = ( ( N / P ) ^ ( 2nd ` e ) ) )
58 55 57 oveq12d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ m = e ) -> ( ( P ^ ( 1st ` m ) ) x. ( ( N / P ) ^ ( 2nd ` m ) ) ) = ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) )
59 simpr 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> e e. ( NN0 X. NN0 ) )
60 ovexd 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) e. _V )
61 52 58 59 60 fvmptd 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( E ` e ) = ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) )
62 prmnn 
 |-  ( P e. Prime -> P e. NN )
63 2 62 syl 
 |-  ( ph -> P e. NN )
64 63 nnzd 
 |-  ( ph -> P e. ZZ )
65 64 adantr 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> P e. ZZ )
66 xp1st 
 |-  ( e e. ( NN0 X. NN0 ) -> ( 1st ` e ) e. NN0 )
67 66 adantl 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( 1st ` e ) e. NN0 )
68 65 67 zexpcld 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( P ^ ( 1st ` e ) ) e. ZZ )
69 63 nnne0d 
 |-  ( ph -> P =/= 0 )
70 1 nnzd 
 |-  ( ph -> N e. ZZ )
71 dvdsval2 
 |-  ( ( P e. ZZ /\ P =/= 0 /\ N e. ZZ ) -> ( P || N <-> ( N / P ) e. ZZ ) )
72 64 69 70 71 syl3anc 
 |-  ( ph -> ( P || N <-> ( N / P ) e. ZZ ) )
73 3 72 mpbid 
 |-  ( ph -> ( N / P ) e. ZZ )
74 73 adantr 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( N / P ) e. ZZ )
75 xp2nd 
 |-  ( e e. ( NN0 X. NN0 ) -> ( 2nd ` e ) e. NN0 )
76 75 adantl 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( 2nd ` e ) e. NN0 )
77 74 76 zexpcld 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( N / P ) ^ ( 2nd ` e ) ) e. ZZ )
78 68 77 zmulcld 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) e. ZZ )
79 61 78 eqeltrd 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( E ` e ) e. ZZ )
80 61 oveq1d 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( E ` e ) gcd R ) = ( ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) gcd R ) )
81 4 nnzd 
 |-  ( ph -> R e. ZZ )
82 81 adantr 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> R e. ZZ )
83 78 82 gcdcomd 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) gcd R ) = ( R gcd ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) ) )
84 81 64 70 3jca 
 |-  ( ph -> ( R e. ZZ /\ P e. ZZ /\ N e. ZZ ) )
85 70 81 jca 
 |-  ( ph -> ( N e. ZZ /\ R e. ZZ ) )
86 gcdcom 
 |-  ( ( N e. ZZ /\ R e. ZZ ) -> ( N gcd R ) = ( R gcd N ) )
87 85 86 syl 
 |-  ( ph -> ( N gcd R ) = ( R gcd N ) )
88 eqeq1 
 |-  ( ( N gcd R ) = ( R gcd N ) -> ( ( N gcd R ) = 1 <-> ( R gcd N ) = 1 ) )
89 87 88 syl 
 |-  ( ph -> ( ( N gcd R ) = 1 <-> ( R gcd N ) = 1 ) )
90 89 pm5.74i 
 |-  ( ( ph -> ( N gcd R ) = 1 ) <-> ( ph -> ( R gcd N ) = 1 ) )
91 5 90 mpbi 
 |-  ( ph -> ( R gcd N ) = 1 )
92 91 3 jca 
 |-  ( ph -> ( ( R gcd N ) = 1 /\ P || N ) )
93 rpdvds 
 |-  ( ( ( R e. ZZ /\ P e. ZZ /\ N e. ZZ ) /\ ( ( R gcd N ) = 1 /\ P || N ) ) -> ( R gcd P ) = 1 )
94 84 92 93 syl2anc 
 |-  ( ph -> ( R gcd P ) = 1 )
95 94 adantr 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( R gcd P ) = 1 )
96 95 adantr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 1st ` e ) e. NN ) -> ( R gcd P ) = 1 )
97 4 ad2antrr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 1st ` e ) e. NN ) -> R e. NN )
98 63 ad2antrr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 1st ` e ) e. NN ) -> P e. NN )
99 simpr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 1st ` e ) e. NN ) -> ( 1st ` e ) e. NN )
100 rprpwr 
 |-  ( ( R e. NN /\ P e. NN /\ ( 1st ` e ) e. NN ) -> ( ( R gcd P ) = 1 -> ( R gcd ( P ^ ( 1st ` e ) ) ) = 1 ) )
101 97 98 99 100 syl3anc 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 1st ` e ) e. NN ) -> ( ( R gcd P ) = 1 -> ( R gcd ( P ^ ( 1st ` e ) ) ) = 1 ) )
102 96 101 mpd 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 1st ` e ) e. NN ) -> ( R gcd ( P ^ ( 1st ` e ) ) ) = 1 )
103 67 anim1i 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 1st ` e ) =/= 0 ) -> ( ( 1st ` e ) e. NN0 /\ ( 1st ` e ) =/= 0 ) )
104 elnnne0 
 |-  ( ( 1st ` e ) e. NN <-> ( ( 1st ` e ) e. NN0 /\ ( 1st ` e ) =/= 0 ) )
105 103 104 sylibr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 1st ` e ) =/= 0 ) -> ( 1st ` e ) e. NN )
106 105 ex 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( 1st ` e ) =/= 0 -> ( 1st ` e ) e. NN ) )
107 106 necon1bd 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( -. ( 1st ` e ) e. NN -> ( 1st ` e ) = 0 ) )
108 107 imp 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 1st ` e ) e. NN ) -> ( 1st ` e ) = 0 )
109 108 oveq2d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 1st ` e ) e. NN ) -> ( P ^ ( 1st ` e ) ) = ( P ^ 0 ) )
110 109 oveq2d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 1st ` e ) e. NN ) -> ( R gcd ( P ^ ( 1st ` e ) ) ) = ( R gcd ( P ^ 0 ) ) )
111 65 zcnd 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> P e. CC )
112 111 adantr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 1st ` e ) e. NN ) -> P e. CC )
113 112 exp0d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 1st ` e ) e. NN ) -> ( P ^ 0 ) = 1 )
114 113 oveq2d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 1st ` e ) e. NN ) -> ( R gcd ( P ^ 0 ) ) = ( R gcd 1 ) )
115 82 adantr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 1st ` e ) e. NN ) -> R e. ZZ )
116 gcd1 
 |-  ( R e. ZZ -> ( R gcd 1 ) = 1 )
117 115 116 syl 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 1st ` e ) e. NN ) -> ( R gcd 1 ) = 1 )
118 114 117 eqtrd 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 1st ` e ) e. NN ) -> ( R gcd ( P ^ 0 ) ) = 1 )
119 110 118 eqtrd 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 1st ` e ) e. NN ) -> ( R gcd ( P ^ ( 1st ` e ) ) ) = 1 )
120 102 119 pm2.61dan 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( R gcd ( P ^ ( 1st ` e ) ) ) = 1 )
121 81 73 70 3jca 
 |-  ( ph -> ( R e. ZZ /\ ( N / P ) e. ZZ /\ N e. ZZ ) )
122 1 nnred 
 |-  ( ph -> N e. RR )
123 122 recnd 
 |-  ( ph -> N e. CC )
124 63 nnred 
 |-  ( ph -> P e. RR )
125 124 recnd 
 |-  ( ph -> P e. CC )
126 1 nngt0d 
 |-  ( ph -> 0 < N )
127 126 gt0ne0d 
 |-  ( ph -> N =/= 0 )
128 123 125 127 69 ddcand 
 |-  ( ph -> ( N / ( N / P ) ) = P )
129 128 64 eqeltrd 
 |-  ( ph -> ( N / ( N / P ) ) e. ZZ )
130 63 nngt0d 
 |-  ( ph -> 0 < P )
131 122 124 126 130 divgt0d 
 |-  ( ph -> 0 < ( N / P ) )
132 131 gt0ne0d 
 |-  ( ph -> ( N / P ) =/= 0 )
133 dvdsval2 
 |-  ( ( ( N / P ) e. ZZ /\ ( N / P ) =/= 0 /\ N e. ZZ ) -> ( ( N / P ) || N <-> ( N / ( N / P ) ) e. ZZ ) )
134 73 132 70 133 syl3anc 
 |-  ( ph -> ( ( N / P ) || N <-> ( N / ( N / P ) ) e. ZZ ) )
135 129 134 mpbird 
 |-  ( ph -> ( N / P ) || N )
136 91 135 jca 
 |-  ( ph -> ( ( R gcd N ) = 1 /\ ( N / P ) || N ) )
137 rpdvds 
 |-  ( ( ( R e. ZZ /\ ( N / P ) e. ZZ /\ N e. ZZ ) /\ ( ( R gcd N ) = 1 /\ ( N / P ) || N ) ) -> ( R gcd ( N / P ) ) = 1 )
138 121 136 137 syl2anc 
 |-  ( ph -> ( R gcd ( N / P ) ) = 1 )
139 138 adantr 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( R gcd ( N / P ) ) = 1 )
140 139 adantr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 2nd ` e ) e. NN ) -> ( R gcd ( N / P ) ) = 1 )
141 4 ad2antrr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 2nd ` e ) e. NN ) -> R e. NN )
142 73 131 jca 
 |-  ( ph -> ( ( N / P ) e. ZZ /\ 0 < ( N / P ) ) )
143 elnnz 
 |-  ( ( N / P ) e. NN <-> ( ( N / P ) e. ZZ /\ 0 < ( N / P ) ) )
144 142 143 sylibr 
 |-  ( ph -> ( N / P ) e. NN )
145 144 adantr 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( N / P ) e. NN )
146 145 adantr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 2nd ` e ) e. NN ) -> ( N / P ) e. NN )
147 simpr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 2nd ` e ) e. NN ) -> ( 2nd ` e ) e. NN )
148 rprpwr 
 |-  ( ( R e. NN /\ ( N / P ) e. NN /\ ( 2nd ` e ) e. NN ) -> ( ( R gcd ( N / P ) ) = 1 -> ( R gcd ( ( N / P ) ^ ( 2nd ` e ) ) ) = 1 ) )
149 141 146 147 148 syl3anc 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 2nd ` e ) e. NN ) -> ( ( R gcd ( N / P ) ) = 1 -> ( R gcd ( ( N / P ) ^ ( 2nd ` e ) ) ) = 1 ) )
150 140 149 mpd 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 2nd ` e ) e. NN ) -> ( R gcd ( ( N / P ) ^ ( 2nd ` e ) ) ) = 1 )
151 76 anim1i 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 2nd ` e ) =/= 0 ) -> ( ( 2nd ` e ) e. NN0 /\ ( 2nd ` e ) =/= 0 ) )
152 elnnne0 
 |-  ( ( 2nd ` e ) e. NN <-> ( ( 2nd ` e ) e. NN0 /\ ( 2nd ` e ) =/= 0 ) )
153 151 152 sylibr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ ( 2nd ` e ) =/= 0 ) -> ( 2nd ` e ) e. NN )
154 153 ex 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( 2nd ` e ) =/= 0 -> ( 2nd ` e ) e. NN ) )
155 154 necon1bd 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( -. ( 2nd ` e ) e. NN -> ( 2nd ` e ) = 0 ) )
156 155 imp 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> ( 2nd ` e ) = 0 )
157 156 oveq2d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> ( ( N / P ) ^ ( 2nd ` e ) ) = ( ( N / P ) ^ 0 ) )
158 157 oveq2d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> ( R gcd ( ( N / P ) ^ ( 2nd ` e ) ) ) = ( R gcd ( ( N / P ) ^ 0 ) ) )
159 123 adantr 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> N e. CC )
160 159 adantr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> N e. CC )
161 111 adantr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> P e. CC )
162 69 ad2antrr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> P =/= 0 )
163 160 161 162 divcld 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> ( N / P ) e. CC )
164 163 exp0d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> ( ( N / P ) ^ 0 ) = 1 )
165 164 oveq2d 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> ( R gcd ( ( N / P ) ^ 0 ) ) = ( R gcd 1 ) )
166 158 165 eqtrd 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> ( R gcd ( ( N / P ) ^ ( 2nd ` e ) ) ) = ( R gcd 1 ) )
167 82 adantr 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> R e. ZZ )
168 167 116 syl 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> ( R gcd 1 ) = 1 )
169 166 168 eqtrd 
 |-  ( ( ( ph /\ e e. ( NN0 X. NN0 ) ) /\ -. ( 2nd ` e ) e. NN ) -> ( R gcd ( ( N / P ) ^ ( 2nd ` e ) ) ) = 1 )
170 150 169 pm2.61dan 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( R gcd ( ( N / P ) ^ ( 2nd ` e ) ) ) = 1 )
171 120 170 jca 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( R gcd ( P ^ ( 1st ` e ) ) ) = 1 /\ ( R gcd ( ( N / P ) ^ ( 2nd ` e ) ) ) = 1 ) )
172 rpmul 
 |-  ( ( R e. ZZ /\ ( P ^ ( 1st ` e ) ) e. ZZ /\ ( ( N / P ) ^ ( 2nd ` e ) ) e. ZZ ) -> ( ( ( R gcd ( P ^ ( 1st ` e ) ) ) = 1 /\ ( R gcd ( ( N / P ) ^ ( 2nd ` e ) ) ) = 1 ) -> ( R gcd ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) ) = 1 ) )
173 82 68 77 172 syl3anc 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( ( R gcd ( P ^ ( 1st ` e ) ) ) = 1 /\ ( R gcd ( ( N / P ) ^ ( 2nd ` e ) ) ) = 1 ) -> ( R gcd ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) ) = 1 ) )
174 171 173 mpd 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( R gcd ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) ) = 1 )
175 83 174 eqtrd 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( ( P ^ ( 1st ` e ) ) x. ( ( N / P ) ^ ( 2nd ` e ) ) ) gcd R ) = 1 )
176 80 175 eqtrd 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( E ` e ) gcd R ) = 1 )
177 79 176 jca 
 |-  ( ( ph /\ e e. ( NN0 X. NN0 ) ) -> ( ( E ` e ) e. ZZ /\ ( ( E ` e ) gcd R ) = 1 ) )
178 51 177 syl 
 |-  ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) -> ( ( E ` e ) e. ZZ /\ ( ( E ` e ) gcd R ) = 1 ) )
179 178 adantr 
 |-  ( ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) /\ ( E ` e ) = c ) -> ( ( E ` e ) e. ZZ /\ ( ( E ` e ) gcd R ) = 1 ) )
180 179 simprd 
 |-  ( ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) /\ ( E ` e ) = c ) -> ( ( E ` e ) gcd R ) = 1 )
181 48 180 eqtrd 
 |-  ( ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) /\ ( E ` e ) = c ) -> ( c gcd R ) = 1 )
182 179 simpld 
 |-  ( ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) /\ ( E ` e ) = c ) -> ( E ` e ) e. ZZ )
183 47 182 eqeltrd 
 |-  ( ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) /\ ( E ` e ) = c ) -> c e. ZZ )
184 181 183 jca 
 |-  ( ( ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) /\ e e. ( NN0 X. NN0 ) ) /\ ( E ` e ) = c ) -> ( ( c gcd R ) = 1 /\ c e. ZZ ) )
185 nfv 
 |-  F/ e ( E ` d ) = c
186 nfv 
 |-  F/ d ( E ` e ) = c
187 fveqeq2 
 |-  ( d = e -> ( ( E ` d ) = c <-> ( E ` e ) = c ) )
188 185 186 187 cbvrexw 
 |-  ( E. d e. ( NN0 X. NN0 ) ( E ` d ) = c <-> E. e e. ( NN0 X. NN0 ) ( E ` e ) = c )
189 188 biimpi 
 |-  ( E. d e. ( NN0 X. NN0 ) ( E ` d ) = c -> E. e e. ( NN0 X. NN0 ) ( E ` e ) = c )
190 189 adantl 
 |-  ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) -> E. e e. ( NN0 X. NN0 ) ( E ` e ) = c )
191 184 190 r19.29a 
 |-  ( ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ E. d e. ( NN0 X. NN0 ) ( E ` d ) = c ) -> ( ( c gcd R ) = 1 /\ c e. ZZ ) )
192 191 ex 
 |-  ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> ( E. d e. ( NN0 X. NN0 ) ( E ` d ) = c -> ( ( c gcd R ) = 1 /\ c e. ZZ ) ) )
193 45 192 mpd 
 |-  ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> ( ( c gcd R ) = 1 /\ c e. ZZ ) )
194 193 simpld 
 |-  ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> ( c gcd R ) = 1 )
195 9 adantr 
 |-  ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> R e. NN0 )
196 193 simprd 
 |-  ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> c e. ZZ )
197 eqid 
 |-  ( Unit ` ( Z/nZ ` R ) ) = ( Unit ` ( Z/nZ ` R ) )
198 10 197 7 znunit 
 |-  ( ( R e. NN0 /\ c e. ZZ ) -> ( ( L ` c ) e. ( Unit ` ( Z/nZ ` R ) ) <-> ( c gcd R ) = 1 ) )
199 195 196 198 syl2anc 
 |-  ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> ( ( L ` c ) e. ( Unit ` ( Z/nZ ` R ) ) <-> ( c gcd R ) = 1 ) )
200 194 199 mpbird 
 |-  ( ( ph /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> ( L ` c ) e. ( Unit ` ( Z/nZ ` R ) ) )
201 28 200 syl 
 |-  ( ( ( ph /\ E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a ) /\ c e. ( E " ( NN0 X. NN0 ) ) ) -> ( L ` c ) e. ( Unit ` ( Z/nZ ` R ) ) )
202 201 adantr 
 |-  ( ( ( ( ph /\ E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a ) /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ ( L ` c ) = a ) -> ( L ` c ) e. ( Unit ` ( Z/nZ ` R ) ) )
203 25 202 eqeltrd 
 |-  ( ( ( ( ph /\ E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a ) /\ c e. ( E " ( NN0 X. NN0 ) ) ) /\ ( L ` c ) = a ) -> a e. ( Unit ` ( Z/nZ ` R ) ) )
204 nfv 
 |-  F/ c ( L ` b ) = a
205 nfv 
 |-  F/ b ( L ` c ) = a
206 fveqeq2 
 |-  ( b = c -> ( ( L ` b ) = a <-> ( L ` c ) = a ) )
207 204 205 206 cbvrexw 
 |-  ( E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a <-> E. c e. ( E " ( NN0 X. NN0 ) ) ( L ` c ) = a )
208 207 biimpi 
 |-  ( E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a -> E. c e. ( E " ( NN0 X. NN0 ) ) ( L ` c ) = a )
209 208 adantl 
 |-  ( ( ph /\ E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a ) -> E. c e. ( E " ( NN0 X. NN0 ) ) ( L ` c ) = a )
210 203 209 r19.29a 
 |-  ( ( ph /\ E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a ) -> a e. ( Unit ` ( Z/nZ ` R ) ) )
211 210 ex 
 |-  ( ph -> ( E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a -> a e. ( Unit ` ( Z/nZ ` R ) ) ) )
212 211 adantr 
 |-  ( ( ph /\ a e. ( L " ( E " ( NN0 X. NN0 ) ) ) ) -> ( E. b e. ( E " ( NN0 X. NN0 ) ) ( L ` b ) = a -> a e. ( Unit ` ( Z/nZ ` R ) ) ) )
213 23 212 mpd 
 |-  ( ( ph /\ a e. ( L " ( E " ( NN0 X. NN0 ) ) ) ) -> a e. ( Unit ` ( Z/nZ ` R ) ) )
214 213 ex 
 |-  ( ph -> ( a e. ( L " ( E " ( NN0 X. NN0 ) ) ) -> a e. ( Unit ` ( Z/nZ ` R ) ) ) )
215 214 ssrdv 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) C_ ( Unit ` ( Z/nZ ` R ) ) )
216 hashss 
 |-  ( ( ( Unit ` ( Z/nZ ` R ) ) e. _V /\ ( L " ( E " ( NN0 X. NN0 ) ) ) C_ ( Unit ` ( Z/nZ ` R ) ) ) -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( Unit ` ( Z/nZ ` R ) ) ) )
217 8 215 216 syl2anc 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( Unit ` ( Z/nZ ` R ) ) ) )
218 10 197 znunithash 
 |-  ( R e. NN -> ( # ` ( Unit ` ( Z/nZ ` R ) ) ) = ( phi ` R ) )
219 4 218 syl 
 |-  ( ph -> ( # ` ( Unit ` ( Z/nZ ` R ) ) ) = ( phi ` R ) )
220 217 219 breqtrd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( phi ` R ) )