Metamath Proof Explorer

Theorem dvdsprmpweqle

Description: If a positive integer divides a prime power, it is a prime power with a smaller exponent. (Contributed by AV, 25-Jul-2021)

Ref Expression
Assertion dvdsprmpweqle 
|- ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN0 ( n <_ N /\ A = ( P ^ n ) ) ) )

Proof

Step Hyp Ref Expression
1 dvdsprmpweq 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN0 A = ( P ^ n ) ) )
2 1 imp 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> E. n e. NN0 A = ( P ^ n ) )
3 nn0re 
 |-  ( N e. NN0 -> N e. RR )
4 3 3ad2ant3 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> N e. RR )
5 4 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> N e. RR )
6 nn0re 
 |-  ( n e. NN0 -> n e. RR )
7 5 6 anim12ci 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n e. NN0 ) -> ( n e. RR /\ N e. RR ) )
8 7 adantr 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> ( n e. RR /\ N e. RR ) )
9 lelttric 
 |-  ( ( n e. RR /\ N e. RR ) -> ( n <_ N \/ N < n ) )
10 8 9 syl 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> ( n <_ N \/ N < n ) )
11 breq1 
 |-  ( A = ( P ^ n ) -> ( A || ( P ^ N ) <-> ( P ^ n ) || ( P ^ N ) ) )
12 11 adantl 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> ( A || ( P ^ N ) <-> ( P ^ n ) || ( P ^ N ) ) )
13 prmnn 
 |-  ( P e. Prime -> P e. NN )
14 13 nnnn0d 
 |-  ( P e. Prime -> P e. NN0 )
15 14 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> P e. NN0 )
16 15 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> P e. NN0 )
17 simpr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> n e. NN0 )
18 16 17 nn0expcld 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( P ^ n ) e. NN0 )
19 18 nn0zd 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( P ^ n ) e. ZZ )
20 13 nncnd 
 |-  ( P e. Prime -> P e. CC )
21 20 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> P e. CC )
22 21 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> P e. CC )
23 13 nnne0d 
 |-  ( P e. Prime -> P =/= 0 )
24 23 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> P =/= 0 )
25 24 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> P =/= 0 )
26 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
27 26 adantl 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> n e. ZZ )
28 22 25 27 expne0d 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( P ^ n ) =/= 0 )
29 simp3 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> N e. NN0 )
30 29 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> N e. NN0 )
31 16 30 nn0expcld 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( P ^ N ) e. NN0 )
32 31 nn0zd 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( P ^ N ) e. ZZ )
33 dvdsval2 
 |-  ( ( ( P ^ n ) e. ZZ /\ ( P ^ n ) =/= 0 /\ ( P ^ N ) e. ZZ ) -> ( ( P ^ n ) || ( P ^ N ) <-> ( ( P ^ N ) / ( P ^ n ) ) e. ZZ ) )
34 19 28 32 33 syl3anc 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( ( P ^ n ) || ( P ^ N ) <-> ( ( P ^ N ) / ( P ^ n ) ) e. ZZ ) )
35 20 23 jca 
 |-  ( P e. Prime -> ( P e. CC /\ P =/= 0 ) )
36 35 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( P e. CC /\ P =/= 0 ) )
37 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
38 37 3ad2ant3 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> N e. ZZ )
39 38 26 anim12i 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( N e. ZZ /\ n e. ZZ ) )
40 expsub 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( N e. ZZ /\ n e. ZZ ) ) -> ( P ^ ( N - n ) ) = ( ( P ^ N ) / ( P ^ n ) ) )
41 40 eqcomd 
 |-  ( ( ( P e. CC /\ P =/= 0 ) /\ ( N e. ZZ /\ n e. ZZ ) ) -> ( ( P ^ N ) / ( P ^ n ) ) = ( P ^ ( N - n ) ) )
42 36 39 41 syl2an2r 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( ( P ^ N ) / ( P ^ n ) ) = ( P ^ ( N - n ) ) )
43 42 eleq1d 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( ( ( P ^ N ) / ( P ^ n ) ) e. ZZ <-> ( P ^ ( N - n ) ) e. ZZ ) )
44 22 adantr 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> P e. CC )
45 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
46 45 3ad2ant3 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> N e. CC )
47 46 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> N e. CC )
48 nn0cn 
 |-  ( n e. NN0 -> n e. CC )
49 48 adantl 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> n e. CC )
50 47 49 subcld 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( N - n ) e. CC )
51 50 adantr 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( N - n ) e. CC )
52 46 48 anim12i 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( N e. CC /\ n e. CC ) )
53 52 adantr 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( N e. CC /\ n e. CC ) )
54 negsubdi2 
 |-  ( ( N e. CC /\ n e. CC ) -> -u ( N - n ) = ( n - N ) )
55 53 54 syl 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> -u ( N - n ) = ( n - N ) )
56 29 anim1ci 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( n e. NN0 /\ N e. NN0 ) )
57 ltsubnn0 
 |-  ( ( n e. NN0 /\ N e. NN0 ) -> ( N < n -> ( n - N ) e. NN0 ) )
58 56 57 syl 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( N < n -> ( n - N ) e. NN0 ) )
59 58 imp 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( n - N ) e. NN0 )
60 55 59 eqeltrd 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> -u ( N - n ) e. NN0 )
61 expneg2 
 |-  ( ( P e. CC /\ ( N - n ) e. CC /\ -u ( N - n ) e. NN0 ) -> ( P ^ ( N - n ) ) = ( 1 / ( P ^ -u ( N - n ) ) ) )
62 44 51 60 61 syl3anc 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( P ^ ( N - n ) ) = ( 1 / ( P ^ -u ( N - n ) ) ) )
63 62 eleq1d 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( ( P ^ ( N - n ) ) e. ZZ <-> ( 1 / ( P ^ -u ( N - n ) ) ) e. ZZ ) )
64 13 nnred 
 |-  ( P e. Prime -> P e. RR )
65 64 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> P e. RR )
66 65 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> P e. RR )
67 66 adantr 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> P e. RR )
68 67 59 reexpcld 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( P ^ ( n - N ) ) e. RR )
69 znnsub 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( N < n <-> ( n - N ) e. NN ) )
70 39 69 syl 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( N < n <-> ( n - N ) e. NN ) )
71 70 biimpa 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( n - N ) e. NN )
72 prmgt1 
 |-  ( P e. Prime -> 1 < P )
73 72 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> 1 < P )
74 73 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> 1 < P )
75 74 adantr 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> 1 < P )
76 expgt1 
 |-  ( ( P e. RR /\ ( n - N ) e. NN /\ 1 < P ) -> 1 < ( P ^ ( n - N ) ) )
77 67 71 75 76 syl3anc 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> 1 < ( P ^ ( n - N ) ) )
78 68 77 jca 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( ( P ^ ( n - N ) ) e. RR /\ 1 < ( P ^ ( n - N ) ) ) )
79 oveq2 
 |-  ( -u ( N - n ) = ( n - N ) -> ( P ^ -u ( N - n ) ) = ( P ^ ( n - N ) ) )
80 79 eleq1d 
 |-  ( -u ( N - n ) = ( n - N ) -> ( ( P ^ -u ( N - n ) ) e. RR <-> ( P ^ ( n - N ) ) e. RR ) )
81 79 breq2d 
 |-  ( -u ( N - n ) = ( n - N ) -> ( 1 < ( P ^ -u ( N - n ) ) <-> 1 < ( P ^ ( n - N ) ) ) )
82 80 81 anbi12d 
 |-  ( -u ( N - n ) = ( n - N ) -> ( ( ( P ^ -u ( N - n ) ) e. RR /\ 1 < ( P ^ -u ( N - n ) ) ) <-> ( ( P ^ ( n - N ) ) e. RR /\ 1 < ( P ^ ( n - N ) ) ) ) )
83 78 82 syl5ibrcom 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( -u ( N - n ) = ( n - N ) -> ( ( P ^ -u ( N - n ) ) e. RR /\ 1 < ( P ^ -u ( N - n ) ) ) ) )
84 55 83 mpd 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( ( P ^ -u ( N - n ) ) e. RR /\ 1 < ( P ^ -u ( N - n ) ) ) )
85 recnz 
 |-  ( ( ( P ^ -u ( N - n ) ) e. RR /\ 1 < ( P ^ -u ( N - n ) ) ) -> -. ( 1 / ( P ^ -u ( N - n ) ) ) e. ZZ )
86 84 85 syl 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> -. ( 1 / ( P ^ -u ( N - n ) ) ) e. ZZ )
87 86 pm2.21d 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( ( 1 / ( P ^ -u ( N - n ) ) ) e. ZZ -> n <_ N ) )
88 63 87 sylbid 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ N < n ) -> ( ( P ^ ( N - n ) ) e. ZZ -> n <_ N ) )
89 88 ex 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( N < n -> ( ( P ^ ( N - n ) ) e. ZZ -> n <_ N ) ) )
90 89 com23 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( ( P ^ ( N - n ) ) e. ZZ -> ( N < n -> n <_ N ) ) )
91 43 90 sylbid 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( ( ( P ^ N ) / ( P ^ n ) ) e. ZZ -> ( N < n -> n <_ N ) ) )
92 34 91 sylbid 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( ( P ^ n ) || ( P ^ N ) -> ( N < n -> n <_ N ) ) )
93 92 adantr 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> ( ( P ^ n ) || ( P ^ N ) -> ( N < n -> n <_ N ) ) )
94 12 93 sylbid 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> ( A || ( P ^ N ) -> ( N < n -> n <_ N ) ) )
95 94 ex 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( A = ( P ^ n ) -> ( A || ( P ^ N ) -> ( N < n -> n <_ N ) ) ) )
96 95 com23 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ n e. NN0 ) -> ( A || ( P ^ N ) -> ( A = ( P ^ n ) -> ( N < n -> n <_ N ) ) ) )
97 96 ex 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( n e. NN0 -> ( A || ( P ^ N ) -> ( A = ( P ^ n ) -> ( N < n -> n <_ N ) ) ) ) )
98 97 com23 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( A || ( P ^ N ) -> ( n e. NN0 -> ( A = ( P ^ n ) -> ( N < n -> n <_ N ) ) ) ) )
99 98 imp41 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> ( N < n -> n <_ N ) )
100 99 com12 
 |-  ( N < n -> ( ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> n <_ N ) )
101 100 jao1i 
 |-  ( ( n <_ N \/ N < n ) -> ( ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> n <_ N ) )
102 10 101 mpcom 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> n <_ N )
103 simpr 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> A = ( P ^ n ) )
104 102 103 jca 
 |-  ( ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n e. NN0 ) /\ A = ( P ^ n ) ) -> ( n <_ N /\ A = ( P ^ n ) ) )
105 104 ex 
 |-  ( ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) /\ n e. NN0 ) -> ( A = ( P ^ n ) -> ( n <_ N /\ A = ( P ^ n ) ) ) )
106 105 reximdva 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> ( E. n e. NN0 A = ( P ^ n ) -> E. n e. NN0 ( n <_ N /\ A = ( P ^ n ) ) ) )
107 2 106 mpd 
 |-  ( ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> E. n e. NN0 ( n <_ N /\ A = ( P ^ n ) ) )
108 107 ex 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN0 ( n <_ N /\ A = ( P ^ n ) ) ) )