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

Metamath Proof Explorer

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 0fi 
 |-  (/) 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