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

Theorem lcmgcdlem 12090
Description: Lemma for lcmgcd 12091 and lcmdvds 12092. 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 8953 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„•)
21nnred 8945 . . . 4 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„)
3 nnz 9285 . . . . . . 7 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„ค)
43adantr 276 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„ค)
54zred 9388 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„)
6 nnz 9285 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ค)
76adantl 277 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„ค)
87zred 9388 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„)
9 0red 7971 . . . . . . 7 (๐‘€ โˆˆ โ„• โ†’ 0 โˆˆ โ„)
10 nnre 8939 . . . . . . 7 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„)
11 nngt0 8957 . . . . . . 7 (๐‘€ โˆˆ โ„• โ†’ 0 < ๐‘€)
129, 10, 11ltled 8089 . . . . . 6 (๐‘€ โˆˆ โ„• โ†’ 0 โ‰ค ๐‘€)
1312adantr 276 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ 0 โ‰ค ๐‘€)
14 0red 7971 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 0 โˆˆ โ„)
15 nnre 8939 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„)
16 nngt0 8957 . . . . . . 7 (๐‘ โˆˆ โ„• โ†’ 0 < ๐‘)
1714, 15, 16ltled 8089 . . . . . 6 (๐‘ โˆˆ โ„• โ†’ 0 โ‰ค ๐‘)
1817adantl 277 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ 0 โ‰ค ๐‘)
195, 8, 13, 18mulge0d 8591 . . . 4 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ 0 โ‰ค (๐‘€ ยท ๐‘))
202, 19absidd 11189 . . 3 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (absโ€˜(๐‘€ ยท ๐‘)) = (๐‘€ ยท ๐‘))
213, 6anim12i 338 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค))
22 nnne0 8960 . . . . . . . . 9 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โ‰  0)
2322neneqd 2378 . . . . . . . 8 (๐‘€ โˆˆ โ„• โ†’ ยฌ ๐‘€ = 0)
24 nnne0 8960 . . . . . . . . 9 (๐‘ โˆˆ โ„• โ†’ ๐‘ โ‰  0)
2524neneqd 2378 . . . . . . . 8 (๐‘ โˆˆ โ„• โ†’ ยฌ ๐‘ = 0)
2623, 25anim12i 338 . . . . . . 7 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (ยฌ ๐‘€ = 0 โˆง ยฌ ๐‘ = 0))
27 ioran 753 . . . . . . 7 (ยฌ (๐‘€ = 0 โˆจ ๐‘ = 0) โ†” (ยฌ ๐‘€ = 0 โˆง ยฌ ๐‘ = 0))
2826, 27sylibr 134 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ยฌ (๐‘€ = 0 โˆจ ๐‘ = 0))
29 lcmn0val 12079 . . . . . 6 (((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โˆง ยฌ (๐‘€ = 0 โˆจ ๐‘ = 0)) โ†’ (๐‘€ lcm ๐‘) = inf({๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}, โ„, < ))
3021, 28, 29syl2anc 411 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ lcm ๐‘) = inf({๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}, โ„, < ))
31 lttri3 8050 . . . . . . 7 ((๐‘“ โˆˆ โ„ โˆง ๐‘” โˆˆ โ„) โ†’ (๐‘“ = ๐‘” โ†” (ยฌ ๐‘“ < ๐‘” โˆง ยฌ ๐‘” < ๐‘“)))
3231adantl 277 . . . . . 6 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘“ โˆˆ โ„ โˆง ๐‘” โˆˆ โ„)) โ†’ (๐‘“ = ๐‘” โ†” (ยฌ ๐‘“ < ๐‘” โˆง ยฌ ๐‘” < ๐‘“)))
33 gcddvds 11977 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โˆง (๐‘€ gcd ๐‘) โˆฅ ๐‘))
3433simpld 112 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ gcd ๐‘) โˆฅ ๐‘€)
35 gcdcl 11980 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„•0)
3635nn0zd 9386 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„ค)
37 dvdsmultr1 11851 . . . . . . . . . . . 12 (((๐‘€ gcd ๐‘) โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โ†’ (๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘)))
38373expb 1205 . . . . . . . . . . 11 (((๐‘€ gcd ๐‘) โˆˆ โ„ค โˆง (๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค)) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โ†’ (๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘)))
3936, 38mpancom 422 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โ†’ (๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘)))
4034, 39mpd 13 . . . . . . . . 9 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘))
4121, 40syl 14 . . . . . . . 8 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘))
42 gcdnncl 11981 . . . . . . . . 9 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„•)
43 nndivdvds 11816 . . . . . . . . 9 (((๐‘€ ยท ๐‘) โˆˆ โ„• โˆง (๐‘€ gcd ๐‘) โˆˆ โ„•) โ†’ ((๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘) โ†” ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„•))
441, 42, 43syl2anc 411 . . . . . . . 8 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ gcd ๐‘) โˆฅ (๐‘€ ยท ๐‘) โ†” ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„•))
4541, 44mpbid 147 . . . . . . 7 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„•)
4645nnred 8945 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„)
4733simprd 114 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ gcd ๐‘) โˆฅ ๐‘)
4821, 47syl 14 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆฅ ๐‘)
4921, 36syl 14 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„ค)
5042nnne0d 8977 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โ‰  0)
51 dvdsval2 11810 . . . . . . . . . . . 12 (((๐‘€ gcd ๐‘) โˆˆ โ„ค โˆง (๐‘€ gcd ๐‘) โ‰  0 โˆง ๐‘ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘ โ†” (๐‘ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค))
5249, 50, 7, 51syl3anc 1248 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘ โ†” (๐‘ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค))
5348, 52mpbid 147 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค)
54 dvdsmul1 11833 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„ค โˆง (๐‘ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค) โ†’ ๐‘€ โˆฅ (๐‘€ ยท (๐‘ / (๐‘€ gcd ๐‘))))
554, 53, 54syl2anc 411 . . . . . . . . 9 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆฅ (๐‘€ ยท (๐‘ / (๐‘€ gcd ๐‘))))
56 nncn 8940 . . . . . . . . . . 11 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„‚)
5756adantr 276 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„‚)
58 nncn 8940 . . . . . . . . . . 11 (๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚)
5958adantl 277 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„‚)
6042nncnd 8946 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„‚)
6142nnap0d 8978 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) # 0)
6257, 59, 60, 61divassapd 8796 . . . . . . . . 9 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) = (๐‘€ ยท (๐‘ / (๐‘€ gcd ๐‘))))
6355, 62breqtrrd 4043 . . . . . . . 8 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))
6421, 34syl 14 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ gcd ๐‘) โˆฅ ๐‘€)
65 dvdsval2 11810 . . . . . . . . . . . 12 (((๐‘€ gcd ๐‘) โˆˆ โ„ค โˆง (๐‘€ gcd ๐‘) โ‰  0 โˆง ๐‘€ โˆˆ โ„ค) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โ†” (๐‘€ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค))
6649, 50, 4, 65syl3anc 1248 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ gcd ๐‘) โˆฅ ๐‘€ โ†” (๐‘€ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค))
6764, 66mpbid 147 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค)
68 dvdsmul1 11833 . . . . . . . . . 10 ((๐‘ โˆˆ โ„ค โˆง (๐‘€ / (๐‘€ gcd ๐‘)) โˆˆ โ„ค) โ†’ ๐‘ โˆฅ (๐‘ ยท (๐‘€ / (๐‘€ gcd ๐‘))))
697, 67, 68syl2anc 411 . . . . . . . . 9 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ โˆฅ (๐‘ ยท (๐‘€ / (๐‘€ gcd ๐‘))))
7057, 59mulcomd 7992 . . . . . . . . . . 11 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ ยท ๐‘) = (๐‘ ยท ๐‘€))
7170oveq1d 5903 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) = ((๐‘ ยท ๐‘€) / (๐‘€ gcd ๐‘)))
7259, 57, 60, 61divassapd 8796 . . . . . . . . . 10 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘ ยท ๐‘€) / (๐‘€ gcd ๐‘)) = (๐‘ ยท (๐‘€ / (๐‘€ gcd ๐‘))))
7371, 72eqtrd 2220 . . . . . . . . 9 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) = (๐‘ ยท (๐‘€ / (๐‘€ gcd ๐‘))))
7469, 73breqtrrd 4043 . . . . . . . 8 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))
7563, 74jca 306 . . . . . . 7 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆง ๐‘ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))))
76 breq2 4019 . . . . . . . . 9 (๐‘ฅ = ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ†’ (๐‘€ โˆฅ ๐‘ฅ โ†” ๐‘€ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))))
77 breq2 4019 . . . . . . . . 9 (๐‘ฅ = ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ†’ (๐‘ โˆฅ ๐‘ฅ โ†” ๐‘ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))))
7876, 77anbi12d 473 . . . . . . . 8 (๐‘ฅ = ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ†’ ((๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ) โ†” (๐‘€ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆง ๐‘ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))))
7978elrab 2905 . . . . . . 7 (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)} โ†” (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„• โˆง (๐‘€ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆง ๐‘ โˆฅ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))))
8045, 75, 79sylanbrc 417 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)})
8146adantr 276 . . . . . . 7 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„)
82 elrabi 2902 . . . . . . . . 9 (๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)} โ†’ ๐‘› โˆˆ โ„•)
8382nnred 8945 . . . . . . . 8 (๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)} โ†’ ๐‘› โˆˆ โ„)
8483adantl 277 . . . . . . 7 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}) โ†’ ๐‘› โˆˆ โ„)
85 breq2 4019 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ (๐‘€ โˆฅ ๐‘ฅ โ†” ๐‘€ โˆฅ ๐‘›))
86 breq2 4019 . . . . . . . . . 10 (๐‘ฅ = ๐‘› โ†’ (๐‘ โˆฅ ๐‘ฅ โ†” ๐‘ โˆฅ ๐‘›))
8785, 86anbi12d 473 . . . . . . . . 9 (๐‘ฅ = ๐‘› โ†’ ((๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ) โ†” (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)))
8887elrab 2905 . . . . . . . 8 (๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)} โ†” (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)))
89 bezout 12025 . . . . . . . . . . . . 13 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)))
9021, 89syl 14 . . . . . . . . . . . 12 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)))
9190adantr 276 . . . . . . . . . . 11 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)))
92 nncn 8940 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„‚)
9392ad2antlr 489 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘› โˆˆ โ„‚)
941nncnd 8946 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„‚)
9594ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ ยท ๐‘) โˆˆ โ„‚)
9660ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ gcd ๐‘) โˆˆ โ„‚)
9757ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘€ โˆˆ โ„‚)
9858ad3antlr 493 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ โˆˆ โ„‚)
99 simplll 533 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘€ โˆˆ โ„•)
10099nnap0d 8978 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘€ # 0)
101 simpllr 534 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ โˆˆ โ„•)
102101nnap0d 8978 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ # 0)
10397, 98, 100, 102mulap0d 8628 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ ยท ๐‘) # 0)
10461ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ gcd ๐‘) # 0)
10593, 95, 96, 103, 104divdivap2d 8793 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = ((๐‘› ยท (๐‘€ gcd ๐‘)) / (๐‘€ ยท ๐‘)))
106105adantr 276 . . . . . . . . . . . . . . . . . . . . 21 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = ((๐‘› ยท (๐‘€ gcd ๐‘)) / (๐‘€ ยท ๐‘)))
107 oveq2 5896 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ (๐‘› ยท (๐‘€ gcd ๐‘)) = (๐‘› ยท ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))))
108107oveq1d 5903 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ ((๐‘› ยท (๐‘€ gcd ๐‘)) / (๐‘€ ยท ๐‘)) = ((๐‘› ยท ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) / (๐‘€ ยท ๐‘)))
109 zcn 9271 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฅ โˆˆ โ„ค โ†’ ๐‘ฅ โˆˆ โ„‚)
110109ad2antrl 490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ฅ โˆˆ โ„‚)
11197, 110mulcld 7991 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ ยท ๐‘ฅ) โˆˆ โ„‚)
112 zcn 9271 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ฆ โˆˆ โ„ค โ†’ ๐‘ฆ โˆˆ โ„‚)
113112ad2antll 491 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ฆ โˆˆ โ„‚)
11498, 113mulcld 7991 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘ ยท ๐‘ฆ) โˆˆ โ„‚)
11593, 111, 114adddid 7995 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) = ((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) + (๐‘› ยท (๐‘ ยท ๐‘ฆ))))
116115oveq1d 5903 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) / (๐‘€ ยท ๐‘)) = (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) + (๐‘› ยท (๐‘ ยท ๐‘ฆ))) / (๐‘€ ยท ๐‘)))
11793, 111mulcld 7991 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท (๐‘€ ยท ๐‘ฅ)) โˆˆ โ„‚)
11893, 114mulcld 7991 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท (๐‘ ยท ๐‘ฆ)) โˆˆ โ„‚)
119117, 118, 95, 103divdirapd 8799 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) + (๐‘› ยท (๐‘ ยท ๐‘ฆ))) / (๐‘€ ยท ๐‘)) = (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) + ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘))))
120116, 119eqtrd 2220 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) / (๐‘€ ยท ๐‘)) = (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) + ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘))))
121108, 120sylan9eqr 2242 . . . . . . . . . . . . . . . . . . . . 21 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ ((๐‘› ยท (๐‘€ gcd ๐‘)) / (๐‘€ ยท ๐‘)) = (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) + ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘))))
12293, 97, 110mul12d 8122 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท (๐‘€ ยท ๐‘ฅ)) = (๐‘€ ยท (๐‘› ยท ๐‘ฅ)))
123122oveq1d 5903 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) = ((๐‘€ ยท (๐‘› ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)))
12493, 110mulcld 7991 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท ๐‘ฅ) โˆˆ โ„‚)
125124, 98, 97, 102, 100divcanap5d 8787 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ ยท (๐‘› ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) = ((๐‘› ยท ๐‘ฅ) / ๐‘))
126123, 125eqtrd 2220 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) = ((๐‘› ยท ๐‘ฅ) / ๐‘))
12793, 98, 113mul12d 8122 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท (๐‘ ยท ๐‘ฆ)) = (๐‘ ยท (๐‘› ยท ๐‘ฆ)))
128127oveq1d 5903 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘)) = ((๐‘ ยท (๐‘› ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘)))
12970ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ ยท ๐‘) = (๐‘ ยท ๐‘€))
130129oveq2d 5904 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘ ยท (๐‘› ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘)) = ((๐‘ ยท (๐‘› ยท ๐‘ฆ)) / (๐‘ ยท ๐‘€)))
13193, 113mulcld 7991 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท ๐‘ฆ) โˆˆ โ„‚)
132131, 97, 98, 100, 102divcanap5d 8787 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘ ยท (๐‘› ยท ๐‘ฆ)) / (๐‘ ยท ๐‘€)) = ((๐‘› ยท ๐‘ฆ) / ๐‘€))
133128, 130, 1323eqtrd 2224 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘)) = ((๐‘› ยท ๐‘ฆ) / ๐‘€))
134126, 133oveq12d 5906 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) + ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)))
135134adantr 276 . . . . . . . . . . . . . . . . . . . . 21 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (((๐‘› ยท (๐‘€ ยท ๐‘ฅ)) / (๐‘€ ยท ๐‘)) + ((๐‘› ยท (๐‘ ยท ๐‘ฆ)) / (๐‘€ ยท ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)))
136106, 121, 1353eqtrd 2224 . . . . . . . . . . . . . . . . . . . 20 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)))
137136ex 115 . . . . . . . . . . . . . . . . . . 19 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€))))
138137adantlrr 483 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€))))
139138imp 124 . . . . . . . . . . . . . . . . 17 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) = (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)))
1406ad3antlr 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ โˆˆ โ„ค)
141 nnz 9285 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„ค)
142141ad2antlr 489 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘› โˆˆ โ„ค)
143 simprl 529 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ฅ โˆˆ โ„ค)
144 dvdsmultr1 11851 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค) โ†’ (๐‘ โˆฅ ๐‘› โ†’ ๐‘ โˆฅ (๐‘› ยท ๐‘ฅ)))
145140, 142, 143, 144syl3anc 1248 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘ โˆฅ ๐‘› โ†’ ๐‘ โˆฅ (๐‘› ยท ๐‘ฅ)))
14624ad3antlr 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ โ‰  0)
147142, 143zmulcld 9394 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท ๐‘ฅ) โˆˆ โ„ค)
148 dvdsval2 11810 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0 โˆง (๐‘› ยท ๐‘ฅ) โˆˆ โ„ค) โ†’ (๐‘ โˆฅ (๐‘› ยท ๐‘ฅ) โ†” ((๐‘› ยท ๐‘ฅ) / ๐‘) โˆˆ โ„ค))
149140, 146, 147, 148syl3anc 1248 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘ โˆฅ (๐‘› ยท ๐‘ฅ) โ†” ((๐‘› ยท ๐‘ฅ) / ๐‘) โˆˆ โ„ค))
150145, 149sylibd 149 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘ โˆฅ ๐‘› โ†’ ((๐‘› ยท ๐‘ฅ) / ๐‘) โˆˆ โ„ค))
151150adantld 278 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›) โ†’ ((๐‘› ยท ๐‘ฅ) / ๐‘) โˆˆ โ„ค))
1521513impia 1201 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)) โ†’ ((๐‘› ยท ๐‘ฅ) / ๐‘) โˆˆ โ„ค)
1533ad3antrrr 492 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘€ โˆˆ โ„ค)
154 simprr 531 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘ฆ โˆˆ โ„ค)
155 dvdsmultr1 11851 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘€ โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ ๐‘› โ†’ ๐‘€ โˆฅ (๐‘› ยท ๐‘ฆ)))
156153, 142, 154, 155syl3anc 1248 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ โˆฅ ๐‘› โ†’ ๐‘€ โˆฅ (๐‘› ยท ๐‘ฆ)))
15722ad3antrrr 492 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘€ โ‰  0)
158142, 154zmulcld 9394 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘› ยท ๐‘ฆ) โˆˆ โ„ค)
159 dvdsval2 11810 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0 โˆง (๐‘› ยท ๐‘ฆ) โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ (๐‘› ยท ๐‘ฆ) โ†” ((๐‘› ยท ๐‘ฆ) / ๐‘€) โˆˆ โ„ค))
160153, 157, 158, 159syl3anc 1248 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ โˆฅ (๐‘› ยท ๐‘ฆ) โ†” ((๐‘› ยท ๐‘ฆ) / ๐‘€) โˆˆ โ„ค))
161156, 160sylibd 149 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (๐‘€ โˆฅ ๐‘› โ†’ ((๐‘› ยท ๐‘ฆ) / ๐‘€) โˆˆ โ„ค))
162161adantrd 279 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›) โ†’ ((๐‘› ยท ๐‘ฆ) / ๐‘€) โˆˆ โ„ค))
1631623impia 1201 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)) โ†’ ((๐‘› ยท ๐‘ฆ) / ๐‘€) โˆˆ โ„ค)
164152, 163zaddcld 9392 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค)
1651643expia 1206 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค))
166165an32s 568 . . . . . . . . . . . . . . . . . . . 20 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง ๐‘› โˆˆ โ„•) โ†’ ((๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค))
167166impr 379 . . . . . . . . . . . . . . . . . . 19 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค)
168167an32s 568 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค)
169168adantr 276 . . . . . . . . . . . . . . . . 17 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (((๐‘› ยท ๐‘ฅ) / ๐‘) + ((๐‘› ยท ๐‘ฆ) / ๐‘€)) โˆˆ โ„ค)
170139, 169eqeltrd 2264 . . . . . . . . . . . . . . . 16 (((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โˆง (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ))) โ†’ (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) โˆˆ โ„ค)
17145nnzd 9387 . . . . . . . . . . . . . . . . . . 19 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„ค)
172171ad2antrr 488 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„ค)
17345nnne0d 8977 . . . . . . . . . . . . . . . . . . 19 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰  0)
174173ad2antrr 488 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰  0)
175142adantlrr 483 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค)) โ†’ ๐‘› โˆˆ โ„ค)
176 dvdsval2 11810 . . . . . . . . . . . . . . . . . 18 ((((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„ค โˆง ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰  0 โˆง ๐‘› โˆˆ โ„ค) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” (๐‘› / ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘))) โˆˆ โ„ค))
177172, 174, 175, 176syl3anc 1248 . . . . . . . . . . . . . . . . 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 2589 . . . . . . . . . . . 12 ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โˆง ๐‘ฅ โˆˆ โ„ค) โ†’ (โˆƒ๐‘ฆ โˆˆ โ„ค (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›))
183182reximdva 2589 . . . . . . . . . . 11 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค (๐‘€ gcd ๐‘) = ((๐‘€ ยท ๐‘ฅ) + (๐‘ ยท ๐‘ฆ)) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›))
18491, 183mpd 13 . . . . . . . . . 10 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›)
185 1z 9292 . . . . . . . . . . . 12 1 โˆˆ โ„ค
186 elex2 2765 . . . . . . . . . . . 12 (1 โˆˆ โ„ค โ†’ โˆƒ๐‘ค ๐‘ค โˆˆ โ„ค)
187 r19.9rmv 3526 . . . . . . . . . . . 12 (โˆƒ๐‘ค ๐‘ค โˆˆ โ„ค โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›))
188185, 186, 187mp2b 8 . . . . . . . . . . 11 (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” โˆƒ๐‘ฆ โˆˆ โ„ค ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘›)
189 r19.9rmv 3526 . . . . . . . . . . . 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 11863 . . . . . . . . . 10 ((((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„•) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰ค ๐‘›))
196193, 194, 195syl2anc 411 . . . . . . . . 9 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰ค ๐‘›))
197192, 196mpd 13 . . . . . . . 8 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰ค ๐‘›)
19888, 197sylan2b 287 . . . . . . 7 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โ‰ค ๐‘›)
19981, 84, 198lensymd 8092 . . . . . 6 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘› โˆˆ {๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}) โ†’ ยฌ ๐‘› < ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))
20032, 46, 80, 199infminti 7039 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ inf({๐‘ฅ โˆˆ โ„• โˆฃ (๐‘€ โˆฅ ๐‘ฅ โˆง ๐‘ โˆฅ ๐‘ฅ)}, โ„, < ) = ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)))
20130, 200eqtr2d 2221 . . . 4 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) = (๐‘€ lcm ๐‘))
202201, 45eqeltrrd 2265 . . . . . 6 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ lcm ๐‘) โˆˆ โ„•)
203202nncnd 8946 . . . . 5 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ lcm ๐‘) โˆˆ โ„‚)
20494, 203, 60, 61divmulap3d 8795 . . . 4 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) = (๐‘€ lcm ๐‘) โ†” (๐‘€ ยท ๐‘) = ((๐‘€ lcm ๐‘) ยท (๐‘€ gcd ๐‘))))
205201, 204mpbid 147 . . 3 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ ยท ๐‘) = ((๐‘€ lcm ๐‘) ยท (๐‘€ gcd ๐‘)))
20620, 205eqtr2d 2221 . 2 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ lcm ๐‘) ยท (๐‘€ gcd ๐‘)) = (absโ€˜(๐‘€ ยท ๐‘)))
207 simprl 529 . . . 4 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ))) โ†’ ๐พ โˆˆ โ„•)
208 eleq1 2250 . . . . . . . 8 (๐‘› = ๐พ โ†’ (๐‘› โˆˆ โ„• โ†” ๐พ โˆˆ โ„•))
209 breq2 4019 . . . . . . . . 9 (๐‘› = ๐พ โ†’ (๐‘€ โˆฅ ๐‘› โ†” ๐‘€ โˆฅ ๐พ))
210 breq2 4019 . . . . . . . . 9 (๐‘› = ๐พ โ†’ (๐‘ โˆฅ ๐‘› โ†” ๐‘ โˆฅ ๐พ))
211209, 210anbi12d 473 . . . . . . . 8 (๐‘› = ๐พ โ†’ ((๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›) โ†” (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ)))
212208, 211anbi12d 473 . . . . . . 7 (๐‘› = ๐พ โ†’ ((๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›)) โ†” (๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ))))
213212anbi2d 464 . . . . . 6 (๐‘› = ๐พ โ†’ (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†” ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ)))))
214 breq2 4019 . . . . . 6 (๐‘› = ๐พ โ†’ ((๐‘€ lcm ๐‘) โˆฅ ๐‘› โ†” (๐‘€ lcm ๐‘) โˆฅ ๐พ))
215213, 214imbi12d 234 . . . . 5 (๐‘› = ๐พ โ†’ ((((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (๐‘€ lcm ๐‘) โˆฅ ๐‘›) โ†” (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐พ โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ))) โ†’ (๐‘€ lcm ๐‘) โˆฅ ๐พ)))
216201breq1d 4025 . . . . . . 7 ((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” (๐‘€ lcm ๐‘) โˆฅ ๐‘›))
217216adantr 276 . . . . . 6 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (((๐‘€ ยท ๐‘) / (๐‘€ gcd ๐‘)) โˆฅ ๐‘› โ†” (๐‘€ lcm ๐‘) โˆฅ ๐‘›))
218192, 217mpbid 147 . . . . 5 (((๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘› โˆˆ โ„• โˆง (๐‘€ โˆฅ ๐‘› โˆง ๐‘ โˆฅ ๐‘›))) โ†’ (๐‘€ lcm ๐‘) โˆฅ ๐‘›)
219215, 218vtoclg 2809 . . . 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 979   = wceq 1363  โˆƒwex 1502   โˆˆ wcel 2158   โ‰  wne 2357  โˆƒwrex 2466  {crab 2469   class class class wbr 4015  โ€˜cfv 5228  (class class class)co 5888  infcinf 6995  โ„‚cc 7822  โ„cr 7823  0cc0 7824  1c1 7825   + caddc 7827   ยท cmul 7829   < clt 8005   โ‰ค cle 8006   # cap 8551   / cdiv 8642  โ„•cn 8932  โ„คcz 9266  abscabs 11019   โˆฅ cdvds 11807   gcd cgcd 11956   lcm clcm 12073
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-mulrcl 7923  ax-addcom 7924  ax-mulcom 7925  ax-addass 7926  ax-mulass 7927  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-1rid 7931  ax-0id 7932  ax-rnegex 7933  ax-precex 7934  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-apti 7939  ax-pre-ltadd 7940  ax-pre-mulgt0 7941  ax-pre-mulext 7942  ax-arch 7943  ax-caucvg 7944
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-frec 6405  df-sup 6996  df-inf 6997  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-reap 8545  df-ap 8552  df-div 8643  df-inn 8933  df-2 8991  df-3 8992  df-4 8993  df-n0 9190  df-z 9267  df-uz 9542  df-q 9633  df-rp 9667  df-fz 10022  df-fzo 10156  df-fl 10283  df-mod 10336  df-seqfrec 10459  df-exp 10533  df-cj 10864  df-re 10865  df-im 10866  df-rsqrt 11020  df-abs 11021  df-dvds 11808  df-gcd 11957  df-lcm 12074
This theorem is referenced by:  lcmgcd  12091  lcmdvds  12092
  Copyright terms: Public domain W3C validator