Theorem lcmf0

Description: The least common multiple of the empty set is 1. (Contributed by AV, 22-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

	Ref	Expression
Assertion	lcmf0	|- ( _lcm ` (/) ) = 1

Proof

Step	Hyp	Ref	Expression
1		0ss	|- (/) C_ ZZ
2		0fin	|- (/) e. Fin
3		noel	|- -. 0 e. (/)
4	3	nelir	|- 0 e/ (/)
5		lcmfn0val	|- ( ( (/) C_ ZZ /\ (/) e. Fin /\ 0 e/ (/) ) -> ( _lcm ` (/) ) = inf ( { n e. NN | A. m e. (/) m || n } , RR , < ) )
6	1 2 4 5	mp3an	|- ( _lcm ` (/) ) = inf ( { n e. NN | A. m e. (/) m || n } , RR , < )
7		ral0	|- A. m e. (/) m || n
8	7	rgenw	|- A. n e. NN A. m e. (/) m || n
9		rabid2	|- ( NN = { n e. NN | A. m e. (/) m || n } <-> A. n e. NN A. m e. (/) m || n )
10	8 9	mpbir	|- NN = { n e. NN | A. m e. (/) m || n }
11	10	eqcomi	|- { n e. NN | A. m e. (/) m || n } = NN
12	11	infeq1i	|- inf ( { n e. NN | A. m e. (/) m || n } , RR , < ) = inf ( NN , RR , < )
13		nninf	|- inf ( NN , RR , < ) = 1
14	6 12 13	3eqtri	|- ( _lcm ` (/) ) = 1