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 30072
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 11758 . . . . . . . 8 𝐴𝐵 ∈ ℕ0
4 dpmul.c . . . . . . . . 9 𝐶 ∈ ℕ0
5 dpmul.d . . . . . . . . 9 𝐷 ∈ ℕ0
64, 5deccl 11758 . . . . . . . 8 𝐶𝐷 ∈ ℕ0
7 dpmul.e . . . . . . . . 9 𝐸 ∈ ℕ0
8 dpmul4.f . . . . . . . . 9 𝐹 ∈ ℕ0
97, 8deccl 11758 . . . . . . . 8 𝐸𝐹 ∈ ℕ0
10 dpmul.g . . . . . . . . 9 𝐺 ∈ ℕ0
11 dpmul4.h . . . . . . . . 9 𝐻 ∈ ℕ0
1210, 11deccl 11758 . . . . . . . 8 𝐺𝐻 ∈ ℕ0
13 dpmul4.l . . . . . . . . . 10 𝐿 ∈ ℕ0
14 dpmul4.m . . . . . . . . . 10 𝑀 ∈ ℕ0
1513, 14deccl 11758 . . . . . . . . 9 𝐿𝑀 ∈ ℕ0
16 dpmul4.n . . . . . . . . 9 𝑁 ∈ ℕ0
1715, 16deccl 11758 . . . . . . . 8 𝐿𝑀𝑁 ∈ ℕ0
18 2nn0 11559 . . . . . . . 8 2 ∈ ℕ0
192nn0rei 11552 . . . . . . . . . . . . 13 𝐵 ∈ ℝ
20 dpcl 30049 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ0𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)
211, 19, 20mp2an 683 . . . . . . . . . . . 12 (𝐴.𝐵) ∈ ℝ
2221recni 10310 . . . . . . . . . . 11 (𝐴.𝐵) ∈ ℂ
23 10nn 11759 . . . . . . . . . . . 12 10 ∈ ℕ
2423nncni 11287 . . . . . . . . . . 11 10 ∈ ℂ
258nn0rei 11552 . . . . . . . . . . . . 13 𝐹 ∈ ℝ
26 dpcl 30049 . . . . . . . . . . . . 13 ((𝐸 ∈ ℕ0𝐹 ∈ ℝ) → (𝐸.𝐹) ∈ ℝ)
277, 25, 26mp2an 683 . . . . . . . . . . . 12 (𝐸.𝐹) ∈ ℝ
2827recni 10310 . . . . . . . . . . 11 (𝐸.𝐹) ∈ ℂ
2922, 24, 28, 24mul4i 10489 . . . . . . . . . 10 (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10)) = (((𝐴.𝐵) · (𝐸.𝐹)) · (10 · 10))
3022, 28mulcli 10303 . . . . . . . . . . 11 ((𝐴.𝐵) · (𝐸.𝐹)) ∈ ℂ
3130, 24, 24mulassi 10307 . . . . . . . . . 10 ((((𝐴.𝐵) · (𝐸.𝐹)) · 10) · 10) = (((𝐴.𝐵) · (𝐸.𝐹)) · (10 · 10))
32 dpmul4.2 . . . . . . . . . . . . 13 ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼.𝐽𝐾)
3332oveq1i 6854 . . . . . . . . . . . 12 (((𝐴.𝐵) · (𝐸.𝐹)) · 10) = ((𝐼.𝐽𝐾) · 10)
34 dpmul4.i . . . . . . . . . . . . 13 𝐼 ∈ ℕ0
35 dpmul.j . . . . . . . . . . . . 13 𝐽 ∈ ℕ0
36 dpmul.k . . . . . . . . . . . . . 14 𝐾 ∈ ℕ0
3736nn0rei 11552 . . . . . . . . . . . . 13 𝐾 ∈ ℝ
3834, 35, 37dp3mul10 30056 . . . . . . . . . . . 12 ((𝐼.𝐽𝐾) · 10) = (𝐼𝐽.𝐾)
3933, 38eqtri 2787 . . . . . . . . . . 11 (((𝐴.𝐵) · (𝐸.𝐹)) · 10) = (𝐼𝐽.𝐾)
4039oveq1i 6854 . . . . . . . . . 10 ((((𝐴.𝐵) · (𝐸.𝐹)) · 10) · 10) = ((𝐼𝐽.𝐾) · 10)
4129, 31, 403eqtr2ri 2794 . . . . . . . . 9 ((𝐼𝐽.𝐾) · 10) = (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10))
4234, 35deccl 11758 . . . . . . . . . 10 𝐼𝐽 ∈ ℕ0
4342, 37dpmul10 30053 . . . . . . . . 9 ((𝐼𝐽.𝐾) · 10) = 𝐼𝐽𝐾
441, 19dpmul10 30053 . . . . . . . . . 10 ((𝐴.𝐵) · 10) = 𝐴𝐵
457, 25dpmul10 30053 . . . . . . . . . 10 ((𝐸.𝐹) · 10) = 𝐸𝐹
4644, 45oveq12i 6856 . . . . . . . . 9 (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10)) = (𝐴𝐵 · 𝐸𝐹)
4741, 43, 463eqtr3ri 2796 . . . . . . . 8 (𝐴𝐵 · 𝐸𝐹) = 𝐼𝐽𝐾
485nn0rei 11552 . . . . . . . . . . . . 13 𝐷 ∈ ℝ
49 dpcl 30049 . . . . . . . . . . . . 13 ((𝐶 ∈ ℕ0𝐷 ∈ ℝ) → (𝐶.𝐷) ∈ ℝ)
504, 48, 49mp2an 683 . . . . . . . . . . . 12 (𝐶.𝐷) ∈ ℝ
5150recni 10310 . . . . . . . . . . 11 (𝐶.𝐷) ∈ ℂ
5211nn0rei 11552 . . . . . . . . . . . . 13 𝐻 ∈ ℝ
53 dpcl 30049 . . . . . . . . . . . . 13 ((𝐺 ∈ ℕ0𝐻 ∈ ℝ) → (𝐺.𝐻) ∈ ℝ)
5410, 52, 53mp2an 683 . . . . . . . . . . . 12 (𝐺.𝐻) ∈ ℝ
5554recni 10310 . . . . . . . . . . 11 (𝐺.𝐻) ∈ ℂ
5651, 24, 55, 24mul4i 10489 . . . . . . . . . 10 (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10)) = (((𝐶.𝐷) · (𝐺.𝐻)) · (10 · 10))
5751, 55mulcli 10303 . . . . . . . . . . 11 ((𝐶.𝐷) · (𝐺.𝐻)) ∈ ℂ
5857, 24, 24mulassi 10307 . . . . . . . . . 10 ((((𝐶.𝐷) · (𝐺.𝐻)) · 10) · 10) = (((𝐶.𝐷) · (𝐺.𝐻)) · (10 · 10))
59 dpmul4.3 . . . . . . . . . . . . 13 ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂.𝑃𝑄)
6059oveq1i 6854 . . . . . . . . . . . 12 (((𝐶.𝐷) · (𝐺.𝐻)) · 10) = ((𝑂.𝑃𝑄) · 10)
61 dpmul4.o . . . . . . . . . . . . 13 𝑂 ∈ ℕ0
62 dpmul4.p . . . . . . . . . . . . 13 𝑃 ∈ ℕ0
63 dpmul4.q . . . . . . . . . . . . . 14 𝑄 ∈ ℕ0
6463nn0rei 11552 . . . . . . . . . . . . 13 𝑄 ∈ ℝ
6561, 62, 64dp3mul10 30056 . . . . . . . . . . . 12 ((𝑂.𝑃𝑄) · 10) = (𝑂𝑃.𝑄)
6660, 65eqtri 2787 . . . . . . . . . . 11 (((𝐶.𝐷) · (𝐺.𝐻)) · 10) = (𝑂𝑃.𝑄)
6766oveq1i 6854 . . . . . . . . . 10 ((((𝐶.𝐷) · (𝐺.𝐻)) · 10) · 10) = ((𝑂𝑃.𝑄) · 10)
6856, 58, 673eqtr2ri 2794 . . . . . . . . 9 ((𝑂𝑃.𝑄) · 10) = (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10))
6961, 62deccl 11758 . . . . . . . . . 10 𝑂𝑃 ∈ ℕ0
7069, 64dpmul10 30053 . . . . . . . . 9 ((𝑂𝑃.𝑄) · 10) = 𝑂𝑃𝑄
714, 48dpmul10 30053 . . . . . . . . . 10 ((𝐶.𝐷) · 10) = 𝐶𝐷
7210, 52dpmul10 30053 . . . . . . . . . 10 ((𝐺.𝐻) · 10) = 𝐺𝐻
7371, 72oveq12i 6856 . . . . . . . . 9 (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10)) = (𝐶𝐷 · 𝐺𝐻)
7468, 70, 733eqtr3ri 2796 . . . . . . . 8 (𝐶𝐷 · 𝐺𝐻) = 𝑂𝑃𝑄
7522, 51, 24adddiri 10309 . . . . . . . . . . . 12 (((𝐴.𝐵) + (𝐶.𝐷)) · 10) = (((𝐴.𝐵) · 10) + ((𝐶.𝐷) · 10))
7644, 71oveq12i 6856 . . . . . . . . . . . 12 (((𝐴.𝐵) · 10) + ((𝐶.𝐷) · 10)) = (𝐴𝐵 + 𝐶𝐷)
7775, 76eqtr2i 2788 . . . . . . . . . . 11 (𝐴𝐵 + 𝐶𝐷) = (((𝐴.𝐵) + (𝐶.𝐷)) · 10)
7828, 55, 24adddiri 10309 . . . . . . . . . . . 12 (((𝐸.𝐹) + (𝐺.𝐻)) · 10) = (((𝐸.𝐹) · 10) + ((𝐺.𝐻) · 10))
7945, 72oveq12i 6856 . . . . . . . . . . . 12 (((𝐸.𝐹) · 10) + ((𝐺.𝐻) · 10)) = (𝐸𝐹 + 𝐺𝐻)
8078, 79eqtr2i 2788 . . . . . . . . . . 11 (𝐸𝐹 + 𝐺𝐻) = (((𝐸.𝐹) + (𝐺.𝐻)) · 10)
8177, 80oveq12i 6856 . . . . . . . . . 10 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · 10) · (((𝐸.𝐹) + (𝐺.𝐻)) · 10))
8222, 51addcli 10302 . . . . . . . . . . 11 ((𝐴.𝐵) + (𝐶.𝐷)) ∈ ℂ
8328, 55addcli 10302 . . . . . . . . . . 11 ((𝐸.𝐹) + (𝐺.𝐻)) ∈ ℂ
8482, 24, 83, 24mul4i 10489 . . . . . . . . . 10 ((((𝐴.𝐵) + (𝐶.𝐷)) · 10) · (((𝐸.𝐹) + (𝐺.𝐻)) · 10)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (10 · 10))
85 dpmul4.5 . . . . . . . . . . 11 (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄))
8685oveq1i 6854 . . . . . . . . . 10 ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (10 · 10)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10))
8781, 84, 863eqtri 2791 . . . . . . . . 9 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10))
88 10nn0 11761 . . . . . . . . . . 11 10 ∈ ℕ0
8988dec0u 11765 . . . . . . . . . 10 (10 · 10) = 100
9089oveq2i 6855 . . . . . . . . 9 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100)
9132, 30eqeltrri 2841 . . . . . . . . . . . 12 (𝐼.𝐽𝐾) ∈ ℂ
9214nn0rei 11552 . . . . . . . . . . . . . . 15 𝑀 ∈ ℝ
9316nn0rei 11552 . . . . . . . . . . . . . . 15 𝑁 ∈ ℝ
94 dp2cl 30038 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀𝑁 ∈ ℝ)
9592, 93, 94mp2an 683 . . . . . . . . . . . . . 14 𝑀𝑁 ∈ ℝ
96 dpcl 30049 . . . . . . . . . . . . . 14 ((𝐿 ∈ ℕ0𝑀𝑁 ∈ ℝ) → (𝐿.𝑀𝑁) ∈ ℝ)
9713, 95, 96mp2an 683 . . . . . . . . . . . . 13 (𝐿.𝑀𝑁) ∈ ℝ
9897recni 10310 . . . . . . . . . . . 12 (𝐿.𝑀𝑁) ∈ ℂ
9991, 98addcli 10302 . . . . . . . . . . 11 ((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) ∈ ℂ
10059, 57eqeltrri 2841 . . . . . . . . . . 11 (𝑂.𝑃𝑄) ∈ ℂ
101 0nn0 11557 . . . . . . . . . . . . 13 0 ∈ ℕ0
10288, 101deccl 11758 . . . . . . . . . . . 12 100 ∈ ℕ0
103102nn0cni 11553 . . . . . . . . . . 11 100 ∈ ℂ
10499, 100, 103adddiri 10309 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) + ((𝑂.𝑃𝑄) · 100))
10591, 98, 103adddiri 10309 . . . . . . . . . . 11 (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) = (((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100))
106105oveq1i 6854 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) + ((𝑂.𝑃𝑄) · 100)) = ((((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) + ((𝑂.𝑃𝑄) · 100))
10734, 35, 37dpmul100 30055 . . . . . . . . . . . 12 ((𝐼.𝐽𝐾) · 100) = 𝐼𝐽𝐾
10813, 14, 93dpmul100 30055 . . . . . . . . . . . 12 ((𝐿.𝑀𝑁) · 100) = 𝐿𝑀𝑁
109107, 108oveq12i 6856 . . . . . . . . . . 11 (((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) = (𝐼𝐽𝐾 + 𝐿𝑀𝑁)
11061, 62, 64dpmul100 30055 . . . . . . . . . . 11 ((𝑂.𝑃𝑄) · 100) = 𝑂𝑃𝑄
111109, 110oveq12i 6856 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) + ((𝑂.𝑃𝑄) · 100)) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
112104, 106, 1113eqtri 2791 . . . . . . . . 9 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
11387, 90, 1123eqtri 2791 . . . . . . . 8 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
114 sq10 13258 . . . . . . . . . . . 12 (10↑2) = 100
115114oveq2i 6855 . . . . . . . . . . 11 (𝐴𝐵 · (10↑2)) = (𝐴𝐵 · 100)
1163nn0cni 11553 . . . . . . . . . . . 12 𝐴𝐵 ∈ ℂ
117103, 116mulcomi 10304 . . . . . . . . . . 11 (100 · 𝐴𝐵) = (𝐴𝐵 · 100)
118115, 117eqtr4i 2790 . . . . . . . . . 10 (𝐴𝐵 · (10↑2)) = (100 · 𝐴𝐵)
119118oveq1i 6854 . . . . . . . . 9 ((𝐴𝐵 · (10↑2)) + 𝐶𝐷) = ((100 · 𝐴𝐵) + 𝐶𝐷)
1203, 4, 48dfdec100 30028 . . . . . . . . 9 𝐴𝐵𝐶𝐷 = ((100 · 𝐴𝐵) + 𝐶𝐷)
121119, 120eqtr4i 2790 . . . . . . . 8 ((𝐴𝐵 · (10↑2)) + 𝐶𝐷) = 𝐴𝐵𝐶𝐷
122114oveq2i 6855 . . . . . . . . . . 11 (𝐸𝐹 · (10↑2)) = (𝐸𝐹 · 100)
1239nn0cni 11553 . . . . . . . . . . . 12 𝐸𝐹 ∈ ℂ
124103, 123mulcomi 10304 . . . . . . . . . . 11 (100 · 𝐸𝐹) = (𝐸𝐹 · 100)
125122, 124eqtr4i 2790 . . . . . . . . . 10 (𝐸𝐹 · (10↑2)) = (100 · 𝐸𝐹)
126125oveq1i 6854 . . . . . . . . 9 ((𝐸𝐹 · (10↑2)) + 𝐺𝐻) = ((100 · 𝐸𝐹) + 𝐺𝐻)
1279, 10, 52dfdec100 30028 . . . . . . . . 9 𝐸𝐹𝐺𝐻 = ((100 · 𝐸𝐹) + 𝐺𝐻)
128126, 127eqtr4i 2790 . . . . . . . 8 ((𝐸𝐹 · (10↑2)) + 𝐺𝐻) = 𝐸𝐹𝐺𝐻
12924sqvali 13153 . . . . . . . . . . . 12 (10↑2) = (10 · 10)
130129oveq2i 6855 . . . . . . . . . . 11 (𝐼𝐽𝐾 · (10↑2)) = (𝐼𝐽𝐾 · (10 · 10))
13142, 36deccl 11758 . . . . . . . . . . . . 13 𝐼𝐽𝐾 ∈ ℕ0
132131nn0cni 11553 . . . . . . . . . . . 12 𝐼𝐽𝐾 ∈ ℂ
133132, 24, 24mulassi 10307 . . . . . . . . . . 11 ((𝐼𝐽𝐾 · 10) · 10) = (𝐼𝐽𝐾 · (10 · 10))
134130, 133eqtr4i 2790 . . . . . . . . . 10 (𝐼𝐽𝐾 · (10↑2)) = ((𝐼𝐽𝐾 · 10) · 10)
135 dpmul4.r . . . . . . . . . . . . . . . 16 𝑅 ∈ ℕ0
136 dpmul4.s . . . . . . . . . . . . . . . 16 𝑆 ∈ ℕ0
137135, 136deccl 11758 . . . . . . . . . . . . . . 15 𝑅𝑆 ∈ ℕ0
138 dpmul4.t . . . . . . . . . . . . . . 15 𝑇 ∈ ℕ0
139137, 138deccl 11758 . . . . . . . . . . . . . 14 𝑅𝑆𝑇 ∈ ℕ0
140139nn0cni 11553 . . . . . . . . . . . . 13 𝑅𝑆𝑇 ∈ ℂ
141 ax-1cn 10249 . . . . . . . . . . . . 13 1 ∈ ℂ
142140, 141addcli 10302 . . . . . . . . . . . 12 (𝑅𝑆𝑇 + 1) ∈ ℂ
143132, 24mulcli 10303 . . . . . . . . . . . 12 (𝐼𝐽𝐾 · 10) ∈ ℂ
144141, 143addcomi 10483 . . . . . . . . . . . . . . . 16 (1 + (𝐼𝐽𝐾 · 10)) = ((𝐼𝐽𝐾 · 10) + 1)
14524, 132mulcomi 10304 . . . . . . . . . . . . . . . . . 18 (10 · 𝐼𝐽𝐾) = (𝐼𝐽𝐾 · 10)
146131dec0u 11765 . . . . . . . . . . . . . . . . . 18 (10 · 𝐼𝐽𝐾) = 𝐼𝐽𝐾0
147145, 146eqtr3i 2789 . . . . . . . . . . . . . . . . 17 (𝐼𝐽𝐾 · 10) = 𝐼𝐽𝐾0
148147oveq1i 6854 . . . . . . . . . . . . . . . 16 ((𝐼𝐽𝐾 · 10) + 1) = (𝐼𝐽𝐾0 + 1)
149141addid2i 10480 . . . . . . . . . . . . . . . . 17 (0 + 1) = 1
150 eqid 2765 . . . . . . . . . . . . . . . . 17 𝐼𝐽𝐾0 = 𝐼𝐽𝐾0
151131, 101, 149, 150decsuc 11775 . . . . . . . . . . . . . . . 16 (𝐼𝐽𝐾0 + 1) = 𝐼𝐽𝐾1
152144, 148, 1513eqtri 2791 . . . . . . . . . . . . . . 15 (1 + (𝐼𝐽𝐾 · 10)) = 𝐼𝐽𝐾1
153152oveq2i 6855 . . . . . . . . . . . . . 14 (𝑅𝑆𝑇 + (1 + (𝐼𝐽𝐾 · 10))) = (𝑅𝑆𝑇 + 𝐼𝐽𝐾1)
154140, 141, 143addassi 10306 . . . . . . . . . . . . . 14 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = (𝑅𝑆𝑇 + (1 + (𝐼𝐽𝐾 · 10)))
155 1nn0 11558 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ0
156131, 155deccl 11758 . . . . . . . . . . . . . . . 16 𝐼𝐽𝐾1 ∈ ℕ0
157156nn0cni 11553 . . . . . . . . . . . . . . 15 𝐼𝐽𝐾1 ∈ ℂ
158157, 140addcomi 10483 . . . . . . . . . . . . . 14 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = (𝑅𝑆𝑇 + 𝐼𝐽𝐾1)
159153, 154, 1583eqtr4i 2797 . . . . . . . . . . . . 13 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = (𝐼𝐽𝐾1 + 𝑅𝑆𝑇)
160 dpmul4.4 . . . . . . . . . . . . 13 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = 𝑊𝑋𝑌𝑍
161159, 160eqtri 2787 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = 𝑊𝑋𝑌𝑍
162142, 143, 161mvlladdi 10555 . . . . . . . . . . 11 (𝐼𝐽𝐾 · 10) = (𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1))
163162oveq1i 6854 . . . . . . . . . 10 ((𝐼𝐽𝐾 · 10) · 10) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10)
164134, 163eqtri 2787 . . . . . . . . 9 (𝐼𝐽𝐾 · (10↑2)) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10)
165164oveq1i 6854 . . . . . . . 8 ((𝐼𝐽𝐾 · (10↑2)) + 𝐿𝑀𝑁) = (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁)
166 eqid 2765 . . . . . . . 8 (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
1673, 6, 9, 12, 17, 18, 47, 74, 113, 121, 128, 165, 166karatsuba 16070 . . . . . . 7 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
168 dpmul4.w . . . . . . . . . . . . . . 15 𝑊 ∈ ℕ0
169 dpmul4.x . . . . . . . . . . . . . . 15 𝑋 ∈ ℕ0
170168, 169deccl 11758 . . . . . . . . . . . . . 14 𝑊𝑋 ∈ ℕ0
171 dpmul4.y . . . . . . . . . . . . . 14 𝑌 ∈ ℕ0
172170, 171deccl 11758 . . . . . . . . . . . . 13 𝑊𝑋𝑌 ∈ ℕ0
173 dpmul4.z . . . . . . . . . . . . 13 𝑍 ∈ ℕ0
174172, 173deccl 11758 . . . . . . . . . . . 12 𝑊𝑋𝑌𝑍 ∈ ℕ0
175174nn0cni 11553 . . . . . . . . . . 11 𝑊𝑋𝑌𝑍 ∈ ℂ
176102, 101deccl 11758 . . . . . . . . . . . 12 1000 ∈ ℕ0
177176nn0cni 11553 . . . . . . . . . . 11 1000 ∈ ℂ
178175, 177mulcli 10303 . . . . . . . . . 10 (𝑊𝑋𝑌𝑍 · 1000) ∈ ℂ
179142, 177mulcli 10303 . . . . . . . . . 10 ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℂ
180178, 179subcli 10613 . . . . . . . . 9 ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) ∈ ℂ
18117nn0cni 11553 . . . . . . . . . 10 𝐿𝑀𝑁 ∈ ℂ
182103, 181mulcli 10303 . . . . . . . . 9 (100 · 𝐿𝑀𝑁) ∈ ℂ
18361, 62, 64dfdec100 30028 . . . . . . . . . 10 𝑂𝑃𝑄 = ((100 · 𝑂) + 𝑃𝑄)
18469, 63deccl 11758 . . . . . . . . . . 11 𝑂𝑃𝑄 ∈ ℕ0
185184nn0cni 11553 . . . . . . . . . 10 𝑂𝑃𝑄 ∈ ℂ
186183, 185eqeltrri 2841 . . . . . . . . 9 ((100 · 𝑂) + 𝑃𝑄) ∈ ℂ
187180, 182, 186addassi 10306 . . . . . . . 8 ((((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) + ((100 · 𝑂) + 𝑃𝑄)) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
18824sqcli 13154 . . . . . . . . . . . . 13 (10↑2) ∈ ℂ
189132, 188mulcli 10303 . . . . . . . . . . . 12 (𝐼𝐽𝐾 · (10↑2)) ∈ ℂ
190164, 189eqeltrri 2841 . . . . . . . . . . 11 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) ∈ ℂ
191190, 181, 103adddiri 10309 . . . . . . . . . 10 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · 100) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) + (𝐿𝑀𝑁 · 100))
192114oveq2i 6855 . . . . . . . . . 10 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · 100)
193175, 142subcli 10613 . . . . . . . . . . . . 13 (𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) ∈ ℂ
194193, 24, 103mulassi 10307 . . . . . . . . . . . 12 (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · (10 · 100))
195102dec0u 11765 . . . . . . . . . . . . 13 (10 · 100) = 1000
196195oveq2i 6855 . . . . . . . . . . . 12 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · (10 · 100)) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 1000)
197175, 142, 177subdiri 10736 . . . . . . . . . . . 12 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 1000) = ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000))
198194, 196, 1973eqtrri 2792 . . . . . . . . . . 11 ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) = (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100)
199103, 181mulcomi 10304 . . . . . . . . . . 11 (100 · 𝐿𝑀𝑁) = (𝐿𝑀𝑁 · 100)
200198, 199oveq12i 6856 . . . . . . . . . 10 (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) + (𝐿𝑀𝑁 · 100))
201191, 192, 2003eqtr4i 2797 . . . . . . . . 9 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁))
202201, 183oveq12i 6856 . . . . . . . 8 (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄) = ((((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) + ((100 · 𝑂) + 𝑃𝑄))
203182, 186addcli 10302 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℂ
204 subsub 10567 . . . . . . . . 9 (((𝑊𝑋𝑌𝑍 · 1000) ∈ ℂ ∧ ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℂ ∧ ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℂ) → ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
205178, 179, 203, 204mp3an 1585 . . . . . . . 8 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
206187, 202, 2053eqtr4ri 2798 . . . . . . 7 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
207167, 206eqtr4i 2790 . . . . . 6 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) = ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
208174nn0rei 11552 . . . . . . . 8 𝑊𝑋𝑌𝑍 ∈ ℝ
209176nn0rei 11552 . . . . . . . 8 1000 ∈ ℝ
210208, 209remulcli 10312 . . . . . . 7 (𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ
211139nn0rei 11552 . . . . . . . . . . 11 𝑅𝑆𝑇 ∈ ℝ
212 1re 10295 . . . . . . . . . . 11 1 ∈ ℝ
213211, 212readdcli 10311 . . . . . . . . . 10 (𝑅𝑆𝑇 + 1) ∈ ℝ
214213, 209remulcli 10312 . . . . . . . . 9 ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℝ
215102nn0rei 11552 . . . . . . . . . . 11 100 ∈ ℝ
21617nn0rei 11552 . . . . . . . . . . 11 𝐿𝑀𝑁 ∈ ℝ
217215, 216remulcli 10312 . . . . . . . . . 10 (100 · 𝐿𝑀𝑁) ∈ ℝ
21861nn0rei 11552 . . . . . . . . . . . 12 𝑂 ∈ ℝ
219215, 218remulcli 10312 . . . . . . . . . . 11 (100 · 𝑂) ∈ ℝ
22062, 63deccl 11758 . . . . . . . . . . . 12 𝑃𝑄 ∈ ℕ0
221220nn0rei 11552 . . . . . . . . . . 11 𝑃𝑄 ∈ ℝ
222219, 221readdcli 10311 . . . . . . . . . 10 ((100 · 𝑂) + 𝑃𝑄) ∈ ℝ
223217, 222readdcli 10311 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℝ
224214, 223resubcli 10599 . . . . . . . 8 (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ
225219recni 10310 . . . . . . . . . . . 12 (100 · 𝑂) ∈ ℂ
226221recni 10310 . . . . . . . . . . . 12 𝑃𝑄 ∈ ℂ
227182, 225, 226addassi 10306 . . . . . . . . . . 11 (((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) + 𝑃𝑄) = ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))
228218recni 10310 . . . . . . . . . . . . . 14 𝑂 ∈ ℂ
229103, 181, 228adddii 10308 . . . . . . . . . . . . 13 (100 · (𝐿𝑀𝑁 + 𝑂)) = ((100 · 𝐿𝑀𝑁) + (100 · 𝑂))
230 dpmul4.1 . . . . . . . . . . . . . 14 (𝐿𝑀𝑁 + 𝑂) = 𝑅𝑆𝑇𝑈
231230oveq2i 6855 . . . . . . . . . . . . 13 (100 · (𝐿𝑀𝑁 + 𝑂)) = (100 · 𝑅𝑆𝑇𝑈)
232229, 231eqtr3i 2789 . . . . . . . . . . . 12 ((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) = (100 · 𝑅𝑆𝑇𝑈)
233232oveq1i 6854 . . . . . . . . . . 11 (((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) + 𝑃𝑄) = ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄)
234227, 233eqtr3i 2789 . . . . . . . . . 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 11777 . . . . . . . . . . . 12 𝑈𝑃𝑄 < 1000
240235, 62deccl 11758 . . . . . . . . . . . . . . 15 𝑈𝑃 ∈ ℕ0
241240, 63deccl 11758 . . . . . . . . . . . . . 14 𝑈𝑃𝑄 ∈ ℕ0
242241nn0rei 11552 . . . . . . . . . . . . 13 𝑈𝑃𝑄 ∈ ℝ
243211, 209remulcli 10312 . . . . . . . . . . . . 13 (𝑅𝑆𝑇 · 1000) ∈ ℝ
244242, 209, 243ltadd2i 10424 . . . . . . . . . . . 12 (𝑈𝑃𝑄 < 1000 ↔ ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) < ((𝑅𝑆𝑇 · 1000) + 1000))
245239, 244mpbi 221 . . . . . . . . . . 11 ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) < ((𝑅𝑆𝑇 · 1000) + 1000)
246140, 177mulcli 10303 . . . . . . . . . . . . 13 (𝑅𝑆𝑇 · 1000) ∈ ℂ
247235nn0cni 11553 . . . . . . . . . . . . . 14 𝑈 ∈ ℂ
248103, 247mulcli 10303 . . . . . . . . . . . . 13 (100 · 𝑈) ∈ ℂ
249246, 248, 226addassi 10306 . . . . . . . . . . . 12 (((𝑅𝑆𝑇 · 1000) + (100 · 𝑈)) + 𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + ((100 · 𝑈) + 𝑃𝑄))
250 dfdec10 11746 . . . . . . . . . . . . . . 15 𝑅𝑆𝑇𝑈 = ((10 · 𝑅𝑆𝑇) + 𝑈)
251250oveq2i 6855 . . . . . . . . . . . . . 14 (100 · 𝑅𝑆𝑇𝑈) = (100 · ((10 · 𝑅𝑆𝑇) + 𝑈))
25224, 140mulcli 10303 . . . . . . . . . . . . . . 15 (10 · 𝑅𝑆𝑇) ∈ ℂ
253103, 252, 247adddii 10308 . . . . . . . . . . . . . 14 (100 · ((10 · 𝑅𝑆𝑇) + 𝑈)) = ((100 · (10 · 𝑅𝑆𝑇)) + (100 · 𝑈))
254140, 177mulcomi 10304 . . . . . . . . . . . . . . . 16 (𝑅𝑆𝑇 · 1000) = (1000 · 𝑅𝑆𝑇)
25524, 103mulcomi 10304 . . . . . . . . . . . . . . . . . 18 (10 · 100) = (100 · 10)
256255, 195eqtr3i 2789 . . . . . . . . . . . . . . . . 17 (100 · 10) = 1000
257256oveq1i 6854 . . . . . . . . . . . . . . . 16 ((100 · 10) · 𝑅𝑆𝑇) = (1000 · 𝑅𝑆𝑇)
258103, 24, 140mulassi 10307 . . . . . . . . . . . . . . . 16 ((100 · 10) · 𝑅𝑆𝑇) = (100 · (10 · 𝑅𝑆𝑇))
259254, 257, 2583eqtr2ri 2794 . . . . . . . . . . . . . . 15 (100 · (10 · 𝑅𝑆𝑇)) = (𝑅𝑆𝑇 · 1000)
260259oveq1i 6854 . . . . . . . . . . . . . 14 ((100 · (10 · 𝑅𝑆𝑇)) + (100 · 𝑈)) = ((𝑅𝑆𝑇 · 1000) + (100 · 𝑈))
261251, 253, 2603eqtri 2791 . . . . . . . . . . . . 13 (100 · 𝑅𝑆𝑇𝑈) = ((𝑅𝑆𝑇 · 1000) + (100 · 𝑈))
262261oveq1i 6854 . . . . . . . . . . . 12 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) = (((𝑅𝑆𝑇 · 1000) + (100 · 𝑈)) + 𝑃𝑄)
263235, 62, 64dfdec100 30028 . . . . . . . . . . . . 13 𝑈𝑃𝑄 = ((100 · 𝑈) + 𝑃𝑄)
264263oveq2i 6855 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + ((100 · 𝑈) + 𝑃𝑄))
265249, 262, 2643eqtr4i 2797 . . . . . . . . . . 11 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄)
266140, 141, 177adddiri 10309 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 + 1) · 1000) = ((𝑅𝑆𝑇 · 1000) + (1 · 1000))
267177mulid2i 10301 . . . . . . . . . . . . 13 (1 · 1000) = 1000
268267oveq2i 6855 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 · 1000) + (1 · 1000)) = ((𝑅𝑆𝑇 · 1000) + 1000)
269266, 268eqtri 2787 . . . . . . . . . . 11 ((𝑅𝑆𝑇 + 1) · 1000) = ((𝑅𝑆𝑇 · 1000) + 1000)
270245, 265, 2693brtr4i 4841 . . . . . . . . . 10 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) < ((𝑅𝑆𝑇 + 1) · 1000)
271234, 270eqbrtri 4832 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) < ((𝑅𝑆𝑇 + 1) · 1000)
272223, 214posdifi 10834 . . . . . . . . 9 (((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) < ((𝑅𝑆𝑇 + 1) · 1000) ↔ 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
273271, 272mpbi 221 . . . . . . . 8 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
274 elrp 12033 . . . . . . . 8 ((((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+ ↔ ((((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ ∧ 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))))
275224, 273, 274mpbir2an 702 . . . . . . 7 (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+
276 ltsubrp 12067 . . . . . . 7 (((𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ ∧ (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+) → ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) < (𝑊𝑋𝑌𝑍 · 1000))
277210, 275, 276mp2an 683 . . . . . 6 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) < (𝑊𝑋𝑌𝑍 · 1000)
278207, 277eqbrtri 4832 . . . . 5 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000)
2793, 4deccl 11758 . . . . . . . . 9 𝐴𝐵𝐶 ∈ ℕ0
280279, 5deccl 11758 . . . . . . . 8 𝐴𝐵𝐶𝐷 ∈ ℕ0
281280nn0rei 11552 . . . . . . 7 𝐴𝐵𝐶𝐷 ∈ ℝ
2829, 10deccl 11758 . . . . . . . . 9 𝐸𝐹𝐺 ∈ ℕ0
283282, 11deccl 11758 . . . . . . . 8 𝐸𝐹𝐺𝐻 ∈ ℕ0
284283nn0rei 11552 . . . . . . 7 𝐸𝐹𝐺𝐻 ∈ ℝ
285281, 284remulcli 10312 . . . . . 6 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) ∈ ℝ
28623decnncl2 11768 . . . . . . . . 9 100 ∈ ℕ
287286decnncl2 11768 . . . . . . . 8 1000 ∈ ℕ
288287nngt0i 11313 . . . . . . 7 0 < 1000
289209, 288pm3.2i 462 . . . . . 6 (1000 ∈ ℝ ∧ 0 < 1000)
290 ltdiv1 11143 . . . . . 6 (((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) ∈ ℝ ∧ (𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ ∧ (1000 ∈ ℝ ∧ 0 < 1000)) → ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000) ↔ ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000)))
291285, 210, 289, 290mp3an 1585 . . . . 5 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000) ↔ ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000))
292278, 291mpbi 221 . . . 4 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000)
293280nn0cni 11553 . . . . . 6 𝐴𝐵𝐶𝐷 ∈ ℂ
294283nn0cni 11553 . . . . . 6 𝐸𝐹𝐺𝐻 ∈ ℂ
295209, 288gt0ne0ii 10820 . . . . . 6 1000 ≠ 0
296293, 294, 177, 295div23i 11039 . . . . 5 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴𝐵𝐶𝐷 / 1000) · 𝐸𝐹𝐺𝐻)
2971, 2, 4, 48dpmul1000 30057 . . . . . . . 8 ((𝐴.𝐵𝐶𝐷) · 1000) = 𝐴𝐵𝐶𝐷
298297oveq1i 6854 . . . . . . 7 (((𝐴.𝐵𝐶𝐷) · 1000) / 1000) = (𝐴𝐵𝐶𝐷 / 1000)
2994nn0rei 11552 . . . . . . . . . . . 12 𝐶 ∈ ℝ
300 dp2cl 30038 . . . . . . . . . . . 12 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → 𝐶𝐷 ∈ ℝ)
301299, 48, 300mp2an 683 . . . . . . . . . . 11 𝐶𝐷 ∈ ℝ
302 dp2cl 30038 . . . . . . . . . . 11 ((𝐵 ∈ ℝ ∧ 𝐶𝐷 ∈ ℝ) → 𝐵𝐶𝐷 ∈ ℝ)
30319, 301, 302mp2an 683 . . . . . . . . . 10 𝐵𝐶𝐷 ∈ ℝ
304 dpcl 30049 . . . . . . . . . 10 ((𝐴 ∈ ℕ0𝐵𝐶𝐷 ∈ ℝ) → (𝐴.𝐵𝐶𝐷) ∈ ℝ)
3051, 303, 304mp2an 683 . . . . . . . . 9 (𝐴.𝐵𝐶𝐷) ∈ ℝ
306305recni 10310 . . . . . . . 8 (𝐴.𝐵𝐶𝐷) ∈ ℂ
307306, 177, 295divcan4i 11028 . . . . . . 7 (((𝐴.𝐵𝐶𝐷) · 1000) / 1000) = (𝐴.𝐵𝐶𝐷)
308298, 307eqtr3i 2789 . . . . . 6 (𝐴𝐵𝐶𝐷 / 1000) = (𝐴.𝐵𝐶𝐷)
309308oveq1i 6854 . . . . 5 ((𝐴𝐵𝐶𝐷 / 1000) · 𝐸𝐹𝐺𝐻) = ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻)
310296, 309eqtri 2787 . . . 4 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻)
311175, 177, 295divcan4i 11028 . . . 4 ((𝑊𝑋𝑌𝑍 · 1000) / 1000) = 𝑊𝑋𝑌𝑍
312292, 310, 3113brtr3i 4840 . . 3 ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍
313305, 284remulcli 10312 . . . 4 ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) ∈ ℝ
314 ltdiv1 11143 . . . 4 ((((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) ∈ ℝ ∧ 𝑊𝑋𝑌𝑍 ∈ ℝ ∧ (1000 ∈ ℝ ∧ 0 < 1000)) → (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍 ↔ (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000)))
315313, 208, 289, 314mp3an 1585 . . 3 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍 ↔ (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000))
316312, 315mpbi 221 . 2 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000)
317306, 294, 177, 295divassi 11037 . . 3 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · (𝐸𝐹𝐺𝐻 / 1000))
3187, 8, 10, 52dpmul1000 30057 . . . . . 6 ((𝐸.𝐹𝐺𝐻) · 1000) = 𝐸𝐹𝐺𝐻
319318oveq1i 6854 . . . . 5 (((𝐸.𝐹𝐺𝐻) · 1000) / 1000) = (𝐸𝐹𝐺𝐻 / 1000)
32010nn0rei 11552 . . . . . . . . . 10 𝐺 ∈ ℝ
321 dp2cl 30038 . . . . . . . . . 10 ((𝐺 ∈ ℝ ∧ 𝐻 ∈ ℝ) → 𝐺𝐻 ∈ ℝ)
322320, 52, 321mp2an 683 . . . . . . . . 9 𝐺𝐻 ∈ ℝ
323 dp2cl 30038 . . . . . . . . 9 ((𝐹 ∈ ℝ ∧ 𝐺𝐻 ∈ ℝ) → 𝐹𝐺𝐻 ∈ ℝ)
32425, 322, 323mp2an 683 . . . . . . . 8 𝐹𝐺𝐻 ∈ ℝ
325 dpcl 30049 . . . . . . . 8 ((𝐸 ∈ ℕ0𝐹𝐺𝐻 ∈ ℝ) → (𝐸.𝐹𝐺𝐻) ∈ ℝ)
3267, 324, 325mp2an 683 . . . . . . 7 (𝐸.𝐹𝐺𝐻) ∈ ℝ
327326recni 10310 . . . . . 6 (𝐸.𝐹𝐺𝐻) ∈ ℂ
328327, 177, 295divcan4i 11028 . . . . 5 (((𝐸.𝐹𝐺𝐻) · 1000) / 1000) = (𝐸.𝐹𝐺𝐻)
329319, 328eqtr3i 2789 . . . 4 (𝐸𝐹𝐺𝐻 / 1000) = (𝐸.𝐹𝐺𝐻)
330329oveq2i 6855 . . 3 ((𝐴.𝐵𝐶𝐷) · (𝐸𝐹𝐺𝐻 / 1000)) = ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻))
331317, 330eqtri 2787 . 2 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻))
332173nn0rei 11552 . . . . 5 𝑍 ∈ ℝ
333168, 169, 171, 332dpmul1000 30057 . . . 4 ((𝑊.𝑋𝑌𝑍) · 1000) = 𝑊𝑋𝑌𝑍
334333oveq1i 6854 . . 3 (((𝑊.𝑋𝑌𝑍) · 1000) / 1000) = (𝑊𝑋𝑌𝑍 / 1000)
335169nn0rei 11552 . . . . . . 7 𝑋 ∈ ℝ
336171nn0rei 11552 . . . . . . . 8 𝑌 ∈ ℝ
337 dp2cl 30038 . . . . . . . 8 ((𝑌 ∈ ℝ ∧ 𝑍 ∈ ℝ) → 𝑌𝑍 ∈ ℝ)
338336, 332, 337mp2an 683 . . . . . . 7 𝑌𝑍 ∈ ℝ
339 dp2cl 30038 . . . . . . 7 ((𝑋 ∈ ℝ ∧ 𝑌𝑍 ∈ ℝ) → 𝑋𝑌𝑍 ∈ ℝ)
340335, 338, 339mp2an 683 . . . . . 6 𝑋𝑌𝑍 ∈ ℝ
341 dpcl 30049 . . . . . 6 ((𝑊 ∈ ℕ0𝑋𝑌𝑍 ∈ ℝ) → (𝑊.𝑋𝑌𝑍) ∈ ℝ)
342168, 340, 341mp2an 683 . . . . 5 (𝑊.𝑋𝑌𝑍) ∈ ℝ
343342recni 10310 . . . 4 (𝑊.𝑋𝑌𝑍) ∈ ℂ
344343, 177, 295divcan4i 11028 . . 3 (((𝑊.𝑋𝑌𝑍) · 1000) / 1000) = (𝑊.𝑋𝑌𝑍)
345334, 344eqtr3i 2789 . 2 (𝑊𝑋𝑌𝑍 / 1000) = (𝑊.𝑋𝑌𝑍)
346316, 331, 3453brtr3i 4840 1 ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻)) < (𝑊.𝑋𝑌𝑍)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1652  wcel 2155   class class class wbr 4811  (class class class)co 6844  cc 10189  cr 10190  0cc0 10191  1c1 10192   + caddc 10194   · cmul 10196   < clt 10330  cmin 10522   / cdiv 10940  2c2 11329  0cn0 11540  cdc 11743  +crp 12031  cexp 13070  cdp2 30029  .cdp 30046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-er 7949  df-en 8163  df-dom 8164  df-sdom 8165  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-7 11342  df-8 11343  df-9 11344  df-n0 11541  df-z 11627  df-dec 11744  df-uz 11890  df-rp 12032  df-seq 13012  df-exp 13071  df-dp2 30030  df-dp 30047
This theorem is referenced by:  hgt750lem2  31184
  Copyright terms: Public domain W3C validator