Step | Hyp | Ref
| Expression |
1 | | nn0opth.1 |
. . . . . . . . . 10
โข ๐ด โ
โ0 |
2 | | nn0opth.2 |
. . . . . . . . . 10
โข ๐ต โ
โ0 |
3 | 1, 2 | nn0addcli 12508 |
. . . . . . . . 9
โข (๐ด + ๐ต) โ
โ0 |
4 | 3 | nn0rei 12482 |
. . . . . . . 8
โข (๐ด + ๐ต) โ โ |
5 | | nn0opth.3 |
. . . . . . . . . 10
โข ๐ถ โ
โ0 |
6 | | nn0opth.4 |
. . . . . . . . . 10
โข ๐ท โ
โ0 |
7 | 5, 6 | nn0addcli 12508 |
. . . . . . . . 9
โข (๐ถ + ๐ท) โ
โ0 |
8 | 7 | nn0rei 12482 |
. . . . . . . 8
โข (๐ถ + ๐ท) โ โ |
9 | 4, 8 | lttri2i 11327 |
. . . . . . 7
โข ((๐ด + ๐ต) โ (๐ถ + ๐ท) โ ((๐ด + ๐ต) < (๐ถ + ๐ท) โจ (๐ถ + ๐ท) < (๐ด + ๐ต))) |
10 | 1, 2, 7, 6 | nn0opthlem2 14228 |
. . . . . . . . 9
โข ((๐ด + ๐ต) < (๐ถ + ๐ท) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต)) |
11 | 10 | necomd 2996 |
. . . . . . . 8
โข ((๐ด + ๐ต) < (๐ถ + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
12 | 5, 6, 3, 2 | nn0opthlem2 14228 |
. . . . . . . 8
โข ((๐ถ + ๐ท) < (๐ด + ๐ต) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
13 | 11, 12 | jaoi 855 |
. . . . . . 7
โข (((๐ด + ๐ต) < (๐ถ + ๐ท) โจ (๐ถ + ๐ท) < (๐ด + ๐ต)) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
14 | 9, 13 | sylbi 216 |
. . . . . 6
โข ((๐ด + ๐ต) โ (๐ถ + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
15 | 14 | necon4i 2976 |
. . . . 5
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (๐ด + ๐ต) = (๐ถ + ๐ท)) |
16 | | id 22 |
. . . . . . . 8
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
17 | 15, 15 | oveq12d 7426 |
. . . . . . . . 9
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ ((๐ด + ๐ต) ยท (๐ด + ๐ต)) = ((๐ถ + ๐ท) ยท (๐ถ + ๐ท))) |
18 | 17 | oveq1d 7423 |
. . . . . . . 8
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ท) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
19 | 16, 18 | eqtr4d 2775 |
. . . . . . 7
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ท)) |
20 | 3 | nn0cni 12483 |
. . . . . . . . 9
โข (๐ด + ๐ต) โ โ |
21 | 20, 20 | mulcli 11220 |
. . . . . . . 8
โข ((๐ด + ๐ต) ยท (๐ด + ๐ต)) โ โ |
22 | 2 | nn0cni 12483 |
. . . . . . . 8
โข ๐ต โ โ |
23 | 6 | nn0cni 12483 |
. . . . . . . 8
โข ๐ท โ โ |
24 | 21, 22, 23 | addcani 11406 |
. . . . . . 7
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ท) โ ๐ต = ๐ท) |
25 | 19, 24 | sylib 217 |
. . . . . 6
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ ๐ต = ๐ท) |
26 | 25 | oveq2d 7424 |
. . . . 5
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (๐ถ + ๐ต) = (๐ถ + ๐ท)) |
27 | 15, 26 | eqtr4d 2775 |
. . . 4
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (๐ด + ๐ต) = (๐ถ + ๐ต)) |
28 | 1 | nn0cni 12483 |
. . . . 5
โข ๐ด โ โ |
29 | 5 | nn0cni 12483 |
. . . . 5
โข ๐ถ โ โ |
30 | 28, 29, 22 | addcan2i 11407 |
. . . 4
โข ((๐ด + ๐ต) = (๐ถ + ๐ต) โ ๐ด = ๐ถ) |
31 | 27, 30 | sylib 217 |
. . 3
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ ๐ด = ๐ถ) |
32 | 31, 25 | jca 512 |
. 2
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (๐ด = ๐ถ โง ๐ต = ๐ท)) |
33 | | oveq12 7417 |
. . . 4
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ (๐ด + ๐ต) = (๐ถ + ๐ท)) |
34 | 33, 33 | oveq12d 7426 |
. . 3
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ ((๐ด + ๐ต) ยท (๐ด + ๐ต)) = ((๐ถ + ๐ท) ยท (๐ถ + ๐ท))) |
35 | | simpr 485 |
. . 3
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ ๐ต = ๐ท) |
36 | 34, 35 | oveq12d 7426 |
. 2
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
37 | 32, 36 | impbii 208 |
1
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (๐ด = ๐ถ โง ๐ต = ๐ท)) |