Step | Hyp | Ref
| Expression |
1 | | breq2 4007 |
. . 3
โข (๐ = ๐ โ (๐ด # ๐ โ ๐ด # ๐ )) |
2 | 1 | cbvralv 2703 |
. 2
โข
(โ๐ โ
โ ๐ด # ๐ โ โ๐ โ โ ๐ด # ๐ ) |
3 | | simplll 533 |
. . . . . . . 8
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ๐ด โ โ) |
4 | 3 | adantr 276 |
. . . . . . 7
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ด โ โ) |
5 | | simplrl 535 |
. . . . . . . 8
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ๐ โ โ) |
6 | 5 | adantr 276 |
. . . . . . 7
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ โ โ) |
7 | | simplrr 536 |
. . . . . . . 8
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ๐ โ โ) |
8 | 7 | adantr 276 |
. . . . . . 7
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ โ โ) |
9 | | simpr 110 |
. . . . . . 7
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ < ๐) |
10 | | breq2 4007 |
. . . . . . . . . 10
โข (๐ = ((๐ + ๐) / 2) โ (๐ด # ๐ โ ๐ด # ((๐ + ๐) / 2))) |
11 | | simpllr 534 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ โ๐ โ โ ๐ด # ๐ ) |
12 | | qaddcl 9634 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + ๐) โ โ) |
13 | 5, 7, 12 | syl2anc 411 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ (๐ + ๐) โ โ) |
14 | | 2z 9280 |
. . . . . . . . . . . 12
โข 2 โ
โค |
15 | | zq 9625 |
. . . . . . . . . . . 12
โข (2 โ
โค โ 2 โ โ) |
16 | 14, 15 | mp1i 10 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ 2 โ โ) |
17 | | 2ne0 9010 |
. . . . . . . . . . . 12
โข 2 โ
0 |
18 | 17 | a1i 9 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ 2 โ 0) |
19 | | qdivcl 9642 |
. . . . . . . . . . 11
โข (((๐ + ๐) โ โ โง 2 โ โ โง
2 โ 0) โ ((๐ +
๐) / 2) โ
โ) |
20 | 13, 16, 18, 19 | syl3anc 1238 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ((๐ + ๐) / 2) โ โ) |
21 | 10, 11, 20 | rspcdva 2846 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ๐ด # ((๐ + ๐) / 2)) |
22 | 3 | recnd 7985 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ๐ด โ โ) |
23 | | qcn 9633 |
. . . . . . . . . . 11
โข (((๐ + ๐) / 2) โ โ โ ((๐ + ๐) / 2) โ โ) |
24 | 20, 23 | syl 14 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ((๐ + ๐) / 2) โ โ) |
25 | | apsym 8562 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ((๐ + ๐) / 2) โ โ) โ (๐ด # ((๐ + ๐) / 2) โ ((๐ + ๐) / 2) # ๐ด)) |
26 | 22, 24, 25 | syl2anc 411 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ (๐ด # ((๐ + ๐) / 2) โ ((๐ + ๐) / 2) # ๐ด)) |
27 | 21, 26 | mpbid 147 |
. . . . . . . 8
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ((๐ + ๐) / 2) # ๐ด) |
28 | 27 | adantr 276 |
. . . . . . 7
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ((๐ + ๐) / 2) # ๐ด) |
29 | 4, 6, 8, 9, 28 | apdifflemf 14730 |
. . . . . 6
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))) |
30 | 3 | adantr 276 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ด โ โ) |
31 | 7 | adantr 276 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ โ โ) |
32 | 5 | adantr 276 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ โ โ) |
33 | | simpr 110 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ < ๐) |
34 | | qcn 9633 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
35 | 5, 34 | syl 14 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ๐ โ โ) |
36 | | qcn 9633 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
37 | 7, 36 | syl 14 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ๐ โ โ) |
38 | 35, 37 | addcomd 8107 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ (๐ + ๐) = (๐ + ๐)) |
39 | 38 | oveq1d 5889 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ((๐ + ๐) / 2) = ((๐ + ๐) / 2)) |
40 | 39, 27 | eqbrtrrd 4027 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ((๐ + ๐) / 2) # ๐ด) |
41 | 40 | adantr 276 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ((๐ + ๐) / 2) # ๐ด) |
42 | 30, 31, 32, 33, 41 | apdifflemf 14730 |
. . . . . . 7
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))) |
43 | 22 | adantr 276 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ด โ โ) |
44 | 31, 36 | syl 14 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ โ โ) |
45 | 43, 44 | subcld 8267 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ (๐ด โ ๐) โ โ) |
46 | 45 | abscld 11189 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ (absโ(๐ด โ ๐)) โ โ) |
47 | 46 | recnd 7985 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ (absโ(๐ด โ ๐)) โ โ) |
48 | 32, 34 | syl 14 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ๐ โ โ) |
49 | 43, 48 | subcld 8267 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ (๐ด โ ๐) โ โ) |
50 | 49 | abscld 11189 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ (absโ(๐ด โ ๐)) โ โ) |
51 | 50 | recnd 7985 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ (absโ(๐ด โ ๐)) โ โ) |
52 | | apsym 8562 |
. . . . . . . 8
โข
(((absโ(๐ด
โ ๐)) โ โ
โง (absโ(๐ด โ
๐)) โ โ) โ
((absโ(๐ด โ
๐)) # (absโ(๐ด โ ๐)) โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) |
53 | 47, 51, 52 | syl2anc 411 |
. . . . . . 7
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ ((absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)) โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) |
54 | 42, 53 | mpbid 147 |
. . . . . 6
โข
(((((๐ด โ
โ โง โ๐
โ โ ๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โง ๐ < ๐) โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))) |
55 | | simpr 110 |
. . . . . . 7
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ ๐ โ ๐) |
56 | | qlttri2 9640 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โ ๐ โ (๐ < ๐ โจ ๐ < ๐))) |
57 | 5, 7, 56 | syl2anc 411 |
. . . . . . 7
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ (๐ โ ๐ โ (๐ < ๐ โจ ๐ < ๐))) |
58 | 55, 57 | mpbid 147 |
. . . . . 6
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ (๐ < ๐ โจ ๐ < ๐)) |
59 | 29, 54, 58 | mpjaodan 798 |
. . . . 5
โข ((((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โง ๐ โ ๐) โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))) |
60 | 59 | ex 115 |
. . . 4
โข (((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) |
61 | 60 | ralrimivva 2559 |
. . 3
โข ((๐ด โ โ โง
โ๐ โ โ
๐ด # ๐ ) โ โ๐ โ โ โ๐ โ โ (๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) |
62 | | simpll 527 |
. . . . 5
โข (((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โ ๐ด โ โ) |
63 | | simpr 110 |
. . . . 5
โข (((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โ ๐ โ โ) |
64 | | simplr 528 |
. . . . . 6
โข (((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โ โ๐ โ โ โ๐ โ โ (๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) |
65 | | neg1rr 9024 |
. . . . . . . 8
โข -1 โ
โ |
66 | | neg1lt0 9026 |
. . . . . . . . 9
โข -1 <
0 |
67 | | 0lt1 8083 |
. . . . . . . . 9
โข 0 <
1 |
68 | | 0re 7956 |
. . . . . . . . . 10
โข 0 โ
โ |
69 | | 1re 7955 |
. . . . . . . . . 10
โข 1 โ
โ |
70 | 65, 68, 69 | lttri 8061 |
. . . . . . . . 9
โข ((-1 <
0 โง 0 < 1) โ -1 < 1) |
71 | 66, 67, 70 | mp2an 426 |
. . . . . . . 8
โข -1 <
1 |
72 | 65, 71 | ltneii 8053 |
. . . . . . 7
โข -1 โ
1 |
73 | 72 | a1i 9 |
. . . . . 6
โข (((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โ -1 โ
1) |
74 | | neg1z 9284 |
. . . . . . . 8
โข -1 โ
โค |
75 | | zq 9625 |
. . . . . . . 8
โข (-1
โ โค โ -1 โ โ) |
76 | 74, 75 | mp1i 10 |
. . . . . . 7
โข (((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โ -1 โ
โ) |
77 | | 1z 9278 |
. . . . . . . 8
โข 1 โ
โค |
78 | | zq 9625 |
. . . . . . . 8
โข (1 โ
โค โ 1 โ โ) |
79 | 77, 78 | mp1i 10 |
. . . . . . 7
โข (((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โ 1 โ
โ) |
80 | | simpl 109 |
. . . . . . . . . 10
โข ((๐ = -1 โง ๐ = 1) โ ๐ = -1) |
81 | | simpr 110 |
. . . . . . . . . 10
โข ((๐ = -1 โง ๐ = 1) โ ๐ = 1) |
82 | 80, 81 | neeq12d 2367 |
. . . . . . . . 9
โข ((๐ = -1 โง ๐ = 1) โ (๐ โ ๐ โ -1 โ 1)) |
83 | 80 | oveq2d 5890 |
. . . . . . . . . . 11
โข ((๐ = -1 โง ๐ = 1) โ (๐ด โ ๐) = (๐ด โ -1)) |
84 | 83 | fveq2d 5519 |
. . . . . . . . . 10
โข ((๐ = -1 โง ๐ = 1) โ (absโ(๐ด โ ๐)) = (absโ(๐ด โ -1))) |
85 | 81 | oveq2d 5890 |
. . . . . . . . . . 11
โข ((๐ = -1 โง ๐ = 1) โ (๐ด โ ๐) = (๐ด โ 1)) |
86 | 85 | fveq2d 5519 |
. . . . . . . . . 10
โข ((๐ = -1 โง ๐ = 1) โ (absโ(๐ด โ ๐)) = (absโ(๐ด โ 1))) |
87 | 84, 86 | breq12d 4016 |
. . . . . . . . 9
โข ((๐ = -1 โง ๐ = 1) โ ((absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)) โ (absโ(๐ด โ -1)) # (absโ(๐ด โ 1)))) |
88 | 82, 87 | imbi12d 234 |
. . . . . . . 8
โข ((๐ = -1 โง ๐ = 1) โ ((๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))) โ (-1 โ 1 โ
(absโ(๐ด โ -1))
# (absโ(๐ด โ
1))))) |
89 | 88 | rspc2gv 2853 |
. . . . . . 7
โข ((-1
โ โ โง 1 โ โ) โ (โ๐ โ โ โ๐ โ โ (๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))) โ (-1 โ 1 โ
(absโ(๐ด โ -1))
# (absโ(๐ด โ
1))))) |
90 | 76, 79, 89 | syl2anc 411 |
. . . . . 6
โข (((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โ (โ๐ โ โ โ๐ โ โ (๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))) โ (-1 โ 1 โ
(absโ(๐ด โ -1))
# (absโ(๐ด โ
1))))) |
91 | 64, 73, 90 | mp2d 47 |
. . . . 5
โข (((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โ (absโ(๐ด โ -1)) #
(absโ(๐ด โ
1))) |
92 | | simpllr 534 |
. . . . . 6
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ โ๐ โ โ โ๐ โ โ (๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) |
93 | | 2cnd 8991 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ 2 โ
โ) |
94 | | simplr 528 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ ๐ โ โ) |
95 | | qcn 9633 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
96 | 94, 95 | syl 14 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ ๐ โ โ) |
97 | | 2ap0 9011 |
. . . . . . . . . 10
โข 2 #
0 |
98 | 97 | a1i 9 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ 2 # 0) |
99 | | simpr 110 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ ๐ โ 0) |
100 | | 0z 9263 |
. . . . . . . . . . . 12
โข 0 โ
โค |
101 | | zq 9625 |
. . . . . . . . . . . 12
โข (0 โ
โค โ 0 โ โ) |
102 | 100, 101 | mp1i 10 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ 0 โ
โ) |
103 | | qapne 9638 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 0 โ
โ) โ (๐ # 0
โ ๐ โ
0)) |
104 | 94, 102, 103 | syl2anc 411 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ (๐ # 0 โ ๐ โ 0)) |
105 | 99, 104 | mpbird 167 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ ๐ # 0) |
106 | 93, 96, 98, 105 | mulap0d 8614 |
. . . . . . . 8
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ (2 ยท ๐ ) # 0) |
107 | 14, 15 | mp1i 10 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ 2 โ
โ) |
108 | | qmulcl 9636 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐ ) โ โ) |
109 | 107, 94, 108 | syl2anc 411 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ (2 ยท ๐ ) โ
โ) |
110 | | qcn 9633 |
. . . . . . . . . 10
โข ((2
ยท ๐ ) โ โ
โ (2 ยท ๐ )
โ โ) |
111 | 109, 110 | syl 14 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ (2 ยท ๐ ) โ
โ) |
112 | | 0cnd 7949 |
. . . . . . . . 9
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ 0 โ
โ) |
113 | | apsym 8562 |
. . . . . . . . 9
โข (((2
ยท ๐ ) โ โ
โง 0 โ โ) โ ((2 ยท ๐ ) # 0 โ 0 # (2 ยท ๐ ))) |
114 | 111, 112,
113 | syl2anc 411 |
. . . . . . . 8
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ ((2 ยท ๐ ) # 0 โ 0 # (2 ยท
๐ ))) |
115 | 106, 114 | mpbid 147 |
. . . . . . 7
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ 0 # (2 ยท ๐ )) |
116 | | qapne 9638 |
. . . . . . . 8
โข ((0
โ โ โง (2 ยท ๐ ) โ โ) โ (0 # (2 ยท
๐ ) โ 0 โ (2
ยท ๐ ))) |
117 | 102, 109,
116 | syl2anc 411 |
. . . . . . 7
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ (0 # (2 ยท ๐ ) โ 0 โ (2 ยท
๐ ))) |
118 | 115, 117 | mpbid 147 |
. . . . . 6
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ 0 โ (2 ยท ๐ )) |
119 | | simpl 109 |
. . . . . . . . . 10
โข ((๐ = 0 โง ๐ = (2 ยท ๐ )) โ ๐ = 0) |
120 | | simpr 110 |
. . . . . . . . . 10
โข ((๐ = 0 โง ๐ = (2 ยท ๐ )) โ ๐ = (2 ยท ๐ )) |
121 | 119, 120 | neeq12d 2367 |
. . . . . . . . 9
โข ((๐ = 0 โง ๐ = (2 ยท ๐ )) โ (๐ โ ๐ โ 0 โ (2 ยท ๐ ))) |
122 | 119 | oveq2d 5890 |
. . . . . . . . . . 11
โข ((๐ = 0 โง ๐ = (2 ยท ๐ )) โ (๐ด โ ๐) = (๐ด โ 0)) |
123 | 122 | fveq2d 5519 |
. . . . . . . . . 10
โข ((๐ = 0 โง ๐ = (2 ยท ๐ )) โ (absโ(๐ด โ ๐)) = (absโ(๐ด โ 0))) |
124 | 120 | oveq2d 5890 |
. . . . . . . . . . 11
โข ((๐ = 0 โง ๐ = (2 ยท ๐ )) โ (๐ด โ ๐) = (๐ด โ (2 ยท ๐ ))) |
125 | 124 | fveq2d 5519 |
. . . . . . . . . 10
โข ((๐ = 0 โง ๐ = (2 ยท ๐ )) โ (absโ(๐ด โ ๐)) = (absโ(๐ด โ (2 ยท ๐ )))) |
126 | 123, 125 | breq12d 4016 |
. . . . . . . . 9
โข ((๐ = 0 โง ๐ = (2 ยท ๐ )) โ ((absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)) โ (absโ(๐ด โ 0)) # (absโ(๐ด โ (2 ยท ๐ ))))) |
127 | 121, 126 | imbi12d 234 |
. . . . . . . 8
โข ((๐ = 0 โง ๐ = (2 ยท ๐ )) โ ((๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))) โ (0 โ (2 ยท ๐ ) โ (absโ(๐ด โ 0)) # (absโ(๐ด โ (2 ยท ๐ )))))) |
128 | 127 | rspc2gv 2853 |
. . . . . . 7
โข ((0
โ โ โง (2 ยท ๐ ) โ โ) โ (โ๐ โ โ โ๐ โ โ (๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))) โ (0 โ (2 ยท ๐ ) โ (absโ(๐ด โ 0)) # (absโ(๐ด โ (2 ยท ๐ )))))) |
129 | 102, 109,
128 | syl2anc 411 |
. . . . . 6
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ (โ๐ โ โ โ๐ โ โ (๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))) โ (0 โ (2 ยท ๐ ) โ (absโ(๐ด โ 0)) # (absโ(๐ด โ (2 ยท ๐ )))))) |
130 | 92, 118, 129 | mp2d 47 |
. . . . 5
โข ((((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โง ๐ โ 0) โ (absโ(๐ด โ 0)) # (absโ(๐ด โ (2 ยท ๐ )))) |
131 | 62, 63, 91, 130 | apdifflemr 14731 |
. . . 4
โข (((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โง ๐ โ โ) โ ๐ด # ๐ ) |
132 | 131 | ralrimiva 2550 |
. . 3
โข ((๐ด โ โ โง
โ๐ โ โ
โ๐ โ โ
(๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐)))) โ โ๐ โ โ ๐ด # ๐ ) |
133 | 61, 132 | impbida 596 |
. 2
โข (๐ด โ โ โ
(โ๐ โ โ
๐ด # ๐ โ โ๐ โ โ โ๐ โ โ (๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))))) |
134 | 2, 133 | bitrid 192 |
1
โข (๐ด โ โ โ
(โ๐ โ โ
๐ด # ๐ โ โ๐ โ โ โ๐ โ โ (๐ โ ๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐))))) |