Metamath Proof Explorer

Theorem aks4d1p8

Description: Show that N and R are coprime for AKS existence theorem, with eliminated hypothesis. (Contributed by metakunt, 10-Nov-2024) (Proof sketch by Thierry Arnoux.)

Ref Expression
Hypotheses aks4d1p8.1 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks4d1p8.2 
|- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
aks4d1p8.3 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
aks4d1p8.4 
|- R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < )
Assertion aks4d1p8 
|- ( ph -> ( N gcd R ) = 1 )

Proof

Step Hyp Ref Expression
1 aks4d1p8.1 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
2 aks4d1p8.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p8.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 aks4d1p8.4 
 |-  R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < )
5 4 a1i 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) )
6 ssrab2 
 |-  { r e. ( 1 ... B ) | -. r || A } C_ ( 1 ... B )
7 6 a1i 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } C_ ( 1 ... B ) )
8 elfznn 
 |-  ( o e. ( 1 ... B ) -> o e. NN )
9 8 adantl 
 |-  ( ( ph /\ o e. ( 1 ... B ) ) -> o e. NN )
10 9 nnred 
 |-  ( ( ph /\ o e. ( 1 ... B ) ) -> o e. RR )
11 10 ex 
 |-  ( ph -> ( o e. ( 1 ... B ) -> o e. RR ) )
12 11 ssrdv 
 |-  ( ph -> ( 1 ... B ) C_ RR )
13 7 12 sstrd 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
14 13 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
15 14 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
16 15 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
17 16 adantr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
18 fzfid 
 |-  ( ph -> ( 1 ... B ) e. Fin )
19 18 7 ssfid 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } e. Fin )
20 1 2 3 aks4d1p3 
 |-  ( ph -> E. r e. ( 1 ... B ) -. r || A )
21 rabn0 
 |-  ( { r e. ( 1 ... B ) | -. r || A } =/= (/) <-> E. r e. ( 1 ... B ) -. r || A )
22 20 21 sylibr 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } =/= (/) )
23 fiminre 
 |-  ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ { r e. ( 1 ... B ) | -. r || A } e. Fin /\ { r e. ( 1 ... B ) | -. r || A } =/= (/) ) -> E. x e. { r e. ( 1 ... B ) | -. r || A } A. y e. { r e. ( 1 ... B ) | -. r || A } x <_ y )
24 13 19 22 23 syl3anc 
 |-  ( ph -> E. x e. { r e. ( 1 ... B ) | -. r || A } A. y e. { r e. ( 1 ... B ) | -. r || A } x <_ y )
25 24 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> E. x e. { r e. ( 1 ... B ) | -. r || A } A. y e. { r e. ( 1 ... B ) | -. r || A } x <_ y )
26 25 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> E. x e. { r e. ( 1 ... B ) | -. r || A } A. y e. { r e. ( 1 ... B ) | -. r || A } x <_ y )
27 26 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> E. x e. { r e. ( 1 ... B ) | -. r || A } A. y e. { r e. ( 1 ... B ) | -. r || A } x <_ y )
28 27 adantr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> E. x e. { r e. ( 1 ... B ) | -. r || A } A. y e. { r e. ( 1 ... B ) | -. r || A } x <_ y )
29 breq1 
 |-  ( r = ( R / p ) -> ( r || A <-> ( R / p ) || A ) )
30 29 notbid 
 |-  ( r = ( R / p ) -> ( -. r || A <-> -. ( R / p ) || A ) )
31 1zzd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> 1 e. ZZ )
32 3 a1i 
 |-  ( ph -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
33 2re 
 |-  2 e. RR
34 33 a1i 
 |-  ( ph -> 2 e. RR )
35 2pos 
 |-  0 < 2
36 35 a1i 
 |-  ( ph -> 0 < 2 )
37 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
38 1 37 syl 
 |-  ( ph -> N e. ZZ )
39 38 zred 
 |-  ( ph -> N e. RR )
40 0red 
 |-  ( ph -> 0 e. RR )
41 3re 
 |-  3 e. RR
42 41 a1i 
 |-  ( ph -> 3 e. RR )
43 3pos 
 |-  0 < 3
44 43 a1i 
 |-  ( ph -> 0 < 3 )
45 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
46 1 45 syl 
 |-  ( ph -> 3 <_ N )
47 40 42 39 44 46 ltletrd 
 |-  ( ph -> 0 < N )
48 1red 
 |-  ( ph -> 1 e. RR )
49 1lt2 
 |-  1 < 2
50 49 a1i 
 |-  ( ph -> 1 < 2 )
51 48 50 ltned 
 |-  ( ph -> 1 =/= 2 )
52 51 necomd 
 |-  ( ph -> 2 =/= 1 )
53 34 36 39 47 52 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
54 5nn0 
 |-  5 e. NN0
55 54 a1i 
 |-  ( ph -> 5 e. NN0 )
56 53 55 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) e. RR )
57 56 ceilcld 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
58 32 57 eqeltrd 
 |-  ( ph -> B e. ZZ )
59 58 ad4antr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> B e. ZZ )
60 simplrl 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> p || R )
61 prmnn 
 |-  ( p e. Prime -> p e. NN )
62 61 adantl 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> p e. NN )
63 62 ad2antrr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> p e. NN )
64 63 nnzd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> p e. ZZ )
65 62 nnne0d 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> p =/= 0 )
66 65 ad2antrr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> p =/= 0 )
67 1 2 3 4 aks4d1p4 
 |-  ( ph -> ( R e. ( 1 ... B ) /\ -. R || A ) )
68 67 simpld 
 |-  ( ph -> R e. ( 1 ... B ) )
69 elfznn 
 |-  ( R e. ( 1 ... B ) -> R e. NN )
70 68 69 syl 
 |-  ( ph -> R e. NN )
71 70 ad4antr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) -> R e. NN )
72 71 adantr 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) -> R e. NN )
73 72 nnzd 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) -> R e. ZZ )
74 anass 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) <-> ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) )
75 74 anbi1i 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) <-> ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) )
76 75 imbi1i 
 |-  ( ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) -> R e. ZZ ) <-> ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> R e. ZZ ) )
77 73 76 mpbi 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> R e. ZZ )
78 dvdsval2 
 |-  ( ( p e. ZZ /\ p =/= 0 /\ R e. ZZ ) -> ( p || R <-> ( R / p ) e. ZZ ) )
79 64 66 77 78 syl3anc 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( p || R <-> ( R / p ) e. ZZ ) )
80 60 79 mpbid 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( R / p ) e. ZZ )
81 63 nncnd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> p e. CC )
82 81 mulid2d 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( 1 x. p ) = p )
83 75 72 sylbir 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> R e. NN )
84 64 83 jca 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( p e. ZZ /\ R e. NN ) )
85 dvdsle 
 |-  ( ( p e. ZZ /\ R e. NN ) -> ( p || R -> p <_ R ) )
86 85 imp 
 |-  ( ( ( p e. ZZ /\ R e. NN ) /\ p || R ) -> p <_ R )
87 84 60 86 syl2anc 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> p <_ R )
88 82 87 eqbrtrd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( 1 x. p ) <_ R )
89 1red 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> 1 e. RR )
90 70 nnred 
 |-  ( ph -> R e. RR )
91 90 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R e. RR )
92 91 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> R e. RR )
93 92 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> R e. RR )
94 93 adantr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> R e. RR )
95 63 nnrpd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> p e. RR+ )
96 89 94 95 lemuldivd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( ( 1 x. p ) <_ R <-> 1 <_ ( R / p ) ) )
97 88 96 mpbid 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> 1 <_ ( R / p ) )
98 90 ad2antrr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> R e. RR )
99 58 ad2antrr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> B e. ZZ )
100 99 zred 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> B e. RR )
101 62 nnred 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> p e. RR )
102 100 101 remulcld 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> ( B x. p ) e. RR )
103 elfzle2 
 |-  ( R e. ( 1 ... B ) -> R <_ B )
104 68 103 syl 
 |-  ( ph -> R <_ B )
105 104 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R <_ B )
106 105 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> R <_ B )
107 58 zred 
 |-  ( ph -> B e. RR )
108 9re 
 |-  9 e. RR
109 108 a1i 
 |-  ( ph -> 9 e. RR )
110 9pos 
 |-  0 < 9
111 110 a1i 
 |-  ( ph -> 0 < 9 )
112 32 107 eqeltrrd 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR )
113 39 46 3lexlogpow5ineq4 
 |-  ( ph -> 9 < ( ( 2 logb N ) ^ 5 ) )
114 56 ceilged 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
115 109 56 112 113 114 ltletrd 
 |-  ( ph -> 9 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
116 115 32 breqtrrd 
 |-  ( ph -> 9 < B )
117 40 109 107 111 116 lttrd 
 |-  ( ph -> 0 < B )
118 40 107 117 ltled 
 |-  ( ph -> 0 <_ B )
119 118 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> 0 <_ B )
120 119 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> 0 <_ B )
121 62 nnge1d 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> 1 <_ p )
122 100 101 120 121 lemulge11d 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> B <_ ( B x. p ) )
123 98 100 102 106 122 letrd 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> R <_ ( B x. p ) )
124 62 nnrpd 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> p e. RR+ )
125 98 100 124 ledivmul2d 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> ( ( R / p ) <_ B <-> R <_ ( B x. p ) ) )
126 123 125 mpbird 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> ( R / p ) <_ B )
127 126 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R / p ) <_ B )
128 127 adantr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( R / p ) <_ B )
129 31 59 80 97 128 elfzd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( R / p ) e. ( 1 ... B ) )
130 93 recnd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> R e. CC )
131 62 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> p e. NN )
132 131 nnzd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> p e. ZZ )
133 simplr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> p e. Prime )
134 71 anasss 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> R e. NN )
135 133 134 pccld 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p pCnt R ) e. NN0 )
136 132 135 zexpcld 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) e. ZZ )
137 136 zcnd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) e. CC )
138 131 nncnd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> p e. CC )
139 65 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> p =/= 0 )
140 135 nn0zd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p pCnt R ) e. ZZ )
141 138 139 140 expne0d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) =/= 0 )
142 130 137 141 divcan1d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( R / ( p ^ ( p pCnt R ) ) ) x. ( p ^ ( p pCnt R ) ) ) = R )
143 142 eqcomd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> R = ( ( R / ( p ^ ( p pCnt R ) ) ) x. ( p ^ ( p pCnt R ) ) ) )
144 pcdvds 
 |-  ( ( p e. Prime /\ R e. NN ) -> ( p ^ ( p pCnt R ) ) || R )
145 133 134 144 syl2anc 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) || R )
146 134 nnzd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> R e. ZZ )
147 dvdsval2 
 |-  ( ( ( p ^ ( p pCnt R ) ) e. ZZ /\ ( p ^ ( p pCnt R ) ) =/= 0 /\ R e. ZZ ) -> ( ( p ^ ( p pCnt R ) ) || R <-> ( R / ( p ^ ( p pCnt R ) ) ) e. ZZ ) )
148 136 141 146 147 syl3anc 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( p ^ ( p pCnt R ) ) || R <-> ( R / ( p ^ ( p pCnt R ) ) ) e. ZZ ) )
149 145 148 mpbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R / ( p ^ ( p pCnt R ) ) ) e. ZZ )
150 38 47 jca 
 |-  ( ph -> ( N e. ZZ /\ 0 < N ) )
151 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
152 151 a1i 
 |-  ( ph -> ( N e. NN <-> ( N e. ZZ /\ 0 < N ) ) )
153 150 152 mpbird 
 |-  ( ph -> N e. NN )
154 153 nnzd 
 |-  ( ph -> N e. ZZ )
155 34 36 107 117 52 relogbcld 
 |-  ( ph -> ( 2 logb B ) e. RR )
156 155 flcld 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. ZZ )
157 34 recnd 
 |-  ( ph -> 2 e. CC )
158 40 36 gtned 
 |-  ( ph -> 2 =/= 0 )
159 logb1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 1 ) = 0 )
160 157 158 52 159 syl3anc 
 |-  ( ph -> ( 2 logb 1 ) = 0 )
161 160 eqcomd 
 |-  ( ph -> 0 = ( 2 logb 1 ) )
162 2z 
 |-  2 e. ZZ
163 162 a1i 
 |-  ( ph -> 2 e. ZZ )
164 34 leidd 
 |-  ( ph -> 2 <_ 2 )
165 0lt1 
 |-  0 < 1
166 165 a1i 
 |-  ( ph -> 0 < 1 )
167 1lt9 
 |-  1 < 9
168 167 a1i 
 |-  ( ph -> 1 < 9 )
169 48 109 107 168 116 lttrd 
 |-  ( ph -> 1 < B )
170 48 107 169 ltled 
 |-  ( ph -> 1 <_ B )
171 163 164 48 166 107 117 170 logblebd 
 |-  ( ph -> ( 2 logb 1 ) <_ ( 2 logb B ) )
172 161 171 eqbrtrd 
 |-  ( ph -> 0 <_ ( 2 logb B ) )
173 0zd 
 |-  ( ph -> 0 e. ZZ )
174 flge 
 |-  ( ( ( 2 logb B ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( 2 logb B ) <-> 0 <_ ( |_ ` ( 2 logb B ) ) ) )
175 155 173 174 syl2anc 
 |-  ( ph -> ( 0 <_ ( 2 logb B ) <-> 0 <_ ( |_ ` ( 2 logb B ) ) ) )
176 172 175 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( 2 logb B ) ) )
177 156 176 jca 
 |-  ( ph -> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
178 elnn0z 
 |-  ( ( |_ ` ( 2 logb B ) ) e. NN0 <-> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
179 178 a1i 
 |-  ( ph -> ( ( |_ ` ( 2 logb B ) ) e. NN0 <-> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) ) )
180 177 179 mpbird 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. NN0 )
181 154 180 zexpcld 
 |-  ( ph -> ( N ^ ( |_ ` ( 2 logb B ) ) ) e. ZZ )
182 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) e. Fin )
183 154 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> N e. ZZ )
184 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> k e. NN )
185 184 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN )
186 185 nnnn0d 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN0 )
187 183 186 zexpcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ k ) e. ZZ )
188 1zzd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 e. ZZ )
189 187 188 zsubcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) e. ZZ )
190 182 189 fprodzcl 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) e. ZZ )
191 181 190 zmulcld 
 |-  ( ph -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) e. ZZ )
192 2 a1i 
 |-  ( ph -> A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
193 192 eleq1d 
 |-  ( ph -> ( A e. ZZ <-> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) e. ZZ ) )
194 191 193 mpbird 
 |-  ( ph -> A e. ZZ )
195 194 ad3antrrr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> A e. ZZ )
196 simprl 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> p || R )
197 134 133 196 aks4d1p8d3 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( R / ( p ^ ( p pCnt R ) ) ) gcd ( p ^ ( p pCnt R ) ) ) = 1 )
198 138 exp0d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ 0 ) = 1 )
199 pcelnn 
 |-  ( ( p e. Prime /\ R e. NN ) -> ( ( p pCnt R ) e. NN <-> p || R ) )
200 133 134 199 syl2anc 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( p pCnt R ) e. NN <-> p || R ) )
201 196 200 mpbird 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p pCnt R ) e. NN )
202 201 nngt0d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 0 < ( p pCnt R ) )
203 101 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> p e. RR )
204 173 ad3antrrr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 0 e. ZZ )
205 prmgt1 
 |-  ( p e. Prime -> 1 < p )
206 205 adantl 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> 1 < p )
207 206 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 1 < p )
208 203 204 140 207 ltexp2d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( 0 < ( p pCnt R ) <-> ( p ^ 0 ) < ( p ^ ( p pCnt R ) ) ) )
209 202 208 mpbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ 0 ) < ( p ^ ( p pCnt R ) ) )
210 198 209 eqbrtrrd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 1 < ( p ^ ( p pCnt R ) ) )
211 136 zred 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) e. RR )
212 70 nnrpd 
 |-  ( ph -> R e. RR+ )
213 212 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> R e. RR+ )
214 213 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> R e. RR+ )
215 214 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> R e. RR+ )
216 211 215 ltmulgt11d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( 1 < ( p ^ ( p pCnt R ) ) <-> R < ( R x. ( p ^ ( p pCnt R ) ) ) ) )
217 210 216 mpbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> R < ( R x. ( p ^ ( p pCnt R ) ) ) )
218 124 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> p e. RR+ )
219 218 140 rpexpcld 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) e. RR+ )
220 93 93 219 ltdivmul2d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( R / ( p ^ ( p pCnt R ) ) ) < R <-> R < ( R x. ( p ^ ( p pCnt R ) ) ) ) )
221 217 220 mpbird 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R / ( p ^ ( p pCnt R ) ) ) < R )
222 93 211 141 redivcld 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R / ( p ^ ( p pCnt R ) ) ) e. RR )
223 222 93 ltnled 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( R / ( p ^ ( p pCnt R ) ) ) < R <-> -. R <_ ( R / ( p ^ ( p pCnt R ) ) ) ) )
224 221 223 mpbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> -. R <_ ( R / ( p ^ ( p pCnt R ) ) ) )
225 4 a1i 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) )
226 225 breq1d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R <_ ( R / ( p ^ ( p pCnt R ) ) ) <-> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / ( p ^ ( p pCnt R ) ) ) ) )
227 226 notbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( -. R <_ ( R / ( p ^ ( p pCnt R ) ) ) <-> -. inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / ( p ^ ( p pCnt R ) ) ) ) )
228 224 227 mpbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> -. inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / ( p ^ ( p pCnt R ) ) ) )
229 elfznn 
 |-  ( f e. ( 1 ... B ) -> f e. NN )
230 229 adantl 
 |-  ( ( ph /\ f e. ( 1 ... B ) ) -> f e. NN )
231 230 nnred 
 |-  ( ( ph /\ f e. ( 1 ... B ) ) -> f e. RR )
232 231 ex 
 |-  ( ph -> ( f e. ( 1 ... B ) -> f e. RR ) )
233 232 ssrdv 
 |-  ( ph -> ( 1 ... B ) C_ RR )
234 7 233 sstrd 
 |-  ( ph -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
235 234 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
236 235 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
237 236 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> { r e. ( 1 ... B ) | -. r || A } C_ RR )
238 19 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> { r e. ( 1 ... B ) | -. r || A } e. Fin )
239 238 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> { r e. ( 1 ... B ) | -. r || A } e. Fin )
240 239 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> { r e. ( 1 ... B ) | -. r || A } e. Fin )
241 infrefilb 
 |-  ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ { r e. ( 1 ... B ) | -. r || A } e. Fin /\ ( R / ( p ^ ( p pCnt R ) ) ) e. { r e. ( 1 ... B ) | -. r || A } ) -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / ( p ^ ( p pCnt R ) ) ) )
242 241 3expa 
 |-  ( ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ { r e. ( 1 ... B ) | -. r || A } e. Fin ) /\ ( R / ( p ^ ( p pCnt R ) ) ) e. { r e. ( 1 ... B ) | -. r || A } ) -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / ( p ^ ( p pCnt R ) ) ) )
243 242 ex 
 |-  ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ { r e. ( 1 ... B ) | -. r || A } e. Fin ) -> ( ( R / ( p ^ ( p pCnt R ) ) ) e. { r e. ( 1 ... B ) | -. r || A } -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / ( p ^ ( p pCnt R ) ) ) ) )
244 243 con3d 
 |-  ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ { r e. ( 1 ... B ) | -. r || A } e. Fin ) -> ( -. inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / ( p ^ ( p pCnt R ) ) ) -> -. ( R / ( p ^ ( p pCnt R ) ) ) e. { r e. ( 1 ... B ) | -. r || A } ) )
245 237 240 244 syl2anc 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( -. inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / ( p ^ ( p pCnt R ) ) ) -> -. ( R / ( p ^ ( p pCnt R ) ) ) e. { r e. ( 1 ... B ) | -. r || A } ) )
246 228 245 mpd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> -. ( R / ( p ^ ( p pCnt R ) ) ) e. { r e. ( 1 ... B ) | -. r || A } )
247 1zzd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 1 e. ZZ )
248 99 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> B e. ZZ )
249 137 mulid2d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( 1 x. ( p ^ ( p pCnt R ) ) ) = ( p ^ ( p pCnt R ) ) )
250 dvdsle 
 |-  ( ( ( p ^ ( p pCnt R ) ) e. ZZ /\ R e. NN ) -> ( ( p ^ ( p pCnt R ) ) || R -> ( p ^ ( p pCnt R ) ) <_ R ) )
251 136 134 250 syl2anc 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( p ^ ( p pCnt R ) ) || R -> ( p ^ ( p pCnt R ) ) <_ R ) )
252 145 251 mpd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) <_ R )
253 249 252 eqbrtrd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( 1 x. ( p ^ ( p pCnt R ) ) ) <_ R )
254 48 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> 1 e. RR )
255 254 ad2antrr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 1 e. RR )
256 255 93 219 lemuldivd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( 1 x. ( p ^ ( p pCnt R ) ) ) <_ R <-> 1 <_ ( R / ( p ^ ( p pCnt R ) ) ) ) )
257 253 256 mpbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 1 <_ ( R / ( p ^ ( p pCnt R ) ) ) )
258 100 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> B e. RR )
259 121 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 1 <_ p )
260 203 135 259 expge1d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 1 <_ ( p ^ ( p pCnt R ) ) )
261 nnledivrp 
 |-  ( ( R e. NN /\ ( p ^ ( p pCnt R ) ) e. RR+ ) -> ( 1 <_ ( p ^ ( p pCnt R ) ) <-> ( R / ( p ^ ( p pCnt R ) ) ) <_ R ) )
262 134 219 261 syl2anc 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( 1 <_ ( p ^ ( p pCnt R ) ) <-> ( R / ( p ^ ( p pCnt R ) ) ) <_ R ) )
263 260 262 mpbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R / ( p ^ ( p pCnt R ) ) ) <_ R )
264 106 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> R <_ B )
265 222 93 258 263 264 letrd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R / ( p ^ ( p pCnt R ) ) ) <_ B )
266 247 248 149 257 265 elfzd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R / ( p ^ ( p pCnt R ) ) ) e. ( 1 ... B ) )
267 breq1 
 |-  ( r = ( R / ( p ^ ( p pCnt R ) ) ) -> ( r || A <-> ( R / ( p ^ ( p pCnt R ) ) ) || A ) )
268 267 notbid 
 |-  ( r = ( R / ( p ^ ( p pCnt R ) ) ) -> ( -. r || A <-> -. ( R / ( p ^ ( p pCnt R ) ) ) || A ) )
269 268 elrab3 
 |-  ( ( R / ( p ^ ( p pCnt R ) ) ) e. ( 1 ... B ) -> ( ( R / ( p ^ ( p pCnt R ) ) ) e. { r e. ( 1 ... B ) | -. r || A } <-> -. ( R / ( p ^ ( p pCnt R ) ) ) || A ) )
270 269 con2bid 
 |-  ( ( R / ( p ^ ( p pCnt R ) ) ) e. ( 1 ... B ) -> ( ( R / ( p ^ ( p pCnt R ) ) ) || A <-> -. ( R / ( p ^ ( p pCnt R ) ) ) e. { r e. ( 1 ... B ) | -. r || A } ) )
271 266 270 syl 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( R / ( p ^ ( p pCnt R ) ) ) || A <-> -. ( R / ( p ^ ( p pCnt R ) ) ) e. { r e. ( 1 ... B ) | -. r || A } ) )
272 246 271 mpbird 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R / ( p ^ ( p pCnt R ) ) ) || A )
273 134 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ q e. Prime ) /\ ( q || N /\ q || R ) ) -> R e. NN )
274 153 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> N e. NN )
275 274 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> N e. NN )
276 275 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) -> N e. NN )
277 276 adantr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) -> N e. NN )
278 74 277 sylbir 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> N e. NN )
279 278 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ q e. Prime ) /\ ( q || N /\ q || R ) ) -> N e. NN )
280 133 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ q e. Prime ) /\ ( q || N /\ q || R ) ) -> p e. Prime )
281 simplr 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ q e. Prime ) /\ ( q || N /\ q || R ) ) -> q e. Prime )
282 196 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ q e. Prime ) /\ ( q || N /\ q || R ) ) -> p || R )
283 simprr 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ q e. Prime ) /\ ( q || N /\ q || R ) ) -> q || R )
284 simplrr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ q e. Prime ) -> -. p || N )
285 284 adantr 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ q e. Prime ) /\ ( q || N /\ q || R ) ) -> -. p || N )
286 simprl 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ q e. Prime ) /\ ( q || N /\ q || R ) ) -> q || N )
287 273 279 280 281 282 283 285 286 aks4d1p8d2 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ q e. Prime ) /\ ( q || N /\ q || R ) ) -> ( p ^ ( p pCnt R ) ) < R )
288 simpr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> 1 < ( N gcd R ) )
289 288 ad2antrr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 1 < ( N gcd R ) )
290 255 289 ltned 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> 1 =/= ( N gcd R ) )
291 290 necomd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( N gcd R ) =/= 1 )
292 278 134 prmdvdsncoprmbd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( E. q e. Prime ( q || N /\ q || R ) <-> ( N gcd R ) =/= 1 ) )
293 292 bicomd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( N gcd R ) =/= 1 <-> E. q e. Prime ( q || N /\ q || R ) ) )
294 293 biimpd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( N gcd R ) =/= 1 -> E. q e. Prime ( q || N /\ q || R ) ) )
295 291 294 mpd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> E. q e. Prime ( q || N /\ q || R ) )
296 287 295 r19.29a 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) < R )
297 211 93 ltnled 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( p ^ ( p pCnt R ) ) < R <-> -. R <_ ( p ^ ( p pCnt R ) ) ) )
298 296 297 mpbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> -. R <_ ( p ^ ( p pCnt R ) ) )
299 225 breq1d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R <_ ( p ^ ( p pCnt R ) ) <-> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( p ^ ( p pCnt R ) ) ) )
300 299 notbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( -. R <_ ( p ^ ( p pCnt R ) ) <-> -. inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( p ^ ( p pCnt R ) ) ) )
301 298 300 mpbid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> -. inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( p ^ ( p pCnt R ) ) )
302 infrefilb 
 |-  ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ { r e. ( 1 ... B ) | -. r || A } e. Fin /\ ( p ^ ( p pCnt R ) ) e. { r e. ( 1 ... B ) | -. r || A } ) -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( p ^ ( p pCnt R ) ) )
303 302 3expa 
 |-  ( ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ { r e. ( 1 ... B ) | -. r || A } e. Fin ) /\ ( p ^ ( p pCnt R ) ) e. { r e. ( 1 ... B ) | -. r || A } ) -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( p ^ ( p pCnt R ) ) )
304 303 ex 
 |-  ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ { r e. ( 1 ... B ) | -. r || A } e. Fin ) -> ( ( p ^ ( p pCnt R ) ) e. { r e. ( 1 ... B ) | -. r || A } -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( p ^ ( p pCnt R ) ) ) )
305 304 con3d 
 |-  ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ { r e. ( 1 ... B ) | -. r || A } e. Fin ) -> ( -. inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( p ^ ( p pCnt R ) ) -> -. ( p ^ ( p pCnt R ) ) e. { r e. ( 1 ... B ) | -. r || A } ) )
306 237 240 305 syl2anc 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( -. inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( p ^ ( p pCnt R ) ) -> -. ( p ^ ( p pCnt R ) ) e. { r e. ( 1 ... B ) | -. r || A } ) )
307 301 306 mpd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> -. ( p ^ ( p pCnt R ) ) e. { r e. ( 1 ... B ) | -. r || A } )
308 211 93 258 252 264 letrd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) <_ B )
309 247 248 136 260 308 elfzd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) e. ( 1 ... B ) )
310 breq1 
 |-  ( r = ( p ^ ( p pCnt R ) ) -> ( r || A <-> ( p ^ ( p pCnt R ) ) || A ) )
311 310 notbid 
 |-  ( r = ( p ^ ( p pCnt R ) ) -> ( -. r || A <-> -. ( p ^ ( p pCnt R ) ) || A ) )
312 311 elrab3 
 |-  ( ( p ^ ( p pCnt R ) ) e. ( 1 ... B ) -> ( ( p ^ ( p pCnt R ) ) e. { r e. ( 1 ... B ) | -. r || A } <-> -. ( p ^ ( p pCnt R ) ) || A ) )
313 309 312 syl 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( p ^ ( p pCnt R ) ) e. { r e. ( 1 ... B ) | -. r || A } <-> -. ( p ^ ( p pCnt R ) ) || A ) )
314 313 con2bid 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( p ^ ( p pCnt R ) ) || A <-> -. ( p ^ ( p pCnt R ) ) e. { r e. ( 1 ... B ) | -. r || A } ) )
315 307 314 mpbird 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( p ^ ( p pCnt R ) ) || A )
316 149 136 195 197 272 315 coprmdvds2d 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( ( R / ( p ^ ( p pCnt R ) ) ) x. ( p ^ ( p pCnt R ) ) ) || A )
317 143 316 eqbrtrd 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> R || A )
318 317 adantr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> R || A )
319 67 simprd 
 |-  ( ph -> -. R || A )
320 319 ad5antr 
 |-  ( ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ p || R ) /\ -. p || N ) /\ ( R / ( N gcd R ) ) || A ) -> -. R || A )
321 75 320 sylbir 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> -. R || A )
322 318 321 pm2.21dd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> -. ( R / p ) || A )
323 30 129 322 elrabd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( R / p ) e. { r e. ( 1 ... B ) | -. r || A } )
324 lbinfle 
 |-  ( ( { r e. ( 1 ... B ) | -. r || A } C_ RR /\ E. x e. { r e. ( 1 ... B ) | -. r || A } A. y e. { r e. ( 1 ... B ) | -. r || A } x <_ y /\ ( R / p ) e. { r e. ( 1 ... B ) | -. r || A } ) -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / p ) )
325 17 28 323 324 syl3anc 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) <_ ( R / p ) )
326 5 325 eqbrtrd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> R <_ ( R / p ) )
327 207 adantr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> 1 < p )
328 1rp 
 |-  1 e. RR+
329 328 a1i 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> 1 e. RR+ )
330 215 adantr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> R e. RR+ )
331 329 95 330 ltdiv2d 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( 1 < p <-> ( R / p ) < ( R / 1 ) ) )
332 327 331 mpbid 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( R / p ) < ( R / 1 ) )
333 130 adantr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> R e. CC )
334 333 div1d 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( R / 1 ) = R )
335 332 334 breqtrd 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( R / p ) < R )
336 98 101 65 redivcld 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) -> ( R / p ) e. RR )
337 336 adantr 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> ( R / p ) e. RR )
338 337 adantr 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( R / p ) e. RR )
339 338 94 ltnled 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> ( ( R / p ) < R <-> -. R <_ ( R / p ) ) )
340 335 339 mpbid 
 |-  ( ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) /\ ( R / ( N gcd R ) ) || A ) -> -. R <_ ( R / p ) )
341 326 340 pm2.65da 
 |-  ( ( ( ( ph /\ 1 < ( N gcd R ) ) /\ p e. Prime ) /\ ( p || R /\ -. p || N ) ) -> -. ( R / ( N gcd R ) ) || A )
342 1 2 3 4 aks4d1p7 
 |-  ( ph -> E. p e. Prime ( p || R /\ -. p || N ) )
343 342 adantr 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> E. p e. Prime ( p || R /\ -. p || N ) )
344 341 343 r19.29a 
 |-  ( ( ph /\ 1 < ( N gcd R ) ) -> -. ( R / ( N gcd R ) ) || A )
345 344 adantr 
 |-  ( ( ( ph /\ 1 < ( N gcd R ) ) /\ ( R / ( N gcd R ) ) || A ) -> -. ( R / ( N gcd R ) ) || A )
346 1 2 3 4 345 aks4d1p5 
 |-  ( ph -> ( N gcd R ) = 1 )