Metamath Proof Explorer

Theorem pclem

Description: - Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Hypothesis pclem.1 ⊢ 𝐴 = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
Assertion pclem ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 pclem.1 ⊢ 𝐴 = { 𝑛 ∈ ℕ0 ∣ ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 }
2 1 ssrab3 ⊢ 𝐴 ⊆ ℕ0
3 nn0ssz ⊢ ℕ0 ⊆ ℤ
4 2 3 sstri ⊢ 𝐴 ⊆ ℤ
5 4 a1i ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝐴 ⊆ ℤ )
6 0nn0 ⊢ 0 ∈ ℕ0
7 6 a1i ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 0 ∈ ℕ0 )
8 eluzelcn ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℂ )
9 8 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑃 ∈ ℂ )
10 9 exp0d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 0 ) = 1 )
11 1dvds ⊢ ( 𝑁 ∈ ℤ → 1 ∥ 𝑁 )
12 11 ad2antrl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 1 ∥ 𝑁 )
13 10 12 eqbrtrd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑃 ↑ 0 ) ∥ 𝑁 )
14 oveq2 ⊢ ( 𝑛 = 0 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 0 ) )
15 14 breq1d ⊢ ( 𝑛 = 0 → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 ↔ ( 𝑃 ↑ 0 ) ∥ 𝑁 ) )
16 15 1 elrab2 ⊢ ( 0 ∈ 𝐴 ↔ ( 0 ∈ ℕ0 ∧ ( 𝑃 ↑ 0 ) ∥ 𝑁 ) )
17 7 13 16 sylanbrc ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 0 ∈ 𝐴 )
18 17 ne0d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝐴 ≠ ∅ )
19 nnssz ⊢ ℕ ⊆ ℤ
20 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
21 20 abscld ⊢ ( 𝑁 ∈ ℤ → ( abs ‘ 𝑁 ) ∈ ℝ )
22 21 ad2antrl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( abs ‘ 𝑁 ) ∈ ℝ )
23 eluzelre ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℝ )
24 23 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 𝑃 ∈ ℝ )
25 eluz2gt1 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑃 )
26 25 adantr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → 1 < 𝑃 )
27 expnbnd ⊢ ( ( ( abs ‘ 𝑁 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ∃ 𝑥 ∈ ℕ ( abs ‘ 𝑁 ) < ( 𝑃 ↑ 𝑥 ) )
28 22 24 26 27 syl3anc ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ∃ 𝑥 ∈ ℕ ( abs ‘ 𝑁 ) < ( 𝑃 ↑ 𝑥 ) )
29 simprr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
30 oveq2 ⊢ ( 𝑛 = 𝑦 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑦 ) )
31 30 breq1d ⊢ ( 𝑛 = 𝑦 → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝑁 ↔ ( 𝑃 ↑ 𝑦 ) ∥ 𝑁 ) )
32 31 1 elrab2 ⊢ ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑦 ) ∥ 𝑁 ) )
33 29 32 sylib ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑦 ∈ ℕ0 ∧ ( 𝑃 ↑ 𝑦 ) ∥ 𝑁 ) )
34 33 simprd ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑃 ↑ 𝑦 ) ∥ 𝑁 )
35 eluz2nn ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℕ )
36 35 ad2antrr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑃 ∈ ℕ )
37 33 simpld ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ ℕ0 )
38 36 37 nnexpcld ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑃 ↑ 𝑦 ) ∈ ℕ )
39 38 nnzd ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑃 ↑ 𝑦 ) ∈ ℤ )
40 simplrl ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑁 ∈ ℤ )
41 simplrr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑁 ≠ 0 )
42 dvdsleabs ⊢ ( ( ( 𝑃 ↑ 𝑦 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( ( 𝑃 ↑ 𝑦 ) ∥ 𝑁 → ( 𝑃 ↑ 𝑦 ) ≤ ( abs ‘ 𝑁 ) ) )
43 39 40 41 42 syl3anc ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑃 ↑ 𝑦 ) ∥ 𝑁 → ( 𝑃 ↑ 𝑦 ) ≤ ( abs ‘ 𝑁 ) ) )
44 34 43 mpd ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑃 ↑ 𝑦 ) ≤ ( abs ‘ 𝑁 ) )
45 38 nnred ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑃 ↑ 𝑦 ) ∈ ℝ )
46 22 adantr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( abs ‘ 𝑁 ) ∈ ℝ )
47 23 ad2antrr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑃 ∈ ℝ )
48 nnnn0 ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ0 )
49 48 ad2antrl ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ ℕ0 )
50 47 49 reexpcld ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑃 ↑ 𝑥 ) ∈ ℝ )
51 lelttr ⊢ ( ( ( 𝑃 ↑ 𝑦 ) ∈ ℝ ∧ ( abs ‘ 𝑁 ) ∈ ℝ ∧ ( 𝑃 ↑ 𝑥 ) ∈ ℝ ) → ( ( ( 𝑃 ↑ 𝑦 ) ≤ ( abs ‘ 𝑁 ) ∧ ( abs ‘ 𝑁 ) < ( 𝑃 ↑ 𝑥 ) ) → ( 𝑃 ↑ 𝑦 ) < ( 𝑃 ↑ 𝑥 ) ) )
52 45 46 50 51 syl3anc ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝑃 ↑ 𝑦 ) ≤ ( abs ‘ 𝑁 ) ∧ ( abs ‘ 𝑁 ) < ( 𝑃 ↑ 𝑥 ) ) → ( 𝑃 ↑ 𝑦 ) < ( 𝑃 ↑ 𝑥 ) ) )
53 44 52 mpand ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( ( abs ‘ 𝑁 ) < ( 𝑃 ↑ 𝑥 ) → ( 𝑃 ↑ 𝑦 ) < ( 𝑃 ↑ 𝑥 ) ) )
54 37 nn0zd ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ ℤ )
55 nnz ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℤ )
56 55 ad2antrl ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ ℤ )
57 25 ad2antrr ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 1 < 𝑃 )
58 47 54 56 57 ltexp2d ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑦 < 𝑥 ↔ ( 𝑃 ↑ 𝑦 ) < ( 𝑃 ↑ 𝑥 ) ) )
59 53 58 sylibrd ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( ( abs ‘ 𝑁 ) < ( 𝑃 ↑ 𝑥 ) → 𝑦 < 𝑥 ) )
60 37 nn0red ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ ℝ )
61 nnre ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ )
62 61 ad2antrl ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ ℝ )
63 ltle ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 < 𝑥 → 𝑦 ≤ 𝑥 ) )
64 60 62 63 syl2anc ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑦 < 𝑥 → 𝑦 ≤ 𝑥 ) )
65 59 64 syld ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( ( abs ‘ 𝑁 ) < ( 𝑃 ↑ 𝑥 ) → 𝑦 ≤ 𝑥 ) )
66 65 anassrs ⊢ ( ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → ( ( abs ‘ 𝑁 ) < ( 𝑃 ↑ 𝑥 ) → 𝑦 ≤ 𝑥 ) )
67 66 ralrimdva ⊢ ( ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) ∧ 𝑥 ∈ ℕ ) → ( ( abs ‘ 𝑁 ) < ( 𝑃 ↑ 𝑥 ) → ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
68 67 reximdva ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( ∃ 𝑥 ∈ ℕ ( abs ‘ 𝑁 ) < ( 𝑃 ↑ 𝑥 ) → ∃ 𝑥 ∈ ℕ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
69 28 68 mpd ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ∃ 𝑥 ∈ ℕ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
70 ssrexv ⊢ ( ℕ ⊆ ℤ → ( ∃ 𝑥 ∈ ℕ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
71 19 69 70 mpsyl ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
72 5 18 71 3jca ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )