ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lcmgcdlem GIF version

Theorem lcmgcdlem 11604
Description: Lemma for lcmgcd 11605 and lcmdvds 11606. Prove them for positive 𝑀, 𝑁, and 𝐾. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.)
Assertion
Ref Expression
lcmgcdlem ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁)) = (abs‘(𝑀 · 𝑁)) ∧ ((𝐾 ∈ ℕ ∧ (𝑀𝐾𝑁𝐾)) → (𝑀 lcm 𝑁) ∥ 𝐾)))

Proof of Theorem lcmgcdlem
Dummy variables 𝑛 𝑓 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnmulcl 8651 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) ∈ ℕ)
21nnred 8643 . . . 4 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) ∈ ℝ)
3 nnz 8977 . . . . . . 7 (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
43adantr 272 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℤ)
54zred 9077 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℝ)
6 nnz 8977 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
76adantl 273 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ)
87zred 9077 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
9 0red 7691 . . . . . . 7 (𝑀 ∈ ℕ → 0 ∈ ℝ)
10 nnre 8637 . . . . . . 7 (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
11 nngt0 8655 . . . . . . 7 (𝑀 ∈ ℕ → 0 < 𝑀)
129, 10, 11ltled 7804 . . . . . 6 (𝑀 ∈ ℕ → 0 ≤ 𝑀)
1312adantr 272 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤ 𝑀)
14 0red 7691 . . . . . . 7 (𝑁 ∈ ℕ → 0 ∈ ℝ)
15 nnre 8637 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
16 nngt0 8655 . . . . . . 7 (𝑁 ∈ ℕ → 0 < 𝑁)
1714, 15, 16ltled 7804 . . . . . 6 (𝑁 ∈ ℕ → 0 ≤ 𝑁)
1817adantl 273 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤ 𝑁)
195, 8, 13, 18mulge0d 8301 . . . 4 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤ (𝑀 · 𝑁))
202, 19absidd 10831 . . 3 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (abs‘(𝑀 · 𝑁)) = (𝑀 · 𝑁))
213, 6anim12i 334 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
22 nnne0 8658 . . . . . . . . 9 (𝑀 ∈ ℕ → 𝑀 ≠ 0)
2322neneqd 2303 . . . . . . . 8 (𝑀 ∈ ℕ → ¬ 𝑀 = 0)
24 nnne0 8658 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
2524neneqd 2303 . . . . . . . 8 (𝑁 ∈ ℕ → ¬ 𝑁 = 0)
2623, 25anim12i 334 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (¬ 𝑀 = 0 ∧ ¬ 𝑁 = 0))
27 ioran 724 . . . . . . 7 (¬ (𝑀 = 0 ∨ 𝑁 = 0) ↔ (¬ 𝑀 = 0 ∧ ¬ 𝑁 = 0))
2826, 27sylibr 133 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ¬ (𝑀 = 0 ∨ 𝑁 = 0))
29 lcmn0val 11593 . . . . . 6 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) = inf({𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)}, ℝ, < ))
3021, 28, 29syl2anc 406 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 lcm 𝑁) = inf({𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)}, ℝ, < ))
31 lttri3 7767 . . . . . . 7 ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
3231adantl 273 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
33 gcddvds 11500 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
3433simpld 111 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ 𝑀)
35 gcdcl 11503 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ0)
3635nn0zd 9075 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℤ)
37 dvdsmultr1 11379 . . . . . . . . . . . 12 (((𝑀 gcd 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁)))
38373expb 1165 . . . . . . . . . . 11 (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑀 gcd 𝑁) ∥ 𝑀 → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁)))
3936, 38mpancom 416 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁)))
4034, 39mpd 13 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁))
4121, 40syl 14 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁))
42 gcdnncl 11504 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ)
43 nndivdvds 11347 . . . . . . . . 9 (((𝑀 · 𝑁) ∈ ℕ ∧ (𝑀 gcd 𝑁) ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁) ↔ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℕ))
441, 42, 43syl2anc 406 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ (𝑀 · 𝑁) ↔ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℕ))
4541, 44mpbid 146 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℕ)
4645nnred 8643 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℝ)
4733simprd 113 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∥ 𝑁)
4821, 47syl 14 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑁)
4921, 36syl 14 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℤ)
5042nnne0d 8675 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ≠ 0)
51 dvdsval2 11344 . . . . . . . . . . . 12 (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ))
5249, 50, 7, 51syl3anc 1199 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ))
5348, 52mpbid 146 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ)
54 dvdsmul1 11363 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ (𝑁 / (𝑀 gcd 𝑁)) ∈ ℤ) → 𝑀 ∥ (𝑀 · (𝑁 / (𝑀 gcd 𝑁))))
554, 53, 54syl2anc 406 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ (𝑀 · (𝑁 / (𝑀 gcd 𝑁))))
56 nncn 8638 . . . . . . . . . . 11 (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
5756adantr 272 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈ ℂ)
58 nncn 8638 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
5958adantl 273 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℂ)
6042nncnd 8644 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℂ)
6142nnap0d 8676 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) # 0)
6257, 59, 60, 61divassapd 8499 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑀 · (𝑁 / (𝑀 gcd 𝑁))))
6355, 62breqtrrd 3921 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))
6421, 34syl 14 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∥ 𝑀)
65 dvdsval2 11344 . . . . . . . . . . . 12 (((𝑀 gcd 𝑁) ∈ ℤ ∧ (𝑀 gcd 𝑁) ≠ 0 ∧ 𝑀 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ))
6649, 50, 4, 65syl3anc 1199 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ↔ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ))
6764, 66mpbid 146 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ)
68 dvdsmul1 11363 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ (𝑀 / (𝑀 gcd 𝑁)) ∈ ℤ) → 𝑁 ∥ (𝑁 · (𝑀 / (𝑀 gcd 𝑁))))
697, 67, 68syl2anc 406 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∥ (𝑁 · (𝑀 / (𝑀 gcd 𝑁))))
7057, 59mulcomd 7711 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) = (𝑁 · 𝑀))
7170oveq1d 5743 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = ((𝑁 · 𝑀) / (𝑀 gcd 𝑁)))
7259, 57, 60, 61divassapd 8499 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝑀) / (𝑀 gcd 𝑁)) = (𝑁 · (𝑀 / (𝑀 gcd 𝑁))))
7371, 72eqtrd 2147 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑁 · (𝑀 / (𝑀 gcd 𝑁))))
7469, 73breqtrrd 3921 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))
7563, 74jca 302 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∧ 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))))
76 breq2 3899 . . . . . . . . 9 (𝑥 = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) → (𝑀𝑥𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))))
77 breq2 3899 . . . . . . . . 9 (𝑥 = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) → (𝑁𝑥𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))))
7876, 77anbi12d 462 . . . . . . . 8 (𝑥 = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) → ((𝑀𝑥𝑁𝑥) ↔ (𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∧ 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))))
7978elrab 2809 . . . . . . 7 (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ {𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)} ↔ (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℕ ∧ (𝑀 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∧ 𝑁 ∥ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))))
8045, 75, 79sylanbrc 411 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ {𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)})
8146adantr 272 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)}) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℝ)
82 elrabi 2806 . . . . . . . . 9 (𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)} → 𝑛 ∈ ℕ)
8382nnred 8643 . . . . . . . 8 (𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)} → 𝑛 ∈ ℝ)
8483adantl 273 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)}) → 𝑛 ∈ ℝ)
85 breq2 3899 . . . . . . . . . 10 (𝑥 = 𝑛 → (𝑀𝑥𝑀𝑛))
86 breq2 3899 . . . . . . . . . 10 (𝑥 = 𝑛 → (𝑁𝑥𝑁𝑛))
8785, 86anbi12d 462 . . . . . . . . 9 (𝑥 = 𝑛 → ((𝑀𝑥𝑁𝑥) ↔ (𝑀𝑛𝑁𝑛)))
8887elrab 2809 . . . . . . . 8 (𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)} ↔ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛)))
89 bezout 11545 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)))
9021, 89syl 14 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)))
9190adantr 272 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)))
92 nncn 8638 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
9392ad2antlr 478 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑛 ∈ ℂ)
941nncnd 8644 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) ∈ ℂ)
9594ad2antrr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑁) ∈ ℂ)
9660ad2antrr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 gcd 𝑁) ∈ ℂ)
9757ad2antrr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑀 ∈ ℂ)
9858ad3antlr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑁 ∈ ℂ)
99 simplll 505 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑀 ∈ ℕ)
10099nnap0d 8676 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑀 # 0)
101 simpllr 506 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑁 ∈ ℕ)
102101nnap0d 8676 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑁 # 0)
10397, 98, 100, 102mulap0d 8332 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑁) # 0)
10461ad2antrr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 gcd 𝑁) # 0)
10593, 95, 96, 103, 104divdivap2d 8496 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁)))
106105adantr 272 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁)))
107 oveq2 5736 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → (𝑛 · (𝑀 gcd 𝑁)) = (𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))))
108107oveq1d 5743 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁)) = ((𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) / (𝑀 · 𝑁)))
109 zcn 8963 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
110109ad2antrl 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈ ℂ)
11197, 110mulcld 7710 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑥) ∈ ℂ)
112 zcn 8963 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℤ → 𝑦 ∈ ℂ)
113112ad2antll 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈ ℂ)
11498, 113mulcld 7710 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁 · 𝑦) ∈ ℂ)
11593, 111, 114adddid 7714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) = ((𝑛 · (𝑀 · 𝑥)) + (𝑛 · (𝑁 · 𝑦))))
116115oveq1d 5743 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) + (𝑛 · (𝑁 · 𝑦))) / (𝑀 · 𝑁)))
11793, 111mulcld 7710 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑀 · 𝑥)) ∈ ℂ)
11893, 114mulcld 7710 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑁 · 𝑦)) ∈ ℂ)
119117, 118, 95, 103divdirapd 8502 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑛 · (𝑀 · 𝑥)) + (𝑛 · (𝑁 · 𝑦))) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁))))
120116, 119eqtrd 2147 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · ((𝑀 · 𝑥) + (𝑁 · 𝑦))) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁))))
121108, 120sylan9eqr 2169 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → ((𝑛 · (𝑀 gcd 𝑁)) / (𝑀 · 𝑁)) = (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁))))
12293, 97, 110mul12d 7837 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑀 · 𝑥)) = (𝑀 · (𝑛 · 𝑥)))
123122oveq1d 5743 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) = ((𝑀 · (𝑛 · 𝑥)) / (𝑀 · 𝑁)))
12493, 110mulcld 7710 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑥) ∈ ℂ)
125124, 98, 97, 102, 100divcanap5d 8490 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 · (𝑛 · 𝑥)) / (𝑀 · 𝑁)) = ((𝑛 · 𝑥) / 𝑁))
126123, 125eqtrd 2147 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) = ((𝑛 · 𝑥) / 𝑁))
12793, 98, 113mul12d 7837 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · (𝑁 · 𝑦)) = (𝑁 · (𝑛 · 𝑦)))
128127oveq1d 5743 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)) = ((𝑁 · (𝑛 · 𝑦)) / (𝑀 · 𝑁)))
12970ad2antrr 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 · 𝑁) = (𝑁 · 𝑀))
130129oveq2d 5744 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑁 · (𝑛 · 𝑦)) / (𝑀 · 𝑁)) = ((𝑁 · (𝑛 · 𝑦)) / (𝑁 · 𝑀)))
13193, 113mulcld 7710 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑦) ∈ ℂ)
132131, 97, 98, 100, 102divcanap5d 8490 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑁 · (𝑛 · 𝑦)) / (𝑁 · 𝑀)) = ((𝑛 · 𝑦) / 𝑀))
133128, 130, 1323eqtrd 2151 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁)) = ((𝑛 · 𝑦) / 𝑀))
134126, 133oveq12d 5746 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)))
135134adantr 272 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (((𝑛 · (𝑀 · 𝑥)) / (𝑀 · 𝑁)) + ((𝑛 · (𝑁 · 𝑦)) / (𝑀 · 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)))
136106, 121, 1353eqtrd 2151 . . . . . . . . . . . . . . . . . . . 20 (((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)))
137136ex 114 . . . . . . . . . . . . . . . . . . 19 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀))))
138137adantlrr 472 . . . . . . . . . . . . . . . . . 18 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀))))
139138imp 123 . . . . . . . . . . . . . . . . 17 (((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) = (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)))
1406ad3antlr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑁 ∈ ℤ)
141 nnz 8977 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
142141ad2antlr 478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑛 ∈ ℤ)
143 simprl 503 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑥 ∈ ℤ)
144 dvdsmultr1 11379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑁𝑛𝑁 ∥ (𝑛 · 𝑥)))
145140, 142, 143, 144syl3anc 1199 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁𝑛𝑁 ∥ (𝑛 · 𝑥)))
14624ad3antlr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑁 ≠ 0)
147142, 143zmulcld 9083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑥) ∈ ℤ)
148 dvdsval2 11344 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑛 · 𝑥) ∈ ℤ) → (𝑁 ∥ (𝑛 · 𝑥) ↔ ((𝑛 · 𝑥) / 𝑁) ∈ ℤ))
149140, 146, 147, 148syl3anc 1199 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁 ∥ (𝑛 · 𝑥) ↔ ((𝑛 · 𝑥) / 𝑁) ∈ ℤ))
150145, 149sylibd 148 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑁𝑛 → ((𝑛 · 𝑥) / 𝑁) ∈ ℤ))
151150adantld 274 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀𝑛𝑁𝑛) → ((𝑛 · 𝑥) / 𝑁) ∈ ℤ))
1521513impia 1161 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑀𝑛𝑁𝑛)) → ((𝑛 · 𝑥) / 𝑁) ∈ ℤ)
1533ad3antrrr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑀 ∈ ℤ)
154 simprr 504 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑦 ∈ ℤ)
155 dvdsmultr1 11379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑀𝑛𝑀 ∥ (𝑛 · 𝑦)))
156153, 142, 154, 155syl3anc 1199 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀𝑛𝑀 ∥ (𝑛 · 𝑦)))
15722ad3antrrr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑀 ≠ 0)
158142, 154zmulcld 9083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑛 · 𝑦) ∈ ℤ)
159 dvdsval2 11344 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝑛 · 𝑦) ∈ ℤ) → (𝑀 ∥ (𝑛 · 𝑦) ↔ ((𝑛 · 𝑦) / 𝑀) ∈ ℤ))
160153, 157, 158, 159syl3anc 1199 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀 ∥ (𝑛 · 𝑦) ↔ ((𝑛 · 𝑦) / 𝑀) ∈ ℤ))
161156, 160sylibd 148 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑀𝑛 → ((𝑛 · 𝑦) / 𝑀) ∈ ℤ))
162161adantrd 275 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀𝑛𝑁𝑛) → ((𝑛 · 𝑦) / 𝑀) ∈ ℤ))
1631623impia 1161 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑀𝑛𝑁𝑛)) → ((𝑛 · 𝑦) / 𝑀) ∈ ℤ)
164152, 163zaddcld 9081 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ (𝑀𝑛𝑁𝑛)) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ)
1651643expia 1166 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀𝑛𝑁𝑛) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ))
166165an32s 540 . . . . . . . . . . . . . . . . . . . 20 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ 𝑛 ∈ ℕ) → ((𝑀𝑛𝑁𝑛) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ))
167166impr 374 . . . . . . . . . . . . . . . . . . 19 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ)
168167an32s 540 . . . . . . . . . . . . . . . . . 18 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ)
169168adantr 272 . . . . . . . . . . . . . . . . 17 (((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (((𝑛 · 𝑥) / 𝑁) + ((𝑛 · 𝑦) / 𝑀)) ∈ ℤ)
170139, 169eqeltrd 2191 . . . . . . . . . . . . . . . 16 (((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ)
17145nnzd 9076 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ)
172171ad2antrr 477 . . . . . . . . . . . . . . . . . 18 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ)
17345nnne0d 8675 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≠ 0)
174173ad2antrr 477 . . . . . . . . . . . . . . . . . 18 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≠ 0)
175142adantlrr 472 . . . . . . . . . . . . . . . . . 18 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑛 ∈ ℤ)
176 dvdsval2 11344 . . . . . . . . . . . . . . . . . 18 ((((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ ∧ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≠ 0 ∧ 𝑛 ∈ ℤ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ))
177172, 174, 175, 176syl3anc 1199 . . . . . . . . . . . . . . . . 17 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ))
178177adantr 272 . . . . . . . . . . . . . . . 16 (((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑛 / ((𝑀 · 𝑁) / (𝑀 gcd 𝑁))) ∈ ℤ))
179170, 178mpbird 166 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)
180179ex 114 . . . . . . . . . . . . . 14 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛))
181180anassrs 395 . . . . . . . . . . . . 13 (((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛))
182181reximdva 2508 . . . . . . . . . . . 12 ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ∧ 𝑥 ∈ ℤ) → (∃𝑦 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛))
183182reximdva 2508 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑥) + (𝑁 · 𝑦)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛))
18491, 183mpd 13 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)
185 1z 8984 . . . . . . . . . . . 12 1 ∈ ℤ
186 elex2 2673 . . . . . . . . . . . 12 (1 ∈ ℤ → ∃𝑤 𝑤 ∈ ℤ)
187 r19.9rmv 3420 . . . . . . . . . . . 12 (∃𝑤 𝑤 ∈ ℤ → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛))
188185, 186, 187mp2b 8 . . . . . . . . . . 11 (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)
189 r19.9rmv 3420 . . . . . . . . . . . 12 (∃𝑤 𝑤 ∈ ℤ → (∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛))
190185, 186, 189mp2b 8 . . . . . . . . . . 11 (∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)
191188, 190bitri 183 . . . . . . . . . 10 (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)
192184, 191sylibr 133 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛)
193171adantr 272 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ)
194 simprl 503 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → 𝑛 ∈ ℕ)
195 dvdsle 11390 . . . . . . . . . 10 ((((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∈ ℤ ∧ 𝑛 ∈ ℕ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛))
196193, 194, 195syl2anc 406 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛))
197192, 196mpd 13 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛)
19888, 197sylan2b 283 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)}) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ≤ 𝑛)
19981, 84, 198lensymd 7807 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)}) → ¬ 𝑛 < ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))
20032, 46, 80, 199infminti 6866 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → inf({𝑥 ∈ ℕ ∣ (𝑀𝑥𝑁𝑥)}, ℝ, < ) = ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)))
20130, 200eqtr2d 2148 . . . 4 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑀 lcm 𝑁))
202201, 45eqeltrrd 2192 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 lcm 𝑁) ∈ ℕ)
203202nncnd 8644 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 lcm 𝑁) ∈ ℂ)
20494, 203, 60, 61divmulap3d 8498 . . . 4 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) = (𝑀 lcm 𝑁) ↔ (𝑀 · 𝑁) = ((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁))))
205201, 204mpbid 146 . . 3 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 · 𝑁) = ((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁)))
20620, 205eqtr2d 2148 . 2 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁)) = (abs‘(𝑀 · 𝑁)))
207 simprl 503 . . . 4 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀𝐾𝑁𝐾))) → 𝐾 ∈ ℕ)
208 eleq1 2177 . . . . . . . 8 (𝑛 = 𝐾 → (𝑛 ∈ ℕ ↔ 𝐾 ∈ ℕ))
209 breq2 3899 . . . . . . . . 9 (𝑛 = 𝐾 → (𝑀𝑛𝑀𝐾))
210 breq2 3899 . . . . . . . . 9 (𝑛 = 𝐾 → (𝑁𝑛𝑁𝐾))
211209, 210anbi12d 462 . . . . . . . 8 (𝑛 = 𝐾 → ((𝑀𝑛𝑁𝑛) ↔ (𝑀𝐾𝑁𝐾)))
212208, 211anbi12d 462 . . . . . . 7 (𝑛 = 𝐾 → ((𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛)) ↔ (𝐾 ∈ ℕ ∧ (𝑀𝐾𝑁𝐾))))
213212anbi2d 457 . . . . . 6 (𝑛 = 𝐾 → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) ↔ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀𝐾𝑁𝐾)))))
214 breq2 3899 . . . . . 6 (𝑛 = 𝐾 → ((𝑀 lcm 𝑁) ∥ 𝑛 ↔ (𝑀 lcm 𝑁) ∥ 𝐾))
215213, 214imbi12d 233 . . . . 5 (𝑛 = 𝐾 → ((((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → (𝑀 lcm 𝑁) ∥ 𝑛) ↔ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀𝐾𝑁𝐾))) → (𝑀 lcm 𝑁) ∥ 𝐾)))
216201breq1d 3905 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑀 lcm 𝑁) ∥ 𝑛))
217216adantr 272 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → (((𝑀 · 𝑁) / (𝑀 gcd 𝑁)) ∥ 𝑛 ↔ (𝑀 lcm 𝑁) ∥ 𝑛))
218192, 217mpbid 146 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑛 ∈ ℕ ∧ (𝑀𝑛𝑁𝑛))) → (𝑀 lcm 𝑁) ∥ 𝑛)
219215, 218vtoclg 2717 . . . 4 (𝐾 ∈ ℕ → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀𝐾𝑁𝐾))) → (𝑀 lcm 𝑁) ∥ 𝐾))
220207, 219mpcom 36 . . 3 (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℕ ∧ (𝑀𝐾𝑁𝐾))) → (𝑀 lcm 𝑁) ∥ 𝐾)
221220ex 114 . 2 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐾 ∈ ℕ ∧ (𝑀𝐾𝑁𝐾)) → (𝑀 lcm 𝑁) ∥ 𝐾))
222206, 221jca 302 1 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑀 lcm 𝑁) · (𝑀 gcd 𝑁)) = (abs‘(𝑀 · 𝑁)) ∧ ((𝐾 ∈ ℕ ∧ (𝑀𝐾𝑁𝐾)) → (𝑀 lcm 𝑁) ∥ 𝐾)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 680  w3a 945   = wceq 1314  wex 1451  wcel 1463  wne 2282  wrex 2391  {crab 2394   class class class wbr 3895  cfv 5081  (class class class)co 5728  infcinf 6822  cc 7545  cr 7546  0cc0 7547  1c1 7548   + caddc 7550   · cmul 7552   < clt 7724  cle 7725   # cap 8261   / cdiv 8345  cn 8630  cz 8958  abscabs 10661  cdvds 11341   gcd cgcd 11483   lcm clcm 11587
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4003  ax-sep 4006  ax-nul 4014  ax-pow 4058  ax-pr 4091  ax-un 4315  ax-setind 4412  ax-iinf 4462  ax-cnex 7636  ax-resscn 7637  ax-1cn 7638  ax-1re 7639  ax-icn 7640  ax-addcl 7641  ax-addrcl 7642  ax-mulcl 7643  ax-mulrcl 7644  ax-addcom 7645  ax-mulcom 7646  ax-addass 7647  ax-mulass 7648  ax-distr 7649  ax-i2m1 7650  ax-0lt1 7651  ax-1rid 7652  ax-0id 7653  ax-rnegex 7654  ax-precex 7655  ax-cnre 7656  ax-pre-ltirr 7657  ax-pre-ltwlin 7658  ax-pre-lttrn 7659  ax-pre-apti 7660  ax-pre-ltadd 7661  ax-pre-mulgt0 7662  ax-pre-mulext 7663  ax-arch 7664  ax-caucvg 7665
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ne 2283  df-nel 2378  df-ral 2395  df-rex 2396  df-reu 2397  df-rmo 2398  df-rab 2399  df-v 2659  df-sbc 2879  df-csb 2972  df-dif 3039  df-un 3041  df-in 3043  df-ss 3050  df-nul 3330  df-if 3441  df-pw 3478  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-int 3738  df-iun 3781  df-br 3896  df-opab 3950  df-mpt 3951  df-tr 3987  df-id 4175  df-po 4178  df-iso 4179  df-iord 4248  df-on 4250  df-ilim 4251  df-suc 4253  df-iom 4465  df-xp 4505  df-rel 4506  df-cnv 4507  df-co 4508  df-dm 4509  df-rn 4510  df-res 4511  df-ima 4512  df-iota 5046  df-fun 5083  df-fn 5084  df-f 5085  df-f1 5086  df-fo 5087  df-f1o 5088  df-fv 5089  df-isom 5090  df-riota 5684  df-ov 5731  df-oprab 5732  df-mpo 5733  df-1st 5992  df-2nd 5993  df-recs 6156  df-frec 6242  df-sup 6823  df-inf 6824  df-pnf 7726  df-mnf 7727  df-xr 7728  df-ltxr 7729  df-le 7730  df-sub 7858  df-neg 7859  df-reap 8255  df-ap 8262  df-div 8346  df-inn 8631  df-2 8689  df-3 8690  df-4 8691  df-n0 8882  df-z 8959  df-uz 9229  df-q 9314  df-rp 9344  df-fz 9684  df-fzo 9813  df-fl 9936  df-mod 9989  df-seqfrec 10112  df-exp 10186  df-cj 10507  df-re 10508  df-im 10509  df-rsqrt 10662  df-abs 10663  df-dvds 11342  df-gcd 11484  df-lcm 11588
This theorem is referenced by:  lcmgcd  11605  lcmdvds  11606
  Copyright terms: Public domain W3C validator