Metamath Proof Explorer

Theorem lcmfdvdsb

Description: Biconditional form of lcmfdvds . (Contributed by AV, 26-Aug-2020)

Ref Expression
Assertion lcmfdvdsb ( ( 𝐾 ∈ ℤ ∧ 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ↔ ( lcm ‘ 𝑍 ) ∥ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 lcmfdvds ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 → ( lcm ‘ 𝑍 ) ∥ 𝐾 ) )
2 dvdslcmf ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ∀ 𝑥 ∈ 𝑍 𝑥 ∥ ( lcm ‘ 𝑍 ) )
3 breq1 ⊢ ( 𝑥 = 𝑚 → ( 𝑥 ∥ ( lcm ‘ 𝑍 ) ↔ 𝑚 ∥ ( lcm ‘ 𝑍 ) ) )
4 3 rspcv ⊢ ( 𝑚 ∈ 𝑍 → ( ∀ 𝑥 ∈ 𝑍 𝑥 ∥ ( lcm ‘ 𝑍 ) → 𝑚 ∥ ( lcm ‘ 𝑍 ) ) )
5 ssel ⊢ ( 𝑍 ⊆ ℤ → ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ℤ ) )
6 5 adantr ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ℤ ) )
7 6 com12 ⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → 𝑚 ∈ ℤ ) )
8 7 adantr ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝐾 ∈ ℤ ) → ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → 𝑚 ∈ ℤ ) )
9 8 imp ⊢ ( ( ( 𝑚 ∈ 𝑍 ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ) → 𝑚 ∈ ℤ )
10 lcmfcl ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( lcm ‘ 𝑍 ) ∈ ℕ0 )
11 10 nn0zd ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( lcm ‘ 𝑍 ) ∈ ℤ )
12 11 adantl ⊢ ( ( ( 𝑚 ∈ 𝑍 ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ) → ( lcm ‘ 𝑍 ) ∈ ℤ )
13 simplr ⊢ ( ( ( 𝑚 ∈ 𝑍 ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ) → 𝐾 ∈ ℤ )
14 dvdstr ⊢ ( ( 𝑚 ∈ ℤ ∧ ( lcm ‘ 𝑍 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑚 ∥ ( lcm ‘ 𝑍 ) ∧ ( lcm ‘ 𝑍 ) ∥ 𝐾 ) → 𝑚 ∥ 𝐾 ) )
15 9 12 13 14 syl3anc ⊢ ( ( ( 𝑚 ∈ 𝑍 ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ) → ( ( 𝑚 ∥ ( lcm ‘ 𝑍 ) ∧ ( lcm ‘ 𝑍 ) ∥ 𝐾 ) → 𝑚 ∥ 𝐾 ) )
16 15 expd ⊢ ( ( ( 𝑚 ∈ 𝑍 ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ) → ( 𝑚 ∥ ( lcm ‘ 𝑍 ) → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → 𝑚 ∥ 𝐾 ) ) )
17 16 exp31 ⊢ ( 𝑚 ∈ 𝑍 → ( 𝐾 ∈ ℤ → ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( 𝑚 ∥ ( lcm ‘ 𝑍 ) → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → 𝑚 ∥ 𝐾 ) ) ) ) )
18 17 com23 ⊢ ( 𝑚 ∈ 𝑍 → ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( 𝐾 ∈ ℤ → ( 𝑚 ∥ ( lcm ‘ 𝑍 ) → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → 𝑚 ∥ 𝐾 ) ) ) ) )
19 18 com24 ⊢ ( 𝑚 ∈ 𝑍 → ( 𝑚 ∥ ( lcm ‘ 𝑍 ) → ( 𝐾 ∈ ℤ → ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → 𝑚 ∥ 𝐾 ) ) ) ) )
20 19 com45 ⊢ ( 𝑚 ∈ 𝑍 → ( 𝑚 ∥ ( lcm ‘ 𝑍 ) → ( 𝐾 ∈ ℤ → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → 𝑚 ∥ 𝐾 ) ) ) ) )
21 4 20 syld ⊢ ( 𝑚 ∈ 𝑍 → ( ∀ 𝑥 ∈ 𝑍 𝑥 ∥ ( lcm ‘ 𝑍 ) → ( 𝐾 ∈ ℤ → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → 𝑚 ∥ 𝐾 ) ) ) ) )
22 21 com15 ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ∀ 𝑥 ∈ 𝑍 𝑥 ∥ ( lcm ‘ 𝑍 ) → ( 𝐾 ∈ ℤ → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → ( 𝑚 ∈ 𝑍 → 𝑚 ∥ 𝐾 ) ) ) ) )
23 2 22 mpd ⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( 𝐾 ∈ ℤ → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → ( 𝑚 ∈ 𝑍 → 𝑚 ∥ 𝐾 ) ) ) )
24 23 com12 ⊢ ( 𝐾 ∈ ℤ → ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → ( 𝑚 ∈ 𝑍 → 𝑚 ∥ 𝐾 ) ) ) )
25 24 3impib ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → ( 𝑚 ∈ 𝑍 → 𝑚 ∥ 𝐾 ) ) )
26 25 ralrimdv ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ( lcm ‘ 𝑍 ) ∥ 𝐾 → ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ) )
27 1 26 impbid ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ↔ ( lcm ‘ 𝑍 ) ∥ 𝐾 ) )