Metamath Proof Explorer

Theorem dpmul4

Description: An upper bound to multiplication of decimal numbers with 4 digits. (Contributed by Thierry Arnoux, 25-Dec-2021)

Ref Expression
Hypotheses dpmul.a 
|- A e. NN0
dpmul.b 
|- B e. NN0
dpmul.c 
|- C e. NN0
dpmul.d 
|- D e. NN0
dpmul.e 
|- E e. NN0
dpmul.g 
|- G e. NN0
dpmul.j 
|- J e. NN0
dpmul.k 
|- K e. NN0
dpmul4.f 
|- F e. NN0
dpmul4.h 
|- H e. NN0
dpmul4.i 
|- I e. NN0
dpmul4.l 
|- L e. NN0
dpmul4.m 
|- M e. NN0
dpmul4.n 
|- N e. NN0
dpmul4.o 
|- O e. NN0
dpmul4.p 
|- P e. NN0
dpmul4.q 
|- Q e. NN0
dpmul4.r 
|- R e. NN0
dpmul4.s 
|- S e. NN0
dpmul4.t 
|- T e. NN0
dpmul4.u 
|- U e. NN0
dpmul4.w 
|- W e. NN0
dpmul4.x 
|- X e. NN0
dpmul4.y 
|- Y e. NN0
dpmul4.z 
|- Z e. NN0
dpmul4.a 
|- U < ; 1 0
dpmul4.b 
|- P < ; 1 0
dpmul4.c 
|- Q < ; 1 0
dpmul4.1 
|- ( ; ; L M N + O ) = ; ; ; R S T U
dpmul4.2 
|- ( ( A . B ) x. ( E . F ) ) = ( I . _ J K )
dpmul4.3 
|- ( ( C . D ) x. ( G . H ) ) = ( O . _ P Q )
dpmul4.4 
|- ( ; ; ; I J K 1 + ; ; R S T ) = ; ; ; W X Y Z
dpmul4.5 
|- ( ( ( A . B ) + ( C . D ) ) x. ( ( E . F ) + ( G . H ) ) ) = ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) )
Assertion dpmul4 
|- ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) ) < ( W . _ X _ Y Z )

Proof

Step Hyp Ref Expression
1 dpmul.a 
 |-  A e. NN0
2 dpmul.b 
 |-  B e. NN0
3 dpmul.c 
 |-  C e. NN0
4 dpmul.d 
 |-  D e. NN0
5 dpmul.e 
 |-  E e. NN0
6 dpmul.g 
 |-  G e. NN0
7 dpmul.j 
 |-  J e. NN0
8 dpmul.k 
 |-  K e. NN0
9 dpmul4.f 
 |-  F e. NN0
10 dpmul4.h 
 |-  H e. NN0
11 dpmul4.i 
 |-  I e. NN0
12 dpmul4.l 
 |-  L e. NN0
13 dpmul4.m 
 |-  M e. NN0
14 dpmul4.n 
 |-  N e. NN0
15 dpmul4.o 
 |-  O e. NN0
16 dpmul4.p 
 |-  P e. NN0
17 dpmul4.q 
 |-  Q e. NN0
18 dpmul4.r 
 |-  R e. NN0
19 dpmul4.s 
 |-  S e. NN0
20 dpmul4.t 
 |-  T e. NN0
21 dpmul4.u 
 |-  U e. NN0
22 dpmul4.w 
 |-  W e. NN0
23 dpmul4.x 
 |-  X e. NN0
24 dpmul4.y 
 |-  Y e. NN0
25 dpmul4.z 
 |-  Z e. NN0
26 dpmul4.a 
 |-  U < ; 1 0
27 dpmul4.b 
 |-  P < ; 1 0
28 dpmul4.c 
 |-  Q < ; 1 0
29 dpmul4.1 
 |-  ( ; ; L M N + O ) = ; ; ; R S T U
30 dpmul4.2 
 |-  ( ( A . B ) x. ( E . F ) ) = ( I . _ J K )
31 dpmul4.3 
 |-  ( ( C . D ) x. ( G . H ) ) = ( O . _ P Q )
32 dpmul4.4 
 |-  ( ; ; ; I J K 1 + ; ; R S T ) = ; ; ; W X Y Z
33 dpmul4.5 
 |-  ( ( ( A . B ) + ( C . D ) ) x. ( ( E . F ) + ( G . H ) ) ) = ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) )
34 1 2 deccl 
 |-  ; A B e. NN0
35 3 4 deccl 
 |-  ; C D e. NN0
36 5 9 deccl 
 |-  ; E F e. NN0
37 6 10 deccl 
 |-  ; G H e. NN0
38 12 13 deccl 
 |-  ; L M e. NN0
39 38 14 deccl 
 |-  ; ; L M N e. NN0
40 2nn0 
 |-  2 e. NN0
41 2 nn0rei 
 |-  B e. RR
42 dpcl 
 |-  ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) e. RR )
43 1 41 42 mp2an 
 |-  ( A . B ) e. RR
44 43 recni 
 |-  ( A . B ) e. CC
45 10nn 
 |-  ; 1 0 e. NN
46 45 nncni 
 |-  ; 1 0 e. CC
47 9 nn0rei 
 |-  F e. RR
48 dpcl 
 |-  ( ( E e. NN0 /\ F e. RR ) -> ( E . F ) e. RR )
49 5 47 48 mp2an 
 |-  ( E . F ) e. RR
50 49 recni 
 |-  ( E . F ) e. CC
51 44 46 50 46 mul4i 
 |-  ( ( ( A . B ) x. ; 1 0 ) x. ( ( E . F ) x. ; 1 0 ) ) = ( ( ( A . B ) x. ( E . F ) ) x. ( ; 1 0 x. ; 1 0 ) )
52 44 50 mulcli 
 |-  ( ( A . B ) x. ( E . F ) ) e. CC
53 52 46 46 mulassi 
 |-  ( ( ( ( A . B ) x. ( E . F ) ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ( A . B ) x. ( E . F ) ) x. ( ; 1 0 x. ; 1 0 ) )
54 30 oveq1i 
 |-  ( ( ( A . B ) x. ( E . F ) ) x. ; 1 0 ) = ( ( I . _ J K ) x. ; 1 0 )
55 8 nn0rei 
 |-  K e. RR
56 11 7 55 dp3mul10 
 |-  ( ( I . _ J K ) x. ; 1 0 ) = ( ; I J . K )
57 54 56 eqtri 
 |-  ( ( ( A . B ) x. ( E . F ) ) x. ; 1 0 ) = ( ; I J . K )
58 57 oveq1i 
 |-  ( ( ( ( A . B ) x. ( E . F ) ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ; I J . K ) x. ; 1 0 )
59 51 53 58 3eqtr2ri 
 |-  ( ( ; I J . K ) x. ; 1 0 ) = ( ( ( A . B ) x. ; 1 0 ) x. ( ( E . F ) x. ; 1 0 ) )
60 11 7 deccl 
 |-  ; I J e. NN0
61 60 55 dpmul10 
 |-  ( ( ; I J . K ) x. ; 1 0 ) = ; ; I J K
62 1 41 dpmul10 
 |-  ( ( A . B ) x. ; 1 0 ) = ; A B
63 5 47 dpmul10 
 |-  ( ( E . F ) x. ; 1 0 ) = ; E F
64 62 63 oveq12i 
 |-  ( ( ( A . B ) x. ; 1 0 ) x. ( ( E . F ) x. ; 1 0 ) ) = ( ; A B x. ; E F )
65 59 61 64 3eqtr3ri 
 |-  ( ; A B x. ; E F ) = ; ; I J K
66 4 nn0rei 
 |-  D e. RR
67 dpcl 
 |-  ( ( C e. NN0 /\ D e. RR ) -> ( C . D ) e. RR )
68 3 66 67 mp2an 
 |-  ( C . D ) e. RR
69 68 recni 
 |-  ( C . D ) e. CC
70 10 nn0rei 
 |-  H e. RR
71 dpcl 
 |-  ( ( G e. NN0 /\ H e. RR ) -> ( G . H ) e. RR )
72 6 70 71 mp2an 
 |-  ( G . H ) e. RR
73 72 recni 
 |-  ( G . H ) e. CC
74 69 46 73 46 mul4i 
 |-  ( ( ( C . D ) x. ; 1 0 ) x. ( ( G . H ) x. ; 1 0 ) ) = ( ( ( C . D ) x. ( G . H ) ) x. ( ; 1 0 x. ; 1 0 ) )
75 69 73 mulcli 
 |-  ( ( C . D ) x. ( G . H ) ) e. CC
76 75 46 46 mulassi 
 |-  ( ( ( ( C . D ) x. ( G . H ) ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ( C . D ) x. ( G . H ) ) x. ( ; 1 0 x. ; 1 0 ) )
77 31 oveq1i 
 |-  ( ( ( C . D ) x. ( G . H ) ) x. ; 1 0 ) = ( ( O . _ P Q ) x. ; 1 0 )
78 17 nn0rei 
 |-  Q e. RR
79 15 16 78 dp3mul10 
 |-  ( ( O . _ P Q ) x. ; 1 0 ) = ( ; O P . Q )
80 77 79 eqtri 
 |-  ( ( ( C . D ) x. ( G . H ) ) x. ; 1 0 ) = ( ; O P . Q )
81 80 oveq1i 
 |-  ( ( ( ( C . D ) x. ( G . H ) ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ; O P . Q ) x. ; 1 0 )
82 74 76 81 3eqtr2ri 
 |-  ( ( ; O P . Q ) x. ; 1 0 ) = ( ( ( C . D ) x. ; 1 0 ) x. ( ( G . H ) x. ; 1 0 ) )
83 15 16 deccl 
 |-  ; O P e. NN0
84 83 78 dpmul10 
 |-  ( ( ; O P . Q ) x. ; 1 0 ) = ; ; O P Q
85 3 66 dpmul10 
 |-  ( ( C . D ) x. ; 1 0 ) = ; C D
86 6 70 dpmul10 
 |-  ( ( G . H ) x. ; 1 0 ) = ; G H
87 85 86 oveq12i 
 |-  ( ( ( C . D ) x. ; 1 0 ) x. ( ( G . H ) x. ; 1 0 ) ) = ( ; C D x. ; G H )
88 82 84 87 3eqtr3ri 
 |-  ( ; C D x. ; G H ) = ; ; O P Q
89 44 69 46 adddiri 
 |-  ( ( ( A . B ) + ( C . D ) ) x. ; 1 0 ) = ( ( ( A . B ) x. ; 1 0 ) + ( ( C . D ) x. ; 1 0 ) )
90 62 85 oveq12i 
 |-  ( ( ( A . B ) x. ; 1 0 ) + ( ( C . D ) x. ; 1 0 ) ) = ( ; A B + ; C D )
91 89 90 eqtr2i 
 |-  ( ; A B + ; C D ) = ( ( ( A . B ) + ( C . D ) ) x. ; 1 0 )
92 50 73 46 adddiri 
 |-  ( ( ( E . F ) + ( G . H ) ) x. ; 1 0 ) = ( ( ( E . F ) x. ; 1 0 ) + ( ( G . H ) x. ; 1 0 ) )
93 63 86 oveq12i 
 |-  ( ( ( E . F ) x. ; 1 0 ) + ( ( G . H ) x. ; 1 0 ) ) = ( ; E F + ; G H )
94 92 93 eqtr2i 
 |-  ( ; E F + ; G H ) = ( ( ( E . F ) + ( G . H ) ) x. ; 1 0 )
95 91 94 oveq12i 
 |-  ( ( ; A B + ; C D ) x. ( ; E F + ; G H ) ) = ( ( ( ( A . B ) + ( C . D ) ) x. ; 1 0 ) x. ( ( ( E . F ) + ( G . H ) ) x. ; 1 0 ) )
96 44 69 addcli 
 |-  ( ( A . B ) + ( C . D ) ) e. CC
97 50 73 addcli 
 |-  ( ( E . F ) + ( G . H ) ) e. CC
98 96 46 97 46 mul4i 
 |-  ( ( ( ( A . B ) + ( C . D ) ) x. ; 1 0 ) x. ( ( ( E . F ) + ( G . H ) ) x. ; 1 0 ) ) = ( ( ( ( A . B ) + ( C . D ) ) x. ( ( E . F ) + ( G . H ) ) ) x. ( ; 1 0 x. ; 1 0 ) )
99 33 oveq1i 
 |-  ( ( ( ( A . B ) + ( C . D ) ) x. ( ( E . F ) + ( G . H ) ) ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ( ; 1 0 x. ; 1 0 ) )
100 95 98 99 3eqtri 
 |-  ( ( ; A B + ; C D ) x. ( ; E F + ; G H ) ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ( ; 1 0 x. ; 1 0 ) )
101 10nn0 
 |-  ; 1 0 e. NN0
102 101 dec0u 
 |-  ( ; 1 0 x. ; 1 0 ) = ; ; 1 0 0
103 102 oveq2i 
 |-  ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ; ; 1 0 0 )
104 30 52 eqeltrri 
 |-  ( I . _ J K ) e. CC
105 13 nn0rei 
 |-  M e. RR
106 14 nn0rei 
 |-  N e. RR
107 dp2cl 
 |-  ( ( M e. RR /\ N e. RR ) -> _ M N e. RR )
108 105 106 107 mp2an 
 |-  _ M N e. RR
109 dpcl 
 |-  ( ( L e. NN0 /\ _ M N e. RR ) -> ( L . _ M N ) e. RR )
110 12 108 109 mp2an 
 |-  ( L . _ M N ) e. RR
111 110 recni 
 |-  ( L . _ M N ) e. CC
112 104 111 addcli 
 |-  ( ( I . _ J K ) + ( L . _ M N ) ) e. CC
113 31 75 eqeltrri 
 |-  ( O . _ P Q ) e. CC
114 0nn0 
 |-  0 e. NN0
115 101 114 deccl 
 |-  ; ; 1 0 0 e. NN0
116 115 nn0cni 
 |-  ; ; 1 0 0 e. CC
117 112 113 116 adddiri 
 |-  ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ; ; 1 0 0 ) = ( ( ( ( I . _ J K ) + ( L . _ M N ) ) x. ; ; 1 0 0 ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) )
118 104 111 116 adddiri 
 |-  ( ( ( I . _ J K ) + ( L . _ M N ) ) x. ; ; 1 0 0 ) = ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) )
119 118 oveq1i 
 |-  ( ( ( ( I . _ J K ) + ( L . _ M N ) ) x. ; ; 1 0 0 ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) ) = ( ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) )
120 11 7 55 dpmul100 
 |-  ( ( I . _ J K ) x. ; ; 1 0 0 ) = ; ; I J K
121 12 13 106 dpmul100 
 |-  ( ( L . _ M N ) x. ; ; 1 0 0 ) = ; ; L M N
122 120 121 oveq12i 
 |-  ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) = ( ; ; I J K + ; ; L M N )
123 15 16 78 dpmul100 
 |-  ( ( O . _ P Q ) x. ; ; 1 0 0 ) = ; ; O P Q
124 122 123 oveq12i 
 |-  ( ( ( ( I . _ J K ) x. ; ; 1 0 0 ) + ( ( L . _ M N ) x. ; ; 1 0 0 ) ) + ( ( O . _ P Q ) x. ; ; 1 0 0 ) ) = ( ( ; ; I J K + ; ; L M N ) + ; ; O P Q )
125 117 119 124 3eqtri 
 |-  ( ( ( ( I . _ J K ) + ( L . _ M N ) ) + ( O . _ P Q ) ) x. ; ; 1 0 0 ) = ( ( ; ; I J K + ; ; L M N ) + ; ; O P Q )
126 100 103 125 3eqtri 
 |-  ( ( ; A B + ; C D ) x. ( ; E F + ; G H ) ) = ( ( ; ; I J K + ; ; L M N ) + ; ; O P Q )
127 sq10 
 |-  ( ; 1 0 ^ 2 ) = ; ; 1 0 0
128 127 oveq2i 
 |-  ( ; A B x. ( ; 1 0 ^ 2 ) ) = ( ; A B x. ; ; 1 0 0 )
129 34 nn0cni 
 |-  ; A B e. CC
130 116 129 mulcomi 
 |-  ( ; ; 1 0 0 x. ; A B ) = ( ; A B x. ; ; 1 0 0 )
131 128 130 eqtr4i 
 |-  ( ; A B x. ( ; 1 0 ^ 2 ) ) = ( ; ; 1 0 0 x. ; A B )
132 131 oveq1i 
 |-  ( ( ; A B x. ( ; 1 0 ^ 2 ) ) + ; C D ) = ( ( ; ; 1 0 0 x. ; A B ) + ; C D )
133 34 3 66 dfdec100 
 |-  ; ; ; A B C D = ( ( ; ; 1 0 0 x. ; A B ) + ; C D )
134 132 133 eqtr4i 
 |-  ( ( ; A B x. ( ; 1 0 ^ 2 ) ) + ; C D ) = ; ; ; A B C D
135 127 oveq2i 
 |-  ( ; E F x. ( ; 1 0 ^ 2 ) ) = ( ; E F x. ; ; 1 0 0 )
136 36 nn0cni 
 |-  ; E F e. CC
137 116 136 mulcomi 
 |-  ( ; ; 1 0 0 x. ; E F ) = ( ; E F x. ; ; 1 0 0 )
138 135 137 eqtr4i 
 |-  ( ; E F x. ( ; 1 0 ^ 2 ) ) = ( ; ; 1 0 0 x. ; E F )
139 138 oveq1i 
 |-  ( ( ; E F x. ( ; 1 0 ^ 2 ) ) + ; G H ) = ( ( ; ; 1 0 0 x. ; E F ) + ; G H )
140 36 6 70 dfdec100 
 |-  ; ; ; E F G H = ( ( ; ; 1 0 0 x. ; E F ) + ; G H )
141 139 140 eqtr4i 
 |-  ( ( ; E F x. ( ; 1 0 ^ 2 ) ) + ; G H ) = ; ; ; E F G H
142 46 sqvali 
 |-  ( ; 1 0 ^ 2 ) = ( ; 1 0 x. ; 1 0 )
143 142 oveq2i 
 |-  ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) = ( ; ; I J K x. ( ; 1 0 x. ; 1 0 ) )
144 60 8 deccl 
 |-  ; ; I J K e. NN0
145 144 nn0cni 
 |-  ; ; I J K e. CC
146 145 46 46 mulassi 
 |-  ( ( ; ; I J K x. ; 1 0 ) x. ; 1 0 ) = ( ; ; I J K x. ( ; 1 0 x. ; 1 0 ) )
147 143 146 eqtr4i 
 |-  ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) = ( ( ; ; I J K x. ; 1 0 ) x. ; 1 0 )
148 18 19 deccl 
 |-  ; R S e. NN0
149 148 20 deccl 
 |-  ; ; R S T e. NN0
150 149 nn0cni 
 |-  ; ; R S T e. CC
151 ax-1cn 
 |-  1 e. CC
152 150 151 addcli 
 |-  ( ; ; R S T + 1 ) e. CC
153 145 46 mulcli 
 |-  ( ; ; I J K x. ; 1 0 ) e. CC
154 151 153 addcomi 
 |-  ( 1 + ( ; ; I J K x. ; 1 0 ) ) = ( ( ; ; I J K x. ; 1 0 ) + 1 )
155 46 145 mulcomi 
 |-  ( ; 1 0 x. ; ; I J K ) = ( ; ; I J K x. ; 1 0 )
156 144 dec0u 
 |-  ( ; 1 0 x. ; ; I J K ) = ; ; ; I J K 0
157 155 156 eqtr3i 
 |-  ( ; ; I J K x. ; 1 0 ) = ; ; ; I J K 0
158 157 oveq1i 
 |-  ( ( ; ; I J K x. ; 1 0 ) + 1 ) = ( ; ; ; I J K 0 + 1 )
159 151 addid2i 
 |-  ( 0 + 1 ) = 1
160 eqid 
 |-  ; ; ; I J K 0 = ; ; ; I J K 0
161 144 114 159 160 decsuc 
 |-  ( ; ; ; I J K 0 + 1 ) = ; ; ; I J K 1
162 154 158 161 3eqtri 
 |-  ( 1 + ( ; ; I J K x. ; 1 0 ) ) = ; ; ; I J K 1
163 162 oveq2i 
 |-  ( ; ; R S T + ( 1 + ( ; ; I J K x. ; 1 0 ) ) ) = ( ; ; R S T + ; ; ; I J K 1 )
164 150 151 153 addassi 
 |-  ( ( ; ; R S T + 1 ) + ( ; ; I J K x. ; 1 0 ) ) = ( ; ; R S T + ( 1 + ( ; ; I J K x. ; 1 0 ) ) )
165 1nn0 
 |-  1 e. NN0
166 144 165 deccl 
 |-  ; ; ; I J K 1 e. NN0
167 166 nn0cni 
 |-  ; ; ; I J K 1 e. CC
168 167 150 addcomi 
 |-  ( ; ; ; I J K 1 + ; ; R S T ) = ( ; ; R S T + ; ; ; I J K 1 )
169 163 164 168 3eqtr4i 
 |-  ( ( ; ; R S T + 1 ) + ( ; ; I J K x. ; 1 0 ) ) = ( ; ; ; I J K 1 + ; ; R S T )
170 169 32 eqtri 
 |-  ( ( ; ; R S T + 1 ) + ( ; ; I J K x. ; 1 0 ) ) = ; ; ; W X Y Z
171 152 153 170 mvlladdi 
 |-  ( ; ; I J K x. ; 1 0 ) = ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) )
172 171 oveq1i 
 |-  ( ( ; ; I J K x. ; 1 0 ) x. ; 1 0 ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 )
173 147 172 eqtri 
 |-  ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 )
174 173 oveq1i 
 |-  ( ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) + ; ; L M N ) = ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N )
175 eqid 
 |-  ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) = ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q )
176 34 35 36 37 39 40 65 88 126 134 141 174 175 karatsuba 
 |-  ( ; ; ; A B C D x. ; ; ; E F G H ) = ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q )
177 22 23 deccl 
 |-  ; W X e. NN0
178 177 24 deccl 
 |-  ; ; W X Y e. NN0
179 178 25 deccl 
 |-  ; ; ; W X Y Z e. NN0
180 179 nn0cni 
 |-  ; ; ; W X Y Z e. CC
181 115 114 deccl 
 |-  ; ; ; 1 0 0 0 e. NN0
182 181 nn0cni 
 |-  ; ; ; 1 0 0 0 e. CC
183 180 182 mulcli 
 |-  ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. CC
184 152 182 mulcli 
 |-  ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) e. CC
185 183 184 subcli 
 |-  ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) e. CC
186 39 nn0cni 
 |-  ; ; L M N e. CC
187 116 186 mulcli 
 |-  ( ; ; 1 0 0 x. ; ; L M N ) e. CC
188 15 16 78 dfdec100 
 |-  ; ; O P Q = ( ( ; ; 1 0 0 x. O ) + ; P Q )
189 83 17 deccl 
 |-  ; ; O P Q e. NN0
190 189 nn0cni 
 |-  ; ; O P Q e. CC
191 188 190 eqeltrri 
 |-  ( ( ; ; 1 0 0 x. O ) + ; P Q ) e. CC
192 185 187 191 addassi 
 |-  ( ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) )
193 46 sqcli 
 |-  ( ; 1 0 ^ 2 ) e. CC
194 145 193 mulcli 
 |-  ( ; ; I J K x. ( ; 1 0 ^ 2 ) ) e. CC
195 173 194 eqeltrri 
 |-  ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) e. CC
196 195 186 116 adddiri 
 |-  ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ; ; 1 0 0 ) = ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) + ( ; ; L M N x. ; ; 1 0 0 ) )
197 127 oveq2i 
 |-  ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) = ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ; ; 1 0 0 )
198 180 152 subcli 
 |-  ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) e. CC
199 198 46 116 mulassi 
 |-  ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ( ; 1 0 x. ; ; 1 0 0 ) )
200 115 dec0u 
 |-  ( ; 1 0 x. ; ; 1 0 0 ) = ; ; ; 1 0 0 0
201 200 oveq2i 
 |-  ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ( ; 1 0 x. ; ; 1 0 0 ) ) = ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; ; ; 1 0 0 0 )
202 180 152 182 subdiri 
 |-  ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; ; ; 1 0 0 0 ) = ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) )
203 199 201 202 3eqtrri 
 |-  ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) = ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 )
204 116 186 mulcomi 
 |-  ( ; ; 1 0 0 x. ; ; L M N ) = ( ; ; L M N x. ; ; 1 0 0 )
205 203 204 oveq12i 
 |-  ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) = ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) x. ; ; 1 0 0 ) + ( ; ; L M N x. ; ; 1 0 0 ) )
206 196 197 205 3eqtr4i 
 |-  ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) )
207 206 188 oveq12i 
 |-  ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q ) = ( ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ; ; 1 0 0 x. ; ; L M N ) ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) )
208 187 191 addcli 
 |-  ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) e. CC
209 subsub 
 |-  ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. CC /\ ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) e. CC /\ ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) e. CC ) -> ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) )
210 183 184 208 209 mp3an 
 |-  ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) = ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) ) + ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) )
211 192 207 210 3eqtr4ri 
 |-  ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) = ( ( ( ( ( ; ; ; W X Y Z - ( ; ; R S T + 1 ) ) x. ; 1 0 ) + ; ; L M N ) x. ( ; 1 0 ^ 2 ) ) + ; ; O P Q )
212 176 211 eqtr4i 
 |-  ( ; ; ; A B C D x. ; ; ; E F G H ) = ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) )
213 179 nn0rei 
 |-  ; ; ; W X Y Z e. RR
214 181 nn0rei 
 |-  ; ; ; 1 0 0 0 e. RR
215 213 214 remulcli 
 |-  ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. RR
216 149 nn0rei 
 |-  ; ; R S T e. RR
217 1re 
 |-  1 e. RR
218 216 217 readdcli 
 |-  ( ; ; R S T + 1 ) e. RR
219 218 214 remulcli 
 |-  ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) e. RR
220 115 nn0rei 
 |-  ; ; 1 0 0 e. RR
221 39 nn0rei 
 |-  ; ; L M N e. RR
222 220 221 remulcli 
 |-  ( ; ; 1 0 0 x. ; ; L M N ) e. RR
223 15 nn0rei 
 |-  O e. RR
224 220 223 remulcli 
 |-  ( ; ; 1 0 0 x. O ) e. RR
225 16 17 deccl 
 |-  ; P Q e. NN0
226 225 nn0rei 
 |-  ; P Q e. RR
227 224 226 readdcli 
 |-  ( ( ; ; 1 0 0 x. O ) + ; P Q ) e. RR
228 222 227 readdcli 
 |-  ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) e. RR
229 219 228 resubcli 
 |-  ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR
230 224 recni 
 |-  ( ; ; 1 0 0 x. O ) e. CC
231 226 recni 
 |-  ; P Q e. CC
232 187 230 231 addassi 
 |-  ( ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) + ; P Q ) = ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) )
233 223 recni 
 |-  O e. CC
234 116 186 233 adddii 
 |-  ( ; ; 1 0 0 x. ( ; ; L M N + O ) ) = ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) )
235 29 oveq2i 
 |-  ( ; ; 1 0 0 x. ( ; ; L M N + O ) ) = ( ; ; 1 0 0 x. ; ; ; R S T U )
236 234 235 eqtr3i 
 |-  ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) = ( ; ; 1 0 0 x. ; ; ; R S T U )
237 236 oveq1i 
 |-  ( ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ; ; 1 0 0 x. O ) ) + ; P Q ) = ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q )
238 232 237 eqtr3i 
 |-  ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) = ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q )
239 21 101 16 114 17 114 26 27 28 3decltc 
 |-  ; ; U P Q < ; ; ; 1 0 0 0
240 21 16 deccl 
 |-  ; U P e. NN0
241 240 17 deccl 
 |-  ; ; U P Q e. NN0
242 241 nn0rei 
 |-  ; ; U P Q e. RR
243 216 214 remulcli 
 |-  ( ; ; R S T x. ; ; ; 1 0 0 0 ) e. RR
244 242 214 243 ltadd2i 
 |-  ( ; ; U P Q < ; ; ; 1 0 0 0 <-> ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) < ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 ) )
245 239 244 mpbi 
 |-  ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) < ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 )
246 150 182 mulcli 
 |-  ( ; ; R S T x. ; ; ; 1 0 0 0 ) e. CC
247 21 nn0cni 
 |-  U e. CC
248 116 247 mulcli 
 |-  ( ; ; 1 0 0 x. U ) e. CC
249 246 248 231 addassi 
 |-  ( ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) ) + ; P Q ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ( ; ; 1 0 0 x. U ) + ; P Q ) )
250 dfdec10 
 |-  ; ; ; R S T U = ( ( ; 1 0 x. ; ; R S T ) + U )
251 250 oveq2i 
 |-  ( ; ; 1 0 0 x. ; ; ; R S T U ) = ( ; ; 1 0 0 x. ( ( ; 1 0 x. ; ; R S T ) + U ) )
252 46 150 mulcli 
 |-  ( ; 1 0 x. ; ; R S T ) e. CC
253 116 252 247 adddii 
 |-  ( ; ; 1 0 0 x. ( ( ; 1 0 x. ; ; R S T ) + U ) ) = ( ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) + ( ; ; 1 0 0 x. U ) )
254 150 182 mulcomi 
 |-  ( ; ; R S T x. ; ; ; 1 0 0 0 ) = ( ; ; ; 1 0 0 0 x. ; ; R S T )
255 46 116 mulcomi 
 |-  ( ; 1 0 x. ; ; 1 0 0 ) = ( ; ; 1 0 0 x. ; 1 0 )
256 255 200 eqtr3i 
 |-  ( ; ; 1 0 0 x. ; 1 0 ) = ; ; ; 1 0 0 0
257 256 oveq1i 
 |-  ( ( ; ; 1 0 0 x. ; 1 0 ) x. ; ; R S T ) = ( ; ; ; 1 0 0 0 x. ; ; R S T )
258 116 46 150 mulassi 
 |-  ( ( ; ; 1 0 0 x. ; 1 0 ) x. ; ; R S T ) = ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) )
259 254 257 258 3eqtr2ri 
 |-  ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) = ( ; ; R S T x. ; ; ; 1 0 0 0 )
260 259 oveq1i 
 |-  ( ( ; ; 1 0 0 x. ( ; 1 0 x. ; ; R S T ) ) + ( ; ; 1 0 0 x. U ) ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) )
261 251 253 260 3eqtri 
 |-  ( ; ; 1 0 0 x. ; ; ; R S T U ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) )
262 261 oveq1i 
 |-  ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) = ( ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ; ; 1 0 0 x. U ) ) + ; P Q )
263 21 16 78 dfdec100 
 |-  ; ; U P Q = ( ( ; ; 1 0 0 x. U ) + ; P Q )
264 263 oveq2i 
 |-  ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( ( ; ; 1 0 0 x. U ) + ; P Q ) )
265 249 262 264 3eqtr4i 
 |-  ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; U P Q )
266 150 151 182 adddiri 
 |-  ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( 1 x. ; ; ; 1 0 0 0 ) )
267 182 mulid2i 
 |-  ( 1 x. ; ; ; 1 0 0 0 ) = ; ; ; 1 0 0 0
268 267 oveq2i 
 |-  ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ( 1 x. ; ; ; 1 0 0 0 ) ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 )
269 266 268 eqtri 
 |-  ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) = ( ( ; ; R S T x. ; ; ; 1 0 0 0 ) + ; ; ; 1 0 0 0 )
270 245 265 269 3brtr4i 
 |-  ( ( ; ; 1 0 0 x. ; ; ; R S T U ) + ; P Q ) < ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 )
271 238 270 eqbrtri 
 |-  ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) < ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 )
272 228 219 posdifi 
 |-  ( ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) < ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) <-> 0 < ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) )
273 271 272 mpbi 
 |-  0 < ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) )
274 elrp 
 |-  ( ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR+ <-> ( ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR /\ 0 < ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) )
275 229 273 274 mpbir2an 
 |-  ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR+
276 ltsubrp 
 |-  ( ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. RR /\ ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) e. RR+ ) -> ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) )
277 215 275 276 mp2an 
 |-  ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) - ( ( ( ; ; R S T + 1 ) x. ; ; ; 1 0 0 0 ) - ( ( ; ; 1 0 0 x. ; ; L M N ) + ( ( ; ; 1 0 0 x. O ) + ; P Q ) ) ) ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 )
278 212 277 eqbrtri 
 |-  ( ; ; ; A B C D x. ; ; ; E F G H ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 )
279 34 3 deccl 
 |-  ; ; A B C e. NN0
280 279 4 deccl 
 |-  ; ; ; A B C D e. NN0
281 280 nn0rei 
 |-  ; ; ; A B C D e. RR
282 36 6 deccl 
 |-  ; ; E F G e. NN0
283 282 10 deccl 
 |-  ; ; ; E F G H e. NN0
284 283 nn0rei 
 |-  ; ; ; E F G H e. RR
285 281 284 remulcli 
 |-  ( ; ; ; A B C D x. ; ; ; E F G H ) e. RR
286 45 decnncl2 
 |-  ; ; 1 0 0 e. NN
287 286 decnncl2 
 |-  ; ; ; 1 0 0 0 e. NN
288 287 nngt0i 
 |-  0 < ; ; ; 1 0 0 0
289 214 288 pm3.2i 
 |-  ( ; ; ; 1 0 0 0 e. RR /\ 0 < ; ; ; 1 0 0 0 )
290 ltdiv1 
 |-  ( ( ( ; ; ; A B C D x. ; ; ; E F G H ) e. RR /\ ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) e. RR /\ ( ; ; ; 1 0 0 0 e. RR /\ 0 < ; ; ; 1 0 0 0 ) ) -> ( ( ; ; ; A B C D x. ; ; ; E F G H ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) <-> ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) ) )
291 285 215 289 290 mp3an 
 |-  ( ( ; ; ; A B C D x. ; ; ; E F G H ) < ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) <-> ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) )
292 278 291 mpbi 
 |-  ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 )
293 280 nn0cni 
 |-  ; ; ; A B C D e. CC
294 283 nn0cni 
 |-  ; ; ; E F G H e. CC
295 214 288 gt0ne0ii 
 |-  ; ; ; 1 0 0 0 =/= 0
296 293 294 182 295 div23i 
 |-  ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) x. ; ; ; E F G H )
297 1 2 3 66 dpmul1000 
 |-  ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) = ; ; ; A B C D
298 297 oveq1i 
 |-  ( ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; A B C D / ; ; ; 1 0 0 0 )
299 3 nn0rei 
 |-  C e. RR
300 dp2cl 
 |-  ( ( C e. RR /\ D e. RR ) -> _ C D e. RR )
301 299 66 300 mp2an 
 |-  _ C D e. RR
302 dp2cl 
 |-  ( ( B e. RR /\ _ C D e. RR ) -> _ B _ C D e. RR )
303 41 301 302 mp2an 
 |-  _ B _ C D e. RR
304 dpcl 
 |-  ( ( A e. NN0 /\ _ B _ C D e. RR ) -> ( A . _ B _ C D ) e. RR )
305 1 303 304 mp2an 
 |-  ( A . _ B _ C D ) e. RR
306 305 recni 
 |-  ( A . _ B _ C D ) e. CC
307 306 182 295 divcan4i 
 |-  ( ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( A . _ B _ C D )
308 298 307 eqtr3i 
 |-  ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) = ( A . _ B _ C D )
309 308 oveq1i 
 |-  ( ( ; ; ; A B C D / ; ; ; 1 0 0 0 ) x. ; ; ; E F G H ) = ( ( A . _ B _ C D ) x. ; ; ; E F G H )
310 296 309 eqtri 
 |-  ( ( ; ; ; A B C D x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( A . _ B _ C D ) x. ; ; ; E F G H )
311 180 182 295 divcan4i 
 |-  ( ( ; ; ; W X Y Z x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ; ; ; W X Y Z
312 292 310 311 3brtr3i 
 |-  ( ( A . _ B _ C D ) x. ; ; ; E F G H ) < ; ; ; W X Y Z
313 305 284 remulcli 
 |-  ( ( A . _ B _ C D ) x. ; ; ; E F G H ) e. RR
314 ltdiv1 
 |-  ( ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) e. RR /\ ; ; ; W X Y Z e. RR /\ ( ; ; ; 1 0 0 0 e. RR /\ 0 < ; ; ; 1 0 0 0 ) ) -> ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) < ; ; ; W X Y Z <-> ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) ) )
315 313 213 289 314 mp3an 
 |-  ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) < ; ; ; W X Y Z <-> ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) )
316 312 315 mpbi 
 |-  ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) < ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 )
317 306 294 182 295 divassi 
 |-  ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( A . _ B _ C D ) x. ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) )
318 5 9 6 70 dpmul1000 
 |-  ( ( E . _ F _ G H ) x. ; ; ; 1 0 0 0 ) = ; ; ; E F G H
319 318 oveq1i 
 |-  ( ( ( E . _ F _ G H ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; E F G H / ; ; ; 1 0 0 0 )
320 6 nn0rei 
 |-  G e. RR
321 dp2cl 
 |-  ( ( G e. RR /\ H e. RR ) -> _ G H e. RR )
322 320 70 321 mp2an 
 |-  _ G H e. RR
323 dp2cl 
 |-  ( ( F e. RR /\ _ G H e. RR ) -> _ F _ G H e. RR )
324 47 322 323 mp2an 
 |-  _ F _ G H e. RR
325 dpcl 
 |-  ( ( E e. NN0 /\ _ F _ G H e. RR ) -> ( E . _ F _ G H ) e. RR )
326 5 324 325 mp2an 
 |-  ( E . _ F _ G H ) e. RR
327 326 recni 
 |-  ( E . _ F _ G H ) e. CC
328 327 182 295 divcan4i 
 |-  ( ( ( E . _ F _ G H ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( E . _ F _ G H )
329 319 328 eqtr3i 
 |-  ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) = ( E . _ F _ G H )
330 329 oveq2i 
 |-  ( ( A . _ B _ C D ) x. ( ; ; ; E F G H / ; ; ; 1 0 0 0 ) ) = ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) )
331 317 330 eqtri 
 |-  ( ( ( A . _ B _ C D ) x. ; ; ; E F G H ) / ; ; ; 1 0 0 0 ) = ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) )
332 25 nn0rei 
 |-  Z e. RR
333 22 23 24 332 dpmul1000 
 |-  ( ( W . _ X _ Y Z ) x. ; ; ; 1 0 0 0 ) = ; ; ; W X Y Z
334 333 oveq1i 
 |-  ( ( ( W . _ X _ Y Z ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 )
335 23 nn0rei 
 |-  X e. RR
336 24 nn0rei 
 |-  Y e. RR
337 dp2cl 
 |-  ( ( Y e. RR /\ Z e. RR ) -> _ Y Z e. RR )
338 336 332 337 mp2an 
 |-  _ Y Z e. RR
339 dp2cl 
 |-  ( ( X e. RR /\ _ Y Z e. RR ) -> _ X _ Y Z e. RR )
340 335 338 339 mp2an 
 |-  _ X _ Y Z e. RR
341 dpcl 
 |-  ( ( W e. NN0 /\ _ X _ Y Z e. RR ) -> ( W . _ X _ Y Z ) e. RR )
342 22 340 341 mp2an 
 |-  ( W . _ X _ Y Z ) e. RR
343 342 recni 
 |-  ( W . _ X _ Y Z ) e. CC
344 343 182 295 divcan4i 
 |-  ( ( ( W . _ X _ Y Z ) x. ; ; ; 1 0 0 0 ) / ; ; ; 1 0 0 0 ) = ( W . _ X _ Y Z )
345 334 344 eqtr3i 
 |-  ( ; ; ; W X Y Z / ; ; ; 1 0 0 0 ) = ( W . _ X _ Y Z )
346 316 331 345 3brtr3i 
 |-  ( ( A . _ B _ C D ) x. ( E . _ F _ G H ) ) < ( W . _ X _ Y Z )