Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . 3
โข
(((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โ (๐ด ยทe ๐ต) โ
โ0) |
2 | | simpr 486 |
. . . . . 6
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ด = +โ) โ ๐ด = +โ) |
3 | 2 | oveq1d 7377 |
. . . . 5
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ด = +โ) โ (๐ด ยทe ๐ต) = (+โ ยทe ๐ต)) |
4 | | xnn0xr 12497 |
. . . . . . . 8
โข (๐ต โ
โ0* โ ๐ต โ
โ*) |
5 | 4 | ad5antlr 734 |
. . . . . . 7
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ด = +โ) โ ๐ต โ
โ*) |
6 | | simp-5r 785 |
. . . . . . . 8
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ด = +โ) โ ๐ต โ
โ0*) |
7 | | simprr 772 |
. . . . . . . . 9
โข (((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ต โ 0) |
8 | 7 | ad3antrrr 729 |
. . . . . . . 8
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ด = +โ) โ ๐ต โ 0) |
9 | | xnn0gt0 31716 |
. . . . . . . 8
โข ((๐ต โ
โ0* โง ๐ต โ 0) โ 0 < ๐ต) |
10 | 6, 8, 9 | syl2anc 585 |
. . . . . . 7
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ด = +โ) โ 0 < ๐ต) |
11 | | xmulpnf2 13201 |
. . . . . . 7
โข ((๐ต โ โ*
โง 0 < ๐ต) โ
(+โ ยทe ๐ต) = +โ) |
12 | 5, 10, 11 | syl2anc 585 |
. . . . . 6
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ด = +โ) โ (+โ
ยทe ๐ต) =
+โ) |
13 | | pnfnre2 11204 |
. . . . . . . 8
โข ยฌ
+โ โ โ |
14 | | nn0re 12429 |
. . . . . . . 8
โข (+โ
โ โ0 โ +โ โ โ) |
15 | 13, 14 | mto 196 |
. . . . . . 7
โข ยฌ
+โ โ โ0 |
16 | 15 | a1i 11 |
. . . . . 6
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ด = +โ) โ ยฌ +โ โ
โ0) |
17 | 12, 16 | eqneltrd 2858 |
. . . . 5
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ด = +โ) โ ยฌ (+โ
ยทe ๐ต)
โ โ0) |
18 | 3, 17 | eqneltrd 2858 |
. . . 4
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ด = +โ) โ ยฌ (๐ด ยทe ๐ต) โ
โ0) |
19 | | simpr 486 |
. . . . . 6
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ต = +โ) โ ๐ต = +โ) |
20 | 19 | oveq2d 7378 |
. . . . 5
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ต = +โ) โ (๐ด ยทe ๐ต) = (๐ด ยทe
+โ)) |
21 | | xnn0xr 12497 |
. . . . . . . 8
โข (๐ด โ
โ0* โ ๐ด โ
โ*) |
22 | 21 | ad5antr 733 |
. . . . . . 7
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ต = +โ) โ ๐ด โ
โ*) |
23 | | simp-5l 784 |
. . . . . . . 8
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ต = +โ) โ ๐ด โ
โ0*) |
24 | | simprl 770 |
. . . . . . . . 9
โข (((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ด โ 0) |
25 | 24 | ad3antrrr 729 |
. . . . . . . 8
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ต = +โ) โ ๐ด โ 0) |
26 | | xnn0gt0 31716 |
. . . . . . . 8
โข ((๐ด โ
โ0* โง ๐ด โ 0) โ 0 < ๐ด) |
27 | 23, 25, 26 | syl2anc 585 |
. . . . . . 7
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ต = +โ) โ 0 < ๐ด) |
28 | | xmulpnf1 13200 |
. . . . . . 7
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
(๐ด ยทe
+โ) = +โ) |
29 | 22, 27, 28 | syl2anc 585 |
. . . . . 6
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ต = +โ) โ (๐ด ยทe +โ) =
+โ) |
30 | 15 | a1i 11 |
. . . . . 6
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ต = +โ) โ ยฌ +โ โ
โ0) |
31 | 29, 30 | eqneltrd 2858 |
. . . . 5
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ต = +โ) โ ยฌ (๐ด ยทe +โ) โ
โ0) |
32 | 20, 31 | eqneltrd 2858 |
. . . 4
โข
((((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โง ๐ต = +โ) โ ยฌ (๐ด ยทe ๐ต) โ
โ0) |
33 | | xnn0nnn0pnf 12505 |
. . . . . . . 8
โข ((๐ด โ
โ0* โง ยฌ ๐ด โ โ0) โ ๐ด = +โ) |
34 | 33 | ad5ant15 758 |
. . . . . . 7
โข
(((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ ๐ด โ
โ0) โ ๐ด = +โ) |
35 | 34 | ex 414 |
. . . . . 6
โข ((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โ (ยฌ ๐ด โ
โ0 โ ๐ด = +โ)) |
36 | | xnn0nnn0pnf 12505 |
. . . . . . . 8
โข ((๐ต โ
โ0* โง ยฌ ๐ต โ โ0) โ ๐ต = +โ) |
37 | 36 | ad5ant25 761 |
. . . . . . 7
โข
(((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ ๐ต โ
โ0) โ ๐ต = +โ) |
38 | 37 | ex 414 |
. . . . . 6
โข ((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โ (ยฌ ๐ต โ
โ0 โ ๐ต = +โ)) |
39 | 35, 38 | orim12d 964 |
. . . . 5
โข ((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โ ((ยฌ ๐ด โ
โ0 โจ ยฌ ๐ต โ โ0) โ (๐ด = +โ โจ ๐ต = +โ))) |
40 | | pm3.13 994 |
. . . . 5
โข (ยฌ
(๐ด โ
โ0 โง ๐ต
โ โ0) โ (ยฌ ๐ด โ โ0 โจ ยฌ ๐ต โ
โ0)) |
41 | 39, 40 | impel 507 |
. . . 4
โข
(((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โ (๐ด = +โ โจ ๐ต = +โ)) |
42 | 18, 32, 41 | mpjaodan 958 |
. . 3
โข
(((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โง ยฌ (๐ด โ
โ0 โง ๐ต
โ โ0)) โ ยฌ (๐ด ยทe ๐ต) โ
โ0) |
43 | 1, 42 | condan 817 |
. 2
โข ((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด ยทe ๐ต) โ โ0)
โ (๐ด โ
โ0 โง ๐ต
โ โ0)) |
44 | | nn0re 12429 |
. . . . 5
โข (๐ด โ โ0
โ ๐ด โ
โ) |
45 | 44 | ad2antrl 727 |
. . . 4
โข ((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด โ โ0
โง ๐ต โ
โ0)) โ ๐ด โ โ) |
46 | | nn0re 12429 |
. . . . 5
โข (๐ต โ โ0
โ ๐ต โ
โ) |
47 | 46 | ad2antll 728 |
. . . 4
โข ((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด โ โ0
โง ๐ต โ
โ0)) โ ๐ต โ โ) |
48 | | rexmul 13197 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต)) |
49 | 45, 47, 48 | syl2anc 585 |
. . 3
โข ((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด โ โ0
โง ๐ต โ
โ0)) โ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต)) |
50 | | nn0mulcl 12456 |
. . . 4
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ (๐ด ยท ๐ต) โ
โ0) |
51 | 50 | adantl 483 |
. . 3
โข ((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด โ โ0
โง ๐ต โ
โ0)) โ (๐ด ยท ๐ต) โ
โ0) |
52 | 49, 51 | eqeltrd 2838 |
. 2
โข ((((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โง (๐ด โ โ0
โง ๐ต โ
โ0)) โ (๐ด ยทe ๐ต) โ
โ0) |
53 | 43, 52 | impbida 800 |
1
โข (((๐ด โ
โ0* โง ๐ต โ โ0*)
โง (๐ด โ 0 โง ๐ต โ 0)) โ ((๐ด ยทe ๐ต) โ โ0
โ (๐ด โ
โ0 โง ๐ต
โ โ0))) |