Step | Hyp | Ref
| Expression |
1 | | ax-icn 7905 |
. . . . . . . . . . 11
โข i โ
โ |
2 | 1 | mul01i 8347 |
. . . . . . . . . 10
โข (i
ยท 0) = 0 |
3 | 2 | oveq2i 5885 |
. . . . . . . . 9
โข (0 + (i
ยท 0)) = (0 + 0) |
4 | | 00id 8097 |
. . . . . . . . 9
โข (0 + 0) =
0 |
5 | 3, 4 | eqtr2i 2199 |
. . . . . . . 8
โข 0 = (0 +
(i ยท 0)) |
6 | 5 | breq2i 4011 |
. . . . . . 7
โข ((๐ด + (i ยท ๐ต)) # 0 โ (๐ด + (i ยท ๐ต)) # (0 + (i ยท 0))) |
7 | | 0re 7956 |
. . . . . . . 8
โข 0 โ
โ |
8 | | apreim 8559 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โ
โ โง 0 โ โ)) โ ((๐ด + (i ยท ๐ต)) # (0 + (i ยท 0)) โ (๐ด # 0 โจ ๐ต # 0))) |
9 | 7, 7, 8 | mpanr12 439 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + (i ยท ๐ต)) # (0 + (i ยท 0)) โ (๐ด # 0 โจ ๐ต # 0))) |
10 | 6, 9 | bitrid 192 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + (i ยท ๐ต)) # 0 โ (๐ด # 0 โจ ๐ต # 0))) |
11 | 10 | pm5.32i 454 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด + (i ยท ๐ต)) # 0) โ ((๐ด โ โ โง ๐ต โ โ) โง (๐ด # 0 โจ ๐ต # 0))) |
12 | | remulcl 7938 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ โ) โ (๐ด ยท ๐ด) โ โ) |
13 | 12 | anidms 397 |
. . . . . . . . 9
โข (๐ด โ โ โ (๐ด ยท ๐ด) โ โ) |
14 | | remulcl 7938 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ต โ โ) โ (๐ต ยท ๐ต) โ โ) |
15 | 14 | anidms 397 |
. . . . . . . . 9
โข (๐ต โ โ โ (๐ต ยท ๐ต) โ โ) |
16 | 13, 15 | anim12i 338 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ด) โ โ โง (๐ต ยท ๐ต) โ โ)) |
17 | 16 | adantr 276 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด # 0) โ ((๐ด ยท ๐ด) โ โ โง (๐ต ยท ๐ต) โ โ)) |
18 | | apsqgt0 8557 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด # 0) โ 0 < (๐ด ยท ๐ด)) |
19 | | msqge0 8572 |
. . . . . . . . 9
โข (๐ต โ โ โ 0 โค
(๐ต ยท ๐ต)) |
20 | 18, 19 | anim12i 338 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ต โ โ) โ (0 < (๐ด ยท ๐ด) โง 0 โค (๐ต ยท ๐ต))) |
21 | 20 | an32s 568 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด # 0) โ (0 < (๐ด ยท ๐ด) โง 0 โค (๐ต ยท ๐ต))) |
22 | | addgtge0 8406 |
. . . . . . 7
โข ((((๐ด ยท ๐ด) โ โ โง (๐ต ยท ๐ต) โ โ) โง (0 < (๐ด ยท ๐ด) โง 0 โค (๐ต ยท ๐ต))) โ 0 < ((๐ด ยท ๐ด) + (๐ต ยท ๐ต))) |
23 | 17, 21, 22 | syl2anc 411 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด # 0) โ 0 < ((๐ด ยท ๐ด) + (๐ต ยท ๐ต))) |
24 | 16 | adantr 276 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ต # 0) โ ((๐ด ยท ๐ด) โ โ โง (๐ต ยท ๐ต) โ โ)) |
25 | | msqge0 8572 |
. . . . . . . . 9
โข (๐ด โ โ โ 0 โค
(๐ด ยท ๐ด)) |
26 | | apsqgt0 8557 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ต # 0) โ 0 < (๐ต ยท ๐ต)) |
27 | 25, 26 | anim12i 338 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต # 0)) โ (0 โค (๐ด ยท ๐ด) โง 0 < (๐ต ยท ๐ต))) |
28 | 27 | anassrs 400 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ต # 0) โ (0 โค (๐ด ยท ๐ด) โง 0 < (๐ต ยท ๐ต))) |
29 | | addgegt0 8405 |
. . . . . . 7
โข ((((๐ด ยท ๐ด) โ โ โง (๐ต ยท ๐ต) โ โ) โง (0 โค (๐ด ยท ๐ด) โง 0 < (๐ต ยท ๐ต))) โ 0 < ((๐ด ยท ๐ด) + (๐ต ยท ๐ต))) |
30 | 24, 28, 29 | syl2anc 411 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ต # 0) โ 0 < ((๐ด ยท ๐ด) + (๐ต ยท ๐ต))) |
31 | 23, 30 | jaodan 797 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด # 0 โจ ๐ต # 0)) โ 0 < ((๐ด ยท ๐ด) + (๐ต ยท ๐ต))) |
32 | 11, 31 | sylbi 121 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด + (i ยท ๐ต)) # 0) โ 0 < ((๐ด ยท ๐ด) + (๐ต ยท ๐ต))) |
33 | 32 | 3impa 1194 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด + (i ยท ๐ต)) # 0) โ 0 < ((๐ด ยท ๐ด) + (๐ต ยท ๐ต))) |
34 | 33 | olcd 734 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด + (i ยท ๐ต)) # 0) โ (((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) < 0 โจ 0 < ((๐ด ยท ๐ด) + (๐ต ยท ๐ต)))) |
35 | | simp1 997 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด + (i ยท ๐ต)) # 0) โ ๐ด โ โ) |
36 | 35, 35 | remulcld 7987 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด + (i ยท ๐ต)) # 0) โ (๐ด ยท ๐ด) โ โ) |
37 | | simp2 998 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด + (i ยท ๐ต)) # 0) โ ๐ต โ โ) |
38 | 37, 37 | remulcld 7987 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด + (i ยท ๐ต)) # 0) โ (๐ต ยท ๐ต) โ โ) |
39 | 36, 38 | readdcld 7986 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด + (i ยท ๐ต)) # 0) โ ((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) โ โ) |
40 | | reaplt 8544 |
. . 3
โข ((((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) โ โ โง 0 โ โ)
โ (((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) # 0 โ (((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) < 0 โจ 0 < ((๐ด ยท ๐ด) + (๐ต ยท ๐ต))))) |
41 | 39, 7, 40 | sylancl 413 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด + (i ยท ๐ต)) # 0) โ (((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) # 0 โ (((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) < 0 โจ 0 < ((๐ด ยท ๐ด) + (๐ต ยท ๐ต))))) |
42 | 34, 41 | mpbird 167 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด + (i ยท ๐ต)) # 0) โ ((๐ด ยท ๐ด) + (๐ต ยท ๐ต)) # 0) |