This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prmfac1

Description: The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014)

Ref Expression
Assertion prmfac1 ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( ! ‘ 𝑁 ) ) → 𝑃 ≤ 𝑁 )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑥 = 0 → ( ! ‘ 𝑥 ) = ( ! ‘ 0 ) )
2 1 breq2d ⊢ ( 𝑥 = 0 → ( 𝑃 ∥ ( ! ‘ 𝑥 ) ↔ 𝑃 ∥ ( ! ‘ 0 ) ) )
3 breq2 ⊢ ( 𝑥 = 0 → ( 𝑃 ≤ 𝑥 ↔ 𝑃 ≤ 0 ) )
4 2 3 imbi12d ⊢ ( 𝑥 = 0 → ( ( 𝑃 ∥ ( ! ‘ 𝑥 ) → 𝑃 ≤ 𝑥 ) ↔ ( 𝑃 ∥ ( ! ‘ 0 ) → 𝑃 ≤ 0 ) ) )
5 4 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 𝑥 ) → 𝑃 ≤ 𝑥 ) ) ↔ ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 0 ) → 𝑃 ≤ 0 ) ) ) )
6 fveq2 ⊢ ( 𝑥 = 𝑘 → ( ! ‘ 𝑥 ) = ( ! ‘ 𝑘 ) )
7 6 breq2d ⊢ ( 𝑥 = 𝑘 → ( 𝑃 ∥ ( ! ‘ 𝑥 ) ↔ 𝑃 ∥ ( ! ‘ 𝑘 ) ) )
8 breq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑃 ≤ 𝑥 ↔ 𝑃 ≤ 𝑘 ) )
9 7 8 imbi12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑃 ∥ ( ! ‘ 𝑥 ) → 𝑃 ≤ 𝑥 ) ↔ ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ 𝑘 ) ) )
10 9 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 𝑥 ) → 𝑃 ≤ 𝑥 ) ) ↔ ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ 𝑘 ) ) ) )
11 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ! ‘ 𝑥 ) = ( ! ‘ ( 𝑘 + 1 ) ) )
12 11 breq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑃 ∥ ( ! ‘ 𝑥 ) ↔ 𝑃 ∥ ( ! ‘ ( 𝑘 + 1 ) ) ) )
13 breq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑃 ≤ 𝑥 ↔ 𝑃 ≤ ( 𝑘 + 1 ) ) )
14 12 13 imbi12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑃 ∥ ( ! ‘ 𝑥 ) → 𝑃 ≤ 𝑥 ) ↔ ( 𝑃 ∥ ( ! ‘ ( 𝑘 + 1 ) ) → 𝑃 ≤ ( 𝑘 + 1 ) ) ) )
15 14 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 𝑥 ) → 𝑃 ≤ 𝑥 ) ) ↔ ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ ( 𝑘 + 1 ) ) → 𝑃 ≤ ( 𝑘 + 1 ) ) ) ) )
16 fveq2 ⊢ ( 𝑥 = 𝑁 → ( ! ‘ 𝑥 ) = ( ! ‘ 𝑁 ) )
17 16 breq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑃 ∥ ( ! ‘ 𝑥 ) ↔ 𝑃 ∥ ( ! ‘ 𝑁 ) ) )
18 breq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑃 ≤ 𝑥 ↔ 𝑃 ≤ 𝑁 ) )
19 17 18 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑃 ∥ ( ! ‘ 𝑥 ) → 𝑃 ≤ 𝑥 ) ↔ ( 𝑃 ∥ ( ! ‘ 𝑁 ) → 𝑃 ≤ 𝑁 ) ) )
20 19 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 𝑥 ) → 𝑃 ≤ 𝑥 ) ) ↔ ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 𝑁 ) → 𝑃 ≤ 𝑁 ) ) ) )
21 fac0 ⊢ ( ! ‘ 0 ) = 1
22 21 breq2i ⊢ ( 𝑃 ∥ ( ! ‘ 0 ) ↔ 𝑃 ∥ 1 )
23 nprmdvds1 ⊢ ( 𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1 )
24 23 pm2.21d ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∥ 1 → 𝑃 ≤ 0 ) )
25 22 24 biimtrid ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 0 ) → 𝑃 ≤ 0 ) )
26 facp1 ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
27 26 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
28 27 breq2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ∥ ( ! ‘ ( 𝑘 + 1 ) ) ↔ 𝑃 ∥ ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ) )
29 simpr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℙ )
30 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
31 30 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( ! ‘ 𝑘 ) ∈ ℕ )
32 31 nnzd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( ! ‘ 𝑘 ) ∈ ℤ )
33 nn0p1nn ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ )
34 33 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑘 + 1 ) ∈ ℕ )
35 34 nnzd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑘 + 1 ) ∈ ℤ )
36 euclemma ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ 𝑘 ) ∈ ℤ ∧ ( 𝑘 + 1 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ↔ ( 𝑃 ∥ ( ! ‘ 𝑘 ) ∨ 𝑃 ∥ ( 𝑘 + 1 ) ) ) )
37 29 32 35 36 syl3anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ∥ ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ↔ ( 𝑃 ∥ ( ! ‘ 𝑘 ) ∨ 𝑃 ∥ ( 𝑘 + 1 ) ) ) )
38 28 37 bitrd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ∥ ( ! ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ∥ ( ! ‘ 𝑘 ) ∨ 𝑃 ∥ ( 𝑘 + 1 ) ) ) )
39 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
40 39 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → 𝑘 ∈ ℝ )
41 40 lep1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → 𝑘 ≤ ( 𝑘 + 1 ) )
42 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
43 42 adantl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℤ )
44 43 zred ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℝ )
45 34 nnred ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑘 + 1 ) ∈ ℝ )
46 letr ⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( ( 𝑃 ≤ 𝑘 ∧ 𝑘 ≤ ( 𝑘 + 1 ) ) → 𝑃 ≤ ( 𝑘 + 1 ) ) )
47 44 40 45 46 syl3anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( ( 𝑃 ≤ 𝑘 ∧ 𝑘 ≤ ( 𝑘 + 1 ) ) → 𝑃 ≤ ( 𝑘 + 1 ) ) )
48 41 47 mpan2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ≤ 𝑘 → 𝑃 ≤ ( 𝑘 + 1 ) ) )
49 48 imim2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ 𝑘 ) → ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ ( 𝑘 + 1 ) ) ) )
50 49 com23 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ∥ ( ! ‘ 𝑘 ) → ( ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ 𝑘 ) → 𝑃 ≤ ( 𝑘 + 1 ) ) ) )
51 dvdsle ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝑃 ∥ ( 𝑘 + 1 ) → 𝑃 ≤ ( 𝑘 + 1 ) ) )
52 43 34 51 syl2anc ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ∥ ( 𝑘 + 1 ) → 𝑃 ≤ ( 𝑘 + 1 ) ) )
53 52 a1dd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ∥ ( 𝑘 + 1 ) → ( ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ 𝑘 ) → 𝑃 ≤ ( 𝑘 + 1 ) ) ) )
54 50 53 jaod ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( ( 𝑃 ∥ ( ! ‘ 𝑘 ) ∨ 𝑃 ∥ ( 𝑘 + 1 ) ) → ( ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ 𝑘 ) → 𝑃 ≤ ( 𝑘 + 1 ) ) ) )
55 38 54 sylbid ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ∥ ( ! ‘ ( 𝑘 + 1 ) ) → ( ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ 𝑘 ) → 𝑃 ≤ ( 𝑘 + 1 ) ) ) )
56 55 com23 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ) → ( ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ 𝑘 ) → ( 𝑃 ∥ ( ! ‘ ( 𝑘 + 1 ) ) → 𝑃 ≤ ( 𝑘 + 1 ) ) ) )
57 56 ex ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑃 ∈ ℙ → ( ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ 𝑘 ) → ( 𝑃 ∥ ( ! ‘ ( 𝑘 + 1 ) ) → 𝑃 ≤ ( 𝑘 + 1 ) ) ) ) )
58 57 a2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 𝑘 ) → 𝑃 ≤ 𝑘 ) ) → ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ ( 𝑘 + 1 ) ) → 𝑃 ≤ ( 𝑘 + 1 ) ) ) ) )
59 5 10 15 20 25 58 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑃 ∈ ℙ → ( 𝑃 ∥ ( ! ‘ 𝑁 ) → 𝑃 ≤ 𝑁 ) ) )
60 59 3imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( ! ‘ 𝑁 ) ) → 𝑃 ≤ 𝑁 )