Proof of Theorem isabvd
Step | Hyp | Ref
| Expression |
1 | | isabvd.2 |
. . . . . 6
|
2 | | isabvd.b |
. . . . . . 7
|
3 | 2 | feq2d 6031 |
. . . . . 6
|
4 | 1, 3 | mpbid 222 |
. . . . 5
|
5 | | ffn 6045 |
. . . . 5
|
6 | 4, 5 | syl 17 |
. . . 4
|
7 | 4 | ffvelrnda 6359 |
. . . . . 6
|
8 | | 0le0 11110 |
. . . . . . . . . 10
|
9 | | isabvd.z |
. . . . . . . . . . . 12
|
10 | 9 | fveq2d 6195 |
. . . . . . . . . . 11
|
11 | | isabvd.3 |
. . . . . . . . . . 11
|
12 | 10, 11 | eqtr3d 2658 |
. . . . . . . . . 10
|
13 | 8, 12 | syl5breqr 4691 |
. . . . . . . . 9
|
14 | 13 | adantr 481 |
. . . . . . . 8
|
15 | | fveq2 6191 |
. . . . . . . . 9
|
16 | 15 | breq2d 4665 |
. . . . . . . 8
|
17 | 14, 16 | syl5ibrcom 237 |
. . . . . . 7
|
18 | | simp1 1061 |
. . . . . . . . . 10
|
19 | | simp2 1062 |
. . . . . . . . . . 11
|
20 | 2 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
21 | 19, 20 | eleqtrrd 2704 |
. . . . . . . . . 10
|
22 | | simp3 1063 |
. . . . . . . . . . 11
|
23 | 9 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
24 | 22, 23 | neeqtrrd 2868 |
. . . . . . . . . 10
|
25 | | isabvd.4 |
. . . . . . . . . 10
|
26 | 18, 21, 24, 25 | syl3anc 1326 |
. . . . . . . . 9
|
27 | | 0re 10040 |
. . . . . . . . . 10
|
28 | 7 | 3adant3 1081 |
. . . . . . . . . 10
|
29 | | ltle 10126 |
. . . . . . . . . 10
|
30 | 27, 28, 29 | sylancr 695 |
. . . . . . . . 9
|
31 | 26, 30 | mpd 15 |
. . . . . . . 8
|
32 | 31 | 3expia 1267 |
. . . . . . 7
|
33 | 17, 32 | pm2.61dne 2880 |
. . . . . 6
|
34 | | elrege0 12278 |
. . . . . 6
|
35 | 7, 33, 34 | sylanbrc 698 |
. . . . 5
|
36 | 35 | ralrimiva 2966 |
. . . 4
|
37 | | ffnfv 6388 |
. . . 4
|
38 | 6, 36, 37 | sylanbrc 698 |
. . 3
|
39 | 26 | gt0ne0d 10592 |
. . . . . . . 8
|
40 | 39 | 3expia 1267 |
. . . . . . 7
|
41 | 40 | necon4d 2818 |
. . . . . 6
|
42 | 12 | adantr 481 |
. . . . . . 7
|
43 | 15 | eqeq1d 2624 |
. . . . . . 7
|
44 | 42, 43 | syl5ibrcom 237 |
. . . . . 6
|
45 | 41, 44 | impbid 202 |
. . . . 5
|
46 | 12 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
47 | 46 | adantr 481 |
. . . . . . . . . 10
|
48 | | oveq1 6657 |
. . . . . . . . . . . 12
|
49 | | isabvd.1 |
. . . . . . . . . . . . . 14
|
50 | 49 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
51 | | simp3 1063 |
. . . . . . . . . . . . 13
|
52 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
53 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
54 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
55 | 52, 53, 54 | ringlz 18587 |
. . . . . . . . . . . . 13
|
56 | 50, 51, 55 | syl2anc 693 |
. . . . . . . . . . . 12
|
57 | 48, 56 | sylan9eqr 2678 |
. . . . . . . . . . 11
|
58 | 57 | fveq2d 6195 |
. . . . . . . . . 10
|
59 | 15, 46 | sylan9eqr 2678 |
. . . . . . . . . . . 12
|
60 | 59 | oveq1d 6665 |
. . . . . . . . . . 11
|
61 | 4 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
62 | 61, 51 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
63 | 62 | recnd 10068 |
. . . . . . . . . . . . 13
|
64 | 63 | adantr 481 |
. . . . . . . . . . . 12
|
65 | 64 | mul02d 10234 |
. . . . . . . . . . 11
|
66 | 60, 65 | eqtrd 2656 |
. . . . . . . . . 10
|
67 | 47, 58, 66 | 3eqtr4d 2666 |
. . . . . . . . 9
|
68 | 46 | adantr 481 |
. . . . . . . . . 10
|
69 | | oveq2 6658 |
. . . . . . . . . . . 12
|
70 | | simp2 1062 |
. . . . . . . . . . . . 13
|
71 | 52, 53, 54 | ringrz 18588 |
. . . . . . . . . . . . 13
|
72 | 50, 70, 71 | syl2anc 693 |
. . . . . . . . . . . 12
|
73 | 69, 72 | sylan9eqr 2678 |
. . . . . . . . . . 11
|
74 | 73 | fveq2d 6195 |
. . . . . . . . . 10
|
75 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
76 | 75, 46 | sylan9eqr 2678 |
. . . . . . . . . . . 12
|
77 | 76 | oveq2d 6666 |
. . . . . . . . . . 11
|
78 | 61, 70 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
79 | 78 | recnd 10068 |
. . . . . . . . . . . . 13
|
80 | 79 | adantr 481 |
. . . . . . . . . . . 12
|
81 | 80 | mul01d 10235 |
. . . . . . . . . . 11
|
82 | 77, 81 | eqtrd 2656 |
. . . . . . . . . 10
|
83 | 68, 74, 82 | 3eqtr4d 2666 |
. . . . . . . . 9
|
84 | | simpl1 1064 |
. . . . . . . . . . . . 13
|
85 | | isabvd.t |
. . . . . . . . . . . . 13
|
86 | 84, 85 | syl 17 |
. . . . . . . . . . . 12
|
87 | 86 | oveqd 6667 |
. . . . . . . . . . 11
|
88 | 87 | fveq2d 6195 |
. . . . . . . . . 10
|
89 | | simpl2 1065 |
. . . . . . . . . . . 12
|
90 | 84, 2 | syl 17 |
. . . . . . . . . . . 12
|
91 | 89, 90 | eleqtrrd 2704 |
. . . . . . . . . . 11
|
92 | | simprl 794 |
. . . . . . . . . . . 12
|
93 | 84, 9 | syl 17 |
. . . . . . . . . . . 12
|
94 | 92, 93 | neeqtrrd 2868 |
. . . . . . . . . . 11
|
95 | | simpl3 1066 |
. . . . . . . . . . . 12
|
96 | 95, 90 | eleqtrrd 2704 |
. . . . . . . . . . 11
|
97 | | simprr 796 |
. . . . . . . . . . . 12
|
98 | 97, 93 | neeqtrrd 2868 |
. . . . . . . . . . 11
|
99 | | isabvd.5 |
. . . . . . . . . . 11
|
100 | 84, 91, 94, 96, 98, 99 | syl122anc 1335 |
. . . . . . . . . 10
|
101 | 88, 100 | eqtr3d 2658 |
. . . . . . . . 9
|
102 | 67, 83, 101 | pm2.61da2ne 2882 |
. . . . . . . 8
|
103 | | oveq1 6657 |
. . . . . . . . . . . 12
|
104 | | ringgrp 18552 |
. . . . . . . . . . . . . 14
|
105 | 50, 104 | syl 17 |
. . . . . . . . . . . . 13
|
106 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
107 | 52, 106, 54 | grplid 17452 |
. . . . . . . . . . . . 13
|
108 | 105, 51, 107 | syl2anc 693 |
. . . . . . . . . . . 12
|
109 | 103, 108 | sylan9eqr 2678 |
. . . . . . . . . . 11
|
110 | 109 | fveq2d 6195 |
. . . . . . . . . 10
|
111 | 8, 59 | syl5breqr 4691 |
. . . . . . . . . . 11
|
112 | 62, 78 | addge02d 10616 |
. . . . . . . . . . . 12
|
113 | 112 | adantr 481 |
. . . . . . . . . . 11
|
114 | 111, 113 | mpbid 222 |
. . . . . . . . . 10
|
115 | 110, 114 | eqbrtrd 4675 |
. . . . . . . . 9
|
116 | | oveq2 6658 |
. . . . . . . . . . . 12
|
117 | 52, 106, 54 | grprid 17453 |
. . . . . . . . . . . . 13
|
118 | 105, 70, 117 | syl2anc 693 |
. . . . . . . . . . . 12
|
119 | 116, 118 | sylan9eqr 2678 |
. . . . . . . . . . 11
|
120 | 119 | fveq2d 6195 |
. . . . . . . . . 10
|
121 | 8, 76 | syl5breqr 4691 |
. . . . . . . . . . 11
|
122 | 78, 62 | addge01d 10615 |
. . . . . . . . . . . 12
|
123 | 122 | adantr 481 |
. . . . . . . . . . 11
|
124 | 121, 123 | mpbid 222 |
. . . . . . . . . 10
|
125 | 120, 124 | eqbrtrd 4675 |
. . . . . . . . 9
|
126 | | isabvd.p |
. . . . . . . . . . . . 13
|
127 | 84, 126 | syl 17 |
. . . . . . . . . . . 12
|
128 | 127 | oveqd 6667 |
. . . . . . . . . . 11
|
129 | 128 | fveq2d 6195 |
. . . . . . . . . 10
|
130 | | isabvd.6 |
. . . . . . . . . . 11
|
131 | 84, 91, 94, 96, 98, 130 | syl122anc 1335 |
. . . . . . . . . 10
|
132 | 129, 131 | eqbrtrrd 4677 |
. . . . . . . . 9
|
133 | 115, 125,
132 | pm2.61da2ne 2882 |
. . . . . . . 8
|
134 | 102, 133 | jca 554 |
. . . . . . 7
|
135 | 134 | 3expia 1267 |
. . . . . 6
|
136 | 135 | ralrimiv 2965 |
. . . . 5
|
137 | 45, 136 | jca 554 |
. . . 4
|
138 | 137 | ralrimiva 2966 |
. . 3
|
139 | | eqid 2622 |
. . . . 5
AbsVal AbsVal |
140 | 139, 52, 106, 53, 54 | isabv 18819 |
. . . 4
AbsVal
|
141 | 49, 140 | syl 17 |
. . 3
AbsVal
|
142 | 38, 138, 141 | mpbir2and 957 |
. 2
AbsVal |
143 | | isabvd.a |
. 2
AbsVal |
144 | 142, 143 | eleqtrrd 2704 |
1
|