Theorem lcmfnnval

Description: The value of the _lcm function for a subset of the positive integers. (Contributed by AV, 21-Aug-2020) (Revised by AV, 16-Sep-2020)

	Ref	Expression
Assertion	lcmfnnval	|- ( ( Z C_ NN /\ Z e. Fin ) -> ( _lcm ` Z ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( Z C_ NN -> Z C_ NN )
2		nnssz	|- NN C_ ZZ
3	1 2	sstrdi	|- ( Z C_ NN -> Z C_ ZZ )
4	3	adantr	|- ( ( Z C_ NN /\ Z e. Fin ) -> Z C_ ZZ )
5		simpr	|- ( ( Z C_ NN /\ Z e. Fin ) -> Z e. Fin )
6		0nnn	|- -. 0 e. NN
7	6	nelir	|- 0 e/ NN
8		ssel	|- ( Z C_ NN -> ( 0 e. Z -> 0 e. NN ) )
9	8	nelcon3d	|- ( Z C_ NN -> ( 0 e/ NN -> 0 e/ Z ) )
10	7 9	mpi	|- ( Z C_ NN -> 0 e/ Z )
11	10	adantr	|- ( ( Z C_ NN /\ Z e. Fin ) -> 0 e/ Z )
12		lcmfn0val	|- ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )
13	4 5 11 12	syl3anc	|- ( ( Z C_ NN /\ Z e. Fin ) -> ( _lcm ` Z ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )