Metamath Proof Explorer

Theorem aks4d1p8d2

Description: Any prime power dividing a positive integer is less than that integer if that integer has another prime factor. (Contributed by metakunt, 13-Nov-2024)

Ref Expression
Hypotheses aks4d1p8d2.1 
|- ( ph -> R e. NN )
aks4d1p8d2.2 
|- ( ph -> N e. NN )
aks4d1p8d2.3 
|- ( ph -> P e. Prime )
aks4d1p8d2.4 
|- ( ph -> Q e. Prime )
aks4d1p8d2.5 
|- ( ph -> P || R )
aks4d1p8d2.6 
|- ( ph -> Q || R )
aks4d1p8d2.7 
|- ( ph -> -. P || N )
aks4d1p8d2.8 
|- ( ph -> Q || N )
Assertion aks4d1p8d2 
|- ( ph -> ( P ^ ( P pCnt R ) ) < R )

Proof

Step Hyp Ref Expression
1 aks4d1p8d2.1 
 |-  ( ph -> R e. NN )
2 aks4d1p8d2.2 
 |-  ( ph -> N e. NN )
3 aks4d1p8d2.3 
 |-  ( ph -> P e. Prime )
4 aks4d1p8d2.4 
 |-  ( ph -> Q e. Prime )
5 aks4d1p8d2.5 
 |-  ( ph -> P || R )
6 aks4d1p8d2.6 
 |-  ( ph -> Q || R )
7 aks4d1p8d2.7 
 |-  ( ph -> -. P || N )
8 aks4d1p8d2.8 
 |-  ( ph -> Q || N )
9 prmnn 
 |-  ( P e. Prime -> P e. NN )
10 3 9 syl 
 |-  ( ph -> P e. NN )
11 10 nnred 
 |-  ( ph -> P e. RR )
12 3 1 pccld 
 |-  ( ph -> ( P pCnt R ) e. NN0 )
13 11 12 reexpcld 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) e. RR )
14 prmnn 
 |-  ( Q e. Prime -> Q e. NN )
15 4 14 syl 
 |-  ( ph -> Q e. NN )
16 15 nnred 
 |-  ( ph -> Q e. RR )
17 13 16 remulcld 
 |-  ( ph -> ( ( P ^ ( P pCnt R ) ) x. Q ) e. RR )
18 1 nnred 
 |-  ( ph -> R e. RR )
19 13 recnd 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) e. CC )
20 19 mulid1d 
 |-  ( ph -> ( ( P ^ ( P pCnt R ) ) x. 1 ) = ( P ^ ( P pCnt R ) ) )
21 1red 
 |-  ( ph -> 1 e. RR )
22 10 nnrpd 
 |-  ( ph -> P e. RR+ )
23 12 nn0zd 
 |-  ( ph -> ( P pCnt R ) e. ZZ )
24 22 23 rpexpcld 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) e. RR+ )
25 prmgt1 
 |-  ( Q e. Prime -> 1 < Q )
26 4 25 syl 
 |-  ( ph -> 1 < Q )
27 21 16 24 26 ltmul2dd 
 |-  ( ph -> ( ( P ^ ( P pCnt R ) ) x. 1 ) < ( ( P ^ ( P pCnt R ) ) x. Q ) )
28 20 27 eqbrtrrd 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) < ( ( P ^ ( P pCnt R ) ) x. Q ) )
29 10 nnzd 
 |-  ( ph -> P e. ZZ )
30 29 12 zexpcld 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) e. ZZ )
31 15 nnzd 
 |-  ( ph -> Q e. ZZ )
32 1 nnzd 
 |-  ( ph -> R e. ZZ )
33 30 31 gcdcomd 
 |-  ( ph -> ( ( P ^ ( P pCnt R ) ) gcd Q ) = ( Q gcd ( P ^ ( P pCnt R ) ) ) )
34 0lt1 
 |-  0 < 1
35 34 a1i 
 |-  ( ph -> 0 < 1 )
36 0red 
 |-  ( ph -> 0 e. RR )
37 36 21 ltnled 
 |-  ( ph -> ( 0 < 1 <-> -. 1 <_ 0 ) )
38 35 37 mpbid 
 |-  ( ph -> -. 1 <_ 0 )
39 16 recnd 
 |-  ( ph -> Q e. CC )
40 39 exp1d 
 |-  ( ph -> ( Q ^ 1 ) = Q )
41 40 eqcomd 
 |-  ( ph -> Q = ( Q ^ 1 ) )
42 41 oveq2d 
 |-  ( ph -> ( Q pCnt Q ) = ( Q pCnt ( Q ^ 1 ) ) )
43 1zzd 
 |-  ( ph -> 1 e. ZZ )
44 pcid 
 |-  ( ( Q e. Prime /\ 1 e. ZZ ) -> ( Q pCnt ( Q ^ 1 ) ) = 1 )
45 4 43 44 syl2anc 
 |-  ( ph -> ( Q pCnt ( Q ^ 1 ) ) = 1 )
46 42 45 eqtrd 
 |-  ( ph -> ( Q pCnt Q ) = 1 )
47 8 adantr 
 |-  ( ( ph /\ P = Q ) -> Q || N )
48 breq1 
 |-  ( P = Q -> ( P || N <-> Q || N ) )
49 48 adantl 
 |-  ( ( ph /\ P = Q ) -> ( P || N <-> Q || N ) )
50 49 bicomd 
 |-  ( ( ph /\ P = Q ) -> ( Q || N <-> P || N ) )
51 50 biimpd 
 |-  ( ( ph /\ P = Q ) -> ( Q || N -> P || N ) )
52 47 51 mpd 
 |-  ( ( ph /\ P = Q ) -> P || N )
53 7 adantr 
 |-  ( ( ph /\ P = Q ) -> -. P || N )
54 52 53 pm2.65da 
 |-  ( ph -> -. P = Q )
55 54 neqcomd 
 |-  ( ph -> -. Q = P )
56 pcelnn 
 |-  ( ( P e. Prime /\ R e. NN ) -> ( ( P pCnt R ) e. NN <-> P || R ) )
57 3 1 56 syl2anc 
 |-  ( ph -> ( ( P pCnt R ) e. NN <-> P || R ) )
58 5 57 mpbird 
 |-  ( ph -> ( P pCnt R ) e. NN )
59 prmdvdsexpb 
 |-  ( ( Q e. Prime /\ P e. Prime /\ ( P pCnt R ) e. NN ) -> ( Q || ( P ^ ( P pCnt R ) ) <-> Q = P ) )
60 4 3 58 59 syl3anc 
 |-  ( ph -> ( Q || ( P ^ ( P pCnt R ) ) <-> Q = P ) )
61 60 notbid 
 |-  ( ph -> ( -. Q || ( P ^ ( P pCnt R ) ) <-> -. Q = P ) )
62 55 61 mpbird 
 |-  ( ph -> -. Q || ( P ^ ( P pCnt R ) ) )
63 10 12 nnexpcld 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) e. NN )
64 pceq0 
 |-  ( ( Q e. Prime /\ ( P ^ ( P pCnt R ) ) e. NN ) -> ( ( Q pCnt ( P ^ ( P pCnt R ) ) ) = 0 <-> -. Q || ( P ^ ( P pCnt R ) ) ) )
65 4 63 64 syl2anc 
 |-  ( ph -> ( ( Q pCnt ( P ^ ( P pCnt R ) ) ) = 0 <-> -. Q || ( P ^ ( P pCnt R ) ) ) )
66 62 65 mpbird 
 |-  ( ph -> ( Q pCnt ( P ^ ( P pCnt R ) ) ) = 0 )
67 46 66 breq12d 
 |-  ( ph -> ( ( Q pCnt Q ) <_ ( Q pCnt ( P ^ ( P pCnt R ) ) ) <-> 1 <_ 0 ) )
68 67 notbid 
 |-  ( ph -> ( -. ( Q pCnt Q ) <_ ( Q pCnt ( P ^ ( P pCnt R ) ) ) <-> -. 1 <_ 0 ) )
69 38 68 mpbird 
 |-  ( ph -> -. ( Q pCnt Q ) <_ ( Q pCnt ( P ^ ( P pCnt R ) ) ) )
70 69 adantr 
 |-  ( ( ph /\ p = Q ) -> -. ( Q pCnt Q ) <_ ( Q pCnt ( P ^ ( P pCnt R ) ) ) )
71 simpr 
 |-  ( ( ph /\ p = Q ) -> p = Q )
72 71 oveq1d 
 |-  ( ( ph /\ p = Q ) -> ( p pCnt Q ) = ( Q pCnt Q ) )
73 71 oveq1d 
 |-  ( ( ph /\ p = Q ) -> ( p pCnt ( P ^ ( P pCnt R ) ) ) = ( Q pCnt ( P ^ ( P pCnt R ) ) ) )
74 72 73 breq12d 
 |-  ( ( ph /\ p = Q ) -> ( ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) <-> ( Q pCnt Q ) <_ ( Q pCnt ( P ^ ( P pCnt R ) ) ) ) )
75 74 notbid 
 |-  ( ( ph /\ p = Q ) -> ( -. ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) <-> -. ( Q pCnt Q ) <_ ( Q pCnt ( P ^ ( P pCnt R ) ) ) ) )
76 70 75 mpbird 
 |-  ( ( ph /\ p = Q ) -> -. ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) )
77 76 4 rspcime 
 |-  ( ph -> E. p e. Prime -. ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) )
78 rexnal 
 |-  ( E. p e. Prime -. ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) <-> -. A. p e. Prime ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) )
79 78 a1i 
 |-  ( ph -> ( E. p e. Prime -. ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) <-> -. A. p e. Prime ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) ) )
80 77 79 mpbid 
 |-  ( ph -> -. A. p e. Prime ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) )
81 pc2dvds 
 |-  ( ( Q e. ZZ /\ ( P ^ ( P pCnt R ) ) e. ZZ ) -> ( Q || ( P ^ ( P pCnt R ) ) <-> A. p e. Prime ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) ) )
82 31 30 81 syl2anc 
 |-  ( ph -> ( Q || ( P ^ ( P pCnt R ) ) <-> A. p e. Prime ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) ) )
83 82 notbid 
 |-  ( ph -> ( -. Q || ( P ^ ( P pCnt R ) ) <-> -. A. p e. Prime ( p pCnt Q ) <_ ( p pCnt ( P ^ ( P pCnt R ) ) ) ) )
84 80 83 mpbird 
 |-  ( ph -> -. Q || ( P ^ ( P pCnt R ) ) )
85 coprm 
 |-  ( ( Q e. Prime /\ ( P ^ ( P pCnt R ) ) e. ZZ ) -> ( -. Q || ( P ^ ( P pCnt R ) ) <-> ( Q gcd ( P ^ ( P pCnt R ) ) ) = 1 ) )
86 4 30 85 syl2anc 
 |-  ( ph -> ( -. Q || ( P ^ ( P pCnt R ) ) <-> ( Q gcd ( P ^ ( P pCnt R ) ) ) = 1 ) )
87 84 86 mpbid 
 |-  ( ph -> ( Q gcd ( P ^ ( P pCnt R ) ) ) = 1 )
88 33 87 eqtrd 
 |-  ( ph -> ( ( P ^ ( P pCnt R ) ) gcd Q ) = 1 )
89 pcdvds 
 |-  ( ( P e. Prime /\ R e. NN ) -> ( P ^ ( P pCnt R ) ) || R )
90 3 1 89 syl2anc 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) || R )
91 30 31 32 88 90 6 coprmdvds2d 
 |-  ( ph -> ( ( P ^ ( P pCnt R ) ) x. Q ) || R )
92 30 31 zmulcld 
 |-  ( ph -> ( ( P ^ ( P pCnt R ) ) x. Q ) e. ZZ )
93 dvdsle 
 |-  ( ( ( ( P ^ ( P pCnt R ) ) x. Q ) e. ZZ /\ R e. NN ) -> ( ( ( P ^ ( P pCnt R ) ) x. Q ) || R -> ( ( P ^ ( P pCnt R ) ) x. Q ) <_ R ) )
94 92 1 93 syl2anc 
 |-  ( ph -> ( ( ( P ^ ( P pCnt R ) ) x. Q ) || R -> ( ( P ^ ( P pCnt R ) ) x. Q ) <_ R ) )
95 91 94 mpd 
 |-  ( ph -> ( ( P ^ ( P pCnt R ) ) x. Q ) <_ R )
96 13 17 18 28 95 ltletrd 
 |-  ( ph -> ( P ^ ( P pCnt R ) ) < R )