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 ⊢ N ∈ ℕ 0 ∧ P ∈ ℙ ∧ P ∥ N ! → P ≤ N

Proof

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