Step | Hyp | Ref
| Expression |
1 | | 2cnd 8992 |
. . . . 5
โข (๐ โ 2 โ
โ) |
2 | | apdifflemr.a |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
3 | 2 | recnd 7986 |
. . . . 5
โข (๐ โ ๐ด โ โ) |
4 | 3 | 2timesd 9161 |
. . . . . 6
โข (๐ โ (2 ยท ๐ด) = (๐ด + ๐ด)) |
5 | | apdifflemr.1 |
. . . . . . . . . . . 12
โข (๐ โ (absโ(๐ด โ -1)) #
(absโ(๐ด โ
1))) |
6 | | 1cnd 7973 |
. . . . . . . . . . . . . 14
โข (๐ โ 1 โ
โ) |
7 | 3, 6 | subnegd 8275 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ด โ -1) = (๐ด + 1)) |
8 | 3, 6, 7 | comraddd 8114 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ด โ -1) = (1 + ๐ด)) |
9 | 8 | fveq2d 5520 |
. . . . . . . . . . . 12
โข (๐ โ (absโ(๐ด โ -1)) = (absโ(1 +
๐ด))) |
10 | 3, 6 | abssubd 11202 |
. . . . . . . . . . . 12
โข (๐ โ (absโ(๐ด โ 1)) = (absโ(1
โ ๐ด))) |
11 | 5, 9, 10 | 3brtr3d 4035 |
. . . . . . . . . . 11
โข (๐ โ (absโ(1 + ๐ด)) # (absโ(1 โ ๐ด))) |
12 | 6, 3 | addcld 7977 |
. . . . . . . . . . . 12
โข (๐ โ (1 + ๐ด) โ โ) |
13 | 6, 3 | subcld 8268 |
. . . . . . . . . . . 12
โข (๐ โ (1 โ ๐ด) โ
โ) |
14 | | absext 11072 |
. . . . . . . . . . . 12
โข (((1 +
๐ด) โ โ โง (1
โ ๐ด) โ โ)
โ ((absโ(1 + ๐ด))
# (absโ(1 โ ๐ด))
โ (1 + ๐ด) # (1 โ
๐ด))) |
15 | 12, 13, 14 | syl2anc 411 |
. . . . . . . . . . 11
โข (๐ โ ((absโ(1 + ๐ด)) # (absโ(1 โ ๐ด)) โ (1 + ๐ด) # (1 โ ๐ด))) |
16 | 11, 15 | mpd 13 |
. . . . . . . . . 10
โข (๐ โ (1 + ๐ด) # (1 โ ๐ด)) |
17 | 6, 3 | negsubd 8274 |
. . . . . . . . . 10
โข (๐ โ (1 + -๐ด) = (1 โ ๐ด)) |
18 | 16, 17 | breqtrrd 4032 |
. . . . . . . . 9
โข (๐ โ (1 + ๐ด) # (1 + -๐ด)) |
19 | 3 | negcld 8255 |
. . . . . . . . . 10
โข (๐ โ -๐ด โ โ) |
20 | | apadd2 8566 |
. . . . . . . . . 10
โข ((๐ด โ โ โง -๐ด โ โ โง 1 โ
โ) โ (๐ด # -๐ด โ (1 + ๐ด) # (1 + -๐ด))) |
21 | 3, 19, 6, 20 | syl3anc 1238 |
. . . . . . . . 9
โข (๐ โ (๐ด # -๐ด โ (1 + ๐ด) # (1 + -๐ด))) |
22 | 18, 21 | mpbird 167 |
. . . . . . . 8
โข (๐ โ ๐ด # -๐ด) |
23 | | apadd2 8566 |
. . . . . . . . 9
โข ((๐ด โ โ โง -๐ด โ โ โง ๐ด โ โ) โ (๐ด # -๐ด โ (๐ด + ๐ด) # (๐ด + -๐ด))) |
24 | 3, 19, 3, 23 | syl3anc 1238 |
. . . . . . . 8
โข (๐ โ (๐ด # -๐ด โ (๐ด + ๐ด) # (๐ด + -๐ด))) |
25 | 22, 24 | mpbid 147 |
. . . . . . 7
โข (๐ โ (๐ด + ๐ด) # (๐ด + -๐ด)) |
26 | 3 | negidd 8258 |
. . . . . . 7
โข (๐ โ (๐ด + -๐ด) = 0) |
27 | 25, 26 | breqtrd 4030 |
. . . . . 6
โข (๐ โ (๐ด + ๐ด) # 0) |
28 | 4, 27 | eqbrtrd 4026 |
. . . . 5
โข (๐ โ (2 ยท ๐ด) # 0) |
29 | 1, 3, 28 | mulap0bbd 8617 |
. . . 4
โข (๐ โ ๐ด # 0) |
30 | 29 | adantr 276 |
. . 3
โข ((๐ โง ๐ = 0) โ ๐ด # 0) |
31 | | simpr 110 |
. . 3
โข ((๐ โง ๐ = 0) โ ๐ = 0) |
32 | 30, 31 | breqtrrd 4032 |
. 2
โข ((๐ โง ๐ = 0) โ ๐ด # ๐) |
33 | 4 | adantr 276 |
. . . 4
โข ((๐ โง ๐ โ 0) โ (2 ยท ๐ด) = (๐ด + ๐ด)) |
34 | | apdifflemr.as |
. . . . . . . 8
โข ((๐ โง ๐ โ 0) โ (absโ(๐ด โ 0)) # (absโ(๐ด โ (2 ยท ๐)))) |
35 | 3 | subid1d 8257 |
. . . . . . . . . . 11
โข (๐ โ (๐ด โ 0) = ๐ด) |
36 | 35 | fveq2d 5520 |
. . . . . . . . . 10
โข (๐ โ (absโ(๐ด โ 0)) = (absโ๐ด)) |
37 | | 2z 9281 |
. . . . . . . . . . . . . . 15
โข 2 โ
โค |
38 | | zq 9626 |
. . . . . . . . . . . . . . 15
โข (2 โ
โค โ 2 โ โ) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
40 | 39 | a1i 9 |
. . . . . . . . . . . . 13
โข (๐ โ 2 โ
โ) |
41 | | apdifflemr.s |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
42 | | qmulcl 9637 |
. . . . . . . . . . . . 13
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
43 | 40, 41, 42 | syl2anc 411 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ๐) โ
โ) |
44 | | qcn 9634 |
. . . . . . . . . . . 12
โข ((2
ยท ๐) โ โ
โ (2 ยท ๐)
โ โ) |
45 | 43, 44 | syl 14 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ๐) โ
โ) |
46 | 3, 45 | abssubd 11202 |
. . . . . . . . . 10
โข (๐ โ (absโ(๐ด โ (2 ยท ๐))) = (absโ((2 ยท
๐) โ ๐ด))) |
47 | 36, 46 | breq12d 4017 |
. . . . . . . . 9
โข (๐ โ ((absโ(๐ด โ 0)) # (absโ(๐ด โ (2 ยท ๐))) โ (absโ๐ด) # (absโ((2 ยท
๐) โ ๐ด)))) |
48 | 47 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ โ 0) โ ((absโ(๐ด โ 0)) # (absโ(๐ด โ (2 ยท ๐))) โ (absโ๐ด) # (absโ((2 ยท
๐) โ ๐ด)))) |
49 | 34, 48 | mpbid 147 |
. . . . . . 7
โข ((๐ โง ๐ โ 0) โ (absโ๐ด) # (absโ((2 ยท ๐) โ ๐ด))) |
50 | 3 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ โ 0) โ ๐ด โ โ) |
51 | 45, 3 | subcld 8268 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐) โ ๐ด) โ โ) |
52 | 51 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ โ 0) โ ((2 ยท ๐) โ ๐ด) โ โ) |
53 | | absext 11072 |
. . . . . . . 8
โข ((๐ด โ โ โง ((2
ยท ๐) โ ๐ด) โ โ) โ
((absโ๐ด) #
(absโ((2 ยท ๐)
โ ๐ด)) โ ๐ด # ((2 ยท ๐) โ ๐ด))) |
54 | 50, 52, 53 | syl2anc 411 |
. . . . . . 7
โข ((๐ โง ๐ โ 0) โ ((absโ๐ด) # (absโ((2 ยท
๐) โ ๐ด)) โ ๐ด # ((2 ยท ๐) โ ๐ด))) |
55 | 49, 54 | mpd 13 |
. . . . . 6
โข ((๐ โง ๐ โ 0) โ ๐ด # ((2 ยท ๐) โ ๐ด)) |
56 | | apadd2 8566 |
. . . . . . 7
โข ((๐ด โ โ โง ((2
ยท ๐) โ ๐ด) โ โ โง ๐ด โ โ) โ (๐ด # ((2 ยท ๐) โ ๐ด) โ (๐ด + ๐ด) # (๐ด + ((2 ยท ๐) โ ๐ด)))) |
57 | 50, 52, 50, 56 | syl3anc 1238 |
. . . . . 6
โข ((๐ โง ๐ โ 0) โ (๐ด # ((2 ยท ๐) โ ๐ด) โ (๐ด + ๐ด) # (๐ด + ((2 ยท ๐) โ ๐ด)))) |
58 | 55, 57 | mpbid 147 |
. . . . 5
โข ((๐ โง ๐ โ 0) โ (๐ด + ๐ด) # (๐ด + ((2 ยท ๐) โ ๐ด))) |
59 | 45 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐ โ 0) โ (2 ยท ๐) โ
โ) |
60 | 50, 59 | pncan3d 8271 |
. . . . 5
โข ((๐ โง ๐ โ 0) โ (๐ด + ((2 ยท ๐) โ ๐ด)) = (2 ยท ๐)) |
61 | 58, 60 | breqtrd 4030 |
. . . 4
โข ((๐ โง ๐ โ 0) โ (๐ด + ๐ด) # (2 ยท ๐)) |
62 | 33, 61 | eqbrtrd 4026 |
. . 3
โข ((๐ โง ๐ โ 0) โ (2 ยท ๐ด) # (2 ยท ๐)) |
63 | | qcn 9634 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
64 | 41, 63 | syl 14 |
. . . . 5
โข (๐ โ ๐ โ โ) |
65 | 64 | adantr 276 |
. . . 4
โข ((๐ โง ๐ โ 0) โ ๐ โ โ) |
66 | | 2cnd 8992 |
. . . 4
โข ((๐ โง ๐ โ 0) โ 2 โ
โ) |
67 | | 2ap0 9012 |
. . . . 5
โข 2 #
0 |
68 | 67 | a1i 9 |
. . . 4
โข ((๐ โง ๐ โ 0) โ 2 # 0) |
69 | | apmul2 8746 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ โง (2 โ
โ โง 2 # 0)) โ (๐ด # ๐ โ (2 ยท ๐ด) # (2 ยท ๐))) |
70 | 50, 65, 66, 68, 69 | syl112anc 1242 |
. . 3
โข ((๐ โง ๐ โ 0) โ (๐ด # ๐ โ (2 ยท ๐ด) # (2 ยท ๐))) |
71 | 62, 70 | mpbird 167 |
. 2
โข ((๐ โง ๐ โ 0) โ ๐ด # ๐) |
72 | | 0z 9264 |
. . . . . 6
โข 0 โ
โค |
73 | | zq 9626 |
. . . . . 6
โข (0 โ
โค โ 0 โ โ) |
74 | 72, 73 | ax-mp 5 |
. . . . 5
โข 0 โ
โ |
75 | | qdceq 10247 |
. . . . 5
โข ((๐ โ โ โง 0 โ
โ) โ DECID ๐ = 0) |
76 | 41, 74, 75 | sylancl 413 |
. . . 4
โข (๐ โ DECID ๐ = 0) |
77 | | exmiddc 836 |
. . . 4
โข
(DECID ๐ = 0 โ (๐ = 0 โจ ยฌ ๐ = 0)) |
78 | 76, 77 | syl 14 |
. . 3
โข (๐ โ (๐ = 0 โจ ยฌ ๐ = 0)) |
79 | | df-ne 2348 |
. . . 4
โข (๐ โ 0 โ ยฌ ๐ = 0) |
80 | 79 | orbi2i 762 |
. . 3
โข ((๐ = 0 โจ ๐ โ 0) โ (๐ = 0 โจ ยฌ ๐ = 0)) |
81 | 78, 80 | sylibr 134 |
. 2
โข (๐ โ (๐ = 0 โจ ๐ โ 0)) |
82 | 32, 71, 81 | mpjaodan 798 |
1
โข (๐ โ ๐ด # ๐) |