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

Theorem lcmgcdlem 12095
Description: Lemma for lcmgcd 12096 and lcmdvds 12097. 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 8958 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„•)
21nnred 8950 . . . 4 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„)
3 nnz 9290 . . . . . . 7 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„ค)
43adantr 276 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„ค)
54zred 9393 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„)
6 nnz 9290 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ค)
76adantl 277 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„ค)
87zred 9393 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„)
9 0red 7976 . . . . . . 7 (๐‘€ โˆˆ โ„• โ†’ 0 โˆˆ โ„)
10 nnre 8944 . . . . . . 7 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„)
11 nngt0 8962 . . . . . . 7 (๐‘€ โˆˆ โ„• โ†’ 0 < ๐‘€)
129, 10, 11ltled 8094 . . . . . 6 (๐‘€ โˆˆ โ„• โ†’ 0 โ‰ค ๐‘€)
1312adantr 276 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ 0 โ‰ค ๐‘€)
14 0red 7976 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 0 โˆˆ โ„)
15 nnre 8944 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„)
16 nngt0 8962 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 0 < ๐‘)
1714, 15, 16ltled 8094 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ๐‘)
1817adantl 277 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ 0 โ‰ค ๐‘)
195, 8, 13, 18mulge0d 8596 . . . 4 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ 0 โ‰ค (๐‘€ ยท ๐‘))
202, 19absidd 11194 . . 3 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (absโ€˜(๐‘€ ยท ๐‘)) = (๐‘€ ยท ๐‘))
213, 6anim12i 338 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค))
22 nnne0 8965 . . . . . . . . 9 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โ‰  0)
2322neneqd 2381 . . . . . . . 8 (๐‘€ โˆˆ โ„• โ†’ ยฌ ๐‘€ = 0)
24 nnne0 8965 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0)
2524neneqd 2381 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ยฌ ๐‘ = 0)
2623, 25anim12i 338 . . . . . . 7 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (ยฌ ๐‘€ = 0 โˆง ยฌ ๐‘ = 0))
27 ioran 753 . . . . . . 7 (ยฌ (๐‘€ = 0 โˆจ ๐‘ = 0) โ†” (ยฌ ๐‘€ = 0 โˆง ยฌ ๐‘ = 0))
2826, 27sylibr 134 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ยฌ (๐‘€ = 0 โˆจ ๐‘ = 0))
29 lcmn0val 12084 . . . . . 6 (((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โˆง ยฌ (๐‘€ = 0 โˆจ ๐‘ = 0)) โ†’ (๐‘€ lcm ๐‘) = inf({๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}, โ„, < ))
3021, 28, 29syl2anc 411 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ lcm ๐‘) = inf({๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}, โ„, < ))
31 lttri3 8055 . . . . . . 7 ((๐‘“ โˆˆ โ„ โˆง ๐‘” โˆˆ โ„) โ†’ (๐‘“ = ๐‘” โ†” (ยฌ ๐‘“ < ๐‘” โˆง ยฌ ๐‘” < ๐‘“)))
3231adantl 277 . . . . . 6 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘“ โˆˆ โ„ โˆง ๐‘” โˆˆ โ„)) โ†’ (๐‘“ = ๐‘” โ†” (ยฌ ๐‘“ < ๐‘” โˆง ยฌ ๐‘” < ๐‘“)))
33 gcddvds 11982 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โˆง (๐‘€ gcd ๐‘) โˆฅ ๐‘))
3433simpld 112 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ gcd ๐‘) โˆฅ ๐‘€)
35 gcdcl 11985 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„•0)
3635nn0zd 9391 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„ค)
37 dvdsmultr1 11856 . . . . . . . . . . . 12 (((๐‘€ gcd ๐‘) โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โ†’ (๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘)))
38373expb 1206 . . . . . . . . . . 11 (((๐‘€ gcd ๐‘) โˆˆ โ„ค โˆง (๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค)) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โ†’ (๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘)))
3936, 38mpancom 422 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โ†’ (๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘)))
4034, 39mpd 13 . . . . . . . . 9 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘))
4121, 40syl 14 . . . . . . . 8 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘))
42 gcdnncl 11986 . . . . . . . . 9 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„•)
43 nndivdvds 11821 . . . . . . . . 9 (((๐‘€ ยท ๐‘) โˆˆ โ„• โˆง (๐‘€ gcd ๐‘) โˆˆ โ„•) โ†’ ((๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘) โ†” ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„•))
441, 42, 43syl2anc 411 . . . . . . . 8 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘) โ†” ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„•))
4541, 44mpbid 147 . . . . . . 7 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„•)
4645nnred 8950 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„)
4733simprd 114 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ gcd ๐‘) โˆฅ ๐‘)
4821, 47syl 14 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆฅ ๐‘)
4921, 36syl 14 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„ค)
5042nnne0d 8982 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โ‰  0)
51 dvdsval2 11815 . . . . . . . . . . . 12 (((๐‘€ gcd ๐‘) โˆˆ โ„ค โˆง (๐‘€ gcd ๐‘) โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘ โ†” (๐‘ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค))
5249, 50, 7, 51syl3anc 1249 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘ โ†” (๐‘ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค))
5348, 52mpbid 147 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค)
54 dvdsmul1 11838 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ค โˆง (๐‘ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค) โ†’ ๐‘€ โˆฅ (๐‘€ ยท (๐‘ / (๐‘€ gcd ๐‘))))
554, 53, 54syl2anc 411 . . . . . . . . 9 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆฅ (๐‘€ ยท (๐‘ / (๐‘€ gcd ๐‘))))
56 nncn 8945 . . . . . . . . . . 11 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„‚)
5756adantr 276 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„‚)
58 nncn 8945 . . . . . . . . . . 11 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚)
5958adantl 277 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„‚)
6042nncnd 8951 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„‚)
6142nnap0d 8983 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) # 0)
6257, 59, 60, 61divassapd 8801 . . . . . . . . 9 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) = (๐‘€ ยท (๐‘ / (๐‘€ gcd ๐‘))))
6355, 62breqtrrd 4046 . . . . . . . 8 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))
6421, 34syl 14 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆฅ ๐‘€)
65 dvdsval2 11815 . . . . . . . . . . . 12 (((๐‘€ gcd ๐‘) โˆˆ โ„ค โˆง (๐‘€ gcd ๐‘) โ‰  0 โˆง ๐‘€ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โ†” (๐‘€ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค))
6649, 50, 4, 65syl3anc 1249 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โ†” (๐‘€ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค))
6764, 66mpbid 147 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค)
68 dvdsmul1 11838 . . . . . . . . . 10 ((๐‘ โˆˆ โ„ค โˆง (๐‘€ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค) โ†’ ๐‘ โˆฅ (๐‘ ยท (๐‘€ / (๐‘€ gcd ๐‘))))
697, 67, 68syl2anc 411 . . . . . . . . 9 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ โˆฅ (๐‘ ยท (๐‘€ / (๐‘€ gcd ๐‘))))
7057, 59mulcomd 7997 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ ยท ๐‘) = (๐‘ ยท ๐‘€))
7170oveq1d 5906 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) = ((๐‘ ยท ๐‘€) / (๐‘€ gcd ๐‘)))
7259, 57, 60, 61divassapd 8801 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘ ยท ๐‘€) / (๐‘€ gcd ๐‘)) = (๐‘ ยท (๐‘€ / (๐‘€ gcd ๐‘))))
7371, 72eqtrd 2222 . . . . . . . . 9 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) = (๐‘ ยท (๐‘€ / (๐‘€ gcd ๐‘))))
7469, 73breqtrrd 4046 . . . . . . . 8 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))
7563, 74jca 306 . . . . . . 7 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆง ๐‘ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))))
76 breq2 4022 . . . . . . . . 9 (๐‘ฅ = ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ†’ (๐‘€ โˆฅ ๐‘ฅ โ†” ๐‘€ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))))
77 breq2 4022 . . . . . . . . 9 (๐‘ฅ = ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ†’ (๐‘ โˆฅ ๐‘ฅ โ†” ๐‘ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))))
7876, 77anbi12d 473 . . . . . . . 8 (๐‘ฅ = ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ†’ ((๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ) โ†” (๐‘€ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆง ๐‘ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))))
7978elrab 2908 . . . . . . 7 (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)} โ†” (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„• โˆง (๐‘€ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆง ๐‘ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))))
8045, 75, 79sylanbrc 417 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)})
8146adantr 276 . . . . . . 7 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„)
82 elrabi 2905 . . . . . . . . 9 (๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)} โ†’ ๐‘› โˆˆ โ„•)
8382nnred 8950 . . . . . . . 8 (๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)} โ†’ ๐‘› โˆˆ โ„)
8483adantl 277 . . . . . . 7 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}) โ†’ ๐‘› โˆˆ โ„)
85 breq2 4022 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ (๐‘€ โˆฅ ๐‘ฅ โ†” ๐‘€ โˆฅ ๐‘›))
86 breq2 4022 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ (๐‘ โˆฅ ๐‘ฅ โ†” ๐‘ โˆฅ ๐‘›))
8785, 86anbi12d 473 . . . . . . . . 9 (๐‘ฅ = ๐‘› โ†’ ((๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ) โ†” (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)))
8887elrab 2908 . . . . . . . 8 (๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)} โ†” (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)))
89 bezout 12030 . . . . . . . . . . . . 13 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)))
9021, 89syl 14 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)))
9190adantr 276 . . . . . . . . . . 11 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)))
92 nncn 8945 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„‚)
9392ad2antlr 489 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘› โˆˆ โ„‚)
941nncnd 8951 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„‚)
9594ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„‚)
9660ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„‚)
9757ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘€ โˆˆ โ„‚)
9858ad3antlr 493 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ โˆˆ โ„‚)
99 simplll 533 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘€ โˆˆ โ„•)
10099nnap0d 8983 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘€ # 0)
101 simpllr 534 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ โˆˆ โ„•)
102101nnap0d 8983 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ # 0)
10397, 98, 100, 102mulap0d 8633 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ ยท ๐‘) # 0)
10461ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ gcd ๐‘) # 0)
10593, 95, 96, 103, 104divdivap2d 8798 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = ((๐‘› ยท (๐‘€ gcd ๐‘)) / (๐‘€ ยท ๐‘)))
106105adantr 276 . . . . . . . . . . . . . . . . . . . . 21 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = ((๐‘› ยท (๐‘€ gcd ๐‘)) / (๐‘€ ยท ๐‘)))
107 oveq2 5899 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ (๐‘› ยท (๐‘€ gcd ๐‘)) = (๐‘› ยท ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))))
108107oveq1d 5906 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ ((๐‘› ยท (๐‘€ gcd ๐‘)) / (๐‘€ ยท ๐‘)) = ((๐‘› ยท ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) / (๐‘€ ยท ๐‘)))
109 zcn 9276 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฅ โˆˆ โ„ค โ†’ ๐‘ฅ โˆˆ โ„‚)
110109ad2antrl 490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ฅ โˆˆ โ„‚)
11197, 110mulcld 7996 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ ยท ๐‘ฅ) โˆˆ โ„‚)
112 zcn 9276 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฆ โˆˆ โ„ค โ†’ ๐‘ฆ โˆˆ โ„‚)
113112ad2antll 491 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ฆ โˆˆ โ„‚)
11498, 113mulcld 7996 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘ ยท ๐‘ฆ) โˆˆ โ„‚)
11593, 111, 114adddid 8000 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) = ((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) + (๐‘› ยท (๐‘ ยท ๐‘ฆ))))
116115oveq1d 5906 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) / (๐‘€ ยท ๐‘)) = (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) + (๐‘› ยท (๐‘ ยท ๐‘ฆ))) / (๐‘€ ยท ๐‘)))
11793, 111mulcld 7996 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท (๐‘€ ยท ๐‘ฅ)) โˆˆ โ„‚)
11893, 114mulcld 7996 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท (๐‘ ยท ๐‘ฆ)) โˆˆ โ„‚)
119117, 118, 95, 103divdirapd 8804 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) + (๐‘› ยท (๐‘ ยท ๐‘ฆ))) / (๐‘€ ยท ๐‘)) = (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) + ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘))))
120116, 119eqtrd 2222 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) / (๐‘€ ยท ๐‘)) = (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) + ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘))))
121108, 120sylan9eqr 2244 . . . . . . . . . . . . . . . . . . . . 21 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ ((๐‘› ยท (๐‘€ gcd ๐‘)) / (๐‘€ ยท ๐‘)) = (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) + ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘))))
12293, 97, 110mul12d 8127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท (๐‘€ ยท ๐‘ฅ)) = (๐‘€ ยท (๐‘› ยท ๐‘ฅ)))
123122oveq1d 5906 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) = ((๐‘€ ยท (๐‘› ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)))
12493, 110mulcld 7996 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท ๐‘ฅ) โˆˆ โ„‚)
125124, 98, 97, 102, 100divcanap5d 8792 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ ยท (๐‘› ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) = ((๐‘› ยท ๐‘ฅ) / ๐‘))
126123, 125eqtrd 2222 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) = ((๐‘› ยท ๐‘ฅ) / ๐‘))
12793, 98, 113mul12d 8127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท (๐‘ ยท ๐‘ฆ)) = (๐‘ ยท (๐‘› ยท ๐‘ฆ)))
128127oveq1d 5906 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘)) = ((๐‘ ยท (๐‘› ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘)))
12970ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ ยท ๐‘) = (๐‘ ยท ๐‘€))
130129oveq2d 5907 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘ ยท (๐‘› ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘)) = ((๐‘ ยท (๐‘› ยท ๐‘ฆ)) / (๐‘ ยท ๐‘€)))
13193, 113mulcld 7996 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท ๐‘ฆ) โˆˆ โ„‚)
132131, 97, 98, 100, 102divcanap5d 8792 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘ ยท (๐‘› ยท ๐‘ฆ)) / (๐‘ ยท ๐‘€)) = ((๐‘› ยท ๐‘ฆ) / ๐‘€))
133128, 130, 1323eqtrd 2226 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘)) = ((๐‘› ยท ๐‘ฆ) / ๐‘€))
134126, 133oveq12d 5909 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) + ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)))
135134adantr 276 . . . . . . . . . . . . . . . . . . . . 21 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) + ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)))
136106, 121, 1353eqtrd 2226 . . . . . . . . . . . . . . . . . . . 20 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)))
137136ex 115 . . . . . . . . . . . . . . . . . . 19 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€))))
138137adantlrr 483 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€))))
139138imp 124 . . . . . . . . . . . . . . . . 17 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)))
1406ad3antlr 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ โˆˆ โ„ค)
141 nnz 9290 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„ค)
142141ad2antlr 489 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘› โˆˆ โ„ค)
143 simprl 529 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ฅ โˆˆ โ„ค)
144 dvdsmultr1 11856 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค) โ†’ (๐‘ โˆฅ ๐‘› โ†’ ๐‘ โˆฅ (๐‘› ยท ๐‘ฅ)))
145140, 142, 143, 144syl3anc 1249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘ โˆฅ ๐‘› โ†’ ๐‘ โˆฅ (๐‘› ยท ๐‘ฅ)))
14624ad3antlr 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ โ‰  0)
147142, 143zmulcld 9399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท ๐‘ฅ) โˆˆ โ„ค)
148 dvdsval2 11815 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0 โˆง (๐‘› ยท ๐‘ฅ) โˆˆ โ„ค) โ†’ (๐‘ โˆฅ (๐‘› ยท ๐‘ฅ) โ†” ((๐‘› ยท ๐‘ฅ) / ๐‘) โˆˆ โ„ค))
149140, 146, 147, 148syl3anc 1249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘ โˆฅ (๐‘› ยท ๐‘ฅ) โ†” ((๐‘› ยท ๐‘ฅ) / ๐‘) โˆˆ โ„ค))
150145, 149sylibd 149 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘ โˆฅ ๐‘› โ†’ ((๐‘› ยท ๐‘ฅ) / ๐‘) โˆˆ โ„ค))
151150adantld 278 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›) โ†’ ((๐‘› ยท ๐‘ฅ) / ๐‘) โˆˆ โ„ค))
1521513impia 1202 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)) โ†’ ((๐‘› ยท ๐‘ฅ) / ๐‘) โˆˆ โ„ค)
1533ad3antrrr 492 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘€ โˆˆ โ„ค)
154 simprr 531 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ฆ โˆˆ โ„ค)
155 dvdsmultr1 11856 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘€ โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ ๐‘› โ†’ ๐‘€ โˆฅ (๐‘› ยท ๐‘ฆ)))
156153, 142, 154, 155syl3anc 1249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ โˆฅ ๐‘› โ†’ ๐‘€ โˆฅ (๐‘› ยท ๐‘ฆ)))
15722ad3antrrr 492 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘€ โ‰  0)
158142, 154zmulcld 9399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท ๐‘ฆ) โˆˆ โ„ค)
159 dvdsval2 11815 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง (๐‘› ยท ๐‘ฆ) โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ (๐‘› ยท ๐‘ฆ) โ†” ((๐‘› ยท ๐‘ฆ) / ๐‘€) โˆˆ โ„ค))
160153, 157, 158, 159syl3anc 1249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ โˆฅ (๐‘› ยท ๐‘ฆ) โ†” ((๐‘› ยท ๐‘ฆ) / ๐‘€) โˆˆ โ„ค))
161156, 160sylibd 149 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ โˆฅ ๐‘› โ†’ ((๐‘› ยท ๐‘ฆ) / ๐‘€) โˆˆ โ„ค))
162161adantrd 279 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›) โ†’ ((๐‘› ยท ๐‘ฆ) / ๐‘€) โˆˆ โ„ค))
1631623impia 1202 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)) โ†’ ((๐‘› ยท ๐‘ฆ) / ๐‘€) โˆˆ โ„ค)
164152, 163zaddcld 9397 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค)
1651643expia 1207 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค))
166165an32s 568 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง ๐‘› โˆˆ โ„•) โ†’ ((๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค))
167166impr 379 . . . . . . . . . . . . . . . . . . 19 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค)
168167an32s 568 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค)
169168adantr 276 . . . . . . . . . . . . . . . . 17 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค)
170139, 169eqeltrd 2266 . . . . . . . . . . . . . . . 16 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) โˆˆ โ„ค)
17145nnzd 9392 . . . . . . . . . . . . . . . . . . 19 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„ค)
172171ad2antrr 488 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„ค)
17345nnne0d 8982 . . . . . . . . . . . . . . . . . . 19 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰  0)
174173ad2antrr 488 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰  0)
175142adantlrr 483 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘› โˆˆ โ„ค)
176 dvdsval2 11815 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„ค โˆง ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰  0 โˆง ๐‘› โˆˆ โ„ค) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) โˆˆ โ„ค))
177172, 174, 175, 176syl3anc 1249 . . . . . . . . . . . . . . . . 17 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) โˆˆ โ„ค))
178177adantr 276 . . . . . . . . . . . . . . . 16 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) โˆˆ โ„ค))
179170, 178mpbird 167 . . . . . . . . . . . . . . 15 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›)
180179ex 115 . . . . . . . . . . . . . 14 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›))
181180anassrs 400 . . . . . . . . . . . . 13 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง ๐‘ฅ โˆˆ โ„ค) โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›))
182181reximdva 2592 . . . . . . . . . . . 12 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง ๐‘ฅ โˆˆ โ„ค) โ†’ (โˆƒ๐‘ฆ โˆˆ โ„ค (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›))
183182reximdva 2592 . . . . . . . . . . 11 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›))
18491, 183mpd 13 . . . . . . . . . 10 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›)
185 1z 9297 . . . . . . . . . . . 12 1 โˆˆ โ„ค
186 elex2 2768 . . . . . . . . . . . 12 (1 โˆˆ โ„ค โ†’ โˆƒ๐‘ค ๐‘ค โˆˆ โ„ค)
187 r19.9rmv 3529 . . . . . . . . . . . 12 (โˆƒ๐‘ค ๐‘ค โˆˆ โ„ค โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›))
188185, 186, 187mp2b 8 . . . . . . . . . . 11 (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›)
189 r19.9rmv 3529 . . . . . . . . . . . 12 (โˆƒ๐‘ค ๐‘ค โˆˆ โ„ค โ†’ (โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›))
190185, 186, 189mp2b 8 . . . . . . . . . . 11 (โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›)
191188, 190bitri 184 . . . . . . . . . 10 (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›)
192184, 191sylibr 134 . . . . . . . . 9 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›)
193171adantr 276 . . . . . . . . . 10 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„ค)
194 simprl 529 . . . . . . . . . 10 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ ๐‘› โˆˆ โ„•)
195 dvdsle 11868 . . . . . . . . . 10 ((((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„•) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰ค ๐‘›))
196193, 194, 195syl2anc 411 . . . . . . . . 9 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰ค ๐‘›))
197192, 196mpd 13 . . . . . . . 8 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰ค ๐‘›)
19888, 197sylan2b 287 . . . . . . 7 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰ค ๐‘›)
19981, 84, 198lensymd 8097 . . . . . 6 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}) โ†’ ยฌ ๐‘› < ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))
20032, 46, 80, 199infminti 7044 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ inf({๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}, โ„, < ) = ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))
20130, 200eqtr2d 2223 . . . 4 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) = (๐‘€ lcm ๐‘))
202201, 45eqeltrrd 2267 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ lcm ๐‘) โˆˆ โ„•)
203202nncnd 8951 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ lcm ๐‘) โˆˆ โ„‚)
20494, 203, 60, 61divmulap3d 8800 . . . 4 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) = (๐‘€ lcm ๐‘) โ†” (๐‘€ ยท ๐‘) = ((๐‘€ lcm ๐‘) ยท (๐‘€ gcd ๐‘))))
205201, 204mpbid 147 . . 3 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ ยท ๐‘) = ((๐‘€ lcm ๐‘) ยท (๐‘€ gcd ๐‘)))
20620, 205eqtr2d 2223 . 2 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ lcm ๐‘) ยท (๐‘€ gcd ๐‘)) = (absโ€˜(๐‘€ ยท ๐‘)))
207 simprl 529 . . . 4 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ))) โ†’ ๐พ โˆˆ โ„•)
208 eleq1 2252 . . . . . . . 8 (๐‘› = ๐พ โ†’ (๐‘› โˆˆ โ„• โ†” ๐พ โˆˆ โ„•))
209 breq2 4022 . . . . . . . . 9 (๐‘› = ๐พ โ†’ (๐‘€ โˆฅ ๐‘› โ†” ๐‘€ โˆฅ ๐พ))
210 breq2 4022 . . . . . . . . 9 (๐‘› = ๐พ โ†’ (๐‘ โˆฅ ๐‘› โ†” ๐‘ โˆฅ ๐พ))
211209, 210anbi12d 473 . . . . . . . 8 (๐‘› = ๐พ โ†’ ((๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›) โ†” (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ)))
212208, 211anbi12d 473 . . . . . . 7 (๐‘› = ๐พ โ†’ ((๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)) โ†” (๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ))))
213212anbi2d 464 . . . . . 6 (๐‘› = ๐พ โ†’ (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†” ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ)))))
214 breq2 4022 . . . . . 6 (๐‘› = ๐พ โ†’ ((๐‘€ lcm ๐‘) โˆฅ ๐‘› โ†” (๐‘€ lcm ๐‘) โˆฅ ๐พ))
215213, 214imbi12d 234 . . . . 5 (๐‘› = ๐พ โ†’ ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (๐‘€ lcm ๐‘) โˆฅ ๐‘›) โ†” (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ))) โ†’ (๐‘€ lcm ๐‘) โˆฅ ๐พ)))
216201breq1d 4028 . . . . . . 7 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” (๐‘€ lcm ๐‘) โˆฅ ๐‘›))
217216adantr 276 . . . . . 6 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” (๐‘€ lcm ๐‘) โˆฅ ๐‘›))
218192, 217mpbid 147 . . . . 5 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (๐‘€ lcm ๐‘) โˆฅ ๐‘›)
219215, 218vtoclg 2812 . . . 4 (๐พ โˆˆ โ„• โ†’ (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ))) โ†’ (๐‘€ lcm ๐‘) โˆฅ ๐พ))
220207, 219mpcom 36 . . 3 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ))) โ†’ (๐‘€ lcm ๐‘) โˆฅ ๐พ)
221220ex 115 . 2 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ)) โ†’ (๐‘€ lcm ๐‘) โˆฅ ๐พ))
222206, 221jca 306 1 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (((๐‘€ lcm ๐‘) ยท (๐‘€ gcd ๐‘)) = (absโ€˜(๐‘€ ยท ๐‘)) โˆง ((๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ)) โ†’ (๐‘€ lcm ๐‘) โˆฅ ๐พ)))
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆจ wo 709   โˆง w3a 980   = wceq 1364  โˆƒwex 1503   โˆˆ wcel 2160   โ‰  wne 2360  โˆƒwrex 2469  {crab 2472   class class class wbr 4018  โ€˜cfv 5231  (class class class)co 5891  infcinf 7000  โ„‚cc 7827  โ„cr 7828  0cc0 7829  1c1 7830   + caddc 7832   ยท cmul 7834   < clt 8010   โ‰ค cle 8011   # cap 8556   / cdiv 8647  โ„•cn 8937  โ„คcz 9271  abscabs 11024   โˆฅ cdvds 11812   gcd cgcd 11961   lcm clcm 12078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602  ax-cnex 7920  ax-resscn 7921  ax-1cn 7922  ax-1re 7923  ax-icn 7924  ax-addcl 7925  ax-addrcl 7926  ax-mulcl 7927  ax-mulrcl 7928  ax-addcom 7929  ax-mulcom 7930  ax-addass 7931  ax-mulass 7932  ax-distr 7933  ax-i2m1 7934  ax-0lt1 7935  ax-1rid 7936  ax-0id 7937  ax-rnegex 7938  ax-precex 7939  ax-cnre 7940  ax-pre-ltirr 7941  ax-pre-ltwlin 7942  ax-pre-lttrn 7943  ax-pre-apti 7944  ax-pre-ltadd 7945  ax-pre-mulgt0 7946  ax-pre-mulext 7947  ax-arch 7948  ax-caucvg 7949
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4308  df-po 4311  df-iso 4312  df-iord 4381  df-on 4383  df-ilim 4384  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5233  df-fn 5234  df-f 5235  df-f1 5236  df-fo 5237  df-f1o 5238  df-fv 5239  df-isom 5240  df-riota 5847  df-ov 5894  df-oprab 5895  df-mpo 5896  df-1st 6159  df-2nd 6160  df-recs 6324  df-frec 6410  df-sup 7001  df-inf 7002  df-pnf 8012  df-mnf 8013  df-xr 8014  df-ltxr 8015  df-le 8016  df-sub 8148  df-neg 8149  df-reap 8550  df-ap 8557  df-div 8648  df-inn 8938  df-2 8996  df-3 8997  df-4 8998  df-n0 9195  df-z 9272  df-uz 9547  df-q 9638  df-rp 9672  df-fz 10027  df-fzo 10161  df-fl 10288  df-mod 10341  df-seqfrec 10464  df-exp 10538  df-cj 10869  df-re 10870  df-im 10871  df-rsqrt 11025  df-abs 11026  df-dvds 11813  df-gcd 11962  df-lcm 12079
This theorem is referenced by:  lcmgcd  12096  lcmdvds  12097
  Copyright terms: Public domain W3C validator