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 29750
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 11550 . . . . . . . 8 𝐴𝐵 ∈ ℕ0
4 dpmul.c . . . . . . . . 9 𝐶 ∈ ℕ0
5 dpmul.d . . . . . . . . 9 𝐷 ∈ ℕ0
64, 5deccl 11550 . . . . . . . 8 𝐶𝐷 ∈ ℕ0
7 dpmul.e . . . . . . . . 9 𝐸 ∈ ℕ0
8 dpmul4.f . . . . . . . . 9 𝐹 ∈ ℕ0
97, 8deccl 11550 . . . . . . . 8 𝐸𝐹 ∈ ℕ0
10 dpmul.g . . . . . . . . 9 𝐺 ∈ ℕ0
11 dpmul4.h . . . . . . . . 9 𝐻 ∈ ℕ0
1210, 11deccl 11550 . . . . . . . 8 𝐺𝐻 ∈ ℕ0
13 dpmul4.l . . . . . . . . . 10 𝐿 ∈ ℕ0
14 dpmul4.m . . . . . . . . . 10 𝑀 ∈ ℕ0
1513, 14deccl 11550 . . . . . . . . 9 𝐿𝑀 ∈ ℕ0
16 dpmul4.n . . . . . . . . 9 𝑁 ∈ ℕ0
1715, 16deccl 11550 . . . . . . . 8 𝐿𝑀𝑁 ∈ ℕ0
18 2nn0 11347 . . . . . . . 8 2 ∈ ℕ0
192nn0rei 11341 . . . . . . . . . . . . 13 𝐵 ∈ ℝ
20 dpcl 29726 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ0𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)
211, 19, 20mp2an 708 . . . . . . . . . . . 12 (𝐴.𝐵) ∈ ℝ
2221recni 10090 . . . . . . . . . . 11 (𝐴.𝐵) ∈ ℂ
23 10nn 11552 . . . . . . . . . . . 12 10 ∈ ℕ
2423nncni 11068 . . . . . . . . . . 11 10 ∈ ℂ
258nn0rei 11341 . . . . . . . . . . . . 13 𝐹 ∈ ℝ
26 dpcl 29726 . . . . . . . . . . . . 13 ((𝐸 ∈ ℕ0𝐹 ∈ ℝ) → (𝐸.𝐹) ∈ ℝ)
277, 25, 26mp2an 708 . . . . . . . . . . . 12 (𝐸.𝐹) ∈ ℝ
2827recni 10090 . . . . . . . . . . 11 (𝐸.𝐹) ∈ ℂ
2922, 24, 28, 24mul4i 10271 . . . . . . . . . 10 (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10)) = (((𝐴.𝐵) · (𝐸.𝐹)) · (10 · 10))
3022, 28mulcli 10083 . . . . . . . . . . 11 ((𝐴.𝐵) · (𝐸.𝐹)) ∈ ℂ
3130, 24, 24mulassi 10087 . . . . . . . . . 10 ((((𝐴.𝐵) · (𝐸.𝐹)) · 10) · 10) = (((𝐴.𝐵) · (𝐸.𝐹)) · (10 · 10))
32 dpmul4.2 . . . . . . . . . . . . 13 ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼.𝐽𝐾)
3332oveq1i 6700 . . . . . . . . . . . 12 (((𝐴.𝐵) · (𝐸.𝐹)) · 10) = ((𝐼.𝐽𝐾) · 10)
34 dpmul4.i . . . . . . . . . . . . 13 𝐼 ∈ ℕ0
35 dpmul.j . . . . . . . . . . . . 13 𝐽 ∈ ℕ0
36 dpmul.k . . . . . . . . . . . . . 14 𝐾 ∈ ℕ0
3736nn0rei 11341 . . . . . . . . . . . . 13 𝐾 ∈ ℝ
3834, 35, 37dp3mul10 29734 . . . . . . . . . . . 12 ((𝐼.𝐽𝐾) · 10) = (𝐼𝐽.𝐾)
3933, 38eqtri 2673 . . . . . . . . . . 11 (((𝐴.𝐵) · (𝐸.𝐹)) · 10) = (𝐼𝐽.𝐾)
4039oveq1i 6700 . . . . . . . . . 10 ((((𝐴.𝐵) · (𝐸.𝐹)) · 10) · 10) = ((𝐼𝐽.𝐾) · 10)
4129, 31, 403eqtr2ri 2680 . . . . . . . . 9 ((𝐼𝐽.𝐾) · 10) = (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10))
4234, 35deccl 11550 . . . . . . . . . 10 𝐼𝐽 ∈ ℕ0
4342, 37dpmul10 29731 . . . . . . . . 9 ((𝐼𝐽.𝐾) · 10) = 𝐼𝐽𝐾
441, 19dpmul10 29731 . . . . . . . . . 10 ((𝐴.𝐵) · 10) = 𝐴𝐵
457, 25dpmul10 29731 . . . . . . . . . 10 ((𝐸.𝐹) · 10) = 𝐸𝐹
4644, 45oveq12i 6702 . . . . . . . . 9 (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10)) = (𝐴𝐵 · 𝐸𝐹)
4741, 43, 463eqtr3ri 2682 . . . . . . . 8 (𝐴𝐵 · 𝐸𝐹) = 𝐼𝐽𝐾
485nn0rei 11341 . . . . . . . . . . . . 13 𝐷 ∈ ℝ
49 dpcl 29726 . . . . . . . . . . . . 13 ((𝐶 ∈ ℕ0𝐷 ∈ ℝ) → (𝐶.𝐷) ∈ ℝ)
504, 48, 49mp2an 708 . . . . . . . . . . . 12 (𝐶.𝐷) ∈ ℝ
5150recni 10090 . . . . . . . . . . 11 (𝐶.𝐷) ∈ ℂ
5211nn0rei 11341 . . . . . . . . . . . . 13 𝐻 ∈ ℝ
53 dpcl 29726 . . . . . . . . . . . . 13 ((𝐺 ∈ ℕ0𝐻 ∈ ℝ) → (𝐺.𝐻) ∈ ℝ)
5410, 52, 53mp2an 708 . . . . . . . . . . . 12 (𝐺.𝐻) ∈ ℝ
5554recni 10090 . . . . . . . . . . 11 (𝐺.𝐻) ∈ ℂ
5651, 24, 55, 24mul4i 10271 . . . . . . . . . 10 (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10)) = (((𝐶.𝐷) · (𝐺.𝐻)) · (10 · 10))
5751, 55mulcli 10083 . . . . . . . . . . 11 ((𝐶.𝐷) · (𝐺.𝐻)) ∈ ℂ
5857, 24, 24mulassi 10087 . . . . . . . . . 10 ((((𝐶.𝐷) · (𝐺.𝐻)) · 10) · 10) = (((𝐶.𝐷) · (𝐺.𝐻)) · (10 · 10))
59 dpmul4.3 . . . . . . . . . . . . 13 ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂.𝑃𝑄)
6059oveq1i 6700 . . . . . . . . . . . 12 (((𝐶.𝐷) · (𝐺.𝐻)) · 10) = ((𝑂.𝑃𝑄) · 10)
61 dpmul4.o . . . . . . . . . . . . 13 𝑂 ∈ ℕ0
62 dpmul4.p . . . . . . . . . . . . 13 𝑃 ∈ ℕ0
63 dpmul4.q . . . . . . . . . . . . . 14 𝑄 ∈ ℕ0
6463nn0rei 11341 . . . . . . . . . . . . 13 𝑄 ∈ ℝ
6561, 62, 64dp3mul10 29734 . . . . . . . . . . . 12 ((𝑂.𝑃𝑄) · 10) = (𝑂𝑃.𝑄)
6660, 65eqtri 2673 . . . . . . . . . . 11 (((𝐶.𝐷) · (𝐺.𝐻)) · 10) = (𝑂𝑃.𝑄)
6766oveq1i 6700 . . . . . . . . . 10 ((((𝐶.𝐷) · (𝐺.𝐻)) · 10) · 10) = ((𝑂𝑃.𝑄) · 10)
6856, 58, 673eqtr2ri 2680 . . . . . . . . 9 ((𝑂𝑃.𝑄) · 10) = (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10))
6961, 62deccl 11550 . . . . . . . . . 10 𝑂𝑃 ∈ ℕ0
7069, 64dpmul10 29731 . . . . . . . . 9 ((𝑂𝑃.𝑄) · 10) = 𝑂𝑃𝑄
714, 48dpmul10 29731 . . . . . . . . . 10 ((𝐶.𝐷) · 10) = 𝐶𝐷
7210, 52dpmul10 29731 . . . . . . . . . 10 ((𝐺.𝐻) · 10) = 𝐺𝐻
7371, 72oveq12i 6702 . . . . . . . . 9 (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10)) = (𝐶𝐷 · 𝐺𝐻)
7468, 70, 733eqtr3ri 2682 . . . . . . . 8 (𝐶𝐷 · 𝐺𝐻) = 𝑂𝑃𝑄
7522, 51, 24adddiri 10089 . . . . . . . . . . . 12 (((𝐴.𝐵) + (𝐶.𝐷)) · 10) = (((𝐴.𝐵) · 10) + ((𝐶.𝐷) · 10))
7644, 71oveq12i 6702 . . . . . . . . . . . 12 (((𝐴.𝐵) · 10) + ((𝐶.𝐷) · 10)) = (𝐴𝐵 + 𝐶𝐷)
7775, 76eqtr2i 2674 . . . . . . . . . . 11 (𝐴𝐵 + 𝐶𝐷) = (((𝐴.𝐵) + (𝐶.𝐷)) · 10)
7828, 55, 24adddiri 10089 . . . . . . . . . . . 12 (((𝐸.𝐹) + (𝐺.𝐻)) · 10) = (((𝐸.𝐹) · 10) + ((𝐺.𝐻) · 10))
7945, 72oveq12i 6702 . . . . . . . . . . . 12 (((𝐸.𝐹) · 10) + ((𝐺.𝐻) · 10)) = (𝐸𝐹 + 𝐺𝐻)
8078, 79eqtr2i 2674 . . . . . . . . . . 11 (𝐸𝐹 + 𝐺𝐻) = (((𝐸.𝐹) + (𝐺.𝐻)) · 10)
8177, 80oveq12i 6702 . . . . . . . . . 10 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · 10) · (((𝐸.𝐹) + (𝐺.𝐻)) · 10))
8222, 51addcli 10082 . . . . . . . . . . 11 ((𝐴.𝐵) + (𝐶.𝐷)) ∈ ℂ
8328, 55addcli 10082 . . . . . . . . . . 11 ((𝐸.𝐹) + (𝐺.𝐻)) ∈ ℂ
8482, 24, 83, 24mul4i 10271 . . . . . . . . . 10 ((((𝐴.𝐵) + (𝐶.𝐷)) · 10) · (((𝐸.𝐹) + (𝐺.𝐻)) · 10)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (10 · 10))
85 dpmul4.5 . . . . . . . . . . 11 (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄))
8685oveq1i 6700 . . . . . . . . . 10 ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (10 · 10)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10))
8781, 84, 863eqtri 2677 . . . . . . . . 9 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10))
88 10nn0 11554 . . . . . . . . . . 11 10 ∈ ℕ0
8988dec0u 11558 . . . . . . . . . 10 (10 · 10) = 100
9089oveq2i 6701 . . . . . . . . 9 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100)
9132, 30eqeltrri 2727 . . . . . . . . . . . 12 (𝐼.𝐽𝐾) ∈ ℂ
9214nn0rei 11341 . . . . . . . . . . . . . . 15 𝑀 ∈ ℝ
9316nn0rei 11341 . . . . . . . . . . . . . . 15 𝑁 ∈ ℝ
94 dp2cl 29715 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀𝑁 ∈ ℝ)
9592, 93, 94mp2an 708 . . . . . . . . . . . . . 14 𝑀𝑁 ∈ ℝ
96 dpcl 29726 . . . . . . . . . . . . . 14 ((𝐿 ∈ ℕ0𝑀𝑁 ∈ ℝ) → (𝐿.𝑀𝑁) ∈ ℝ)
9713, 95, 96mp2an 708 . . . . . . . . . . . . 13 (𝐿.𝑀𝑁) ∈ ℝ
9897recni 10090 . . . . . . . . . . . 12 (𝐿.𝑀𝑁) ∈ ℂ
9991, 98addcli 10082 . . . . . . . . . . 11 ((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) ∈ ℂ
10059, 57eqeltrri 2727 . . . . . . . . . . 11 (𝑂.𝑃𝑄) ∈ ℂ
101 0nn0 11345 . . . . . . . . . . . . 13 0 ∈ ℕ0
10288, 101deccl 11550 . . . . . . . . . . . 12 100 ∈ ℕ0
103102nn0cni 11342 . . . . . . . . . . 11 100 ∈ ℂ
10499, 100, 103adddiri 10089 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) + ((𝑂.𝑃𝑄) · 100))
10591, 98, 103adddiri 10089 . . . . . . . . . . 11 (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) = (((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100))
106105oveq1i 6700 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) + ((𝑂.𝑃𝑄) · 100)) = ((((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) + ((𝑂.𝑃𝑄) · 100))
10734, 35, 37dpmul100 29733 . . . . . . . . . . . 12 ((𝐼.𝐽𝐾) · 100) = 𝐼𝐽𝐾
10813, 14, 93dpmul100 29733 . . . . . . . . . . . 12 ((𝐿.𝑀𝑁) · 100) = 𝐿𝑀𝑁
109107, 108oveq12i 6702 . . . . . . . . . . 11 (((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) = (𝐼𝐽𝐾 + 𝐿𝑀𝑁)
11061, 62, 64dpmul100 29733 . . . . . . . . . . 11 ((𝑂.𝑃𝑄) · 100) = 𝑂𝑃𝑄
111109, 110oveq12i 6702 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) + ((𝑂.𝑃𝑄) · 100)) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
112104, 106, 1113eqtri 2677 . . . . . . . . 9 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
11387, 90, 1123eqtri 2677 . . . . . . . 8 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
114 sq10 13088 . . . . . . . . . . . 12 (10↑2) = 100
115114oveq2i 6701 . . . . . . . . . . 11 (𝐴𝐵 · (10↑2)) = (𝐴𝐵 · 100)
1163nn0cni 11342 . . . . . . . . . . . 12 𝐴𝐵 ∈ ℂ
117103, 116mulcomi 10084 . . . . . . . . . . 11 (100 · 𝐴𝐵) = (𝐴𝐵 · 100)
118115, 117eqtr4i 2676 . . . . . . . . . 10 (𝐴𝐵 · (10↑2)) = (100 · 𝐴𝐵)
119118oveq1i 6700 . . . . . . . . 9 ((𝐴𝐵 · (10↑2)) + 𝐶𝐷) = ((100 · 𝐴𝐵) + 𝐶𝐷)
1203, 4, 48dfdec100 29704 . . . . . . . . 9 𝐴𝐵𝐶𝐷 = ((100 · 𝐴𝐵) + 𝐶𝐷)
121119, 120eqtr4i 2676 . . . . . . . 8 ((𝐴𝐵 · (10↑2)) + 𝐶𝐷) = 𝐴𝐵𝐶𝐷
122114oveq2i 6701 . . . . . . . . . . 11 (𝐸𝐹 · (10↑2)) = (𝐸𝐹 · 100)
1239nn0cni 11342 . . . . . . . . . . . 12 𝐸𝐹 ∈ ℂ
124103, 123mulcomi 10084 . . . . . . . . . . 11 (100 · 𝐸𝐹) = (𝐸𝐹 · 100)
125122, 124eqtr4i 2676 . . . . . . . . . 10 (𝐸𝐹 · (10↑2)) = (100 · 𝐸𝐹)
126125oveq1i 6700 . . . . . . . . 9 ((𝐸𝐹 · (10↑2)) + 𝐺𝐻) = ((100 · 𝐸𝐹) + 𝐺𝐻)
1279, 10, 52dfdec100 29704 . . . . . . . . 9 𝐸𝐹𝐺𝐻 = ((100 · 𝐸𝐹) + 𝐺𝐻)
128126, 127eqtr4i 2676 . . . . . . . 8 ((𝐸𝐹 · (10↑2)) + 𝐺𝐻) = 𝐸𝐹𝐺𝐻
12924sqvali 12983 . . . . . . . . . . . 12 (10↑2) = (10 · 10)
130129oveq2i 6701 . . . . . . . . . . 11 (𝐼𝐽𝐾 · (10↑2)) = (𝐼𝐽𝐾 · (10 · 10))
13142, 36deccl 11550 . . . . . . . . . . . . 13 𝐼𝐽𝐾 ∈ ℕ0
132131nn0cni 11342 . . . . . . . . . . . 12 𝐼𝐽𝐾 ∈ ℂ
133132, 24, 24mulassi 10087 . . . . . . . . . . 11 ((𝐼𝐽𝐾 · 10) · 10) = (𝐼𝐽𝐾 · (10 · 10))
134130, 133eqtr4i 2676 . . . . . . . . . 10 (𝐼𝐽𝐾 · (10↑2)) = ((𝐼𝐽𝐾 · 10) · 10)
135 dpmul4.r . . . . . . . . . . . . . . . 16 𝑅 ∈ ℕ0
136 dpmul4.s . . . . . . . . . . . . . . . 16 𝑆 ∈ ℕ0
137135, 136deccl 11550 . . . . . . . . . . . . . . 15 𝑅𝑆 ∈ ℕ0
138 dpmul4.t . . . . . . . . . . . . . . 15 𝑇 ∈ ℕ0
139137, 138deccl 11550 . . . . . . . . . . . . . 14 𝑅𝑆𝑇 ∈ ℕ0
140139nn0cni 11342 . . . . . . . . . . . . 13 𝑅𝑆𝑇 ∈ ℂ
141 ax-1cn 10032 . . . . . . . . . . . . 13 1 ∈ ℂ
142140, 141addcli 10082 . . . . . . . . . . . 12 (𝑅𝑆𝑇 + 1) ∈ ℂ
143132, 24mulcli 10083 . . . . . . . . . . . 12 (𝐼𝐽𝐾 · 10) ∈ ℂ
144141, 143addcomi 10265 . . . . . . . . . . . . . . . 16 (1 + (𝐼𝐽𝐾 · 10)) = ((𝐼𝐽𝐾 · 10) + 1)
14524, 132mulcomi 10084 . . . . . . . . . . . . . . . . . 18 (10 · 𝐼𝐽𝐾) = (𝐼𝐽𝐾 · 10)
146131dec0u 11558 . . . . . . . . . . . . . . . . . 18 (10 · 𝐼𝐽𝐾) = 𝐼𝐽𝐾0
147145, 146eqtr3i 2675 . . . . . . . . . . . . . . . . 17 (𝐼𝐽𝐾 · 10) = 𝐼𝐽𝐾0
148147oveq1i 6700 . . . . . . . . . . . . . . . 16 ((𝐼𝐽𝐾 · 10) + 1) = (𝐼𝐽𝐾0 + 1)
149141addid2i 10262 . . . . . . . . . . . . . . . . 17 (0 + 1) = 1
150 eqid 2651 . . . . . . . . . . . . . . . . 17 𝐼𝐽𝐾0 = 𝐼𝐽𝐾0
151131, 101, 149, 150decsuc 11573 . . . . . . . . . . . . . . . 16 (𝐼𝐽𝐾0 + 1) = 𝐼𝐽𝐾1
152144, 148, 1513eqtri 2677 . . . . . . . . . . . . . . 15 (1 + (𝐼𝐽𝐾 · 10)) = 𝐼𝐽𝐾1
153152oveq2i 6701 . . . . . . . . . . . . . 14 (𝑅𝑆𝑇 + (1 + (𝐼𝐽𝐾 · 10))) = (𝑅𝑆𝑇 + 𝐼𝐽𝐾1)
154140, 141, 143addassi 10086 . . . . . . . . . . . . . 14 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = (𝑅𝑆𝑇 + (1 + (𝐼𝐽𝐾 · 10)))
155 1nn0 11346 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ0
156131, 155deccl 11550 . . . . . . . . . . . . . . . 16 𝐼𝐽𝐾1 ∈ ℕ0
157156nn0cni 11342 . . . . . . . . . . . . . . 15 𝐼𝐽𝐾1 ∈ ℂ
158157, 140addcomi 10265 . . . . . . . . . . . . . 14 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = (𝑅𝑆𝑇 + 𝐼𝐽𝐾1)
159153, 154, 1583eqtr4i 2683 . . . . . . . . . . . . 13 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = (𝐼𝐽𝐾1 + 𝑅𝑆𝑇)
160 dpmul4.4 . . . . . . . . . . . . 13 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = 𝑊𝑋𝑌𝑍
161159, 160eqtri 2673 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = 𝑊𝑋𝑌𝑍
162142, 143, 161mvlladdi 10337 . . . . . . . . . . 11 (𝐼𝐽𝐾 · 10) = (𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1))
163162oveq1i 6700 . . . . . . . . . 10 ((𝐼𝐽𝐾 · 10) · 10) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10)
164134, 163eqtri 2673 . . . . . . . . 9 (𝐼𝐽𝐾 · (10↑2)) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10)
165164oveq1i 6700 . . . . . . . 8 ((𝐼𝐽𝐾 · (10↑2)) + 𝐿𝑀𝑁) = (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁)
166 eqid 2651 . . . . . . . 8 (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
1673, 6, 9, 12, 17, 18, 47, 74, 113, 121, 128, 165, 166karatsuba 15839 . . . . . . 7 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
168 dpmul4.w . . . . . . . . . . . . . . 15 𝑊 ∈ ℕ0
169 dpmul4.x . . . . . . . . . . . . . . 15 𝑋 ∈ ℕ0
170168, 169deccl 11550 . . . . . . . . . . . . . 14 𝑊𝑋 ∈ ℕ0
171 dpmul4.y . . . . . . . . . . . . . 14 𝑌 ∈ ℕ0
172170, 171deccl 11550 . . . . . . . . . . . . 13 𝑊𝑋𝑌 ∈ ℕ0
173 dpmul4.z . . . . . . . . . . . . 13 𝑍 ∈ ℕ0
174172, 173deccl 11550 . . . . . . . . . . . 12 𝑊𝑋𝑌𝑍 ∈ ℕ0
175174nn0cni 11342 . . . . . . . . . . 11 𝑊𝑋𝑌𝑍 ∈ ℂ
176102, 101deccl 11550 . . . . . . . . . . . 12 1000 ∈ ℕ0
177176nn0cni 11342 . . . . . . . . . . 11 1000 ∈ ℂ
178175, 177mulcli 10083 . . . . . . . . . 10 (𝑊𝑋𝑌𝑍 · 1000) ∈ ℂ
179142, 177mulcli 10083 . . . . . . . . . 10 ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℂ
180178, 179subcli 10395 . . . . . . . . 9 ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) ∈ ℂ
18117nn0cni 11342 . . . . . . . . . 10 𝐿𝑀𝑁 ∈ ℂ
182103, 181mulcli 10083 . . . . . . . . 9 (100 · 𝐿𝑀𝑁) ∈ ℂ
18361, 62, 64dfdec100 29704 . . . . . . . . . 10 𝑂𝑃𝑄 = ((100 · 𝑂) + 𝑃𝑄)
18469, 63deccl 11550 . . . . . . . . . . 11 𝑂𝑃𝑄 ∈ ℕ0
185184nn0cni 11342 . . . . . . . . . 10 𝑂𝑃𝑄 ∈ ℂ
186183, 185eqeltrri 2727 . . . . . . . . 9 ((100 · 𝑂) + 𝑃𝑄) ∈ ℂ
187180, 182, 186addassi 10086 . . . . . . . 8 ((((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) + ((100 · 𝑂) + 𝑃𝑄)) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
18824sqcli 12984 . . . . . . . . . . . . 13 (10↑2) ∈ ℂ
189132, 188mulcli 10083 . . . . . . . . . . . 12 (𝐼𝐽𝐾 · (10↑2)) ∈ ℂ
190164, 189eqeltrri 2727 . . . . . . . . . . 11 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) ∈ ℂ
191190, 181, 103adddiri 10089 . . . . . . . . . 10 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · 100) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) + (𝐿𝑀𝑁 · 100))
192114oveq2i 6701 . . . . . . . . . 10 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · 100)
193175, 142subcli 10395 . . . . . . . . . . . . 13 (𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) ∈ ℂ
194193, 24, 103mulassi 10087 . . . . . . . . . . . 12 (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · (10 · 100))
195102dec0u 11558 . . . . . . . . . . . . 13 (10 · 100) = 1000
196195oveq2i 6701 . . . . . . . . . . . 12 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · (10 · 100)) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 1000)
197175, 142, 177subdiri 10518 . . . . . . . . . . . 12 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 1000) = ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000))
198194, 196, 1973eqtrri 2678 . . . . . . . . . . 11 ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) = (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100)
199103, 181mulcomi 10084 . . . . . . . . . . 11 (100 · 𝐿𝑀𝑁) = (𝐿𝑀𝑁 · 100)
200198, 199oveq12i 6702 . . . . . . . . . 10 (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) + (𝐿𝑀𝑁 · 100))
201191, 192, 2003eqtr4i 2683 . . . . . . . . 9 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁))
202201, 183oveq12i 6702 . . . . . . . 8 (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄) = ((((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) + ((100 · 𝑂) + 𝑃𝑄))
203182, 186addcli 10082 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℂ
204 subsub 10349 . . . . . . . . 9 (((𝑊𝑋𝑌𝑍 · 1000) ∈ ℂ ∧ ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℂ ∧ ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℂ) → ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
205178, 179, 203, 204mp3an 1464 . . . . . . . 8 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
206187, 202, 2053eqtr4ri 2684 . . . . . . 7 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
207167, 206eqtr4i 2676 . . . . . 6 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) = ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
208174nn0rei 11341 . . . . . . . 8 𝑊𝑋𝑌𝑍 ∈ ℝ
209176nn0rei 11341 . . . . . . . 8 1000 ∈ ℝ
210208, 209remulcli 10092 . . . . . . 7 (𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ
211139nn0rei 11341 . . . . . . . . . . 11 𝑅𝑆𝑇 ∈ ℝ
212 1re 10077 . . . . . . . . . . 11 1 ∈ ℝ
213211, 212readdcli 10091 . . . . . . . . . 10 (𝑅𝑆𝑇 + 1) ∈ ℝ
214213, 209remulcli 10092 . . . . . . . . 9 ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℝ
215102nn0rei 11341 . . . . . . . . . . 11 100 ∈ ℝ
21617nn0rei 11341 . . . . . . . . . . 11 𝐿𝑀𝑁 ∈ ℝ
217215, 216remulcli 10092 . . . . . . . . . 10 (100 · 𝐿𝑀𝑁) ∈ ℝ
21861nn0rei 11341 . . . . . . . . . . . 12 𝑂 ∈ ℝ
219215, 218remulcli 10092 . . . . . . . . . . 11 (100 · 𝑂) ∈ ℝ
22062, 63deccl 11550 . . . . . . . . . . . 12 𝑃𝑄 ∈ ℕ0
221220nn0rei 11341 . . . . . . . . . . 11 𝑃𝑄 ∈ ℝ
222219, 221readdcli 10091 . . . . . . . . . 10 ((100 · 𝑂) + 𝑃𝑄) ∈ ℝ
223217, 222readdcli 10091 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℝ
224214, 223resubcli 10381 . . . . . . . 8 (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ
225219recni 10090 . . . . . . . . . . . 12 (100 · 𝑂) ∈ ℂ
226221recni 10090 . . . . . . . . . . . 12 𝑃𝑄 ∈ ℂ
227182, 225, 226addassi 10086 . . . . . . . . . . 11 (((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) + 𝑃𝑄) = ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))
228218recni 10090 . . . . . . . . . . . . . 14 𝑂 ∈ ℂ
229103, 181, 228adddii 10088 . . . . . . . . . . . . 13 (100 · (𝐿𝑀𝑁 + 𝑂)) = ((100 · 𝐿𝑀𝑁) + (100 · 𝑂))
230 dpmul4.1 . . . . . . . . . . . . . 14 (𝐿𝑀𝑁 + 𝑂) = 𝑅𝑆𝑇𝑈
231230oveq2i 6701 . . . . . . . . . . . . 13 (100 · (𝐿𝑀𝑁 + 𝑂)) = (100 · 𝑅𝑆𝑇𝑈)
232229, 231eqtr3i 2675 . . . . . . . . . . . 12 ((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) = (100 · 𝑅𝑆𝑇𝑈)
233232oveq1i 6700 . . . . . . . . . . 11 (((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) + 𝑃𝑄) = ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄)
234227, 233eqtr3i 2675 . . . . . . . . . 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 11576 . . . . . . . . . . . 12 𝑈𝑃𝑄 < 1000
240235, 62deccl 11550 . . . . . . . . . . . . . . 15 𝑈𝑃 ∈ ℕ0
241240, 63deccl 11550 . . . . . . . . . . . . . 14 𝑈𝑃𝑄 ∈ ℕ0
242241nn0rei 11341 . . . . . . . . . . . . 13 𝑈𝑃𝑄 ∈ ℝ
243211, 209remulcli 10092 . . . . . . . . . . . . 13 (𝑅𝑆𝑇 · 1000) ∈ ℝ
244242, 209, 243ltadd2i 10206 . . . . . . . . . . . 12 (𝑈𝑃𝑄 < 1000 ↔ ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) < ((𝑅𝑆𝑇 · 1000) + 1000))
245239, 244mpbi 220 . . . . . . . . . . 11 ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) < ((𝑅𝑆𝑇 · 1000) + 1000)
246140, 177mulcli 10083 . . . . . . . . . . . . 13 (𝑅𝑆𝑇 · 1000) ∈ ℂ
247235nn0cni 11342 . . . . . . . . . . . . . 14 𝑈 ∈ ℂ
248103, 247mulcli 10083 . . . . . . . . . . . . 13 (100 · 𝑈) ∈ ℂ
249246, 248, 226addassi 10086 . . . . . . . . . . . 12 (((𝑅𝑆𝑇 · 1000) + (100 · 𝑈)) + 𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + ((100 · 𝑈) + 𝑃𝑄))
250 dfdec10 11535 . . . . . . . . . . . . . . 15 𝑅𝑆𝑇𝑈 = ((10 · 𝑅𝑆𝑇) + 𝑈)
251250oveq2i 6701 . . . . . . . . . . . . . 14 (100 · 𝑅𝑆𝑇𝑈) = (100 · ((10 · 𝑅𝑆𝑇) + 𝑈))
25224, 140mulcli 10083 . . . . . . . . . . . . . . 15 (10 · 𝑅𝑆𝑇) ∈ ℂ
253103, 252, 247adddii 10088 . . . . . . . . . . . . . 14 (100 · ((10 · 𝑅𝑆𝑇) + 𝑈)) = ((100 · (10 · 𝑅𝑆𝑇)) + (100 · 𝑈))
254140, 177mulcomi 10084 . . . . . . . . . . . . . . . 16 (𝑅𝑆𝑇 · 1000) = (1000 · 𝑅𝑆𝑇)
25524, 103mulcomi 10084 . . . . . . . . . . . . . . . . . 18 (10 · 100) = (100 · 10)
256255, 195eqtr3i 2675 . . . . . . . . . . . . . . . . 17 (100 · 10) = 1000
257256oveq1i 6700 . . . . . . . . . . . . . . . 16 ((100 · 10) · 𝑅𝑆𝑇) = (1000 · 𝑅𝑆𝑇)
258103, 24, 140mulassi 10087 . . . . . . . . . . . . . . . 16 ((100 · 10) · 𝑅𝑆𝑇) = (100 · (10 · 𝑅𝑆𝑇))
259254, 257, 2583eqtr2ri 2680 . . . . . . . . . . . . . . 15 (100 · (10 · 𝑅𝑆𝑇)) = (𝑅𝑆𝑇 · 1000)
260259oveq1i 6700 . . . . . . . . . . . . . 14 ((100 · (10 · 𝑅𝑆𝑇)) + (100 · 𝑈)) = ((𝑅𝑆𝑇 · 1000) + (100 · 𝑈))
261251, 253, 2603eqtri 2677 . . . . . . . . . . . . 13 (100 · 𝑅𝑆𝑇𝑈) = ((𝑅𝑆𝑇 · 1000) + (100 · 𝑈))
262261oveq1i 6700 . . . . . . . . . . . 12 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) = (((𝑅𝑆𝑇 · 1000) + (100 · 𝑈)) + 𝑃𝑄)
263235, 62, 64dfdec100 29704 . . . . . . . . . . . . 13 𝑈𝑃𝑄 = ((100 · 𝑈) + 𝑃𝑄)
264263oveq2i 6701 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + ((100 · 𝑈) + 𝑃𝑄))
265249, 262, 2643eqtr4i 2683 . . . . . . . . . . 11 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄)
266140, 141, 177adddiri 10089 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 + 1) · 1000) = ((𝑅𝑆𝑇 · 1000) + (1 · 1000))
267177mulid2i 10081 . . . . . . . . . . . . 13 (1 · 1000) = 1000
268267oveq2i 6701 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 · 1000) + (1 · 1000)) = ((𝑅𝑆𝑇 · 1000) + 1000)
269266, 268eqtri 2673 . . . . . . . . . . 11 ((𝑅𝑆𝑇 + 1) · 1000) = ((𝑅𝑆𝑇 · 1000) + 1000)
270245, 265, 2693brtr4i 4715 . . . . . . . . . 10 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) < ((𝑅𝑆𝑇 + 1) · 1000)
271234, 270eqbrtri 4706 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) < ((𝑅𝑆𝑇 + 1) · 1000)
272223, 214posdifi 10616 . . . . . . . . 9 (((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) < ((𝑅𝑆𝑇 + 1) · 1000) ↔ 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
273271, 272mpbi 220 . . . . . . . 8 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
274 elrp 11872 . . . . . . . 8 ((((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+ ↔ ((((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ ∧ 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))))
275224, 273, 274mpbir2an 975 . . . . . . 7 (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+
276 ltsubrp 11904 . . . . . . 7 (((𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ ∧ (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+) → ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) < (𝑊𝑋𝑌𝑍 · 1000))
277210, 275, 276mp2an 708 . . . . . 6 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) < (𝑊𝑋𝑌𝑍 · 1000)
278207, 277eqbrtri 4706 . . . . 5 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000)
2793, 4deccl 11550 . . . . . . . . 9 𝐴𝐵𝐶 ∈ ℕ0
280279, 5deccl 11550 . . . . . . . 8 𝐴𝐵𝐶𝐷 ∈ ℕ0
281280nn0rei 11341 . . . . . . 7 𝐴𝐵𝐶𝐷 ∈ ℝ
2829, 10deccl 11550 . . . . . . . . 9 𝐸𝐹𝐺 ∈ ℕ0
283282, 11deccl 11550 . . . . . . . 8 𝐸𝐹𝐺𝐻 ∈ ℕ0
284283nn0rei 11341 . . . . . . 7 𝐸𝐹𝐺𝐻 ∈ ℝ
285281, 284remulcli 10092 . . . . . 6 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) ∈ ℝ
28623decnncl2 11563 . . . . . . . . 9 100 ∈ ℕ
287286decnncl2 11563 . . . . . . . 8 1000 ∈ ℕ
288287nngt0i 11092 . . . . . . 7 0 < 1000
289209, 288pm3.2i 470 . . . . . 6 (1000 ∈ ℝ ∧ 0 < 1000)
290 ltdiv1 10925 . . . . . 6 (((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) ∈ ℝ ∧ (𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ ∧ (1000 ∈ ℝ ∧ 0 < 1000)) → ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000) ↔ ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000)))
291285, 210, 289, 290mp3an 1464 . . . . 5 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000) ↔ ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000))
292278, 291mpbi 220 . . . 4 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000)
293280nn0cni 11342 . . . . . 6 𝐴𝐵𝐶𝐷 ∈ ℂ
294283nn0cni 11342 . . . . . 6 𝐸𝐹𝐺𝐻 ∈ ℂ
295209, 288gt0ne0ii 10602 . . . . . 6 1000 ≠ 0
296293, 294, 177, 295div23i 10821 . . . . 5 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴𝐵𝐶𝐷 / 1000) · 𝐸𝐹𝐺𝐻)
2971, 2, 4, 48dpmul1000 29735 . . . . . . . 8 ((𝐴.𝐵𝐶𝐷) · 1000) = 𝐴𝐵𝐶𝐷
298297oveq1i 6700 . . . . . . 7 (((𝐴.𝐵𝐶𝐷) · 1000) / 1000) = (𝐴𝐵𝐶𝐷 / 1000)
2994nn0rei 11341 . . . . . . . . . . . 12 𝐶 ∈ ℝ
300 dp2cl 29715 . . . . . . . . . . . 12 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → 𝐶𝐷 ∈ ℝ)
301299, 48, 300mp2an 708 . . . . . . . . . . 11 𝐶𝐷 ∈ ℝ
302 dp2cl 29715 . . . . . . . . . . 11 ((𝐵 ∈ ℝ ∧ 𝐶𝐷 ∈ ℝ) → 𝐵𝐶𝐷 ∈ ℝ)
30319, 301, 302mp2an 708 . . . . . . . . . 10 𝐵𝐶𝐷 ∈ ℝ
304 dpcl 29726 . . . . . . . . . 10 ((𝐴 ∈ ℕ0𝐵𝐶𝐷 ∈ ℝ) → (𝐴.𝐵𝐶𝐷) ∈ ℝ)
3051, 303, 304mp2an 708 . . . . . . . . 9 (𝐴.𝐵𝐶𝐷) ∈ ℝ
306305recni 10090 . . . . . . . 8 (𝐴.𝐵𝐶𝐷) ∈ ℂ
307306, 177, 295divcan4i 10810 . . . . . . 7 (((𝐴.𝐵𝐶𝐷) · 1000) / 1000) = (𝐴.𝐵𝐶𝐷)
308298, 307eqtr3i 2675 . . . . . 6 (𝐴𝐵𝐶𝐷 / 1000) = (𝐴.𝐵𝐶𝐷)
309308oveq1i 6700 . . . . 5 ((𝐴𝐵𝐶𝐷 / 1000) · 𝐸𝐹𝐺𝐻) = ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻)
310296, 309eqtri 2673 . . . 4 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻)
311175, 177, 295divcan4i 10810 . . . 4 ((𝑊𝑋𝑌𝑍 · 1000) / 1000) = 𝑊𝑋𝑌𝑍
312292, 310, 3113brtr3i 4714 . . 3 ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍
313305, 284remulcli 10092 . . . 4 ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) ∈ ℝ
314 ltdiv1 10925 . . . 4 ((((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) ∈ ℝ ∧ 𝑊𝑋𝑌𝑍 ∈ ℝ ∧ (1000 ∈ ℝ ∧ 0 < 1000)) → (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍 ↔ (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000)))
315313, 208, 289, 314mp3an 1464 . . 3 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍 ↔ (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000))
316312, 315mpbi 220 . 2 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000)
317306, 294, 177, 295divassi 10819 . . 3 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · (𝐸𝐹𝐺𝐻 / 1000))
3187, 8, 10, 52dpmul1000 29735 . . . . . 6 ((𝐸.𝐹𝐺𝐻) · 1000) = 𝐸𝐹𝐺𝐻
319318oveq1i 6700 . . . . 5 (((𝐸.𝐹𝐺𝐻) · 1000) / 1000) = (𝐸𝐹𝐺𝐻 / 1000)
32010nn0rei 11341 . . . . . . . . . 10 𝐺 ∈ ℝ
321 dp2cl 29715 . . . . . . . . . 10 ((𝐺 ∈ ℝ ∧ 𝐻 ∈ ℝ) → 𝐺𝐻 ∈ ℝ)
322320, 52, 321mp2an 708 . . . . . . . . 9 𝐺𝐻 ∈ ℝ
323 dp2cl 29715 . . . . . . . . 9 ((𝐹 ∈ ℝ ∧ 𝐺𝐻 ∈ ℝ) → 𝐹𝐺𝐻 ∈ ℝ)
32425, 322, 323mp2an 708 . . . . . . . 8 𝐹𝐺𝐻 ∈ ℝ
325 dpcl 29726 . . . . . . . 8 ((𝐸 ∈ ℕ0𝐹𝐺𝐻 ∈ ℝ) → (𝐸.𝐹𝐺𝐻) ∈ ℝ)
3267, 324, 325mp2an 708 . . . . . . 7 (𝐸.𝐹𝐺𝐻) ∈ ℝ
327326recni 10090 . . . . . 6 (𝐸.𝐹𝐺𝐻) ∈ ℂ
328327, 177, 295divcan4i 10810 . . . . 5 (((𝐸.𝐹𝐺𝐻) · 1000) / 1000) = (𝐸.𝐹𝐺𝐻)
329319, 328eqtr3i 2675 . . . 4 (𝐸𝐹𝐺𝐻 / 1000) = (𝐸.𝐹𝐺𝐻)
330329oveq2i 6701 . . 3 ((𝐴.𝐵𝐶𝐷) · (𝐸𝐹𝐺𝐻 / 1000)) = ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻))
331317, 330eqtri 2673 . 2 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻))
332173nn0rei 11341 . . . . 5 𝑍 ∈ ℝ
333168, 169, 171, 332dpmul1000 29735 . . . 4 ((𝑊.𝑋𝑌𝑍) · 1000) = 𝑊𝑋𝑌𝑍
334333oveq1i 6700 . . 3 (((𝑊.𝑋𝑌𝑍) · 1000) / 1000) = (𝑊𝑋𝑌𝑍 / 1000)
335169nn0rei 11341 . . . . . . 7 𝑋 ∈ ℝ
336171nn0rei 11341 . . . . . . . 8 𝑌 ∈ ℝ
337 dp2cl 29715 . . . . . . . 8 ((𝑌 ∈ ℝ ∧ 𝑍 ∈ ℝ) → 𝑌𝑍 ∈ ℝ)
338336, 332, 337mp2an 708 . . . . . . 7 𝑌𝑍 ∈ ℝ
339 dp2cl 29715 . . . . . . 7 ((𝑋 ∈ ℝ ∧ 𝑌𝑍 ∈ ℝ) → 𝑋𝑌𝑍 ∈ ℝ)
340335, 338, 339mp2an 708 . . . . . 6 𝑋𝑌𝑍 ∈ ℝ
341 dpcl 29726 . . . . . 6 ((𝑊 ∈ ℕ0𝑋𝑌𝑍 ∈ ℝ) → (𝑊.𝑋𝑌𝑍) ∈ ℝ)
342168, 340, 341mp2an 708 . . . . 5 (𝑊.𝑋𝑌𝑍) ∈ ℝ
343342recni 10090 . . . 4 (𝑊.𝑋𝑌𝑍) ∈ ℂ
344343, 177, 295divcan4i 10810 . . 3 (((𝑊.𝑋𝑌𝑍) · 1000) / 1000) = (𝑊.𝑋𝑌𝑍)
345334, 344eqtr3i 2675 . 2 (𝑊𝑋𝑌𝑍 / 1000) = (𝑊.𝑋𝑌𝑍)
346316, 331, 3453brtr3i 4714 1 ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻)) < (𝑊.𝑋𝑌𝑍)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1523  wcel 2030   class class class wbr 4685  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cmin 10304   / cdiv 10722  2c2 11108  0cn0 11330  cdc 11531  +crp 11870  cexp 12900  cdp2 29705  .cdp 29723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-rp 11871  df-seq 12842  df-exp 12901  df-dp2 29706  df-dp 29724
This theorem is referenced by:  hgt750lem2  30858
  Copyright terms: Public domain W3C validator