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 ⊢ 𝐴 ∈ ℕ0
dpmul.b ⊢ 𝐵 ∈ ℕ0
dpmul.c ⊢ 𝐶 ∈ ℕ0
dpmul.d ⊢ 𝐷 ∈ ℕ0
dpmul.e ⊢ 𝐸 ∈ ℕ0
dpmul.g ⊢ 𝐺 ∈ ℕ0
dpmul.j ⊢ 𝐽 ∈ ℕ0
dpmul.k ⊢ 𝐾 ∈ ℕ0
dpmul4.f ⊢ 𝐹 ∈ ℕ0
dpmul4.h ⊢ 𝐻 ∈ ℕ0
dpmul4.i ⊢ 𝐼 ∈ ℕ0
dpmul4.l ⊢ 𝐿 ∈ ℕ0
dpmul4.m ⊢ 𝑀 ∈ ℕ0
dpmul4.n ⊢ 𝑁 ∈ ℕ0
dpmul4.o ⊢ 𝑂 ∈ ℕ0
dpmul4.p ⊢ 𝑃 ∈ ℕ0
dpmul4.q ⊢ 𝑄 ∈ ℕ0
dpmul4.r ⊢ 𝑅 ∈ ℕ0
dpmul4.s ⊢ 𝑆 ∈ ℕ0
dpmul4.t ⊢ 𝑇 ∈ ℕ0
dpmul4.u ⊢ 𝑈 ∈ ℕ0
dpmul4.w ⊢ 𝑊 ∈ ℕ0
dpmul4.x ⊢ 𝑋 ∈ ℕ0
dpmul4.y ⊢ 𝑌 ∈ ℕ0
dpmul4.z ⊢ 𝑍 ∈ ℕ0
dpmul4.a ⊢ 𝑈 < 1 0
dpmul4.b ⊢ 𝑃 < 1 0
dpmul4.c ⊢ 𝑄 < 1 0
dpmul4.1 ⊢ ( 𝐿 𝑀 𝑁 + 𝑂 ) = 𝑅 𝑆 𝑇 𝑈
dpmul4.2 ⊢ ( ( 𝐴 . 𝐵 ) · ( 𝐸 . 𝐹 ) ) = ( 𝐼 . 𝐽 𝐾 )
dpmul4.3 ⊢ ( ( 𝐶 . 𝐷 ) · ( 𝐺 . 𝐻 ) ) = ( 𝑂 . 𝑃 𝑄 )
dpmul4.4 ⊢ ( 𝐼 𝐽 𝐾 1 + 𝑅 𝑆 𝑇 ) = 𝑊 𝑋 𝑌 𝑍
dpmul4.5 ⊢ ( ( ( 𝐴 . 𝐵 ) + ( 𝐶 . 𝐷 ) ) · ( ( 𝐸 . 𝐹 ) + ( 𝐺 . 𝐻 ) ) ) = ( ( ( 𝐼 . 𝐽 𝐾 ) + ( 𝐿 . 𝑀 𝑁 ) ) + ( 𝑂 . 𝑃 𝑄 ) )
Assertion dpmul4 ( ( 𝐴 . 𝐵 𝐶 𝐷 ) · ( 𝐸 . 𝐹 𝐺 𝐻 ) ) < ( 𝑊 . 𝑋 𝑌 𝑍 )

Proof

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