Metamath Proof Explorer

Theorem etransclem10

Description: The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem10.n ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem10.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
etransclem10.c ⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
etransclem10.j ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
Assertion etransclem10 ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 etransclem10.n ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2 etransclem10.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3 etransclem10.c ⊢ ( 𝜑 → 𝐶 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
4 etransclem10.j ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
5 0zd ⊢ ( ( 𝜑 ∧ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → 0 ∈ ℤ )
6 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
7 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
8 1 7 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
9 8 nn0zd ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℤ )
10 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
11 2 10 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
12 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
13 11 12 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
14 3 13 ffvelrnd ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ( 0 ... 𝑁 ) )
15 14 elfzelzd ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ℤ )
16 9 15 zsubcld ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℤ )
17 6 9 16 3jca ⊢ ( 𝜑 → ( 0 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℤ ) )
18 17 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 0 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℤ ) )
19 15 zred ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ ℝ )
20 19 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝐶 ‘ 0 ) ∈ ℝ )
21 8 nn0red ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ )
22 21 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝑃 − 1 ) ∈ ℝ )
23 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) )
24 20 22 23 nltled ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝐶 ‘ 0 ) ≤ ( 𝑃 − 1 ) )
25 22 20 subge0d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 0 ≤ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ↔ ( 𝐶 ‘ 0 ) ≤ ( 𝑃 − 1 ) ) )
26 24 25 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → 0 ≤ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) )
27 elfzle1 ⊢ ( ( 𝐶 ‘ 0 ) ∈ ( 0 ... 𝑁 ) → 0 ≤ ( 𝐶 ‘ 0 ) )
28 14 27 syl ⊢ ( 𝜑 → 0 ≤ ( 𝐶 ‘ 0 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → 0 ≤ ( 𝐶 ‘ 0 ) )
30 22 20 subge02d ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 0 ≤ ( 𝐶 ‘ 0 ) ↔ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ≤ ( 𝑃 − 1 ) ) )
31 29 30 mpbid ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ≤ ( 𝑃 − 1 ) )
32 18 26 31 jca32 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( 0 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℤ ) ∧ ( 0 ≤ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∧ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ≤ ( 𝑃 − 1 ) ) ) )
33 elfz2 ⊢ ( ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ( 0 ... ( 𝑃 − 1 ) ) ↔ ( ( 0 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℤ ) ∧ ( 0 ≤ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∧ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ≤ ( 𝑃 − 1 ) ) ) )
34 32 33 sylibr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ( 0 ... ( 𝑃 − 1 ) ) )
35 permnn ⊢ ( ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ( 0 ... ( 𝑃 − 1 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ∈ ℕ )
36 34 35 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ∈ ℕ )
37 36 nnzd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ∈ ℤ )
38 4 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → 𝐽 ∈ ℤ )
39 16 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℤ )
40 elnn0z ⊢ ( ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℕ0 ↔ ( ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℤ ∧ 0 ≤ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) )
41 39 26 40 sylanbrc ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℕ0 )
42 zexpcl ⊢ ( ( 𝐽 ∈ ℤ ∧ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ∈ ℕ0 ) → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ∈ ℤ )
43 38 41 42 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ∈ ℤ )
44 37 43 zmulcld ⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) ) → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ∈ ℤ )
45 5 44 ifclda ⊢ ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐶 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐶 ‘ 0 ) ) ) ) ) ∈ ℤ )