Step |
Hyp |
Ref |
Expression |
1 |
|
mulclpi |
โข ( ( ๐ด โ N โง ๐ต โ N ) โ ( ๐ด ยทN ๐ต ) โ N ) |
2 |
|
eleq1 |
โข ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ ( ( ๐ด ยทN ๐ต ) โ N โ ( ๐ด ยทN ๐ถ ) โ N ) ) |
3 |
1 2
|
syl5ib |
โข ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ ( ( ๐ด โ N โง ๐ต โ N ) โ ( ๐ด ยทN ๐ถ ) โ N ) ) |
4 |
3
|
imp |
โข ( ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โง ( ๐ด โ N โง ๐ต โ N ) ) โ ( ๐ด ยทN ๐ถ ) โ N ) |
5 |
|
dmmulpi |
โข dom ยทN = ( N ร N ) |
6 |
|
0npi |
โข ยฌ โ
โ N |
7 |
5 6
|
ndmovrcl |
โข ( ( ๐ด ยทN ๐ถ ) โ N โ ( ๐ด โ N โง ๐ถ โ N ) ) |
8 |
|
simpr |
โข ( ( ๐ด โ N โง ๐ถ โ N ) โ ๐ถ โ N ) |
9 |
4 7 8
|
3syl |
โข ( ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โง ( ๐ด โ N โง ๐ต โ N ) ) โ ๐ถ โ N ) |
10 |
|
mulpiord |
โข ( ( ๐ด โ N โง ๐ต โ N ) โ ( ๐ด ยทN ๐ต ) = ( ๐ด ยทo ๐ต ) ) |
11 |
10
|
adantr |
โข ( ( ( ๐ด โ N โง ๐ต โ N ) โง ๐ถ โ N ) โ ( ๐ด ยทN ๐ต ) = ( ๐ด ยทo ๐ต ) ) |
12 |
|
mulpiord |
โข ( ( ๐ด โ N โง ๐ถ โ N ) โ ( ๐ด ยทN ๐ถ ) = ( ๐ด ยทo ๐ถ ) ) |
13 |
12
|
adantlr |
โข ( ( ( ๐ด โ N โง ๐ต โ N ) โง ๐ถ โ N ) โ ( ๐ด ยทN ๐ถ ) = ( ๐ด ยทo ๐ถ ) ) |
14 |
11 13
|
eqeq12d |
โข ( ( ( ๐ด โ N โง ๐ต โ N ) โง ๐ถ โ N ) โ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) ) ) |
15 |
|
pinn |
โข ( ๐ด โ N โ ๐ด โ ฯ ) |
16 |
|
pinn |
โข ( ๐ต โ N โ ๐ต โ ฯ ) |
17 |
|
pinn |
โข ( ๐ถ โ N โ ๐ถ โ ฯ ) |
18 |
|
elni2 |
โข ( ๐ด โ N โ ( ๐ด โ ฯ โง โ
โ ๐ด ) ) |
19 |
18
|
simprbi |
โข ( ๐ด โ N โ โ
โ ๐ด ) |
20 |
|
nnmcan |
โข ( ( ( ๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ ) โง โ
โ ๐ด ) โ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ ๐ต = ๐ถ ) ) |
21 |
20
|
biimpd |
โข ( ( ( ๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ ) โง โ
โ ๐ด ) โ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ ๐ต = ๐ถ ) ) |
22 |
19 21
|
sylan2 |
โข ( ( ( ๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ ) โง ๐ด โ N ) โ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ ๐ต = ๐ถ ) ) |
23 |
22
|
ex |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ โ ฯ ) โ ( ๐ด โ N โ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ ๐ต = ๐ถ ) ) ) |
24 |
15 16 17 23
|
syl3an |
โข ( ( ๐ด โ N โง ๐ต โ N โง ๐ถ โ N ) โ ( ๐ด โ N โ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ ๐ต = ๐ถ ) ) ) |
25 |
24
|
3exp |
โข ( ๐ด โ N โ ( ๐ต โ N โ ( ๐ถ โ N โ ( ๐ด โ N โ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ ๐ต = ๐ถ ) ) ) ) ) |
26 |
25
|
com4r |
โข ( ๐ด โ N โ ( ๐ด โ N โ ( ๐ต โ N โ ( ๐ถ โ N โ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ ๐ต = ๐ถ ) ) ) ) ) |
27 |
26
|
pm2.43i |
โข ( ๐ด โ N โ ( ๐ต โ N โ ( ๐ถ โ N โ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ ๐ต = ๐ถ ) ) ) ) |
28 |
27
|
imp31 |
โข ( ( ( ๐ด โ N โง ๐ต โ N ) โง ๐ถ โ N ) โ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ ๐ต = ๐ถ ) ) |
29 |
14 28
|
sylbid |
โข ( ( ( ๐ด โ N โง ๐ต โ N ) โง ๐ถ โ N ) โ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ ๐ต = ๐ถ ) ) |
30 |
9 29
|
sylan2 |
โข ( ( ( ๐ด โ N โง ๐ต โ N ) โง ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โง ( ๐ด โ N โง ๐ต โ N ) ) ) โ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ ๐ต = ๐ถ ) ) |
31 |
30
|
exp32 |
โข ( ( ๐ด โ N โง ๐ต โ N ) โ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ ( ( ๐ด โ N โง ๐ต โ N ) โ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ ๐ต = ๐ถ ) ) ) ) |
32 |
31
|
imp4b |
โข ( ( ( ๐ด โ N โง ๐ต โ N ) โง ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) ) โ ( ( ( ๐ด โ N โง ๐ต โ N ) โง ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) ) โ ๐ต = ๐ถ ) ) |
33 |
32
|
pm2.43i |
โข ( ( ( ๐ด โ N โง ๐ต โ N ) โง ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) ) โ ๐ต = ๐ถ ) |
34 |
33
|
ex |
โข ( ( ๐ด โ N โง ๐ต โ N ) โ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ ๐ต = ๐ถ ) ) |
35 |
|
oveq2 |
โข ( ๐ต = ๐ถ โ ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) ) |
36 |
34 35
|
impbid1 |
โข ( ( ๐ด โ N โง ๐ต โ N ) โ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ ๐ต = ๐ถ ) ) |