Step | Hyp | Ref
| Expression |
1 | | simplrl 776 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ถ โ โ) |
2 | 1 | recnd 11191 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ถ โ โ) |
3 | | simplll 774 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ด โ โ) |
4 | 3 | recnd 11191 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ด โ โ) |
5 | | simpr 486 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) |
6 | | ax-icn 11118 |
. . . . . . . . . . 11
โข i โ
โ |
7 | 6 | a1i 11 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ i โ
โ) |
8 | | simpllr 775 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ต โ โ) |
9 | 8 | recnd 11191 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ต โ โ) |
10 | 7, 9 | mulcld 11183 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (i ยท ๐ต) โ โ) |
11 | | simplrr 777 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ท โ โ) |
12 | 11 | recnd 11191 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ท โ โ) |
13 | 7, 12 | mulcld 11183 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (i ยท ๐ท) โ โ) |
14 | 4, 10, 2, 13 | addsubeq4d 11571 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ((๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท)) โ (๐ถ โ ๐ด) = ((i ยท ๐ต) โ (i ยท ๐ท)))) |
15 | 5, 14 | mpbid 231 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (๐ถ โ ๐ด) = ((i ยท ๐ต) โ (i ยท ๐ท))) |
16 | 8, 11 | resubcld 11591 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (๐ต โ ๐ท) โ โ) |
17 | 7, 9, 12 | subdid 11619 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (i ยท (๐ต โ ๐ท)) = ((i ยท ๐ต) โ (i ยท ๐ท))) |
18 | 17, 15 | eqtr4d 2776 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (i ยท (๐ต โ ๐ท)) = (๐ถ โ ๐ด)) |
19 | 1, 3 | resubcld 11591 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (๐ถ โ ๐ด) โ โ) |
20 | 18, 19 | eqeltrd 2834 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (i ยท (๐ต โ ๐ท)) โ โ) |
21 | | rimul 12152 |
. . . . . . . . . . 11
โข (((๐ต โ ๐ท) โ โ โง (i ยท (๐ต โ ๐ท)) โ โ) โ (๐ต โ ๐ท) = 0) |
22 | 16, 20, 21 | syl2anc 585 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (๐ต โ ๐ท) = 0) |
23 | 9, 12, 22 | subeq0d 11528 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ต = ๐ท) |
24 | 23 | oveq2d 7377 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (i ยท ๐ต) = (i ยท ๐ท)) |
25 | 24 | oveq1d 7376 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ((i ยท ๐ต) โ (i ยท ๐ท)) = ((i ยท ๐ท) โ (i ยท ๐ท))) |
26 | 13 | subidd 11508 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ((i ยท ๐ท) โ (i ยท ๐ท)) = 0) |
27 | 15, 25, 26 | 3eqtrd 2777 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (๐ถ โ ๐ด) = 0) |
28 | 2, 4, 27 | subeq0d 11528 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ถ = ๐ด) |
29 | 28 | eqcomd 2739 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ ๐ด = ๐ถ) |
30 | 29, 23 | jca 513 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) โ (๐ด = ๐ถ โง ๐ต = ๐ท)) |
31 | 30 | ex 414 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท)) โ (๐ด = ๐ถ โง ๐ต = ๐ท))) |
32 | | oveq2 7369 |
. . 3
โข (๐ต = ๐ท โ (i ยท ๐ต) = (i ยท ๐ท)) |
33 | | oveq12 7370 |
. . 3
โข ((๐ด = ๐ถ โง (i ยท ๐ต) = (i ยท ๐ท)) โ (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) |
34 | 32, 33 | sylan2 594 |
. 2
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ (๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท))) |
35 | 31, 34 | impbid1 224 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + (i ยท ๐ต)) = (๐ถ + (i ยท ๐ท)) โ (๐ด = ๐ถ โง ๐ต = ๐ท))) |