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

Metamath Proof Explorer

Theorem prmolefac

Description: The primorial of a positive integer is less than or equal to the factorial of the integer. (Contributed by AV, 15-Aug-2020) (Revised by AV, 29-Aug-2020)

Ref Expression
Assertion prmolefac ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ≤ ( ! ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑘 𝑁 ∈ ℕ0
2 fzfid ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ∈ Fin )
3 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
4 3 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
5 1nn ⊢ 1 ∈ ℕ
6 5 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℕ )
7 4 6 ifcld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℕ )
8 7 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℝ )
9 ifeqor ⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 ∨ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 )
10 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
11 10 nn0ge0d ⊢ ( 𝑘 ∈ ℕ → 0 ≤ 𝑘 )
12 3 11 syl ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 0 ≤ 𝑘 )
13 12 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ 𝑘 )
14 breq2 ⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 → ( 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ↔ 0 ≤ 𝑘 ) )
15 13 14 imbitrrid ⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) )
16 0le1 ⊢ 0 ≤ 1
17 breq2 ⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 → ( 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ↔ 0 ≤ 1 ) )
18 17 adantr ⊢ ( ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ) → ( 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ↔ 0 ≤ 1 ) )
19 16 18 mpbiri ⊢ ( ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
20 19 ex ⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) )
21 15 20 jaoi ⊢ ( ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 ∨ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) )
22 9 21 ax-mp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
23 4 nnred ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℝ )
24 23 leidd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ≤ 𝑘 )
25 breq1 ⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 → ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 ↔ 𝑘 ≤ 𝑘 ) )
26 24 25 imbitrrid ⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 ) )
27 4 nnge1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 1 ≤ 𝑘 )
28 breq1 ⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 → ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 ↔ 1 ≤ 𝑘 ) )
29 27 28 imbitrrid ⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 ) )
30 26 29 jaoi ⊢ ( ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 ∨ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 ) )
31 9 30 ax-mp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 )
32 1 2 8 22 23 31 fprodle ⊢ ( 𝑁 ∈ ℕ0 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ ∏ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 )
33 prmoval ⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
34 fprodfac ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 )
35 32 33 34 3brtr4d ⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ≤ ( ! ‘ 𝑁 ) )