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 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks4d1p8d2.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks4d1p8d2.3 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks4d1p8d2.4 ⊢ ( 𝜑 → 𝑄 ∈ ℙ )
aks4d1p8d2.5 ⊢ ( 𝜑 → 𝑃 ∥ 𝑅 )
aks4d1p8d2.6 ⊢ ( 𝜑 → 𝑄 ∥ 𝑅 )
aks4d1p8d2.7 ⊢ ( 𝜑 → ¬ 𝑃 ∥ 𝑁 )
aks4d1p8d2.8 ⊢ ( 𝜑 → 𝑄 ∥ 𝑁 )
Assertion aks4d1p8d2 ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) < 𝑅 )

Proof

Step Hyp Ref Expression
1 aks4d1p8d2.1 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2 aks4d1p8d2.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 aks4d1p8d2.3 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
4 aks4d1p8d2.4 ⊢ ( 𝜑 → 𝑄 ∈ ℙ )
5 aks4d1p8d2.5 ⊢ ( 𝜑 → 𝑃 ∥ 𝑅 )
6 aks4d1p8d2.6 ⊢ ( 𝜑 → 𝑄 ∥ 𝑅 )
7 aks4d1p8d2.7 ⊢ ( 𝜑 → ¬ 𝑃 ∥ 𝑁 )
8 aks4d1p8d2.8 ⊢ ( 𝜑 → 𝑄 ∥ 𝑁 )
9 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
10 3 9 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
11 10 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
12 3 1 pccld ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑅 ) ∈ ℕ0 )
13 11 12 reexpcld ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℝ )
14 prmnn ⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℕ )
15 4 14 syl ⊢ ( 𝜑 → 𝑄 ∈ ℕ )
16 15 nnred ⊢ ( 𝜑 → 𝑄 ∈ ℝ )
17 13 16 remulcld ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) ∈ ℝ )
18 1 nnred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
19 13 recnd ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℂ )
20 19 mulid1d ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 1 ) = ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) )
21 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
22 10 nnrpd ⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
23 12 nn0zd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑅 ) ∈ ℤ )
24 22 23 rpexpcld ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℝ+ )
25 prmgt1 ⊢ ( 𝑄 ∈ ℙ → 1 < 𝑄 )
26 4 25 syl ⊢ ( 𝜑 → 1 < 𝑄 )
27 21 16 24 26 ltmul2dd ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 1 ) < ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) )
28 20 27 eqbrtrrd ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) < ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) )
29 10 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
30 29 12 zexpcld ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℤ )
31 15 nnzd ⊢ ( 𝜑 → 𝑄 ∈ ℤ )
32 1 nnzd ⊢ ( 𝜑 → 𝑅 ∈ ℤ )
33 30 31 gcdcomd ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) gcd 𝑄 ) = ( 𝑄 gcd ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) )
34 0lt1 ⊢ 0 < 1
35 34 a1i ⊢ ( 𝜑 → 0 < 1 )
36 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
37 36 21 ltnled ⊢ ( 𝜑 → ( 0 < 1 ↔ ¬ 1 ≤ 0 ) )
38 35 37 mpbid ⊢ ( 𝜑 → ¬ 1 ≤ 0 )
39 16 recnd ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
40 39 exp1d ⊢ ( 𝜑 → ( 𝑄 ↑ 1 ) = 𝑄 )
41 40 eqcomd ⊢ ( 𝜑 → 𝑄 = ( 𝑄 ↑ 1 ) )
42 41 oveq2d ⊢ ( 𝜑 → ( 𝑄 pCnt 𝑄 ) = ( 𝑄 pCnt ( 𝑄 ↑ 1 ) ) )
43 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
44 pcid ⊢ ( ( 𝑄 ∈ ℙ ∧ 1 ∈ ℤ ) → ( 𝑄 pCnt ( 𝑄 ↑ 1 ) ) = 1 )
45 4 43 44 syl2anc ⊢ ( 𝜑 → ( 𝑄 pCnt ( 𝑄 ↑ 1 ) ) = 1 )
46 42 45 eqtrd ⊢ ( 𝜑 → ( 𝑄 pCnt 𝑄 ) = 1 )
47 8 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → 𝑄 ∥ 𝑁 )
48 breq1 ⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∥ 𝑁 ↔ 𝑄 ∥ 𝑁 ) )
49 48 adantl ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( 𝑃 ∥ 𝑁 ↔ 𝑄 ∥ 𝑁 ) )
50 49 bicomd ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( 𝑄 ∥ 𝑁 ↔ 𝑃 ∥ 𝑁 ) )
51 50 biimpd ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( 𝑄 ∥ 𝑁 → 𝑃 ∥ 𝑁 ) )
52 47 51 mpd ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → 𝑃 ∥ 𝑁 )
53 7 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ¬ 𝑃 ∥ 𝑁 )
54 52 53 pm2.65da ⊢ ( 𝜑 → ¬ 𝑃 = 𝑄 )
55 54 neqcomd ⊢ ( 𝜑 → ¬ 𝑄 = 𝑃 )
56 pcelnn ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℕ ) → ( ( 𝑃 pCnt 𝑅 ) ∈ ℕ ↔ 𝑃 ∥ 𝑅 ) )
57 3 1 56 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝑅 ) ∈ ℕ ↔ 𝑃 ∥ 𝑅 ) )
58 5 57 mpbird ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑅 ) ∈ ℕ )
59 prmdvdsexpb ⊢ ( ( 𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ ( 𝑃 pCnt 𝑅 ) ∈ ℕ ) → ( 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ↔ 𝑄 = 𝑃 ) )
60 4 3 58 59 syl3anc ⊢ ( 𝜑 → ( 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ↔ 𝑄 = 𝑃 ) )
61 60 notbid ⊢ ( 𝜑 → ( ¬ 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ↔ ¬ 𝑄 = 𝑃 ) )
62 55 61 mpbird ⊢ ( 𝜑 → ¬ 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) )
63 10 12 nnexpcld ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℕ )
64 pceq0 ⊢ ( ( 𝑄 ∈ ℙ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℕ ) → ( ( 𝑄 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) = 0 ↔ ¬ 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) )
65 4 63 64 syl2anc ⊢ ( 𝜑 → ( ( 𝑄 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) = 0 ↔ ¬ 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) )
66 62 65 mpbird ⊢ ( 𝜑 → ( 𝑄 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) = 0 )
67 46 66 breq12d ⊢ ( 𝜑 → ( ( 𝑄 pCnt 𝑄 ) ≤ ( 𝑄 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ↔ 1 ≤ 0 ) )
68 67 notbid ⊢ ( 𝜑 → ( ¬ ( 𝑄 pCnt 𝑄 ) ≤ ( 𝑄 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ↔ ¬ 1 ≤ 0 ) )
69 38 68 mpbird ⊢ ( 𝜑 → ¬ ( 𝑄 pCnt 𝑄 ) ≤ ( 𝑄 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑝 = 𝑄 ) → ¬ ( 𝑄 pCnt 𝑄 ) ≤ ( 𝑄 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑝 = 𝑄 ) → 𝑝 = 𝑄 )
72 71 oveq1d ⊢ ( ( 𝜑 ∧ 𝑝 = 𝑄 ) → ( 𝑝 pCnt 𝑄 ) = ( 𝑄 pCnt 𝑄 ) )
73 71 oveq1d ⊢ ( ( 𝜑 ∧ 𝑝 = 𝑄 ) → ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) = ( 𝑄 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) )
74 72 73 breq12d ⊢ ( ( 𝜑 ∧ 𝑝 = 𝑄 ) → ( ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ↔ ( 𝑄 pCnt 𝑄 ) ≤ ( 𝑄 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ) )
75 74 notbid ⊢ ( ( 𝜑 ∧ 𝑝 = 𝑄 ) → ( ¬ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ↔ ¬ ( 𝑄 pCnt 𝑄 ) ≤ ( 𝑄 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ) )
76 70 75 mpbird ⊢ ( ( 𝜑 ∧ 𝑝 = 𝑄 ) → ¬ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) )
77 76 4 rspcime ⊢ ( 𝜑 → ∃ 𝑝 ∈ ℙ ¬ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) )
78 rexnal ⊢ ( ∃ 𝑝 ∈ ℙ ¬ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ↔ ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) )
79 78 a1i ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ℙ ¬ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ↔ ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ) )
80 77 79 mpbid ⊢ ( 𝜑 → ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) )
81 pc2dvds ⊢ ( ( 𝑄 ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℤ ) → ( 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ) )
82 31 30 81 syl2anc ⊢ ( 𝜑 → ( 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ) )
83 82 notbid ⊢ ( 𝜑 → ( ¬ 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ↔ ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝑄 ) ≤ ( 𝑝 pCnt ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) ) )
84 80 83 mpbird ⊢ ( 𝜑 → ¬ 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) )
85 coprm ⊢ ( ( 𝑄 ∈ ℙ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∈ ℤ ) → ( ¬ 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ↔ ( 𝑄 gcd ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) = 1 ) )
86 4 30 85 syl2anc ⊢ ( 𝜑 → ( ¬ 𝑄 ∥ ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ↔ ( 𝑄 gcd ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) = 1 ) )
87 84 86 mpbid ⊢ ( 𝜑 → ( 𝑄 gcd ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ) = 1 )
88 33 87 eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) gcd 𝑄 ) = 1 )
89 pcdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∥ 𝑅 )
90 3 1 89 syl2anc ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) ∥ 𝑅 )
91 30 31 32 88 90 6 coprmdvds2d ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) ∥ 𝑅 )
92 30 31 zmulcld ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) ∈ ℤ )
93 dvdsle ⊢ ( ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) ∈ ℤ ∧ 𝑅 ∈ ℕ ) → ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) ∥ 𝑅 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) ≤ 𝑅 ) )
94 92 1 93 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) ∥ 𝑅 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) ≤ 𝑅 ) )
95 91 94 mpd ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) · 𝑄 ) ≤ 𝑅 )
96 13 17 18 28 95 ltletrd ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑅 ) ) < 𝑅 )