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	ffvelcdmd	⊢ ( 𝜑 → ( 𝐶 ‘ 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 ) ) ) ) ) ∈ ℤ )