Step |
Hyp |
Ref |
Expression |
1 |
|
nndivre |
โข ( ( ๐ด โ โ โง ๐ โ โ ) โ ( ๐ด / ๐ ) โ โ ) |
2 |
|
fldiv |
โข ( ( ( ๐ด / ๐ ) โ โ โง ๐ โ โ ) โ ( โ โ ( ( โ โ ( ๐ด / ๐ ) ) / ๐ ) ) = ( โ โ ( ( ๐ด / ๐ ) / ๐ ) ) ) |
3 |
1 2
|
stoic3 |
โข ( ( ๐ด โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( โ โ ( ( โ โ ( ๐ด / ๐ ) ) / ๐ ) ) = ( โ โ ( ( ๐ด / ๐ ) / ๐ ) ) ) |
4 |
|
recn |
โข ( ๐ด โ โ โ ๐ด โ โ ) |
5 |
|
nncn |
โข ( ๐ โ โ โ ๐ โ โ ) |
6 |
|
nnne0 |
โข ( ๐ โ โ โ ๐ โ 0 ) |
7 |
5 6
|
jca |
โข ( ๐ โ โ โ ( ๐ โ โ โง ๐ โ 0 ) ) |
8 |
|
nncn |
โข ( ๐ โ โ โ ๐ โ โ ) |
9 |
|
nnne0 |
โข ( ๐ โ โ โ ๐ โ 0 ) |
10 |
8 9
|
jca |
โข ( ๐ โ โ โ ( ๐ โ โ โง ๐ โ 0 ) ) |
11 |
|
divdiv1 |
โข ( ( ๐ด โ โ โง ( ๐ โ โ โง ๐ โ 0 ) โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ( ( ๐ด / ๐ ) / ๐ ) = ( ๐ด / ( ๐ ยท ๐ ) ) ) |
12 |
4 7 10 11
|
syl3an |
โข ( ( ๐ด โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ( ๐ด / ๐ ) / ๐ ) = ( ๐ด / ( ๐ ยท ๐ ) ) ) |
13 |
12
|
fveq2d |
โข ( ( ๐ด โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( โ โ ( ( ๐ด / ๐ ) / ๐ ) ) = ( โ โ ( ๐ด / ( ๐ ยท ๐ ) ) ) ) |
14 |
3 13
|
eqtrd |
โข ( ( ๐ด โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( โ โ ( ( โ โ ( ๐ด / ๐ ) ) / ๐ ) ) = ( โ โ ( ๐ด / ( ๐ ยท ๐ ) ) ) ) |