Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dpmul4 Structured version   Visualization version   GIF version

Theorem dpmul4 31090
Description: An upper bound to multiplication of decimal numbers with 4 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.)
Hypotheses
Ref Expression
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 𝑈 < 10
dpmul4.b 𝑃 < 10
dpmul4.c 𝑄 < 10
dpmul4.1 (𝐿𝑀𝑁 + 𝑂) = 𝑅𝑆𝑇𝑈
dpmul4.2 ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼.𝐽𝐾)
dpmul4.3 ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂.𝑃𝑄)
dpmul4.4 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = 𝑊𝑋𝑌𝑍
dpmul4.5 (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄))
Assertion
Ref Expression
dpmul4 ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻)) < (𝑊.𝑋𝑌𝑍)

Proof of Theorem dpmul4
StepHypRef Expression
1 dpmul.a . . . . . . . . 9 𝐴 ∈ ℕ0
2 dpmul.b . . . . . . . . 9 𝐵 ∈ ℕ0
31, 2deccl 12381 . . . . . . . 8 𝐴𝐵 ∈ ℕ0
4 dpmul.c . . . . . . . . 9 𝐶 ∈ ℕ0
5 dpmul.d . . . . . . . . 9 𝐷 ∈ ℕ0
64, 5deccl 12381 . . . . . . . 8 𝐶𝐷 ∈ ℕ0
7 dpmul.e . . . . . . . . 9 𝐸 ∈ ℕ0
8 dpmul4.f . . . . . . . . 9 𝐹 ∈ ℕ0
97, 8deccl 12381 . . . . . . . 8 𝐸𝐹 ∈ ℕ0
10 dpmul.g . . . . . . . . 9 𝐺 ∈ ℕ0
11 dpmul4.h . . . . . . . . 9 𝐻 ∈ ℕ0
1210, 11deccl 12381 . . . . . . . 8 𝐺𝐻 ∈ ℕ0
13 dpmul4.l . . . . . . . . . 10 𝐿 ∈ ℕ0
14 dpmul4.m . . . . . . . . . 10 𝑀 ∈ ℕ0
1513, 14deccl 12381 . . . . . . . . 9 𝐿𝑀 ∈ ℕ0
16 dpmul4.n . . . . . . . . 9 𝑁 ∈ ℕ0
1715, 16deccl 12381 . . . . . . . 8 𝐿𝑀𝑁 ∈ ℕ0
18 2nn0 12180 . . . . . . . 8 2 ∈ ℕ0
192nn0rei 12174 . . . . . . . . . . . . 13 𝐵 ∈ ℝ
20 dpcl 31067 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ0𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)
211, 19, 20mp2an 688 . . . . . . . . . . . 12 (𝐴.𝐵) ∈ ℝ
2221recni 10920 . . . . . . . . . . 11 (𝐴.𝐵) ∈ ℂ
23 10nn 12382 . . . . . . . . . . . 12 10 ∈ ℕ
2423nncni 11913 . . . . . . . . . . 11 10 ∈ ℂ
258nn0rei 12174 . . . . . . . . . . . . 13 𝐹 ∈ ℝ
26 dpcl 31067 . . . . . . . . . . . . 13 ((𝐸 ∈ ℕ0𝐹 ∈ ℝ) → (𝐸.𝐹) ∈ ℝ)
277, 25, 26mp2an 688 . . . . . . . . . . . 12 (𝐸.𝐹) ∈ ℝ
2827recni 10920 . . . . . . . . . . 11 (𝐸.𝐹) ∈ ℂ
2922, 24, 28, 24mul4i 11102 . . . . . . . . . 10 (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10)) = (((𝐴.𝐵) · (𝐸.𝐹)) · (10 · 10))
3022, 28mulcli 10913 . . . . . . . . . . 11 ((𝐴.𝐵) · (𝐸.𝐹)) ∈ ℂ
3130, 24, 24mulassi 10917 . . . . . . . . . 10 ((((𝐴.𝐵) · (𝐸.𝐹)) · 10) · 10) = (((𝐴.𝐵) · (𝐸.𝐹)) · (10 · 10))
32 dpmul4.2 . . . . . . . . . . . . 13 ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼.𝐽𝐾)
3332oveq1i 7265 . . . . . . . . . . . 12 (((𝐴.𝐵) · (𝐸.𝐹)) · 10) = ((𝐼.𝐽𝐾) · 10)
34 dpmul4.i . . . . . . . . . . . . 13 𝐼 ∈ ℕ0
35 dpmul.j . . . . . . . . . . . . 13 𝐽 ∈ ℕ0
36 dpmul.k . . . . . . . . . . . . . 14 𝐾 ∈ ℕ0
3736nn0rei 12174 . . . . . . . . . . . . 13 𝐾 ∈ ℝ
3834, 35, 37dp3mul10 31074 . . . . . . . . . . . 12 ((𝐼.𝐽𝐾) · 10) = (𝐼𝐽.𝐾)
3933, 38eqtri 2766 . . . . . . . . . . 11 (((𝐴.𝐵) · (𝐸.𝐹)) · 10) = (𝐼𝐽.𝐾)
4039oveq1i 7265 . . . . . . . . . 10 ((((𝐴.𝐵) · (𝐸.𝐹)) · 10) · 10) = ((𝐼𝐽.𝐾) · 10)
4129, 31, 403eqtr2ri 2773 . . . . . . . . 9 ((𝐼𝐽.𝐾) · 10) = (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10))
4234, 35deccl 12381 . . . . . . . . . 10 𝐼𝐽 ∈ ℕ0
4342, 37dpmul10 31071 . . . . . . . . 9 ((𝐼𝐽.𝐾) · 10) = 𝐼𝐽𝐾
441, 19dpmul10 31071 . . . . . . . . . 10 ((𝐴.𝐵) · 10) = 𝐴𝐵
457, 25dpmul10 31071 . . . . . . . . . 10 ((𝐸.𝐹) · 10) = 𝐸𝐹
4644, 45oveq12i 7267 . . . . . . . . 9 (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10)) = (𝐴𝐵 · 𝐸𝐹)
4741, 43, 463eqtr3ri 2775 . . . . . . . 8 (𝐴𝐵 · 𝐸𝐹) = 𝐼𝐽𝐾
485nn0rei 12174 . . . . . . . . . . . . 13 𝐷 ∈ ℝ
49 dpcl 31067 . . . . . . . . . . . . 13 ((𝐶 ∈ ℕ0𝐷 ∈ ℝ) → (𝐶.𝐷) ∈ ℝ)
504, 48, 49mp2an 688 . . . . . . . . . . . 12 (𝐶.𝐷) ∈ ℝ
5150recni 10920 . . . . . . . . . . 11 (𝐶.𝐷) ∈ ℂ
5211nn0rei 12174 . . . . . . . . . . . . 13 𝐻 ∈ ℝ
53 dpcl 31067 . . . . . . . . . . . . 13 ((𝐺 ∈ ℕ0𝐻 ∈ ℝ) → (𝐺.𝐻) ∈ ℝ)
5410, 52, 53mp2an 688 . . . . . . . . . . . 12 (𝐺.𝐻) ∈ ℝ
5554recni 10920 . . . . . . . . . . 11 (𝐺.𝐻) ∈ ℂ
5651, 24, 55, 24mul4i 11102 . . . . . . . . . 10 (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10)) = (((𝐶.𝐷) · (𝐺.𝐻)) · (10 · 10))
5751, 55mulcli 10913 . . . . . . . . . . 11 ((𝐶.𝐷) · (𝐺.𝐻)) ∈ ℂ
5857, 24, 24mulassi 10917 . . . . . . . . . 10 ((((𝐶.𝐷) · (𝐺.𝐻)) · 10) · 10) = (((𝐶.𝐷) · (𝐺.𝐻)) · (10 · 10))
59 dpmul4.3 . . . . . . . . . . . . 13 ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂.𝑃𝑄)
6059oveq1i 7265 . . . . . . . . . . . 12 (((𝐶.𝐷) · (𝐺.𝐻)) · 10) = ((𝑂.𝑃𝑄) · 10)
61 dpmul4.o . . . . . . . . . . . . 13 𝑂 ∈ ℕ0
62 dpmul4.p . . . . . . . . . . . . 13 𝑃 ∈ ℕ0
63 dpmul4.q . . . . . . . . . . . . . 14 𝑄 ∈ ℕ0
6463nn0rei 12174 . . . . . . . . . . . . 13 𝑄 ∈ ℝ
6561, 62, 64dp3mul10 31074 . . . . . . . . . . . 12 ((𝑂.𝑃𝑄) · 10) = (𝑂𝑃.𝑄)
6660, 65eqtri 2766 . . . . . . . . . . 11 (((𝐶.𝐷) · (𝐺.𝐻)) · 10) = (𝑂𝑃.𝑄)
6766oveq1i 7265 . . . . . . . . . 10 ((((𝐶.𝐷) · (𝐺.𝐻)) · 10) · 10) = ((𝑂𝑃.𝑄) · 10)
6856, 58, 673eqtr2ri 2773 . . . . . . . . 9 ((𝑂𝑃.𝑄) · 10) = (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10))
6961, 62deccl 12381 . . . . . . . . . 10 𝑂𝑃 ∈ ℕ0
7069, 64dpmul10 31071 . . . . . . . . 9 ((𝑂𝑃.𝑄) · 10) = 𝑂𝑃𝑄
714, 48dpmul10 31071 . . . . . . . . . 10 ((𝐶.𝐷) · 10) = 𝐶𝐷
7210, 52dpmul10 31071 . . . . . . . . . 10 ((𝐺.𝐻) · 10) = 𝐺𝐻
7371, 72oveq12i 7267 . . . . . . . . 9 (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10)) = (𝐶𝐷 · 𝐺𝐻)
7468, 70, 733eqtr3ri 2775 . . . . . . . 8 (𝐶𝐷 · 𝐺𝐻) = 𝑂𝑃𝑄
7522, 51, 24adddiri 10919 . . . . . . . . . . . 12 (((𝐴.𝐵) + (𝐶.𝐷)) · 10) = (((𝐴.𝐵) · 10) + ((𝐶.𝐷) · 10))
7644, 71oveq12i 7267 . . . . . . . . . . . 12 (((𝐴.𝐵) · 10) + ((𝐶.𝐷) · 10)) = (𝐴𝐵 + 𝐶𝐷)
7775, 76eqtr2i 2767 . . . . . . . . . . 11 (𝐴𝐵 + 𝐶𝐷) = (((𝐴.𝐵) + (𝐶.𝐷)) · 10)
7828, 55, 24adddiri 10919 . . . . . . . . . . . 12 (((𝐸.𝐹) + (𝐺.𝐻)) · 10) = (((𝐸.𝐹) · 10) + ((𝐺.𝐻) · 10))
7945, 72oveq12i 7267 . . . . . . . . . . . 12 (((𝐸.𝐹) · 10) + ((𝐺.𝐻) · 10)) = (𝐸𝐹 + 𝐺𝐻)
8078, 79eqtr2i 2767 . . . . . . . . . . 11 (𝐸𝐹 + 𝐺𝐻) = (((𝐸.𝐹) + (𝐺.𝐻)) · 10)
8177, 80oveq12i 7267 . . . . . . . . . 10 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · 10) · (((𝐸.𝐹) + (𝐺.𝐻)) · 10))
8222, 51addcli 10912 . . . . . . . . . . 11 ((𝐴.𝐵) + (𝐶.𝐷)) ∈ ℂ
8328, 55addcli 10912 . . . . . . . . . . 11 ((𝐸.𝐹) + (𝐺.𝐻)) ∈ ℂ
8482, 24, 83, 24mul4i 11102 . . . . . . . . . 10 ((((𝐴.𝐵) + (𝐶.𝐷)) · 10) · (((𝐸.𝐹) + (𝐺.𝐻)) · 10)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (10 · 10))
85 dpmul4.5 . . . . . . . . . . 11 (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄))
8685oveq1i 7265 . . . . . . . . . 10 ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (10 · 10)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10))
8781, 84, 863eqtri 2770 . . . . . . . . 9 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10))
88 10nn0 12384 . . . . . . . . . . 11 10 ∈ ℕ0
8988dec0u 12387 . . . . . . . . . 10 (10 · 10) = 100
9089oveq2i 7266 . . . . . . . . 9 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100)
9132, 30eqeltrri 2836 . . . . . . . . . . . 12 (𝐼.𝐽𝐾) ∈ ℂ
9214nn0rei 12174 . . . . . . . . . . . . . . 15 𝑀 ∈ ℝ
9316nn0rei 12174 . . . . . . . . . . . . . . 15 𝑁 ∈ ℝ
94 dp2cl 31056 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀𝑁 ∈ ℝ)
9592, 93, 94mp2an 688 . . . . . . . . . . . . . 14 𝑀𝑁 ∈ ℝ
96 dpcl 31067 . . . . . . . . . . . . . 14 ((𝐿 ∈ ℕ0𝑀𝑁 ∈ ℝ) → (𝐿.𝑀𝑁) ∈ ℝ)
9713, 95, 96mp2an 688 . . . . . . . . . . . . 13 (𝐿.𝑀𝑁) ∈ ℝ
9897recni 10920 . . . . . . . . . . . 12 (𝐿.𝑀𝑁) ∈ ℂ
9991, 98addcli 10912 . . . . . . . . . . 11 ((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) ∈ ℂ
10059, 57eqeltrri 2836 . . . . . . . . . . 11 (𝑂.𝑃𝑄) ∈ ℂ
101 0nn0 12178 . . . . . . . . . . . . 13 0 ∈ ℕ0
10288, 101deccl 12381 . . . . . . . . . . . 12 100 ∈ ℕ0
103102nn0cni 12175 . . . . . . . . . . 11 100 ∈ ℂ
10499, 100, 103adddiri 10919 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) + ((𝑂.𝑃𝑄) · 100))
10591, 98, 103adddiri 10919 . . . . . . . . . . 11 (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) = (((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100))
106105oveq1i 7265 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) + ((𝑂.𝑃𝑄) · 100)) = ((((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) + ((𝑂.𝑃𝑄) · 100))
10734, 35, 37dpmul100 31073 . . . . . . . . . . . 12 ((𝐼.𝐽𝐾) · 100) = 𝐼𝐽𝐾
10813, 14, 93dpmul100 31073 . . . . . . . . . . . 12 ((𝐿.𝑀𝑁) · 100) = 𝐿𝑀𝑁
109107, 108oveq12i 7267 . . . . . . . . . . 11 (((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) = (𝐼𝐽𝐾 + 𝐿𝑀𝑁)
11061, 62, 64dpmul100 31073 . . . . . . . . . . 11 ((𝑂.𝑃𝑄) · 100) = 𝑂𝑃𝑄
111109, 110oveq12i 7267 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) + ((𝑂.𝑃𝑄) · 100)) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
112104, 106, 1113eqtri 2770 . . . . . . . . 9 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
11387, 90, 1123eqtri 2770 . . . . . . . 8 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
114 sq10 13906 . . . . . . . . . . . 12 (10↑2) = 100
115114oveq2i 7266 . . . . . . . . . . 11 (𝐴𝐵 · (10↑2)) = (𝐴𝐵 · 100)
1163nn0cni 12175 . . . . . . . . . . . 12 𝐴𝐵 ∈ ℂ
117103, 116mulcomi 10914 . . . . . . . . . . 11 (100 · 𝐴𝐵) = (𝐴𝐵 · 100)
118115, 117eqtr4i 2769 . . . . . . . . . 10 (𝐴𝐵 · (10↑2)) = (100 · 𝐴𝐵)
119118oveq1i 7265 . . . . . . . . 9 ((𝐴𝐵 · (10↑2)) + 𝐶𝐷) = ((100 · 𝐴𝐵) + 𝐶𝐷)
1203, 4, 48dfdec100 31046 . . . . . . . . 9 𝐴𝐵𝐶𝐷 = ((100 · 𝐴𝐵) + 𝐶𝐷)
121119, 120eqtr4i 2769 . . . . . . . 8 ((𝐴𝐵 · (10↑2)) + 𝐶𝐷) = 𝐴𝐵𝐶𝐷
122114oveq2i 7266 . . . . . . . . . . 11 (𝐸𝐹 · (10↑2)) = (𝐸𝐹 · 100)
1239nn0cni 12175 . . . . . . . . . . . 12 𝐸𝐹 ∈ ℂ
124103, 123mulcomi 10914 . . . . . . . . . . 11 (100 · 𝐸𝐹) = (𝐸𝐹 · 100)
125122, 124eqtr4i 2769 . . . . . . . . . 10 (𝐸𝐹 · (10↑2)) = (100 · 𝐸𝐹)
126125oveq1i 7265 . . . . . . . . 9 ((𝐸𝐹 · (10↑2)) + 𝐺𝐻) = ((100 · 𝐸𝐹) + 𝐺𝐻)
1279, 10, 52dfdec100 31046 . . . . . . . . 9 𝐸𝐹𝐺𝐻 = ((100 · 𝐸𝐹) + 𝐺𝐻)
128126, 127eqtr4i 2769 . . . . . . . 8 ((𝐸𝐹 · (10↑2)) + 𝐺𝐻) = 𝐸𝐹𝐺𝐻
12924sqvali 13825 . . . . . . . . . . . 12 (10↑2) = (10 · 10)
130129oveq2i 7266 . . . . . . . . . . 11 (𝐼𝐽𝐾 · (10↑2)) = (𝐼𝐽𝐾 · (10 · 10))
13142, 36deccl 12381 . . . . . . . . . . . . 13 𝐼𝐽𝐾 ∈ ℕ0
132131nn0cni 12175 . . . . . . . . . . . 12 𝐼𝐽𝐾 ∈ ℂ
133132, 24, 24mulassi 10917 . . . . . . . . . . 11 ((𝐼𝐽𝐾 · 10) · 10) = (𝐼𝐽𝐾 · (10 · 10))
134130, 133eqtr4i 2769 . . . . . . . . . 10 (𝐼𝐽𝐾 · (10↑2)) = ((𝐼𝐽𝐾 · 10) · 10)
135 dpmul4.r . . . . . . . . . . . . . . . 16 𝑅 ∈ ℕ0
136 dpmul4.s . . . . . . . . . . . . . . . 16 𝑆 ∈ ℕ0
137135, 136deccl 12381 . . . . . . . . . . . . . . 15 𝑅𝑆 ∈ ℕ0
138 dpmul4.t . . . . . . . . . . . . . . 15 𝑇 ∈ ℕ0
139137, 138deccl 12381 . . . . . . . . . . . . . 14 𝑅𝑆𝑇 ∈ ℕ0
140139nn0cni 12175 . . . . . . . . . . . . 13 𝑅𝑆𝑇 ∈ ℂ
141 ax-1cn 10860 . . . . . . . . . . . . 13 1 ∈ ℂ
142140, 141addcli 10912 . . . . . . . . . . . 12 (𝑅𝑆𝑇 + 1) ∈ ℂ
143132, 24mulcli 10913 . . . . . . . . . . . 12 (𝐼𝐽𝐾 · 10) ∈ ℂ
144141, 143addcomi 11096 . . . . . . . . . . . . . . . 16 (1 + (𝐼𝐽𝐾 · 10)) = ((𝐼𝐽𝐾 · 10) + 1)
14524, 132mulcomi 10914 . . . . . . . . . . . . . . . . . 18 (10 · 𝐼𝐽𝐾) = (𝐼𝐽𝐾 · 10)
146131dec0u 12387 . . . . . . . . . . . . . . . . . 18 (10 · 𝐼𝐽𝐾) = 𝐼𝐽𝐾0
147145, 146eqtr3i 2768 . . . . . . . . . . . . . . . . 17 (𝐼𝐽𝐾 · 10) = 𝐼𝐽𝐾0
148147oveq1i 7265 . . . . . . . . . . . . . . . 16 ((𝐼𝐽𝐾 · 10) + 1) = (𝐼𝐽𝐾0 + 1)
149141addid2i 11093 . . . . . . . . . . . . . . . . 17 (0 + 1) = 1
150 eqid 2738 . . . . . . . . . . . . . . . . 17 𝐼𝐽𝐾0 = 𝐼𝐽𝐾0
151131, 101, 149, 150decsuc 12397 . . . . . . . . . . . . . . . 16 (𝐼𝐽𝐾0 + 1) = 𝐼𝐽𝐾1
152144, 148, 1513eqtri 2770 . . . . . . . . . . . . . . 15 (1 + (𝐼𝐽𝐾 · 10)) = 𝐼𝐽𝐾1
153152oveq2i 7266 . . . . . . . . . . . . . 14 (𝑅𝑆𝑇 + (1 + (𝐼𝐽𝐾 · 10))) = (𝑅𝑆𝑇 + 𝐼𝐽𝐾1)
154140, 141, 143addassi 10916 . . . . . . . . . . . . . 14 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = (𝑅𝑆𝑇 + (1 + (𝐼𝐽𝐾 · 10)))
155 1nn0 12179 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ0
156131, 155deccl 12381 . . . . . . . . . . . . . . . 16 𝐼𝐽𝐾1 ∈ ℕ0
157156nn0cni 12175 . . . . . . . . . . . . . . 15 𝐼𝐽𝐾1 ∈ ℂ
158157, 140addcomi 11096 . . . . . . . . . . . . . 14 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = (𝑅𝑆𝑇 + 𝐼𝐽𝐾1)
159153, 154, 1583eqtr4i 2776 . . . . . . . . . . . . 13 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = (𝐼𝐽𝐾1 + 𝑅𝑆𝑇)
160 dpmul4.4 . . . . . . . . . . . . 13 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = 𝑊𝑋𝑌𝑍
161159, 160eqtri 2766 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = 𝑊𝑋𝑌𝑍
162142, 143, 161mvlladdi 11169 . . . . . . . . . . 11 (𝐼𝐽𝐾 · 10) = (𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1))
163162oveq1i 7265 . . . . . . . . . 10 ((𝐼𝐽𝐾 · 10) · 10) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10)
164134, 163eqtri 2766 . . . . . . . . 9 (𝐼𝐽𝐾 · (10↑2)) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10)
165164oveq1i 7265 . . . . . . . 8 ((𝐼𝐽𝐾 · (10↑2)) + 𝐿𝑀𝑁) = (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁)
166 eqid 2738 . . . . . . . 8 (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
1673, 6, 9, 12, 17, 18, 47, 74, 113, 121, 128, 165, 166karatsuba 16713 . . . . . . 7 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
168 dpmul4.w . . . . . . . . . . . . . . 15 𝑊 ∈ ℕ0
169 dpmul4.x . . . . . . . . . . . . . . 15 𝑋 ∈ ℕ0
170168, 169deccl 12381 . . . . . . . . . . . . . 14 𝑊𝑋 ∈ ℕ0
171 dpmul4.y . . . . . . . . . . . . . 14 𝑌 ∈ ℕ0
172170, 171deccl 12381 . . . . . . . . . . . . 13 𝑊𝑋𝑌 ∈ ℕ0
173 dpmul4.z . . . . . . . . . . . . 13 𝑍 ∈ ℕ0
174172, 173deccl 12381 . . . . . . . . . . . 12 𝑊𝑋𝑌𝑍 ∈ ℕ0
175174nn0cni 12175 . . . . . . . . . . 11 𝑊𝑋𝑌𝑍 ∈ ℂ
176102, 101deccl 12381 . . . . . . . . . . . 12 1000 ∈ ℕ0
177176nn0cni 12175 . . . . . . . . . . 11 1000 ∈ ℂ
178175, 177mulcli 10913 . . . . . . . . . 10 (𝑊𝑋𝑌𝑍 · 1000) ∈ ℂ
179142, 177mulcli 10913 . . . . . . . . . 10 ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℂ
180178, 179subcli 11227 . . . . . . . . 9 ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) ∈ ℂ
18117nn0cni 12175 . . . . . . . . . 10 𝐿𝑀𝑁 ∈ ℂ
182103, 181mulcli 10913 . . . . . . . . 9 (100 · 𝐿𝑀𝑁) ∈ ℂ
18361, 62, 64dfdec100 31046 . . . . . . . . . 10 𝑂𝑃𝑄 = ((100 · 𝑂) + 𝑃𝑄)
18469, 63deccl 12381 . . . . . . . . . . 11 𝑂𝑃𝑄 ∈ ℕ0
185184nn0cni 12175 . . . . . . . . . 10 𝑂𝑃𝑄 ∈ ℂ
186183, 185eqeltrri 2836 . . . . . . . . 9 ((100 · 𝑂) + 𝑃𝑄) ∈ ℂ
187180, 182, 186addassi 10916 . . . . . . . 8 ((((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) + ((100 · 𝑂) + 𝑃𝑄)) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
18824sqcli 13826 . . . . . . . . . . . . 13 (10↑2) ∈ ℂ
189132, 188mulcli 10913 . . . . . . . . . . . 12 (𝐼𝐽𝐾 · (10↑2)) ∈ ℂ
190164, 189eqeltrri 2836 . . . . . . . . . . 11 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) ∈ ℂ
191190, 181, 103adddiri 10919 . . . . . . . . . 10 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · 100) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) + (𝐿𝑀𝑁 · 100))
192114oveq2i 7266 . . . . . . . . . 10 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · 100)
193175, 142subcli 11227 . . . . . . . . . . . . 13 (𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) ∈ ℂ
194193, 24, 103mulassi 10917 . . . . . . . . . . . 12 (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · (10 · 100))
195102dec0u 12387 . . . . . . . . . . . . 13 (10 · 100) = 1000
196195oveq2i 7266 . . . . . . . . . . . 12 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · (10 · 100)) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 1000)
197175, 142, 177subdiri 11355 . . . . . . . . . . . 12 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 1000) = ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000))
198194, 196, 1973eqtrri 2771 . . . . . . . . . . 11 ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) = (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100)
199103, 181mulcomi 10914 . . . . . . . . . . 11 (100 · 𝐿𝑀𝑁) = (𝐿𝑀𝑁 · 100)
200198, 199oveq12i 7267 . . . . . . . . . 10 (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) + (𝐿𝑀𝑁 · 100))
201191, 192, 2003eqtr4i 2776 . . . . . . . . 9 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁))
202201, 183oveq12i 7267 . . . . . . . 8 (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄) = ((((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) + ((100 · 𝑂) + 𝑃𝑄))
203182, 186addcli 10912 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℂ
204 subsub 11181 . . . . . . . . 9 (((𝑊𝑋𝑌𝑍 · 1000) ∈ ℂ ∧ ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℂ ∧ ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℂ) → ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
205178, 179, 203, 204mp3an 1459 . . . . . . . 8 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
206187, 202, 2053eqtr4ri 2777 . . . . . . 7 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
207167, 206eqtr4i 2769 . . . . . 6 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) = ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
208174nn0rei 12174 . . . . . . . 8 𝑊𝑋𝑌𝑍 ∈ ℝ
209176nn0rei 12174 . . . . . . . 8 1000 ∈ ℝ
210208, 209remulcli 10922 . . . . . . 7 (𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ
211139nn0rei 12174 . . . . . . . . . . 11 𝑅𝑆𝑇 ∈ ℝ
212 1re 10906 . . . . . . . . . . 11 1 ∈ ℝ
213211, 212readdcli 10921 . . . . . . . . . 10 (𝑅𝑆𝑇 + 1) ∈ ℝ
214213, 209remulcli 10922 . . . . . . . . 9 ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℝ
215102nn0rei 12174 . . . . . . . . . . 11 100 ∈ ℝ
21617nn0rei 12174 . . . . . . . . . . 11 𝐿𝑀𝑁 ∈ ℝ
217215, 216remulcli 10922 . . . . . . . . . 10 (100 · 𝐿𝑀𝑁) ∈ ℝ
21861nn0rei 12174 . . . . . . . . . . . 12 𝑂 ∈ ℝ
219215, 218remulcli 10922 . . . . . . . . . . 11 (100 · 𝑂) ∈ ℝ
22062, 63deccl 12381 . . . . . . . . . . . 12 𝑃𝑄 ∈ ℕ0
221220nn0rei 12174 . . . . . . . . . . 11 𝑃𝑄 ∈ ℝ
222219, 221readdcli 10921 . . . . . . . . . 10 ((100 · 𝑂) + 𝑃𝑄) ∈ ℝ
223217, 222readdcli 10921 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℝ
224214, 223resubcli 11213 . . . . . . . 8 (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ
225219recni 10920 . . . . . . . . . . . 12 (100 · 𝑂) ∈ ℂ
226221recni 10920 . . . . . . . . . . . 12 𝑃𝑄 ∈ ℂ
227182, 225, 226addassi 10916 . . . . . . . . . . 11 (((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) + 𝑃𝑄) = ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))
228218recni 10920 . . . . . . . . . . . . . 14 𝑂 ∈ ℂ
229103, 181, 228adddii 10918 . . . . . . . . . . . . 13 (100 · (𝐿𝑀𝑁 + 𝑂)) = ((100 · 𝐿𝑀𝑁) + (100 · 𝑂))
230 dpmul4.1 . . . . . . . . . . . . . 14 (𝐿𝑀𝑁 + 𝑂) = 𝑅𝑆𝑇𝑈
231230oveq2i 7266 . . . . . . . . . . . . 13 (100 · (𝐿𝑀𝑁 + 𝑂)) = (100 · 𝑅𝑆𝑇𝑈)
232229, 231eqtr3i 2768 . . . . . . . . . . . 12 ((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) = (100 · 𝑅𝑆𝑇𝑈)
233232oveq1i 7265 . . . . . . . . . . 11 (((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) + 𝑃𝑄) = ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄)
234227, 233eqtr3i 2768 . . . . . . . . . 10 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) = ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄)
235 dpmul4.u . . . . . . . . . . . . 13 𝑈 ∈ ℕ0
236 dpmul4.a . . . . . . . . . . . . 13 𝑈 < 10
237 dpmul4.b . . . . . . . . . . . . 13 𝑃 < 10
238 dpmul4.c . . . . . . . . . . . . 13 𝑄 < 10
239235, 88, 62, 101, 63, 101, 236, 237, 2383decltc 12399 . . . . . . . . . . . 12 𝑈𝑃𝑄 < 1000
240235, 62deccl 12381 . . . . . . . . . . . . . . 15 𝑈𝑃 ∈ ℕ0
241240, 63deccl 12381 . . . . . . . . . . . . . 14 𝑈𝑃𝑄 ∈ ℕ0
242241nn0rei 12174 . . . . . . . . . . . . 13 𝑈𝑃𝑄 ∈ ℝ
243211, 209remulcli 10922 . . . . . . . . . . . . 13 (𝑅𝑆𝑇 · 1000) ∈ ℝ
244242, 209, 243ltadd2i 11036 . . . . . . . . . . . 12 (𝑈𝑃𝑄 < 1000 ↔ ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) < ((𝑅𝑆𝑇 · 1000) + 1000))
245239, 244mpbi 229 . . . . . . . . . . 11 ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) < ((𝑅𝑆𝑇 · 1000) + 1000)
246140, 177mulcli 10913 . . . . . . . . . . . . 13 (𝑅𝑆𝑇 · 1000) ∈ ℂ
247235nn0cni 12175 . . . . . . . . . . . . . 14 𝑈 ∈ ℂ
248103, 247mulcli 10913 . . . . . . . . . . . . 13 (100 · 𝑈) ∈ ℂ
249246, 248, 226addassi 10916 . . . . . . . . . . . 12 (((𝑅𝑆𝑇 · 1000) + (100 · 𝑈)) + 𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + ((100 · 𝑈) + 𝑃𝑄))
250 dfdec10 12369 . . . . . . . . . . . . . . 15 𝑅𝑆𝑇𝑈 = ((10 · 𝑅𝑆𝑇) + 𝑈)
251250oveq2i 7266 . . . . . . . . . . . . . 14 (100 · 𝑅𝑆𝑇𝑈) = (100 · ((10 · 𝑅𝑆𝑇) + 𝑈))
25224, 140mulcli 10913 . . . . . . . . . . . . . . 15 (10 · 𝑅𝑆𝑇) ∈ ℂ
253103, 252, 247adddii 10918 . . . . . . . . . . . . . 14 (100 · ((10 · 𝑅𝑆𝑇) + 𝑈)) = ((100 · (10 · 𝑅𝑆𝑇)) + (100 · 𝑈))
254140, 177mulcomi 10914 . . . . . . . . . . . . . . . 16 (𝑅𝑆𝑇 · 1000) = (1000 · 𝑅𝑆𝑇)
25524, 103mulcomi 10914 . . . . . . . . . . . . . . . . . 18 (10 · 100) = (100 · 10)
256255, 195eqtr3i 2768 . . . . . . . . . . . . . . . . 17 (100 · 10) = 1000
257256oveq1i 7265 . . . . . . . . . . . . . . . 16 ((100 · 10) · 𝑅𝑆𝑇) = (1000 · 𝑅𝑆𝑇)
258103, 24, 140mulassi 10917 . . . . . . . . . . . . . . . 16 ((100 · 10) · 𝑅𝑆𝑇) = (100 · (10 · 𝑅𝑆𝑇))
259254, 257, 2583eqtr2ri 2773 . . . . . . . . . . . . . . 15 (100 · (10 · 𝑅𝑆𝑇)) = (𝑅𝑆𝑇 · 1000)
260259oveq1i 7265 . . . . . . . . . . . . . 14 ((100 · (10 · 𝑅𝑆𝑇)) + (100 · 𝑈)) = ((𝑅𝑆𝑇 · 1000) + (100 · 𝑈))
261251, 253, 2603eqtri 2770 . . . . . . . . . . . . 13 (100 · 𝑅𝑆𝑇𝑈) = ((𝑅𝑆𝑇 · 1000) + (100 · 𝑈))
262261oveq1i 7265 . . . . . . . . . . . 12 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) = (((𝑅𝑆𝑇 · 1000) + (100 · 𝑈)) + 𝑃𝑄)
263235, 62, 64dfdec100 31046 . . . . . . . . . . . . 13 𝑈𝑃𝑄 = ((100 · 𝑈) + 𝑃𝑄)
264263oveq2i 7266 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + ((100 · 𝑈) + 𝑃𝑄))
265249, 262, 2643eqtr4i 2776 . . . . . . . . . . 11 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄)
266140, 141, 177adddiri 10919 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 + 1) · 1000) = ((𝑅𝑆𝑇 · 1000) + (1 · 1000))
267177mulid2i 10911 . . . . . . . . . . . . 13 (1 · 1000) = 1000
268267oveq2i 7266 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 · 1000) + (1 · 1000)) = ((𝑅𝑆𝑇 · 1000) + 1000)
269266, 268eqtri 2766 . . . . . . . . . . 11 ((𝑅𝑆𝑇 + 1) · 1000) = ((𝑅𝑆𝑇 · 1000) + 1000)
270245, 265, 2693brtr4i 5100 . . . . . . . . . 10 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) < ((𝑅𝑆𝑇 + 1) · 1000)
271234, 270eqbrtri 5091 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) < ((𝑅𝑆𝑇 + 1) · 1000)
272223, 214posdifi 11455 . . . . . . . . 9 (((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) < ((𝑅𝑆𝑇 + 1) · 1000) ↔ 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
273271, 272mpbi 229 . . . . . . . 8 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
274 elrp 12661 . . . . . . . 8 ((((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+ ↔ ((((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ ∧ 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))))
275224, 273, 274mpbir2an 707 . . . . . . 7 (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+
276 ltsubrp 12695 . . . . . . 7 (((𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ ∧ (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+) → ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) < (𝑊𝑋𝑌𝑍 · 1000))
277210, 275, 276mp2an 688 . . . . . 6 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) < (𝑊𝑋𝑌𝑍 · 1000)
278207, 277eqbrtri 5091 . . . . 5 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000)
2793, 4deccl 12381 . . . . . . . . 9 𝐴𝐵𝐶 ∈ ℕ0
280279, 5deccl 12381 . . . . . . . 8 𝐴𝐵𝐶𝐷 ∈ ℕ0
281280nn0rei 12174 . . . . . . 7 𝐴𝐵𝐶𝐷 ∈ ℝ
2829, 10deccl 12381 . . . . . . . . 9 𝐸𝐹𝐺 ∈ ℕ0
283282, 11deccl 12381 . . . . . . . 8 𝐸𝐹𝐺𝐻 ∈ ℕ0
284283nn0rei 12174 . . . . . . 7 𝐸𝐹𝐺𝐻 ∈ ℝ
285281, 284remulcli 10922 . . . . . 6 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) ∈ ℝ
28623decnncl2 12390 . . . . . . . . 9 100 ∈ ℕ
287286decnncl2 12390 . . . . . . . 8 1000 ∈ ℕ
288287nngt0i 11942 . . . . . . 7 0 < 1000
289209, 288pm3.2i 470 . . . . . 6 (1000 ∈ ℝ ∧ 0 < 1000)
290 ltdiv1 11769 . . . . . 6 (((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) ∈ ℝ ∧ (𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ ∧ (1000 ∈ ℝ ∧ 0 < 1000)) → ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000) ↔ ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000)))
291285, 210, 289, 290mp3an 1459 . . . . 5 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000) ↔ ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000))
292278, 291mpbi 229 . . . 4 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000)
293280nn0cni 12175 . . . . . 6 𝐴𝐵𝐶𝐷 ∈ ℂ
294283nn0cni 12175 . . . . . 6 𝐸𝐹𝐺𝐻 ∈ ℂ
295209, 288gt0ne0ii 11441 . . . . . 6 1000 ≠ 0
296293, 294, 177, 295div23i 11663 . . . . 5 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴𝐵𝐶𝐷 / 1000) · 𝐸𝐹𝐺𝐻)
2971, 2, 4, 48dpmul1000 31075 . . . . . . . 8 ((𝐴.𝐵𝐶𝐷) · 1000) = 𝐴𝐵𝐶𝐷
298297oveq1i 7265 . . . . . . 7 (((𝐴.𝐵𝐶𝐷) · 1000) / 1000) = (𝐴𝐵𝐶𝐷 / 1000)
2994nn0rei 12174 . . . . . . . . . . . 12 𝐶 ∈ ℝ
300 dp2cl 31056 . . . . . . . . . . . 12 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → 𝐶𝐷 ∈ ℝ)
301299, 48, 300mp2an 688 . . . . . . . . . . 11 𝐶𝐷 ∈ ℝ
302 dp2cl 31056 . . . . . . . . . . 11 ((𝐵 ∈ ℝ ∧ 𝐶𝐷 ∈ ℝ) → 𝐵𝐶𝐷 ∈ ℝ)
30319, 301, 302mp2an 688 . . . . . . . . . 10 𝐵𝐶𝐷 ∈ ℝ
304 dpcl 31067 . . . . . . . . . 10 ((𝐴 ∈ ℕ0𝐵𝐶𝐷 ∈ ℝ) → (𝐴.𝐵𝐶𝐷) ∈ ℝ)
3051, 303, 304mp2an 688 . . . . . . . . 9 (𝐴.𝐵𝐶𝐷) ∈ ℝ
306305recni 10920 . . . . . . . 8 (𝐴.𝐵𝐶𝐷) ∈ ℂ
307306, 177, 295divcan4i 11652 . . . . . . 7 (((𝐴.𝐵𝐶𝐷) · 1000) / 1000) = (𝐴.𝐵𝐶𝐷)
308298, 307eqtr3i 2768 . . . . . 6 (𝐴𝐵𝐶𝐷 / 1000) = (𝐴.𝐵𝐶𝐷)
309308oveq1i 7265 . . . . 5 ((𝐴𝐵𝐶𝐷 / 1000) · 𝐸𝐹𝐺𝐻) = ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻)
310296, 309eqtri 2766 . . . 4 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻)
311175, 177, 295divcan4i 11652 . . . 4 ((𝑊𝑋𝑌𝑍 · 1000) / 1000) = 𝑊𝑋𝑌𝑍
312292, 310, 3113brtr3i 5099 . . 3 ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍
313305, 284remulcli 10922 . . . 4 ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) ∈ ℝ
314 ltdiv1 11769 . . . 4 ((((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) ∈ ℝ ∧ 𝑊𝑋𝑌𝑍 ∈ ℝ ∧ (1000 ∈ ℝ ∧ 0 < 1000)) → (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍 ↔ (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000)))
315313, 208, 289, 314mp3an 1459 . . 3 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍 ↔ (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000))
316312, 315mpbi 229 . 2 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000)
317306, 294, 177, 295divassi 11661 . . 3 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · (𝐸𝐹𝐺𝐻 / 1000))
3187, 8, 10, 52dpmul1000 31075 . . . . . 6 ((𝐸.𝐹𝐺𝐻) · 1000) = 𝐸𝐹𝐺𝐻
319318oveq1i 7265 . . . . 5 (((𝐸.𝐹𝐺𝐻) · 1000) / 1000) = (𝐸𝐹𝐺𝐻 / 1000)
32010nn0rei 12174 . . . . . . . . . 10 𝐺 ∈ ℝ
321 dp2cl 31056 . . . . . . . . . 10 ((𝐺 ∈ ℝ ∧ 𝐻 ∈ ℝ) → 𝐺𝐻 ∈ ℝ)
322320, 52, 321mp2an 688 . . . . . . . . 9 𝐺𝐻 ∈ ℝ
323 dp2cl 31056 . . . . . . . . 9 ((𝐹 ∈ ℝ ∧ 𝐺𝐻 ∈ ℝ) → 𝐹𝐺𝐻 ∈ ℝ)
32425, 322, 323mp2an 688 . . . . . . . 8 𝐹𝐺𝐻 ∈ ℝ
325 dpcl 31067 . . . . . . . 8 ((𝐸 ∈ ℕ0𝐹𝐺𝐻 ∈ ℝ) → (𝐸.𝐹𝐺𝐻) ∈ ℝ)
3267, 324, 325mp2an 688 . . . . . . 7 (𝐸.𝐹𝐺𝐻) ∈ ℝ
327326recni 10920 . . . . . 6 (𝐸.𝐹𝐺𝐻) ∈ ℂ
328327, 177, 295divcan4i 11652 . . . . 5 (((𝐸.𝐹𝐺𝐻) · 1000) / 1000) = (𝐸.𝐹𝐺𝐻)
329319, 328eqtr3i 2768 . . . 4 (𝐸𝐹𝐺𝐻 / 1000) = (𝐸.𝐹𝐺𝐻)
330329oveq2i 7266 . . 3 ((𝐴.𝐵𝐶𝐷) · (𝐸𝐹𝐺𝐻 / 1000)) = ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻))
331317, 330eqtri 2766 . 2 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻))
332173nn0rei 12174 . . . . 5 𝑍 ∈ ℝ
333168, 169, 171, 332dpmul1000 31075 . . . 4 ((𝑊.𝑋𝑌𝑍) · 1000) = 𝑊𝑋𝑌𝑍
334333oveq1i 7265 . . 3 (((𝑊.𝑋𝑌𝑍) · 1000) / 1000) = (𝑊𝑋𝑌𝑍 / 1000)
335169nn0rei 12174 . . . . . . 7 𝑋 ∈ ℝ
336171nn0rei 12174 . . . . . . . 8 𝑌 ∈ ℝ
337 dp2cl 31056 . . . . . . . 8 ((𝑌 ∈ ℝ ∧ 𝑍 ∈ ℝ) → 𝑌𝑍 ∈ ℝ)
338336, 332, 337mp2an 688 . . . . . . 7 𝑌𝑍 ∈ ℝ
339 dp2cl 31056 . . . . . . 7 ((𝑋 ∈ ℝ ∧ 𝑌𝑍 ∈ ℝ) → 𝑋𝑌𝑍 ∈ ℝ)
340335, 338, 339mp2an 688 . . . . . 6 𝑋𝑌𝑍 ∈ ℝ
341 dpcl 31067 . . . . . 6 ((𝑊 ∈ ℕ0𝑋𝑌𝑍 ∈ ℝ) → (𝑊.𝑋𝑌𝑍) ∈ ℝ)
342168, 340, 341mp2an 688 . . . . 5 (𝑊.𝑋𝑌𝑍) ∈ ℝ
343342recni 10920 . . . 4 (𝑊.𝑋𝑌𝑍) ∈ ℂ
344343, 177, 295divcan4i 11652 . . 3 (((𝑊.𝑋𝑌𝑍) · 1000) / 1000) = (𝑊.𝑋𝑌𝑍)
345334, 344eqtr3i 2768 . 2 (𝑊𝑋𝑌𝑍 / 1000) = (𝑊.𝑋𝑌𝑍)
346316, 331, 3453brtr3i 5099 1 ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻)) < (𝑊.𝑋𝑌𝑍)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395   = wceq 1539  wcel 2108   class class class wbr 5070  (class class class)co 7255  cc 10800  cr 10801  0cc0 10802  1c1 10803   + caddc 10805   · cmul 10807   < clt 10940  cmin 11135   / cdiv 11562  2c2 11958  0cn0 12163  cdc 12366  +crp 12659  cexp 13710  cdp2 31047  .cdp 31064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-4 11968  df-5 11969  df-6 11970  df-7 11971  df-8 11972  df-9 11973  df-n0 12164  df-z 12250  df-dec 12367  df-uz 12512  df-rp 12660  df-seq 13650  df-exp 13711  df-dp2 31048  df-dp 31065
This theorem is referenced by:  hgt750lem2  32532
  Copyright terms: Public domain W3C validator