Step |
Hyp |
Ref |
Expression |
1 |
|
c0ex |
⊢ 0 ∈ V |
2 |
1
|
elpr |
⊢ ( 0 ∈ { 𝑀 , 𝑁 } ↔ ( 0 = 𝑀 ∨ 0 = 𝑁 ) ) |
3 |
|
eqcom |
⊢ ( 0 = 𝑀 ↔ 𝑀 = 0 ) |
4 |
|
eqcom |
⊢ ( 0 = 𝑁 ↔ 𝑁 = 0 ) |
5 |
3 4
|
orbi12i |
⊢ ( ( 0 = 𝑀 ∨ 0 = 𝑁 ) ↔ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) |
6 |
2 5
|
bitri |
⊢ ( 0 ∈ { 𝑀 , 𝑁 } ↔ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) |
7 |
6
|
a1i |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ∈ { 𝑀 , 𝑁 } ↔ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) ) |
8 |
|
breq1 |
⊢ ( 𝑚 = 𝑀 → ( 𝑚 ∥ 𝑛 ↔ 𝑀 ∥ 𝑛 ) ) |
9 |
|
breq1 |
⊢ ( 𝑚 = 𝑁 → ( 𝑚 ∥ 𝑛 ↔ 𝑁 ∥ 𝑛 ) ) |
10 |
8 9
|
ralprg |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚 ∥ 𝑛 ↔ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) ) ) |
11 |
10
|
rabbidv |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚 ∥ 𝑛 } = { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } ) |
12 |
11
|
infeq1d |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚 ∥ 𝑛 } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) |
13 |
7 12
|
ifbieq2d |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → if ( 0 ∈ { 𝑀 , 𝑁 } , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚 ∥ 𝑛 } , ℝ , < ) ) = if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) ) |
14 |
|
prssi |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → { 𝑀 , 𝑁 } ⊆ ℤ ) |
15 |
|
prfi |
⊢ { 𝑀 , 𝑁 } ∈ Fin |
16 |
|
lcmfval |
⊢ ( ( { 𝑀 , 𝑁 } ⊆ ℤ ∧ { 𝑀 , 𝑁 } ∈ Fin ) → ( lcm ‘ { 𝑀 , 𝑁 } ) = if ( 0 ∈ { 𝑀 , 𝑁 } , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚 ∥ 𝑛 } , ℝ , < ) ) ) |
17 |
14 15 16
|
sylancl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( lcm ‘ { 𝑀 , 𝑁 } ) = if ( 0 ∈ { 𝑀 , 𝑁 } , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚 ∥ 𝑛 } , ℝ , < ) ) ) |
18 |
|
lcmval |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) = if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) ) |
19 |
13 17 18
|
3eqtr4d |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( lcm ‘ { 𝑀 , 𝑁 } ) = ( 𝑀 lcm 𝑁 ) ) |