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 29952
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 11724 . . . . . . . 8 𝐴𝐵 ∈ ℕ0
4 dpmul.c . . . . . . . . 9 𝐶 ∈ ℕ0
5 dpmul.d . . . . . . . . 9 𝐷 ∈ ℕ0
64, 5deccl 11724 . . . . . . . 8 𝐶𝐷 ∈ ℕ0
7 dpmul.e . . . . . . . . 9 𝐸 ∈ ℕ0
8 dpmul4.f . . . . . . . . 9 𝐹 ∈ ℕ0
97, 8deccl 11724 . . . . . . . 8 𝐸𝐹 ∈ ℕ0
10 dpmul.g . . . . . . . . 9 𝐺 ∈ ℕ0
11 dpmul4.h . . . . . . . . 9 𝐻 ∈ ℕ0
1210, 11deccl 11724 . . . . . . . 8 𝐺𝐻 ∈ ℕ0
13 dpmul4.l . . . . . . . . . 10 𝐿 ∈ ℕ0
14 dpmul4.m . . . . . . . . . 10 𝑀 ∈ ℕ0
1513, 14deccl 11724 . . . . . . . . 9 𝐿𝑀 ∈ ℕ0
16 dpmul4.n . . . . . . . . 9 𝑁 ∈ ℕ0
1715, 16deccl 11724 . . . . . . . 8 𝐿𝑀𝑁 ∈ ℕ0
18 2nn0 11521 . . . . . . . 8 2 ∈ ℕ0
192nn0rei 11515 . . . . . . . . . . . . 13 𝐵 ∈ ℝ
20 dpcl 29928 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ0𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)
211, 19, 20mp2an 710 . . . . . . . . . . . 12 (𝐴.𝐵) ∈ ℝ
2221recni 10264 . . . . . . . . . . 11 (𝐴.𝐵) ∈ ℂ
23 10nn 11726 . . . . . . . . . . . 12 10 ∈ ℕ
2423nncni 11242 . . . . . . . . . . 11 10 ∈ ℂ
258nn0rei 11515 . . . . . . . . . . . . 13 𝐹 ∈ ℝ
26 dpcl 29928 . . . . . . . . . . . . 13 ((𝐸 ∈ ℕ0𝐹 ∈ ℝ) → (𝐸.𝐹) ∈ ℝ)
277, 25, 26mp2an 710 . . . . . . . . . . . 12 (𝐸.𝐹) ∈ ℝ
2827recni 10264 . . . . . . . . . . 11 (𝐸.𝐹) ∈ ℂ
2922, 24, 28, 24mul4i 10445 . . . . . . . . . 10 (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10)) = (((𝐴.𝐵) · (𝐸.𝐹)) · (10 · 10))
3022, 28mulcli 10257 . . . . . . . . . . 11 ((𝐴.𝐵) · (𝐸.𝐹)) ∈ ℂ
3130, 24, 24mulassi 10261 . . . . . . . . . 10 ((((𝐴.𝐵) · (𝐸.𝐹)) · 10) · 10) = (((𝐴.𝐵) · (𝐸.𝐹)) · (10 · 10))
32 dpmul4.2 . . . . . . . . . . . . 13 ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼.𝐽𝐾)
3332oveq1i 6824 . . . . . . . . . . . 12 (((𝐴.𝐵) · (𝐸.𝐹)) · 10) = ((𝐼.𝐽𝐾) · 10)
34 dpmul4.i . . . . . . . . . . . . 13 𝐼 ∈ ℕ0
35 dpmul.j . . . . . . . . . . . . 13 𝐽 ∈ ℕ0
36 dpmul.k . . . . . . . . . . . . . 14 𝐾 ∈ ℕ0
3736nn0rei 11515 . . . . . . . . . . . . 13 𝐾 ∈ ℝ
3834, 35, 37dp3mul10 29936 . . . . . . . . . . . 12 ((𝐼.𝐽𝐾) · 10) = (𝐼𝐽.𝐾)
3933, 38eqtri 2782 . . . . . . . . . . 11 (((𝐴.𝐵) · (𝐸.𝐹)) · 10) = (𝐼𝐽.𝐾)
4039oveq1i 6824 . . . . . . . . . 10 ((((𝐴.𝐵) · (𝐸.𝐹)) · 10) · 10) = ((𝐼𝐽.𝐾) · 10)
4129, 31, 403eqtr2ri 2789 . . . . . . . . 9 ((𝐼𝐽.𝐾) · 10) = (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10))
4234, 35deccl 11724 . . . . . . . . . 10 𝐼𝐽 ∈ ℕ0
4342, 37dpmul10 29933 . . . . . . . . 9 ((𝐼𝐽.𝐾) · 10) = 𝐼𝐽𝐾
441, 19dpmul10 29933 . . . . . . . . . 10 ((𝐴.𝐵) · 10) = 𝐴𝐵
457, 25dpmul10 29933 . . . . . . . . . 10 ((𝐸.𝐹) · 10) = 𝐸𝐹
4644, 45oveq12i 6826 . . . . . . . . 9 (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10)) = (𝐴𝐵 · 𝐸𝐹)
4741, 43, 463eqtr3ri 2791 . . . . . . . 8 (𝐴𝐵 · 𝐸𝐹) = 𝐼𝐽𝐾
485nn0rei 11515 . . . . . . . . . . . . 13 𝐷 ∈ ℝ
49 dpcl 29928 . . . . . . . . . . . . 13 ((𝐶 ∈ ℕ0𝐷 ∈ ℝ) → (𝐶.𝐷) ∈ ℝ)
504, 48, 49mp2an 710 . . . . . . . . . . . 12 (𝐶.𝐷) ∈ ℝ
5150recni 10264 . . . . . . . . . . 11 (𝐶.𝐷) ∈ ℂ
5211nn0rei 11515 . . . . . . . . . . . . 13 𝐻 ∈ ℝ
53 dpcl 29928 . . . . . . . . . . . . 13 ((𝐺 ∈ ℕ0𝐻 ∈ ℝ) → (𝐺.𝐻) ∈ ℝ)
5410, 52, 53mp2an 710 . . . . . . . . . . . 12 (𝐺.𝐻) ∈ ℝ
5554recni 10264 . . . . . . . . . . 11 (𝐺.𝐻) ∈ ℂ
5651, 24, 55, 24mul4i 10445 . . . . . . . . . 10 (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10)) = (((𝐶.𝐷) · (𝐺.𝐻)) · (10 · 10))
5751, 55mulcli 10257 . . . . . . . . . . 11 ((𝐶.𝐷) · (𝐺.𝐻)) ∈ ℂ
5857, 24, 24mulassi 10261 . . . . . . . . . 10 ((((𝐶.𝐷) · (𝐺.𝐻)) · 10) · 10) = (((𝐶.𝐷) · (𝐺.𝐻)) · (10 · 10))
59 dpmul4.3 . . . . . . . . . . . . 13 ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂.𝑃𝑄)
6059oveq1i 6824 . . . . . . . . . . . 12 (((𝐶.𝐷) · (𝐺.𝐻)) · 10) = ((𝑂.𝑃𝑄) · 10)
61 dpmul4.o . . . . . . . . . . . . 13 𝑂 ∈ ℕ0
62 dpmul4.p . . . . . . . . . . . . 13 𝑃 ∈ ℕ0
63 dpmul4.q . . . . . . . . . . . . . 14 𝑄 ∈ ℕ0
6463nn0rei 11515 . . . . . . . . . . . . 13 𝑄 ∈ ℝ
6561, 62, 64dp3mul10 29936 . . . . . . . . . . . 12 ((𝑂.𝑃𝑄) · 10) = (𝑂𝑃.𝑄)
6660, 65eqtri 2782 . . . . . . . . . . 11 (((𝐶.𝐷) · (𝐺.𝐻)) · 10) = (𝑂𝑃.𝑄)
6766oveq1i 6824 . . . . . . . . . 10 ((((𝐶.𝐷) · (𝐺.𝐻)) · 10) · 10) = ((𝑂𝑃.𝑄) · 10)
6856, 58, 673eqtr2ri 2789 . . . . . . . . 9 ((𝑂𝑃.𝑄) · 10) = (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10))
6961, 62deccl 11724 . . . . . . . . . 10 𝑂𝑃 ∈ ℕ0
7069, 64dpmul10 29933 . . . . . . . . 9 ((𝑂𝑃.𝑄) · 10) = 𝑂𝑃𝑄
714, 48dpmul10 29933 . . . . . . . . . 10 ((𝐶.𝐷) · 10) = 𝐶𝐷
7210, 52dpmul10 29933 . . . . . . . . . 10 ((𝐺.𝐻) · 10) = 𝐺𝐻
7371, 72oveq12i 6826 . . . . . . . . 9 (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10)) = (𝐶𝐷 · 𝐺𝐻)
7468, 70, 733eqtr3ri 2791 . . . . . . . 8 (𝐶𝐷 · 𝐺𝐻) = 𝑂𝑃𝑄
7522, 51, 24adddiri 10263 . . . . . . . . . . . 12 (((𝐴.𝐵) + (𝐶.𝐷)) · 10) = (((𝐴.𝐵) · 10) + ((𝐶.𝐷) · 10))
7644, 71oveq12i 6826 . . . . . . . . . . . 12 (((𝐴.𝐵) · 10) + ((𝐶.𝐷) · 10)) = (𝐴𝐵 + 𝐶𝐷)
7775, 76eqtr2i 2783 . . . . . . . . . . 11 (𝐴𝐵 + 𝐶𝐷) = (((𝐴.𝐵) + (𝐶.𝐷)) · 10)
7828, 55, 24adddiri 10263 . . . . . . . . . . . 12 (((𝐸.𝐹) + (𝐺.𝐻)) · 10) = (((𝐸.𝐹) · 10) + ((𝐺.𝐻) · 10))
7945, 72oveq12i 6826 . . . . . . . . . . . 12 (((𝐸.𝐹) · 10) + ((𝐺.𝐻) · 10)) = (𝐸𝐹 + 𝐺𝐻)
8078, 79eqtr2i 2783 . . . . . . . . . . 11 (𝐸𝐹 + 𝐺𝐻) = (((𝐸.𝐹) + (𝐺.𝐻)) · 10)
8177, 80oveq12i 6826 . . . . . . . . . 10 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · 10) · (((𝐸.𝐹) + (𝐺.𝐻)) · 10))
8222, 51addcli 10256 . . . . . . . . . . 11 ((𝐴.𝐵) + (𝐶.𝐷)) ∈ ℂ
8328, 55addcli 10256 . . . . . . . . . . 11 ((𝐸.𝐹) + (𝐺.𝐻)) ∈ ℂ
8482, 24, 83, 24mul4i 10445 . . . . . . . . . 10 ((((𝐴.𝐵) + (𝐶.𝐷)) · 10) · (((𝐸.𝐹) + (𝐺.𝐻)) · 10)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (10 · 10))
85 dpmul4.5 . . . . . . . . . . 11 (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄))
8685oveq1i 6824 . . . . . . . . . 10 ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (10 · 10)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10))
8781, 84, 863eqtri 2786 . . . . . . . . 9 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10))
88 10nn0 11728 . . . . . . . . . . 11 10 ∈ ℕ0
8988dec0u 11732 . . . . . . . . . 10 (10 · 10) = 100
9089oveq2i 6825 . . . . . . . . 9 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100)
9132, 30eqeltrri 2836 . . . . . . . . . . . 12 (𝐼.𝐽𝐾) ∈ ℂ
9214nn0rei 11515 . . . . . . . . . . . . . . 15 𝑀 ∈ ℝ
9316nn0rei 11515 . . . . . . . . . . . . . . 15 𝑁 ∈ ℝ
94 dp2cl 29917 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀𝑁 ∈ ℝ)
9592, 93, 94mp2an 710 . . . . . . . . . . . . . 14 𝑀𝑁 ∈ ℝ
96 dpcl 29928 . . . . . . . . . . . . . 14 ((𝐿 ∈ ℕ0𝑀𝑁 ∈ ℝ) → (𝐿.𝑀𝑁) ∈ ℝ)
9713, 95, 96mp2an 710 . . . . . . . . . . . . 13 (𝐿.𝑀𝑁) ∈ ℝ
9897recni 10264 . . . . . . . . . . . 12 (𝐿.𝑀𝑁) ∈ ℂ
9991, 98addcli 10256 . . . . . . . . . . 11 ((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) ∈ ℂ
10059, 57eqeltrri 2836 . . . . . . . . . . 11 (𝑂.𝑃𝑄) ∈ ℂ
101 0nn0 11519 . . . . . . . . . . . . 13 0 ∈ ℕ0
10288, 101deccl 11724 . . . . . . . . . . . 12 100 ∈ ℕ0
103102nn0cni 11516 . . . . . . . . . . 11 100 ∈ ℂ
10499, 100, 103adddiri 10263 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) + ((𝑂.𝑃𝑄) · 100))
10591, 98, 103adddiri 10263 . . . . . . . . . . 11 (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) = (((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100))
106105oveq1i 6824 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) + ((𝑂.𝑃𝑄) · 100)) = ((((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) + ((𝑂.𝑃𝑄) · 100))
10734, 35, 37dpmul100 29935 . . . . . . . . . . . 12 ((𝐼.𝐽𝐾) · 100) = 𝐼𝐽𝐾
10813, 14, 93dpmul100 29935 . . . . . . . . . . . 12 ((𝐿.𝑀𝑁) · 100) = 𝐿𝑀𝑁
109107, 108oveq12i 6826 . . . . . . . . . . 11 (((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) = (𝐼𝐽𝐾 + 𝐿𝑀𝑁)
11061, 62, 64dpmul100 29935 . . . . . . . . . . 11 ((𝑂.𝑃𝑄) · 100) = 𝑂𝑃𝑄
111109, 110oveq12i 6826 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) + ((𝑂.𝑃𝑄) · 100)) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
112104, 106, 1113eqtri 2786 . . . . . . . . 9 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
11387, 90, 1123eqtri 2786 . . . . . . . 8 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
114 sq10 13262 . . . . . . . . . . . 12 (10↑2) = 100
115114oveq2i 6825 . . . . . . . . . . 11 (𝐴𝐵 · (10↑2)) = (𝐴𝐵 · 100)
1163nn0cni 11516 . . . . . . . . . . . 12 𝐴𝐵 ∈ ℂ
117103, 116mulcomi 10258 . . . . . . . . . . 11 (100 · 𝐴𝐵) = (𝐴𝐵 · 100)
118115, 117eqtr4i 2785 . . . . . . . . . 10 (𝐴𝐵 · (10↑2)) = (100 · 𝐴𝐵)
119118oveq1i 6824 . . . . . . . . 9 ((𝐴𝐵 · (10↑2)) + 𝐶𝐷) = ((100 · 𝐴𝐵) + 𝐶𝐷)
1203, 4, 48dfdec100 29906 . . . . . . . . 9 𝐴𝐵𝐶𝐷 = ((100 · 𝐴𝐵) + 𝐶𝐷)
121119, 120eqtr4i 2785 . . . . . . . 8 ((𝐴𝐵 · (10↑2)) + 𝐶𝐷) = 𝐴𝐵𝐶𝐷
122114oveq2i 6825 . . . . . . . . . . 11 (𝐸𝐹 · (10↑2)) = (𝐸𝐹 · 100)
1239nn0cni 11516 . . . . . . . . . . . 12 𝐸𝐹 ∈ ℂ
124103, 123mulcomi 10258 . . . . . . . . . . 11 (100 · 𝐸𝐹) = (𝐸𝐹 · 100)
125122, 124eqtr4i 2785 . . . . . . . . . 10 (𝐸𝐹 · (10↑2)) = (100 · 𝐸𝐹)
126125oveq1i 6824 . . . . . . . . 9 ((𝐸𝐹 · (10↑2)) + 𝐺𝐻) = ((100 · 𝐸𝐹) + 𝐺𝐻)
1279, 10, 52dfdec100 29906 . . . . . . . . 9 𝐸𝐹𝐺𝐻 = ((100 · 𝐸𝐹) + 𝐺𝐻)
128126, 127eqtr4i 2785 . . . . . . . 8 ((𝐸𝐹 · (10↑2)) + 𝐺𝐻) = 𝐸𝐹𝐺𝐻
12924sqvali 13157 . . . . . . . . . . . 12 (10↑2) = (10 · 10)
130129oveq2i 6825 . . . . . . . . . . 11 (𝐼𝐽𝐾 · (10↑2)) = (𝐼𝐽𝐾 · (10 · 10))
13142, 36deccl 11724 . . . . . . . . . . . . 13 𝐼𝐽𝐾 ∈ ℕ0
132131nn0cni 11516 . . . . . . . . . . . 12 𝐼𝐽𝐾 ∈ ℂ
133132, 24, 24mulassi 10261 . . . . . . . . . . 11 ((𝐼𝐽𝐾 · 10) · 10) = (𝐼𝐽𝐾 · (10 · 10))
134130, 133eqtr4i 2785 . . . . . . . . . 10 (𝐼𝐽𝐾 · (10↑2)) = ((𝐼𝐽𝐾 · 10) · 10)
135 dpmul4.r . . . . . . . . . . . . . . . 16 𝑅 ∈ ℕ0
136 dpmul4.s . . . . . . . . . . . . . . . 16 𝑆 ∈ ℕ0
137135, 136deccl 11724 . . . . . . . . . . . . . . 15 𝑅𝑆 ∈ ℕ0
138 dpmul4.t . . . . . . . . . . . . . . 15 𝑇 ∈ ℕ0
139137, 138deccl 11724 . . . . . . . . . . . . . 14 𝑅𝑆𝑇 ∈ ℕ0
140139nn0cni 11516 . . . . . . . . . . . . 13 𝑅𝑆𝑇 ∈ ℂ
141 ax-1cn 10206 . . . . . . . . . . . . 13 1 ∈ ℂ
142140, 141addcli 10256 . . . . . . . . . . . 12 (𝑅𝑆𝑇 + 1) ∈ ℂ
143132, 24mulcli 10257 . . . . . . . . . . . 12 (𝐼𝐽𝐾 · 10) ∈ ℂ
144141, 143addcomi 10439 . . . . . . . . . . . . . . . 16 (1 + (𝐼𝐽𝐾 · 10)) = ((𝐼𝐽𝐾 · 10) + 1)
14524, 132mulcomi 10258 . . . . . . . . . . . . . . . . . 18 (10 · 𝐼𝐽𝐾) = (𝐼𝐽𝐾 · 10)
146131dec0u 11732 . . . . . . . . . . . . . . . . . 18 (10 · 𝐼𝐽𝐾) = 𝐼𝐽𝐾0
147145, 146eqtr3i 2784 . . . . . . . . . . . . . . . . 17 (𝐼𝐽𝐾 · 10) = 𝐼𝐽𝐾0
148147oveq1i 6824 . . . . . . . . . . . . . . . 16 ((𝐼𝐽𝐾 · 10) + 1) = (𝐼𝐽𝐾0 + 1)
149141addid2i 10436 . . . . . . . . . . . . . . . . 17 (0 + 1) = 1
150 eqid 2760 . . . . . . . . . . . . . . . . 17 𝐼𝐽𝐾0 = 𝐼𝐽𝐾0
151131, 101, 149, 150decsuc 11747 . . . . . . . . . . . . . . . 16 (𝐼𝐽𝐾0 + 1) = 𝐼𝐽𝐾1
152144, 148, 1513eqtri 2786 . . . . . . . . . . . . . . 15 (1 + (𝐼𝐽𝐾 · 10)) = 𝐼𝐽𝐾1
153152oveq2i 6825 . . . . . . . . . . . . . 14 (𝑅𝑆𝑇 + (1 + (𝐼𝐽𝐾 · 10))) = (𝑅𝑆𝑇 + 𝐼𝐽𝐾1)
154140, 141, 143addassi 10260 . . . . . . . . . . . . . 14 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = (𝑅𝑆𝑇 + (1 + (𝐼𝐽𝐾 · 10)))
155 1nn0 11520 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ0
156131, 155deccl 11724 . . . . . . . . . . . . . . . 16 𝐼𝐽𝐾1 ∈ ℕ0
157156nn0cni 11516 . . . . . . . . . . . . . . 15 𝐼𝐽𝐾1 ∈ ℂ
158157, 140addcomi 10439 . . . . . . . . . . . . . 14 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = (𝑅𝑆𝑇 + 𝐼𝐽𝐾1)
159153, 154, 1583eqtr4i 2792 . . . . . . . . . . . . 13 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = (𝐼𝐽𝐾1 + 𝑅𝑆𝑇)
160 dpmul4.4 . . . . . . . . . . . . 13 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = 𝑊𝑋𝑌𝑍
161159, 160eqtri 2782 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = 𝑊𝑋𝑌𝑍
162142, 143, 161mvlladdi 10511 . . . . . . . . . . 11 (𝐼𝐽𝐾 · 10) = (𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1))
163162oveq1i 6824 . . . . . . . . . 10 ((𝐼𝐽𝐾 · 10) · 10) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10)
164134, 163eqtri 2782 . . . . . . . . 9 (𝐼𝐽𝐾 · (10↑2)) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10)
165164oveq1i 6824 . . . . . . . 8 ((𝐼𝐽𝐾 · (10↑2)) + 𝐿𝑀𝑁) = (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁)
166 eqid 2760 . . . . . . . 8 (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
1673, 6, 9, 12, 17, 18, 47, 74, 113, 121, 128, 165, 166karatsuba 16014 . . . . . . 7 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
168 dpmul4.w . . . . . . . . . . . . . . 15 𝑊 ∈ ℕ0
169 dpmul4.x . . . . . . . . . . . . . . 15 𝑋 ∈ ℕ0
170168, 169deccl 11724 . . . . . . . . . . . . . 14 𝑊𝑋 ∈ ℕ0
171 dpmul4.y . . . . . . . . . . . . . 14 𝑌 ∈ ℕ0
172170, 171deccl 11724 . . . . . . . . . . . . 13 𝑊𝑋𝑌 ∈ ℕ0
173 dpmul4.z . . . . . . . . . . . . 13 𝑍 ∈ ℕ0
174172, 173deccl 11724 . . . . . . . . . . . 12 𝑊𝑋𝑌𝑍 ∈ ℕ0
175174nn0cni 11516 . . . . . . . . . . 11 𝑊𝑋𝑌𝑍 ∈ ℂ
176102, 101deccl 11724 . . . . . . . . . . . 12 1000 ∈ ℕ0
177176nn0cni 11516 . . . . . . . . . . 11 1000 ∈ ℂ
178175, 177mulcli 10257 . . . . . . . . . 10 (𝑊𝑋𝑌𝑍 · 1000) ∈ ℂ
179142, 177mulcli 10257 . . . . . . . . . 10 ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℂ
180178, 179subcli 10569 . . . . . . . . 9 ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) ∈ ℂ
18117nn0cni 11516 . . . . . . . . . 10 𝐿𝑀𝑁 ∈ ℂ
182103, 181mulcli 10257 . . . . . . . . 9 (100 · 𝐿𝑀𝑁) ∈ ℂ
18361, 62, 64dfdec100 29906 . . . . . . . . . 10 𝑂𝑃𝑄 = ((100 · 𝑂) + 𝑃𝑄)
18469, 63deccl 11724 . . . . . . . . . . 11 𝑂𝑃𝑄 ∈ ℕ0
185184nn0cni 11516 . . . . . . . . . 10 𝑂𝑃𝑄 ∈ ℂ
186183, 185eqeltrri 2836 . . . . . . . . 9 ((100 · 𝑂) + 𝑃𝑄) ∈ ℂ
187180, 182, 186addassi 10260 . . . . . . . 8 ((((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) + ((100 · 𝑂) + 𝑃𝑄)) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
18824sqcli 13158 . . . . . . . . . . . . 13 (10↑2) ∈ ℂ
189132, 188mulcli 10257 . . . . . . . . . . . 12 (𝐼𝐽𝐾 · (10↑2)) ∈ ℂ
190164, 189eqeltrri 2836 . . . . . . . . . . 11 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) ∈ ℂ
191190, 181, 103adddiri 10263 . . . . . . . . . 10 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · 100) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) + (𝐿𝑀𝑁 · 100))
192114oveq2i 6825 . . . . . . . . . 10 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · 100)
193175, 142subcli 10569 . . . . . . . . . . . . 13 (𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) ∈ ℂ
194193, 24, 103mulassi 10261 . . . . . . . . . . . 12 (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · (10 · 100))
195102dec0u 11732 . . . . . . . . . . . . 13 (10 · 100) = 1000
196195oveq2i 6825 . . . . . . . . . . . 12 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · (10 · 100)) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 1000)
197175, 142, 177subdiri 10692 . . . . . . . . . . . 12 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 1000) = ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000))
198194, 196, 1973eqtrri 2787 . . . . . . . . . . 11 ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) = (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100)
199103, 181mulcomi 10258 . . . . . . . . . . 11 (100 · 𝐿𝑀𝑁) = (𝐿𝑀𝑁 · 100)
200198, 199oveq12i 6826 . . . . . . . . . 10 (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) + (𝐿𝑀𝑁 · 100))
201191, 192, 2003eqtr4i 2792 . . . . . . . . 9 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁))
202201, 183oveq12i 6826 . . . . . . . 8 (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄) = ((((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) + ((100 · 𝑂) + 𝑃𝑄))
203182, 186addcli 10256 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℂ
204 subsub 10523 . . . . . . . . 9 (((𝑊𝑋𝑌𝑍 · 1000) ∈ ℂ ∧ ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℂ ∧ ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℂ) → ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
205178, 179, 203, 204mp3an 1573 . . . . . . . 8 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
206187, 202, 2053eqtr4ri 2793 . . . . . . 7 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
207167, 206eqtr4i 2785 . . . . . 6 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) = ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
208174nn0rei 11515 . . . . . . . 8 𝑊𝑋𝑌𝑍 ∈ ℝ
209176nn0rei 11515 . . . . . . . 8 1000 ∈ ℝ
210208, 209remulcli 10266 . . . . . . 7 (𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ
211139nn0rei 11515 . . . . . . . . . . 11 𝑅𝑆𝑇 ∈ ℝ
212 1re 10251 . . . . . . . . . . 11 1 ∈ ℝ
213211, 212readdcli 10265 . . . . . . . . . 10 (𝑅𝑆𝑇 + 1) ∈ ℝ
214213, 209remulcli 10266 . . . . . . . . 9 ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℝ
215102nn0rei 11515 . . . . . . . . . . 11 100 ∈ ℝ
21617nn0rei 11515 . . . . . . . . . . 11 𝐿𝑀𝑁 ∈ ℝ
217215, 216remulcli 10266 . . . . . . . . . 10 (100 · 𝐿𝑀𝑁) ∈ ℝ
21861nn0rei 11515 . . . . . . . . . . . 12 𝑂 ∈ ℝ
219215, 218remulcli 10266 . . . . . . . . . . 11 (100 · 𝑂) ∈ ℝ
22062, 63deccl 11724 . . . . . . . . . . . 12 𝑃𝑄 ∈ ℕ0
221220nn0rei 11515 . . . . . . . . . . 11 𝑃𝑄 ∈ ℝ
222219, 221readdcli 10265 . . . . . . . . . 10 ((100 · 𝑂) + 𝑃𝑄) ∈ ℝ
223217, 222readdcli 10265 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℝ
224214, 223resubcli 10555 . . . . . . . 8 (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ
225219recni 10264 . . . . . . . . . . . 12 (100 · 𝑂) ∈ ℂ
226221recni 10264 . . . . . . . . . . . 12 𝑃𝑄 ∈ ℂ
227182, 225, 226addassi 10260 . . . . . . . . . . 11 (((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) + 𝑃𝑄) = ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))
228218recni 10264 . . . . . . . . . . . . . 14 𝑂 ∈ ℂ
229103, 181, 228adddii 10262 . . . . . . . . . . . . 13 (100 · (𝐿𝑀𝑁 + 𝑂)) = ((100 · 𝐿𝑀𝑁) + (100 · 𝑂))
230 dpmul4.1 . . . . . . . . . . . . . 14 (𝐿𝑀𝑁 + 𝑂) = 𝑅𝑆𝑇𝑈
231230oveq2i 6825 . . . . . . . . . . . . 13 (100 · (𝐿𝑀𝑁 + 𝑂)) = (100 · 𝑅𝑆𝑇𝑈)
232229, 231eqtr3i 2784 . . . . . . . . . . . 12 ((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) = (100 · 𝑅𝑆𝑇𝑈)
233232oveq1i 6824 . . . . . . . . . . 11 (((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) + 𝑃𝑄) = ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄)
234227, 233eqtr3i 2784 . . . . . . . . . 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 11750 . . . . . . . . . . . 12 𝑈𝑃𝑄 < 1000
240235, 62deccl 11724 . . . . . . . . . . . . . . 15 𝑈𝑃 ∈ ℕ0
241240, 63deccl 11724 . . . . . . . . . . . . . 14 𝑈𝑃𝑄 ∈ ℕ0
242241nn0rei 11515 . . . . . . . . . . . . 13 𝑈𝑃𝑄 ∈ ℝ
243211, 209remulcli 10266 . . . . . . . . . . . . 13 (𝑅𝑆𝑇 · 1000) ∈ ℝ
244242, 209, 243ltadd2i 10380 . . . . . . . . . . . 12 (𝑈𝑃𝑄 < 1000 ↔ ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) < ((𝑅𝑆𝑇 · 1000) + 1000))
245239, 244mpbi 220 . . . . . . . . . . 11 ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) < ((𝑅𝑆𝑇 · 1000) + 1000)
246140, 177mulcli 10257 . . . . . . . . . . . . 13 (𝑅𝑆𝑇 · 1000) ∈ ℂ
247235nn0cni 11516 . . . . . . . . . . . . . 14 𝑈 ∈ ℂ
248103, 247mulcli 10257 . . . . . . . . . . . . 13 (100 · 𝑈) ∈ ℂ
249246, 248, 226addassi 10260 . . . . . . . . . . . 12 (((𝑅𝑆𝑇 · 1000) + (100 · 𝑈)) + 𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + ((100 · 𝑈) + 𝑃𝑄))
250 dfdec10 11709 . . . . . . . . . . . . . . 15 𝑅𝑆𝑇𝑈 = ((10 · 𝑅𝑆𝑇) + 𝑈)
251250oveq2i 6825 . . . . . . . . . . . . . 14 (100 · 𝑅𝑆𝑇𝑈) = (100 · ((10 · 𝑅𝑆𝑇) + 𝑈))
25224, 140mulcli 10257 . . . . . . . . . . . . . . 15 (10 · 𝑅𝑆𝑇) ∈ ℂ
253103, 252, 247adddii 10262 . . . . . . . . . . . . . 14 (100 · ((10 · 𝑅𝑆𝑇) + 𝑈)) = ((100 · (10 · 𝑅𝑆𝑇)) + (100 · 𝑈))
254140, 177mulcomi 10258 . . . . . . . . . . . . . . . 16 (𝑅𝑆𝑇 · 1000) = (1000 · 𝑅𝑆𝑇)
25524, 103mulcomi 10258 . . . . . . . . . . . . . . . . . 18 (10 · 100) = (100 · 10)
256255, 195eqtr3i 2784 . . . . . . . . . . . . . . . . 17 (100 · 10) = 1000
257256oveq1i 6824 . . . . . . . . . . . . . . . 16 ((100 · 10) · 𝑅𝑆𝑇) = (1000 · 𝑅𝑆𝑇)
258103, 24, 140mulassi 10261 . . . . . . . . . . . . . . . 16 ((100 · 10) · 𝑅𝑆𝑇) = (100 · (10 · 𝑅𝑆𝑇))
259254, 257, 2583eqtr2ri 2789 . . . . . . . . . . . . . . 15 (100 · (10 · 𝑅𝑆𝑇)) = (𝑅𝑆𝑇 · 1000)
260259oveq1i 6824 . . . . . . . . . . . . . 14 ((100 · (10 · 𝑅𝑆𝑇)) + (100 · 𝑈)) = ((𝑅𝑆𝑇 · 1000) + (100 · 𝑈))
261251, 253, 2603eqtri 2786 . . . . . . . . . . . . 13 (100 · 𝑅𝑆𝑇𝑈) = ((𝑅𝑆𝑇 · 1000) + (100 · 𝑈))
262261oveq1i 6824 . . . . . . . . . . . 12 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) = (((𝑅𝑆𝑇 · 1000) + (100 · 𝑈)) + 𝑃𝑄)
263235, 62, 64dfdec100 29906 . . . . . . . . . . . . 13 𝑈𝑃𝑄 = ((100 · 𝑈) + 𝑃𝑄)
264263oveq2i 6825 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + ((100 · 𝑈) + 𝑃𝑄))
265249, 262, 2643eqtr4i 2792 . . . . . . . . . . 11 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄)
266140, 141, 177adddiri 10263 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 + 1) · 1000) = ((𝑅𝑆𝑇 · 1000) + (1 · 1000))
267177mulid2i 10255 . . . . . . . . . . . . 13 (1 · 1000) = 1000
268267oveq2i 6825 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 · 1000) + (1 · 1000)) = ((𝑅𝑆𝑇 · 1000) + 1000)
269266, 268eqtri 2782 . . . . . . . . . . 11 ((𝑅𝑆𝑇 + 1) · 1000) = ((𝑅𝑆𝑇 · 1000) + 1000)
270245, 265, 2693brtr4i 4834 . . . . . . . . . 10 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) < ((𝑅𝑆𝑇 + 1) · 1000)
271234, 270eqbrtri 4825 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) < ((𝑅𝑆𝑇 + 1) · 1000)
272223, 214posdifi 10790 . . . . . . . . 9 (((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) < ((𝑅𝑆𝑇 + 1) · 1000) ↔ 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
273271, 272mpbi 220 . . . . . . . 8 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
274 elrp 12047 . . . . . . . 8 ((((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+ ↔ ((((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ ∧ 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))))
275224, 273, 274mpbir2an 993 . . . . . . 7 (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+
276 ltsubrp 12079 . . . . . . 7 (((𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ ∧ (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ+) → ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) < (𝑊𝑋𝑌𝑍 · 1000))
277210, 275, 276mp2an 710 . . . . . 6 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) < (𝑊𝑋𝑌𝑍 · 1000)
278207, 277eqbrtri 4825 . . . . 5 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000)
2793, 4deccl 11724 . . . . . . . . 9 𝐴𝐵𝐶 ∈ ℕ0
280279, 5deccl 11724 . . . . . . . 8 𝐴𝐵𝐶𝐷 ∈ ℕ0
281280nn0rei 11515 . . . . . . 7 𝐴𝐵𝐶𝐷 ∈ ℝ
2829, 10deccl 11724 . . . . . . . . 9 𝐸𝐹𝐺 ∈ ℕ0
283282, 11deccl 11724 . . . . . . . 8 𝐸𝐹𝐺𝐻 ∈ ℕ0
284283nn0rei 11515 . . . . . . 7 𝐸𝐹𝐺𝐻 ∈ ℝ
285281, 284remulcli 10266 . . . . . 6 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) ∈ ℝ
28623decnncl2 11737 . . . . . . . . 9 100 ∈ ℕ
287286decnncl2 11737 . . . . . . . 8 1000 ∈ ℕ
288287nngt0i 11266 . . . . . . 7 0 < 1000
289209, 288pm3.2i 470 . . . . . 6 (1000 ∈ ℝ ∧ 0 < 1000)
290 ltdiv1 11099 . . . . . 6 (((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) ∈ ℝ ∧ (𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ ∧ (1000 ∈ ℝ ∧ 0 < 1000)) → ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000) ↔ ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000)))
291285, 210, 289, 290mp3an 1573 . . . . 5 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000) ↔ ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000))
292278, 291mpbi 220 . . . 4 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000)
293280nn0cni 11516 . . . . . 6 𝐴𝐵𝐶𝐷 ∈ ℂ
294283nn0cni 11516 . . . . . 6 𝐸𝐹𝐺𝐻 ∈ ℂ
295209, 288gt0ne0ii 10776 . . . . . 6 1000 ≠ 0
296293, 294, 177, 295div23i 10995 . . . . 5 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴𝐵𝐶𝐷 / 1000) · 𝐸𝐹𝐺𝐻)
2971, 2, 4, 48dpmul1000 29937 . . . . . . . 8 ((𝐴.𝐵𝐶𝐷) · 1000) = 𝐴𝐵𝐶𝐷
298297oveq1i 6824 . . . . . . 7 (((𝐴.𝐵𝐶𝐷) · 1000) / 1000) = (𝐴𝐵𝐶𝐷 / 1000)
2994nn0rei 11515 . . . . . . . . . . . 12 𝐶 ∈ ℝ
300 dp2cl 29917 . . . . . . . . . . . 12 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → 𝐶𝐷 ∈ ℝ)
301299, 48, 300mp2an 710 . . . . . . . . . . 11 𝐶𝐷 ∈ ℝ
302 dp2cl 29917 . . . . . . . . . . 11 ((𝐵 ∈ ℝ ∧ 𝐶𝐷 ∈ ℝ) → 𝐵𝐶𝐷 ∈ ℝ)
30319, 301, 302mp2an 710 . . . . . . . . . 10 𝐵𝐶𝐷 ∈ ℝ
304 dpcl 29928 . . . . . . . . . 10 ((𝐴 ∈ ℕ0𝐵𝐶𝐷 ∈ ℝ) → (𝐴.𝐵𝐶𝐷) ∈ ℝ)
3051, 303, 304mp2an 710 . . . . . . . . 9 (𝐴.𝐵𝐶𝐷) ∈ ℝ
306305recni 10264 . . . . . . . 8 (𝐴.𝐵𝐶𝐷) ∈ ℂ
307306, 177, 295divcan4i 10984 . . . . . . 7 (((𝐴.𝐵𝐶𝐷) · 1000) / 1000) = (𝐴.𝐵𝐶𝐷)
308298, 307eqtr3i 2784 . . . . . 6 (𝐴𝐵𝐶𝐷 / 1000) = (𝐴.𝐵𝐶𝐷)
309308oveq1i 6824 . . . . 5 ((𝐴𝐵𝐶𝐷 / 1000) · 𝐸𝐹𝐺𝐻) = ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻)
310296, 309eqtri 2782 . . . 4 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻)
311175, 177, 295divcan4i 10984 . . . 4 ((𝑊𝑋𝑌𝑍 · 1000) / 1000) = 𝑊𝑋𝑌𝑍
312292, 310, 3113brtr3i 4833 . . 3 ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍
313305, 284remulcli 10266 . . . 4 ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) ∈ ℝ
314 ltdiv1 11099 . . . 4 ((((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) ∈ ℝ ∧ 𝑊𝑋𝑌𝑍 ∈ ℝ ∧ (1000 ∈ ℝ ∧ 0 < 1000)) → (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍 ↔ (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000)))
315313, 208, 289, 314mp3an 1573 . . 3 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍 ↔ (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000))
316312, 315mpbi 220 . 2 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000)
317306, 294, 177, 295divassi 10993 . . 3 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · (𝐸𝐹𝐺𝐻 / 1000))
3187, 8, 10, 52dpmul1000 29937 . . . . . 6 ((𝐸.𝐹𝐺𝐻) · 1000) = 𝐸𝐹𝐺𝐻
319318oveq1i 6824 . . . . 5 (((𝐸.𝐹𝐺𝐻) · 1000) / 1000) = (𝐸𝐹𝐺𝐻 / 1000)
32010nn0rei 11515 . . . . . . . . . 10 𝐺 ∈ ℝ
321 dp2cl 29917 . . . . . . . . . 10 ((𝐺 ∈ ℝ ∧ 𝐻 ∈ ℝ) → 𝐺𝐻 ∈ ℝ)
322320, 52, 321mp2an 710 . . . . . . . . 9 𝐺𝐻 ∈ ℝ
323 dp2cl 29917 . . . . . . . . 9 ((𝐹 ∈ ℝ ∧ 𝐺𝐻 ∈ ℝ) → 𝐹𝐺𝐻 ∈ ℝ)
32425, 322, 323mp2an 710 . . . . . . . 8 𝐹𝐺𝐻 ∈ ℝ
325 dpcl 29928 . . . . . . . 8 ((𝐸 ∈ ℕ0𝐹𝐺𝐻 ∈ ℝ) → (𝐸.𝐹𝐺𝐻) ∈ ℝ)
3267, 324, 325mp2an 710 . . . . . . 7 (𝐸.𝐹𝐺𝐻) ∈ ℝ
327326recni 10264 . . . . . 6 (𝐸.𝐹𝐺𝐻) ∈ ℂ
328327, 177, 295divcan4i 10984 . . . . 5 (((𝐸.𝐹𝐺𝐻) · 1000) / 1000) = (𝐸.𝐹𝐺𝐻)
329319, 328eqtr3i 2784 . . . 4 (𝐸𝐹𝐺𝐻 / 1000) = (𝐸.𝐹𝐺𝐻)
330329oveq2i 6825 . . 3 ((𝐴.𝐵𝐶𝐷) · (𝐸𝐹𝐺𝐻 / 1000)) = ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻))
331317, 330eqtri 2782 . 2 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻))
332173nn0rei 11515 . . . . 5 𝑍 ∈ ℝ
333168, 169, 171, 332dpmul1000 29937 . . . 4 ((𝑊.𝑋𝑌𝑍) · 1000) = 𝑊𝑋𝑌𝑍
334333oveq1i 6824 . . 3 (((𝑊.𝑋𝑌𝑍) · 1000) / 1000) = (𝑊𝑋𝑌𝑍 / 1000)
335169nn0rei 11515 . . . . . . 7 𝑋 ∈ ℝ
336171nn0rei 11515 . . . . . . . 8 𝑌 ∈ ℝ
337 dp2cl 29917 . . . . . . . 8 ((𝑌 ∈ ℝ ∧ 𝑍 ∈ ℝ) → 𝑌𝑍 ∈ ℝ)
338336, 332, 337mp2an 710 . . . . . . 7 𝑌𝑍 ∈ ℝ
339 dp2cl 29917 . . . . . . 7 ((𝑋 ∈ ℝ ∧ 𝑌𝑍 ∈ ℝ) → 𝑋𝑌𝑍 ∈ ℝ)
340335, 338, 339mp2an 710 . . . . . 6 𝑋𝑌𝑍 ∈ ℝ
341 dpcl 29928 . . . . . 6 ((𝑊 ∈ ℕ0𝑋𝑌𝑍 ∈ ℝ) → (𝑊.𝑋𝑌𝑍) ∈ ℝ)
342168, 340, 341mp2an 710 . . . . 5 (𝑊.𝑋𝑌𝑍) ∈ ℝ
343342recni 10264 . . . 4 (𝑊.𝑋𝑌𝑍) ∈ ℂ
344343, 177, 295divcan4i 10984 . . 3 (((𝑊.𝑋𝑌𝑍) · 1000) / 1000) = (𝑊.𝑋𝑌𝑍)
345334, 344eqtr3i 2784 . 2 (𝑊𝑋𝑌𝑍 / 1000) = (𝑊.𝑋𝑌𝑍)
346316, 331, 3453brtr3i 4833 1 ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻)) < (𝑊.𝑋𝑌𝑍)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1632  wcel 2139   class class class wbr 4804  (class class class)co 6814  cc 10146  cr 10147  0cc0 10148  1c1 10149   + caddc 10151   · cmul 10153   < clt 10286  cmin 10478   / cdiv 10896  2c2 11282  0cn0 11504  cdc 11705  +crp 12045  cexp 13074  cdp2 29907  .cdp 29925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-5 11294  df-6 11295  df-7 11296  df-8 11297  df-9 11298  df-n0 11505  df-z 11590  df-dec 11706  df-uz 11900  df-rp 12046  df-seq 13016  df-exp 13075  df-dp2 29908  df-dp 29926
This theorem is referenced by:  hgt750lem2  31060
  Copyright terms: Public domain W3C validator