Step | Hyp | Ref
| Expression |
1 | | 3anass 982 |
. . 3
โข ((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โ (๐ด โ โ โง (๐ถ โ โ โง ๐ถ # 0))) |
2 | | 3anass 982 |
. . 3
โข ((๐ต โ โ โง ๐ท โ โ โง ๐ท # 0) โ (๐ต โ โ โง (๐ท โ โ โง ๐ท # 0))) |
3 | | divclap 8637 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โ (๐ด / ๐ถ) โ โ) |
4 | | divclap 8637 |
. . . . . 6
โข ((๐ต โ โ โง ๐ท โ โ โง ๐ท # 0) โ (๐ต / ๐ท) โ โ) |
5 | | mulcl 7940 |
. . . . . 6
โข (((๐ด / ๐ถ) โ โ โง (๐ต / ๐ท) โ โ) โ ((๐ด / ๐ถ) ยท (๐ต / ๐ท)) โ โ) |
6 | 3, 4, 5 | syl2an 289 |
. . . . 5
โข (((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ ((๐ด / ๐ถ) ยท (๐ต / ๐ท)) โ โ) |
7 | | mulcl 7940 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ท โ โ) โ (๐ถ ยท ๐ท) โ โ) |
8 | 7 | ad2ant2r 509 |
. . . . . . 7
โข (((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0)) โ (๐ถ ยท ๐ท) โ โ) |
9 | 8 | 3adantr1 1156 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ (๐ถ ยท ๐ท) โ โ) |
10 | 9 | 3adantl1 1153 |
. . . . 5
โข (((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ (๐ถ ยท ๐ท) โ โ) |
11 | | mulap0 8613 |
. . . . . . 7
โข (((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0)) โ (๐ถ ยท ๐ท) # 0) |
12 | 11 | 3adantr1 1156 |
. . . . . 6
โข (((๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ (๐ถ ยท ๐ท) # 0) |
13 | 12 | 3adantl1 1153 |
. . . . 5
โข (((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ (๐ถ ยท ๐ท) # 0) |
14 | | divcanap3 8657 |
. . . . 5
โข ((((๐ด / ๐ถ) ยท (๐ต / ๐ท)) โ โ โง (๐ถ ยท ๐ท) โ โ โง (๐ถ ยท ๐ท) # 0) โ (((๐ถ ยท ๐ท) ยท ((๐ด / ๐ถ) ยท (๐ต / ๐ท))) / (๐ถ ยท ๐ท)) = ((๐ด / ๐ถ) ยท (๐ต / ๐ท))) |
15 | 6, 10, 13, 14 | syl3anc 1238 |
. . . 4
โข (((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ (((๐ถ ยท ๐ท) ยท ((๐ด / ๐ถ) ยท (๐ต / ๐ท))) / (๐ถ ยท ๐ท)) = ((๐ด / ๐ถ) ยท (๐ต / ๐ท))) |
16 | | simp2 998 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โ ๐ถ โ โ) |
17 | 16, 3 | jca 306 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โ (๐ถ โ โ โง (๐ด / ๐ถ) โ โ)) |
18 | | simp2 998 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ท โ โ โง ๐ท # 0) โ ๐ท โ โ) |
19 | 18, 4 | jca 306 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ท โ โ โง ๐ท # 0) โ (๐ท โ โ โง (๐ต / ๐ท) โ โ)) |
20 | | mul4 8091 |
. . . . . . 7
โข (((๐ถ โ โ โง (๐ด / ๐ถ) โ โ) โง (๐ท โ โ โง (๐ต / ๐ท) โ โ)) โ ((๐ถ ยท (๐ด / ๐ถ)) ยท (๐ท ยท (๐ต / ๐ท))) = ((๐ถ ยท ๐ท) ยท ((๐ด / ๐ถ) ยท (๐ต / ๐ท)))) |
21 | 17, 19, 20 | syl2an 289 |
. . . . . 6
โข (((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ ((๐ถ ยท (๐ด / ๐ถ)) ยท (๐ท ยท (๐ต / ๐ท))) = ((๐ถ ยท ๐ท) ยท ((๐ด / ๐ถ) ยท (๐ต / ๐ท)))) |
22 | | divcanap2 8639 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โ (๐ถ ยท (๐ด / ๐ถ)) = ๐ด) |
23 | | divcanap2 8639 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ท โ โ โง ๐ท # 0) โ (๐ท ยท (๐ต / ๐ท)) = ๐ต) |
24 | 22, 23 | oveqan12d 5896 |
. . . . . 6
โข (((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ ((๐ถ ยท (๐ด / ๐ถ)) ยท (๐ท ยท (๐ต / ๐ท))) = (๐ด ยท ๐ต)) |
25 | 21, 24 | eqtr3d 2212 |
. . . . 5
โข (((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ ((๐ถ ยท ๐ท) ยท ((๐ด / ๐ถ) ยท (๐ต / ๐ท))) = (๐ด ยท ๐ต)) |
26 | 25 | oveq1d 5892 |
. . . 4
โข (((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ (((๐ถ ยท ๐ท) ยท ((๐ด / ๐ถ) ยท (๐ต / ๐ท))) / (๐ถ ยท ๐ท)) = ((๐ด ยท ๐ต) / (๐ถ ยท ๐ท))) |
27 | 15, 26 | eqtr3d 2212 |
. . 3
โข (((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โง (๐ต โ โ โง ๐ท โ โ โง ๐ท # 0)) โ ((๐ด / ๐ถ) ยท (๐ต / ๐ท)) = ((๐ด ยท ๐ต) / (๐ถ ยท ๐ท))) |
28 | 1, 2, 27 | syl2anbr 292 |
. 2
โข (((๐ด โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โง (๐ต โ โ โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด / ๐ถ) ยท (๐ต / ๐ท)) = ((๐ด ยท ๐ต) / (๐ถ ยท ๐ท))) |
29 | 28 | an4s 588 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด / ๐ถ) ยท (๐ต / ๐ท)) = ((๐ด ยท ๐ต) / (๐ถ ยท ๐ท))) |