Step | Hyp | Ref
| Expression |
1 | | oveq1 7416 |
. . . . . 6
โข (๐พ = if(๐พ โ โค, ๐พ, 0) โ (๐พ ยท ๐) = (if(๐พ โ โค, ๐พ, 0) ยท ๐)) |
2 | 1 | oveq1d 7424 |
. . . . 5
โข (๐พ = if(๐พ โ โค, ๐พ, 0) โ ((๐พ ยท ๐) + ๐) = ((if(๐พ โ โค, ๐พ, 0) ยท ๐) + ๐)) |
3 | 2 | oveq2d 7425 |
. . . 4
โข (๐พ = if(๐พ โ โค, ๐พ, 0) โ (๐ gcd ((๐พ ยท ๐) + ๐)) = (๐ gcd ((if(๐พ โ โค, ๐พ, 0) ยท ๐) + ๐))) |
4 | 3 | eqeq2d 2744 |
. . 3
โข (๐พ = if(๐พ โ โค, ๐พ, 0) โ ((๐ gcd ๐) = (๐ gcd ((๐พ ยท ๐) + ๐)) โ (๐ gcd ๐) = (๐ gcd ((if(๐พ โ โค, ๐พ, 0) ยท ๐) + ๐)))) |
5 | | oveq1 7416 |
. . . 4
โข (๐ = if(๐ โ โค, ๐, 0) โ (๐ gcd ๐) = (if(๐ โ โค, ๐, 0) gcd ๐)) |
6 | | id 22 |
. . . . 5
โข (๐ = if(๐ โ โค, ๐, 0) โ ๐ = if(๐ โ โค, ๐, 0)) |
7 | | oveq2 7417 |
. . . . . 6
โข (๐ = if(๐ โ โค, ๐, 0) โ (if(๐พ โ โค, ๐พ, 0) ยท ๐) = (if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0))) |
8 | 7 | oveq1d 7424 |
. . . . 5
โข (๐ = if(๐ โ โค, ๐, 0) โ ((if(๐พ โ โค, ๐พ, 0) ยท ๐) + ๐) = ((if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0)) + ๐)) |
9 | 6, 8 | oveq12d 7427 |
. . . 4
โข (๐ = if(๐ โ โค, ๐, 0) โ (๐ gcd ((if(๐พ โ โค, ๐พ, 0) ยท ๐) + ๐)) = (if(๐ โ โค, ๐, 0) gcd ((if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0)) + ๐))) |
10 | 5, 9 | eqeq12d 2749 |
. . 3
โข (๐ = if(๐ โ โค, ๐, 0) โ ((๐ gcd ๐) = (๐ gcd ((if(๐พ โ โค, ๐พ, 0) ยท ๐) + ๐)) โ (if(๐ โ โค, ๐, 0) gcd ๐) = (if(๐ โ โค, ๐, 0) gcd ((if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0)) + ๐)))) |
11 | | oveq2 7417 |
. . . 4
โข (๐ = if(๐ โ โค, ๐, 0) โ (if(๐ โ โค, ๐, 0) gcd ๐) = (if(๐ โ โค, ๐, 0) gcd if(๐ โ โค, ๐, 0))) |
12 | | oveq2 7417 |
. . . . 5
โข (๐ = if(๐ โ โค, ๐, 0) โ ((if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0)) + ๐) = ((if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0)) + if(๐ โ โค, ๐, 0))) |
13 | 12 | oveq2d 7425 |
. . . 4
โข (๐ = if(๐ โ โค, ๐, 0) โ (if(๐ โ โค, ๐, 0) gcd ((if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0)) + ๐)) = (if(๐ โ โค, ๐, 0) gcd ((if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0)) + if(๐ โ โค, ๐, 0)))) |
14 | 11, 13 | eqeq12d 2749 |
. . 3
โข (๐ = if(๐ โ โค, ๐, 0) โ ((if(๐ โ โค, ๐, 0) gcd ๐) = (if(๐ โ โค, ๐, 0) gcd ((if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0)) + ๐)) โ (if(๐ โ โค, ๐, 0) gcd if(๐ โ โค, ๐, 0)) = (if(๐ โ โค, ๐, 0) gcd ((if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0)) + if(๐ โ โค, ๐, 0))))) |
15 | | 0z 12569 |
. . . . 5
โข 0 โ
โค |
16 | 15 | elimel 4598 |
. . . 4
โข if(๐พ โ โค, ๐พ, 0) โ
โค |
17 | 15 | elimel 4598 |
. . . 4
โข if(๐ โ โค, ๐, 0) โ
โค |
18 | 15 | elimel 4598 |
. . . 4
โข if(๐ โ โค, ๐, 0) โ
โค |
19 | 16, 17, 18 | gcdaddmlem 16465 |
. . 3
โข (if(๐ โ โค, ๐, 0) gcd if(๐ โ โค, ๐, 0)) = (if(๐ โ โค, ๐, 0) gcd ((if(๐พ โ โค, ๐พ, 0) ยท if(๐ โ โค, ๐, 0)) + if(๐ โ โค, ๐, 0))) |
20 | 4, 10, 14, 19 | dedth3h 4589 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) = (๐ gcd ((๐พ ยท ๐) + ๐))) |
21 | | zcn 12563 |
. . . . . 6
โข (๐พ โ โค โ ๐พ โ
โ) |
22 | | zcn 12563 |
. . . . . 6
โข (๐ โ โค โ ๐ โ
โ) |
23 | | mulcl 11194 |
. . . . . 6
โข ((๐พ โ โ โง ๐ โ โ) โ (๐พ ยท ๐) โ โ) |
24 | 21, 22, 23 | syl2an 597 |
. . . . 5
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ ยท ๐) โ โ) |
25 | | zcn 12563 |
. . . . 5
โข (๐ โ โค โ ๐ โ
โ) |
26 | | addcom 11400 |
. . . . 5
โข (((๐พ ยท ๐) โ โ โง ๐ โ โ) โ ((๐พ ยท ๐) + ๐) = (๐ + (๐พ ยท ๐))) |
27 | 24, 25, 26 | syl2an 597 |
. . . 4
โข (((๐พ โ โค โง ๐ โ โค) โง ๐ โ โค) โ ((๐พ ยท ๐) + ๐) = (๐ + (๐พ ยท ๐))) |
28 | 27 | 3impa 1111 |
. . 3
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) + ๐) = (๐ + (๐พ ยท ๐))) |
29 | 28 | oveq2d 7425 |
. 2
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ gcd ((๐พ ยท ๐) + ๐)) = (๐ gcd (๐ + (๐พ ยท ๐)))) |
30 | 20, 29 | eqtrd 2773 |
1
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) = (๐ gcd (๐ + (๐พ ยท ๐)))) |