Step | Hyp | Ref
| Expression |
1 | | nn0opthd.1 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด โ
โ0) |
2 | | nn0opthd.2 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ต โ
โ0) |
3 | | nn0opthd.3 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ถ โ
โ0) |
4 | | nn0opthd.4 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ท โ
โ0) |
5 | 3, 4 | nn0addcld 9232 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ถ + ๐ท) โ
โ0) |
6 | 1, 2, 5, 4 | nn0opthlem2d 10700 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ด + ๐ต) < (๐ถ + ๐ท) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต))) |
7 | 6 | imp 124 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ด + ๐ต) < (๐ถ + ๐ท)) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต)) |
8 | 7 | necomd 2433 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ด + ๐ต) < (๐ถ + ๐ท)) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
9 | 8 | ex 115 |
. . . . . . . . . . 11
โข (๐ โ ((๐ด + ๐ต) < (๐ถ + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท))) |
10 | 1, 2 | nn0addcld 9232 |
. . . . . . . . . . . 12
โข (๐ โ (๐ด + ๐ต) โ
โ0) |
11 | 3, 4, 10, 2 | nn0opthlem2d 10700 |
. . . . . . . . . . 11
โข (๐ โ ((๐ถ + ๐ท) < (๐ด + ๐ต) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท))) |
12 | 9, 11 | jaod 717 |
. . . . . . . . . 10
โข (๐ โ (((๐ด + ๐ต) < (๐ถ + ๐ท) โจ (๐ถ + ๐ท) < (๐ด + ๐ต)) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท))) |
13 | 10 | nn0red 9229 |
. . . . . . . . . . 11
โข (๐ โ (๐ด + ๐ต) โ โ) |
14 | 5 | nn0red 9229 |
. . . . . . . . . . 11
โข (๐ โ (๐ถ + ๐ท) โ โ) |
15 | | reaplt 8544 |
. . . . . . . . . . 11
โข (((๐ด + ๐ต) โ โ โง (๐ถ + ๐ท) โ โ) โ ((๐ด + ๐ต) # (๐ถ + ๐ท) โ ((๐ด + ๐ต) < (๐ถ + ๐ท) โจ (๐ถ + ๐ท) < (๐ด + ๐ต)))) |
16 | 13, 14, 15 | syl2anc 411 |
. . . . . . . . . 10
โข (๐ โ ((๐ด + ๐ต) # (๐ถ + ๐ท) โ ((๐ด + ๐ต) < (๐ถ + ๐ท) โจ (๐ถ + ๐ท) < (๐ด + ๐ต)))) |
17 | 10, 10 | nn0mulcld 9233 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ด + ๐ต) ยท (๐ด + ๐ต)) โ
โ0) |
18 | 17, 2 | nn0addcld 9232 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ
โ0) |
19 | 18 | nn0zd 9372 |
. . . . . . . . . . 11
โข (๐ โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ โค) |
20 | 5, 5 | nn0mulcld 9233 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) โ
โ0) |
21 | 20, 4 | nn0addcld 9232 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ
โ0) |
22 | 21 | nn0zd 9372 |
. . . . . . . . . . 11
โข (๐ โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ โค) |
23 | | zapne 9326 |
. . . . . . . . . . 11
โข
(((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ โค โง (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ โค) โ ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) # (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท))) |
24 | 19, 22, 23 | syl2anc 411 |
. . . . . . . . . 10
โข (๐ โ ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) # (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท))) |
25 | 12, 16, 24 | 3imtr4d 203 |
. . . . . . . . 9
โข (๐ โ ((๐ด + ๐ต) # (๐ถ + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) # (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท))) |
26 | 25 | con3d 631 |
. . . . . . . 8
โข (๐ โ (ยฌ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) # (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ ยฌ (๐ด + ๐ต) # (๐ถ + ๐ท))) |
27 | 18 | nn0cnd 9230 |
. . . . . . . . 9
โข (๐ โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ โ) |
28 | 21 | nn0cnd 9230 |
. . . . . . . . 9
โข (๐ โ (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ โ) |
29 | | apti 8578 |
. . . . . . . . 9
โข
(((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ โ โง (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ โ) โ ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ ยฌ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) # (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท))) |
30 | 27, 28, 29 | syl2anc 411 |
. . . . . . . 8
โข (๐ โ ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ ยฌ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) # (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท))) |
31 | 10 | nn0cnd 9230 |
. . . . . . . . 9
โข (๐ โ (๐ด + ๐ต) โ โ) |
32 | 5 | nn0cnd 9230 |
. . . . . . . . 9
โข (๐ โ (๐ถ + ๐ท) โ โ) |
33 | | apti 8578 |
. . . . . . . . 9
โข (((๐ด + ๐ต) โ โ โง (๐ถ + ๐ท) โ โ) โ ((๐ด + ๐ต) = (๐ถ + ๐ท) โ ยฌ (๐ด + ๐ต) # (๐ถ + ๐ท))) |
34 | 31, 32, 33 | syl2anc 411 |
. . . . . . . 8
โข (๐ โ ((๐ด + ๐ต) = (๐ถ + ๐ท) โ ยฌ (๐ด + ๐ต) # (๐ถ + ๐ท))) |
35 | 26, 30, 34 | 3imtr4d 203 |
. . . . . . 7
โข (๐ โ ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (๐ด + ๐ต) = (๐ถ + ๐ท))) |
36 | 35 | imp 124 |
. . . . . 6
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ (๐ด + ๐ต) = (๐ถ + ๐ท)) |
37 | | simpr 110 |
. . . . . . . . 9
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
38 | 36, 36 | oveq12d 5892 |
. . . . . . . . . 10
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ ((๐ด + ๐ต) ยท (๐ด + ๐ต)) = ((๐ถ + ๐ท) ยท (๐ถ + ๐ท))) |
39 | 38 | oveq1d 5889 |
. . . . . . . . 9
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ท) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
40 | 37, 39 | eqtr4d 2213 |
. . . . . . . 8
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ท)) |
41 | 31, 31 | mulcld 7977 |
. . . . . . . . . 10
โข (๐ โ ((๐ด + ๐ต) ยท (๐ด + ๐ต)) โ โ) |
42 | 2 | nn0cnd 9230 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ โ) |
43 | 4 | nn0cnd 9230 |
. . . . . . . . . 10
โข (๐ โ ๐ท โ โ) |
44 | 41, 42, 43 | addcand 8140 |
. . . . . . . . 9
โข (๐ โ ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ท) โ ๐ต = ๐ท)) |
45 | 44 | adantr 276 |
. . . . . . . 8
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ท) โ ๐ต = ๐ท)) |
46 | 40, 45 | mpbid 147 |
. . . . . . 7
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ ๐ต = ๐ท) |
47 | 46 | oveq2d 5890 |
. . . . . 6
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ (๐ถ + ๐ต) = (๐ถ + ๐ท)) |
48 | 36, 47 | eqtr4d 2213 |
. . . . 5
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ (๐ด + ๐ต) = (๐ถ + ๐ต)) |
49 | 1 | nn0cnd 9230 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
50 | 3 | nn0cnd 9230 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
51 | 49, 50, 42 | addcan2d 8141 |
. . . . . 6
โข (๐ โ ((๐ด + ๐ต) = (๐ถ + ๐ต) โ ๐ด = ๐ถ)) |
52 | 51 | adantr 276 |
. . . . 5
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ ((๐ด + ๐ต) = (๐ถ + ๐ต) โ ๐ด = ๐ถ)) |
53 | 48, 52 | mpbid 147 |
. . . 4
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ ๐ด = ๐ถ) |
54 | 53, 46 | jca 306 |
. . 3
โข ((๐ โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) โ (๐ด = ๐ถ โง ๐ต = ๐ท)) |
55 | 54 | ex 115 |
. 2
โข (๐ โ ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (๐ด = ๐ถ โง ๐ต = ๐ท))) |
56 | | oveq12 5883 |
. . . 4
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ (๐ด + ๐ต) = (๐ถ + ๐ท)) |
57 | 56, 56 | oveq12d 5892 |
. . 3
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ ((๐ด + ๐ต) ยท (๐ด + ๐ต)) = ((๐ถ + ๐ท) ยท (๐ถ + ๐ท))) |
58 | | simpr 110 |
. . 3
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ ๐ต = ๐ท) |
59 | 57, 58 | oveq12d 5892 |
. 2
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท)) |
60 | 55, 59 | impbid1 142 |
1
โข (๐ โ ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (๐ด = ๐ถ โง ๐ต = ๐ท))) |