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 30517
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 12101 . . . . . . . 8 𝐴𝐵 ∈ ℕ0
4 dpmul.c . . . . . . . . 9 𝐶 ∈ ℕ0
5 dpmul.d . . . . . . . . 9 𝐷 ∈ ℕ0
64, 5deccl 12101 . . . . . . . 8 𝐶𝐷 ∈ ℕ0
7 dpmul.e . . . . . . . . 9 𝐸 ∈ ℕ0
8 dpmul4.f . . . . . . . . 9 𝐹 ∈ ℕ0
97, 8deccl 12101 . . . . . . . 8 𝐸𝐹 ∈ ℕ0
10 dpmul.g . . . . . . . . 9 𝐺 ∈ ℕ0
11 dpmul4.h . . . . . . . . 9 𝐻 ∈ ℕ0
1210, 11deccl 12101 . . . . . . . 8 𝐺𝐻 ∈ ℕ0
13 dpmul4.l . . . . . . . . . 10 𝐿 ∈ ℕ0
14 dpmul4.m . . . . . . . . . 10 𝑀 ∈ ℕ0
1513, 14deccl 12101 . . . . . . . . 9 𝐿𝑀 ∈ ℕ0
16 dpmul4.n . . . . . . . . 9 𝑁 ∈ ℕ0
1715, 16deccl 12101 . . . . . . . 8 𝐿𝑀𝑁 ∈ ℕ0
18 2nn0 11902 . . . . . . . 8 2 ∈ ℕ0
192nn0rei 11896 . . . . . . . . . . . . 13 𝐵 ∈ ℝ
20 dpcl 30494 . . . . . . . . . . . . 13 ((𝐴 ∈ ℕ0𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)
211, 19, 20mp2an 688 . . . . . . . . . . . 12 (𝐴.𝐵) ∈ ℝ
2221recni 10643 . . . . . . . . . . 11 (𝐴.𝐵) ∈ ℂ
23 10nn 12102 . . . . . . . . . . . 12 10 ∈ ℕ
2423nncni 11636 . . . . . . . . . . 11 10 ∈ ℂ
258nn0rei 11896 . . . . . . . . . . . . 13 𝐹 ∈ ℝ
26 dpcl 30494 . . . . . . . . . . . . 13 ((𝐸 ∈ ℕ0𝐹 ∈ ℝ) → (𝐸.𝐹) ∈ ℝ)
277, 25, 26mp2an 688 . . . . . . . . . . . 12 (𝐸.𝐹) ∈ ℝ
2827recni 10643 . . . . . . . . . . 11 (𝐸.𝐹) ∈ ℂ
2922, 24, 28, 24mul4i 10825 . . . . . . . . . 10 (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10)) = (((𝐴.𝐵) · (𝐸.𝐹)) · (10 · 10))
3022, 28mulcli 10636 . . . . . . . . . . 11 ((𝐴.𝐵) · (𝐸.𝐹)) ∈ ℂ
3130, 24, 24mulassi 10640 . . . . . . . . . 10 ((((𝐴.𝐵) · (𝐸.𝐹)) · 10) · 10) = (((𝐴.𝐵) · (𝐸.𝐹)) · (10 · 10))
32 dpmul4.2 . . . . . . . . . . . . 13 ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼.𝐽𝐾)
3332oveq1i 7155 . . . . . . . . . . . 12 (((𝐴.𝐵) · (𝐸.𝐹)) · 10) = ((𝐼.𝐽𝐾) · 10)
34 dpmul4.i . . . . . . . . . . . . 13 𝐼 ∈ ℕ0
35 dpmul.j . . . . . . . . . . . . 13 𝐽 ∈ ℕ0
36 dpmul.k . . . . . . . . . . . . . 14 𝐾 ∈ ℕ0
3736nn0rei 11896 . . . . . . . . . . . . 13 𝐾 ∈ ℝ
3834, 35, 37dp3mul10 30501 . . . . . . . . . . . 12 ((𝐼.𝐽𝐾) · 10) = (𝐼𝐽.𝐾)
3933, 38eqtri 2841 . . . . . . . . . . 11 (((𝐴.𝐵) · (𝐸.𝐹)) · 10) = (𝐼𝐽.𝐾)
4039oveq1i 7155 . . . . . . . . . 10 ((((𝐴.𝐵) · (𝐸.𝐹)) · 10) · 10) = ((𝐼𝐽.𝐾) · 10)
4129, 31, 403eqtr2ri 2848 . . . . . . . . 9 ((𝐼𝐽.𝐾) · 10) = (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10))
4234, 35deccl 12101 . . . . . . . . . 10 𝐼𝐽 ∈ ℕ0
4342, 37dpmul10 30498 . . . . . . . . 9 ((𝐼𝐽.𝐾) · 10) = 𝐼𝐽𝐾
441, 19dpmul10 30498 . . . . . . . . . 10 ((𝐴.𝐵) · 10) = 𝐴𝐵
457, 25dpmul10 30498 . . . . . . . . . 10 ((𝐸.𝐹) · 10) = 𝐸𝐹
4644, 45oveq12i 7157 . . . . . . . . 9 (((𝐴.𝐵) · 10) · ((𝐸.𝐹) · 10)) = (𝐴𝐵 · 𝐸𝐹)
4741, 43, 463eqtr3ri 2850 . . . . . . . 8 (𝐴𝐵 · 𝐸𝐹) = 𝐼𝐽𝐾
485nn0rei 11896 . . . . . . . . . . . . 13 𝐷 ∈ ℝ
49 dpcl 30494 . . . . . . . . . . . . 13 ((𝐶 ∈ ℕ0𝐷 ∈ ℝ) → (𝐶.𝐷) ∈ ℝ)
504, 48, 49mp2an 688 . . . . . . . . . . . 12 (𝐶.𝐷) ∈ ℝ
5150recni 10643 . . . . . . . . . . 11 (𝐶.𝐷) ∈ ℂ
5211nn0rei 11896 . . . . . . . . . . . . 13 𝐻 ∈ ℝ
53 dpcl 30494 . . . . . . . . . . . . 13 ((𝐺 ∈ ℕ0𝐻 ∈ ℝ) → (𝐺.𝐻) ∈ ℝ)
5410, 52, 53mp2an 688 . . . . . . . . . . . 12 (𝐺.𝐻) ∈ ℝ
5554recni 10643 . . . . . . . . . . 11 (𝐺.𝐻) ∈ ℂ
5651, 24, 55, 24mul4i 10825 . . . . . . . . . 10 (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10)) = (((𝐶.𝐷) · (𝐺.𝐻)) · (10 · 10))
5751, 55mulcli 10636 . . . . . . . . . . 11 ((𝐶.𝐷) · (𝐺.𝐻)) ∈ ℂ
5857, 24, 24mulassi 10640 . . . . . . . . . 10 ((((𝐶.𝐷) · (𝐺.𝐻)) · 10) · 10) = (((𝐶.𝐷) · (𝐺.𝐻)) · (10 · 10))
59 dpmul4.3 . . . . . . . . . . . . 13 ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂.𝑃𝑄)
6059oveq1i 7155 . . . . . . . . . . . 12 (((𝐶.𝐷) · (𝐺.𝐻)) · 10) = ((𝑂.𝑃𝑄) · 10)
61 dpmul4.o . . . . . . . . . . . . 13 𝑂 ∈ ℕ0
62 dpmul4.p . . . . . . . . . . . . 13 𝑃 ∈ ℕ0
63 dpmul4.q . . . . . . . . . . . . . 14 𝑄 ∈ ℕ0
6463nn0rei 11896 . . . . . . . . . . . . 13 𝑄 ∈ ℝ
6561, 62, 64dp3mul10 30501 . . . . . . . . . . . 12 ((𝑂.𝑃𝑄) · 10) = (𝑂𝑃.𝑄)
6660, 65eqtri 2841 . . . . . . . . . . 11 (((𝐶.𝐷) · (𝐺.𝐻)) · 10) = (𝑂𝑃.𝑄)
6766oveq1i 7155 . . . . . . . . . 10 ((((𝐶.𝐷) · (𝐺.𝐻)) · 10) · 10) = ((𝑂𝑃.𝑄) · 10)
6856, 58, 673eqtr2ri 2848 . . . . . . . . 9 ((𝑂𝑃.𝑄) · 10) = (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10))
6961, 62deccl 12101 . . . . . . . . . 10 𝑂𝑃 ∈ ℕ0
7069, 64dpmul10 30498 . . . . . . . . 9 ((𝑂𝑃.𝑄) · 10) = 𝑂𝑃𝑄
714, 48dpmul10 30498 . . . . . . . . . 10 ((𝐶.𝐷) · 10) = 𝐶𝐷
7210, 52dpmul10 30498 . . . . . . . . . 10 ((𝐺.𝐻) · 10) = 𝐺𝐻
7371, 72oveq12i 7157 . . . . . . . . 9 (((𝐶.𝐷) · 10) · ((𝐺.𝐻) · 10)) = (𝐶𝐷 · 𝐺𝐻)
7468, 70, 733eqtr3ri 2850 . . . . . . . 8 (𝐶𝐷 · 𝐺𝐻) = 𝑂𝑃𝑄
7522, 51, 24adddiri 10642 . . . . . . . . . . . 12 (((𝐴.𝐵) + (𝐶.𝐷)) · 10) = (((𝐴.𝐵) · 10) + ((𝐶.𝐷) · 10))
7644, 71oveq12i 7157 . . . . . . . . . . . 12 (((𝐴.𝐵) · 10) + ((𝐶.𝐷) · 10)) = (𝐴𝐵 + 𝐶𝐷)
7775, 76eqtr2i 2842 . . . . . . . . . . 11 (𝐴𝐵 + 𝐶𝐷) = (((𝐴.𝐵) + (𝐶.𝐷)) · 10)
7828, 55, 24adddiri 10642 . . . . . . . . . . . 12 (((𝐸.𝐹) + (𝐺.𝐻)) · 10) = (((𝐸.𝐹) · 10) + ((𝐺.𝐻) · 10))
7945, 72oveq12i 7157 . . . . . . . . . . . 12 (((𝐸.𝐹) · 10) + ((𝐺.𝐻) · 10)) = (𝐸𝐹 + 𝐺𝐻)
8078, 79eqtr2i 2842 . . . . . . . . . . 11 (𝐸𝐹 + 𝐺𝐻) = (((𝐸.𝐹) + (𝐺.𝐻)) · 10)
8177, 80oveq12i 7157 . . . . . . . . . 10 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · 10) · (((𝐸.𝐹) + (𝐺.𝐻)) · 10))
8222, 51addcli 10635 . . . . . . . . . . 11 ((𝐴.𝐵) + (𝐶.𝐷)) ∈ ℂ
8328, 55addcli 10635 . . . . . . . . . . 11 ((𝐸.𝐹) + (𝐺.𝐻)) ∈ ℂ
8482, 24, 83, 24mul4i 10825 . . . . . . . . . 10 ((((𝐴.𝐵) + (𝐶.𝐷)) · 10) · (((𝐸.𝐹) + (𝐺.𝐻)) · 10)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (10 · 10))
85 dpmul4.5 . . . . . . . . . . 11 (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄))
8685oveq1i 7155 . . . . . . . . . 10 ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (10 · 10)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10))
8781, 84, 863eqtri 2845 . . . . . . . . 9 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10))
88 10nn0 12104 . . . . . . . . . . 11 10 ∈ ℕ0
8988dec0u 12107 . . . . . . . . . 10 (10 · 10) = 100
9089oveq2i 7156 . . . . . . . . 9 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · (10 · 10)) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100)
9132, 30eqeltrri 2907 . . . . . . . . . . . 12 (𝐼.𝐽𝐾) ∈ ℂ
9214nn0rei 11896 . . . . . . . . . . . . . . 15 𝑀 ∈ ℝ
9316nn0rei 11896 . . . . . . . . . . . . . . 15 𝑁 ∈ ℝ
94 dp2cl 30483 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀𝑁 ∈ ℝ)
9592, 93, 94mp2an 688 . . . . . . . . . . . . . 14 𝑀𝑁 ∈ ℝ
96 dpcl 30494 . . . . . . . . . . . . . 14 ((𝐿 ∈ ℕ0𝑀𝑁 ∈ ℝ) → (𝐿.𝑀𝑁) ∈ ℝ)
9713, 95, 96mp2an 688 . . . . . . . . . . . . 13 (𝐿.𝑀𝑁) ∈ ℝ
9897recni 10643 . . . . . . . . . . . 12 (𝐿.𝑀𝑁) ∈ ℂ
9991, 98addcli 10635 . . . . . . . . . . 11 ((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) ∈ ℂ
10059, 57eqeltrri 2907 . . . . . . . . . . 11 (𝑂.𝑃𝑄) ∈ ℂ
101 0nn0 11900 . . . . . . . . . . . . 13 0 ∈ ℕ0
10288, 101deccl 12101 . . . . . . . . . . . 12 100 ∈ ℕ0
103102nn0cni 11897 . . . . . . . . . . 11 100 ∈ ℂ
10499, 100, 103adddiri 10642 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100) = ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) + ((𝑂.𝑃𝑄) · 100))
10591, 98, 103adddiri 10642 . . . . . . . . . . 11 (((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) = (((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100))
106105oveq1i 7155 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) · 100) + ((𝑂.𝑃𝑄) · 100)) = ((((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) + ((𝑂.𝑃𝑄) · 100))
10734, 35, 37dpmul100 30500 . . . . . . . . . . . 12 ((𝐼.𝐽𝐾) · 100) = 𝐼𝐽𝐾
10813, 14, 93dpmul100 30500 . . . . . . . . . . . 12 ((𝐿.𝑀𝑁) · 100) = 𝐿𝑀𝑁
109107, 108oveq12i 7157 . . . . . . . . . . 11 (((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) = (𝐼𝐽𝐾 + 𝐿𝑀𝑁)
11061, 62, 64dpmul100 30500 . . . . . . . . . . 11 ((𝑂.𝑃𝑄) · 100) = 𝑂𝑃𝑄
111109, 110oveq12i 7157 . . . . . . . . . 10 ((((𝐼.𝐽𝐾) · 100) + ((𝐿.𝑀𝑁) · 100)) + ((𝑂.𝑃𝑄) · 100)) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
112104, 106, 1113eqtri 2845 . . . . . . . . 9 ((((𝐼.𝐽𝐾) + (𝐿.𝑀𝑁)) + (𝑂.𝑃𝑄)) · 100) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
11387, 90, 1123eqtri 2845 . . . . . . . 8 ((𝐴𝐵 + 𝐶𝐷) · (𝐸𝐹 + 𝐺𝐻)) = ((𝐼𝐽𝐾 + 𝐿𝑀𝑁) + 𝑂𝑃𝑄)
114 sq10 13612 . . . . . . . . . . . 12 (10↑2) = 100
115114oveq2i 7156 . . . . . . . . . . 11 (𝐴𝐵 · (10↑2)) = (𝐴𝐵 · 100)
1163nn0cni 11897 . . . . . . . . . . . 12 𝐴𝐵 ∈ ℂ
117103, 116mulcomi 10637 . . . . . . . . . . 11 (100 · 𝐴𝐵) = (𝐴𝐵 · 100)
118115, 117eqtr4i 2844 . . . . . . . . . 10 (𝐴𝐵 · (10↑2)) = (100 · 𝐴𝐵)
119118oveq1i 7155 . . . . . . . . 9 ((𝐴𝐵 · (10↑2)) + 𝐶𝐷) = ((100 · 𝐴𝐵) + 𝐶𝐷)
1203, 4, 48dfdec100 30473 . . . . . . . . 9 𝐴𝐵𝐶𝐷 = ((100 · 𝐴𝐵) + 𝐶𝐷)
121119, 120eqtr4i 2844 . . . . . . . 8 ((𝐴𝐵 · (10↑2)) + 𝐶𝐷) = 𝐴𝐵𝐶𝐷
122114oveq2i 7156 . . . . . . . . . . 11 (𝐸𝐹 · (10↑2)) = (𝐸𝐹 · 100)
1239nn0cni 11897 . . . . . . . . . . . 12 𝐸𝐹 ∈ ℂ
124103, 123mulcomi 10637 . . . . . . . . . . 11 (100 · 𝐸𝐹) = (𝐸𝐹 · 100)
125122, 124eqtr4i 2844 . . . . . . . . . 10 (𝐸𝐹 · (10↑2)) = (100 · 𝐸𝐹)
126125oveq1i 7155 . . . . . . . . 9 ((𝐸𝐹 · (10↑2)) + 𝐺𝐻) = ((100 · 𝐸𝐹) + 𝐺𝐻)
1279, 10, 52dfdec100 30473 . . . . . . . . 9 𝐸𝐹𝐺𝐻 = ((100 · 𝐸𝐹) + 𝐺𝐻)
128126, 127eqtr4i 2844 . . . . . . . 8 ((𝐸𝐹 · (10↑2)) + 𝐺𝐻) = 𝐸𝐹𝐺𝐻
12924sqvali 13531 . . . . . . . . . . . 12 (10↑2) = (10 · 10)
130129oveq2i 7156 . . . . . . . . . . 11 (𝐼𝐽𝐾 · (10↑2)) = (𝐼𝐽𝐾 · (10 · 10))
13142, 36deccl 12101 . . . . . . . . . . . . 13 𝐼𝐽𝐾 ∈ ℕ0
132131nn0cni 11897 . . . . . . . . . . . 12 𝐼𝐽𝐾 ∈ ℂ
133132, 24, 24mulassi 10640 . . . . . . . . . . 11 ((𝐼𝐽𝐾 · 10) · 10) = (𝐼𝐽𝐾 · (10 · 10))
134130, 133eqtr4i 2844 . . . . . . . . . 10 (𝐼𝐽𝐾 · (10↑2)) = ((𝐼𝐽𝐾 · 10) · 10)
135 dpmul4.r . . . . . . . . . . . . . . . 16 𝑅 ∈ ℕ0
136 dpmul4.s . . . . . . . . . . . . . . . 16 𝑆 ∈ ℕ0
137135, 136deccl 12101 . . . . . . . . . . . . . . 15 𝑅𝑆 ∈ ℕ0
138 dpmul4.t . . . . . . . . . . . . . . 15 𝑇 ∈ ℕ0
139137, 138deccl 12101 . . . . . . . . . . . . . 14 𝑅𝑆𝑇 ∈ ℕ0
140139nn0cni 11897 . . . . . . . . . . . . 13 𝑅𝑆𝑇 ∈ ℂ
141 ax-1cn 10583 . . . . . . . . . . . . 13 1 ∈ ℂ
142140, 141addcli 10635 . . . . . . . . . . . 12 (𝑅𝑆𝑇 + 1) ∈ ℂ
143132, 24mulcli 10636 . . . . . . . . . . . 12 (𝐼𝐽𝐾 · 10) ∈ ℂ
144141, 143addcomi 10819 . . . . . . . . . . . . . . . 16 (1 + (𝐼𝐽𝐾 · 10)) = ((𝐼𝐽𝐾 · 10) + 1)
14524, 132mulcomi 10637 . . . . . . . . . . . . . . . . . 18 (10 · 𝐼𝐽𝐾) = (𝐼𝐽𝐾 · 10)
146131dec0u 12107 . . . . . . . . . . . . . . . . . 18 (10 · 𝐼𝐽𝐾) = 𝐼𝐽𝐾0
147145, 146eqtr3i 2843 . . . . . . . . . . . . . . . . 17 (𝐼𝐽𝐾 · 10) = 𝐼𝐽𝐾0
148147oveq1i 7155 . . . . . . . . . . . . . . . 16 ((𝐼𝐽𝐾 · 10) + 1) = (𝐼𝐽𝐾0 + 1)
149141addid2i 10816 . . . . . . . . . . . . . . . . 17 (0 + 1) = 1
150 eqid 2818 . . . . . . . . . . . . . . . . 17 𝐼𝐽𝐾0 = 𝐼𝐽𝐾0
151131, 101, 149, 150decsuc 12117 . . . . . . . . . . . . . . . 16 (𝐼𝐽𝐾0 + 1) = 𝐼𝐽𝐾1
152144, 148, 1513eqtri 2845 . . . . . . . . . . . . . . 15 (1 + (𝐼𝐽𝐾 · 10)) = 𝐼𝐽𝐾1
153152oveq2i 7156 . . . . . . . . . . . . . 14 (𝑅𝑆𝑇 + (1 + (𝐼𝐽𝐾 · 10))) = (𝑅𝑆𝑇 + 𝐼𝐽𝐾1)
154140, 141, 143addassi 10639 . . . . . . . . . . . . . 14 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = (𝑅𝑆𝑇 + (1 + (𝐼𝐽𝐾 · 10)))
155 1nn0 11901 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ0
156131, 155deccl 12101 . . . . . . . . . . . . . . . 16 𝐼𝐽𝐾1 ∈ ℕ0
157156nn0cni 11897 . . . . . . . . . . . . . . 15 𝐼𝐽𝐾1 ∈ ℂ
158157, 140addcomi 10819 . . . . . . . . . . . . . 14 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = (𝑅𝑆𝑇 + 𝐼𝐽𝐾1)
159153, 154, 1583eqtr4i 2851 . . . . . . . . . . . . 13 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = (𝐼𝐽𝐾1 + 𝑅𝑆𝑇)
160 dpmul4.4 . . . . . . . . . . . . 13 (𝐼𝐽𝐾1 + 𝑅𝑆𝑇) = 𝑊𝑋𝑌𝑍
161159, 160eqtri 2841 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 + 1) + (𝐼𝐽𝐾 · 10)) = 𝑊𝑋𝑌𝑍
162142, 143, 161mvlladdi 10892 . . . . . . . . . . 11 (𝐼𝐽𝐾 · 10) = (𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1))
163162oveq1i 7155 . . . . . . . . . 10 ((𝐼𝐽𝐾 · 10) · 10) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10)
164134, 163eqtri 2841 . . . . . . . . 9 (𝐼𝐽𝐾 · (10↑2)) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10)
165164oveq1i 7155 . . . . . . . 8 ((𝐼𝐽𝐾 · (10↑2)) + 𝐿𝑀𝑁) = (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁)
166 eqid 2818 . . . . . . . 8 (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
1673, 6, 9, 12, 17, 18, 47, 74, 113, 121, 128, 165, 166karatsuba 16408 . . . . . . 7 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
168 dpmul4.w . . . . . . . . . . . . . . 15 𝑊 ∈ ℕ0
169 dpmul4.x . . . . . . . . . . . . . . 15 𝑋 ∈ ℕ0
170168, 169deccl 12101 . . . . . . . . . . . . . 14 𝑊𝑋 ∈ ℕ0
171 dpmul4.y . . . . . . . . . . . . . 14 𝑌 ∈ ℕ0
172170, 171deccl 12101 . . . . . . . . . . . . 13 𝑊𝑋𝑌 ∈ ℕ0
173 dpmul4.z . . . . . . . . . . . . 13 𝑍 ∈ ℕ0
174172, 173deccl 12101 . . . . . . . . . . . 12 𝑊𝑋𝑌𝑍 ∈ ℕ0
175174nn0cni 11897 . . . . . . . . . . 11 𝑊𝑋𝑌𝑍 ∈ ℂ
176102, 101deccl 12101 . . . . . . . . . . . 12 1000 ∈ ℕ0
177176nn0cni 11897 . . . . . . . . . . 11 1000 ∈ ℂ
178175, 177mulcli 10636 . . . . . . . . . 10 (𝑊𝑋𝑌𝑍 · 1000) ∈ ℂ
179142, 177mulcli 10636 . . . . . . . . . 10 ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℂ
180178, 179subcli 10950 . . . . . . . . 9 ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) ∈ ℂ
18117nn0cni 11897 . . . . . . . . . 10 𝐿𝑀𝑁 ∈ ℂ
182103, 181mulcli 10636 . . . . . . . . 9 (100 · 𝐿𝑀𝑁) ∈ ℂ
18361, 62, 64dfdec100 30473 . . . . . . . . . 10 𝑂𝑃𝑄 = ((100 · 𝑂) + 𝑃𝑄)
18469, 63deccl 12101 . . . . . . . . . . 11 𝑂𝑃𝑄 ∈ ℕ0
185184nn0cni 11897 . . . . . . . . . 10 𝑂𝑃𝑄 ∈ ℂ
186183, 185eqeltrri 2907 . . . . . . . . 9 ((100 · 𝑂) + 𝑃𝑄) ∈ ℂ
187180, 182, 186addassi 10639 . . . . . . . 8 ((((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) + ((100 · 𝑂) + 𝑃𝑄)) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
18824sqcli 13532 . . . . . . . . . . . . 13 (10↑2) ∈ ℂ
189132, 188mulcli 10636 . . . . . . . . . . . 12 (𝐼𝐽𝐾 · (10↑2)) ∈ ℂ
190164, 189eqeltrri 2907 . . . . . . . . . . 11 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) ∈ ℂ
191190, 181, 103adddiri 10642 . . . . . . . . . 10 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · 100) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) + (𝐿𝑀𝑁 · 100))
192114oveq2i 7156 . . . . . . . . . 10 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · 100)
193175, 142subcli 10950 . . . . . . . . . . . . 13 (𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) ∈ ℂ
194193, 24, 103mulassi 10640 . . . . . . . . . . . 12 (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · (10 · 100))
195102dec0u 12107 . . . . . . . . . . . . 13 (10 · 100) = 1000
196195oveq2i 7156 . . . . . . . . . . . 12 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · (10 · 100)) = ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 1000)
197175, 142, 177subdiri 11078 . . . . . . . . . . . 12 ((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 1000) = ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000))
198194, 196, 1973eqtrri 2846 . . . . . . . . . . 11 ((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) = (((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100)
199103, 181mulcomi 10637 . . . . . . . . . . 11 (100 · 𝐿𝑀𝑁) = (𝐿𝑀𝑁 · 100)
200198, 199oveq12i 7157 . . . . . . . . . 10 (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) = ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) · 100) + (𝐿𝑀𝑁 · 100))
201191, 192, 2003eqtr4i 2851 . . . . . . . . 9 ((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁))
202201, 183oveq12i 7157 . . . . . . . 8 (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄) = ((((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + (100 · 𝐿𝑀𝑁)) + ((100 · 𝑂) + 𝑃𝑄))
203182, 186addcli 10635 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℂ
204 subsub 10904 . . . . . . . . 9 (((𝑊𝑋𝑌𝑍 · 1000) ∈ ℂ ∧ ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℂ ∧ ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℂ) → ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
205178, 179, 203, 204mp3an 1452 . . . . . . . 8 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((𝑊𝑋𝑌𝑍 · 1000) − ((𝑅𝑆𝑇 + 1) · 1000)) + ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
206187, 202, 2053eqtr4ri 2852 . . . . . . 7 ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))) = (((((𝑊𝑋𝑌𝑍 − (𝑅𝑆𝑇 + 1)) · 10) + 𝐿𝑀𝑁) · (10↑2)) + 𝑂𝑃𝑄)
207167, 206eqtr4i 2844 . . . . . 6 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) = ((𝑊𝑋𝑌𝑍 · 1000) − (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
208174nn0rei 11896 . . . . . . . 8 𝑊𝑋𝑌𝑍 ∈ ℝ
209176nn0rei 11896 . . . . . . . 8 1000 ∈ ℝ
210208, 209remulcli 10645 . . . . . . 7 (𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ
211139nn0rei 11896 . . . . . . . . . . 11 𝑅𝑆𝑇 ∈ ℝ
212 1re 10629 . . . . . . . . . . 11 1 ∈ ℝ
213211, 212readdcli 10644 . . . . . . . . . 10 (𝑅𝑆𝑇 + 1) ∈ ℝ
214213, 209remulcli 10645 . . . . . . . . 9 ((𝑅𝑆𝑇 + 1) · 1000) ∈ ℝ
215102nn0rei 11896 . . . . . . . . . . 11 100 ∈ ℝ
21617nn0rei 11896 . . . . . . . . . . 11 𝐿𝑀𝑁 ∈ ℝ
217215, 216remulcli 10645 . . . . . . . . . 10 (100 · 𝐿𝑀𝑁) ∈ ℝ
21861nn0rei 11896 . . . . . . . . . . . 12 𝑂 ∈ ℝ
219215, 218remulcli 10645 . . . . . . . . . . 11 (100 · 𝑂) ∈ ℝ
22062, 63deccl 12101 . . . . . . . . . . . 12 𝑃𝑄 ∈ ℕ0
221220nn0rei 11896 . . . . . . . . . . 11 𝑃𝑄 ∈ ℝ
222219, 221readdcli 10644 . . . . . . . . . 10 ((100 · 𝑂) + 𝑃𝑄) ∈ ℝ
223217, 222readdcli 10644 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) ∈ ℝ
224214, 223resubcli 10936 . . . . . . . 8 (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))) ∈ ℝ
225219recni 10643 . . . . . . . . . . . 12 (100 · 𝑂) ∈ ℂ
226221recni 10643 . . . . . . . . . . . 12 𝑃𝑄 ∈ ℂ
227182, 225, 226addassi 10639 . . . . . . . . . . 11 (((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) + 𝑃𝑄) = ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))
228218recni 10643 . . . . . . . . . . . . . 14 𝑂 ∈ ℂ
229103, 181, 228adddii 10641 . . . . . . . . . . . . 13 (100 · (𝐿𝑀𝑁 + 𝑂)) = ((100 · 𝐿𝑀𝑁) + (100 · 𝑂))
230 dpmul4.1 . . . . . . . . . . . . . 14 (𝐿𝑀𝑁 + 𝑂) = 𝑅𝑆𝑇𝑈
231230oveq2i 7156 . . . . . . . . . . . . 13 (100 · (𝐿𝑀𝑁 + 𝑂)) = (100 · 𝑅𝑆𝑇𝑈)
232229, 231eqtr3i 2843 . . . . . . . . . . . 12 ((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) = (100 · 𝑅𝑆𝑇𝑈)
233232oveq1i 7155 . . . . . . . . . . 11 (((100 · 𝐿𝑀𝑁) + (100 · 𝑂)) + 𝑃𝑄) = ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄)
234227, 233eqtr3i 2843 . . . . . . . . . 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 12119 . . . . . . . . . . . 12 𝑈𝑃𝑄 < 1000
240235, 62deccl 12101 . . . . . . . . . . . . . . 15 𝑈𝑃 ∈ ℕ0
241240, 63deccl 12101 . . . . . . . . . . . . . 14 𝑈𝑃𝑄 ∈ ℕ0
242241nn0rei 11896 . . . . . . . . . . . . 13 𝑈𝑃𝑄 ∈ ℝ
243211, 209remulcli 10645 . . . . . . . . . . . . 13 (𝑅𝑆𝑇 · 1000) ∈ ℝ
244242, 209, 243ltadd2i 10759 . . . . . . . . . . . 12 (𝑈𝑃𝑄 < 1000 ↔ ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) < ((𝑅𝑆𝑇 · 1000) + 1000))
245239, 244mpbi 231 . . . . . . . . . . 11 ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) < ((𝑅𝑆𝑇 · 1000) + 1000)
246140, 177mulcli 10636 . . . . . . . . . . . . 13 (𝑅𝑆𝑇 · 1000) ∈ ℂ
247235nn0cni 11897 . . . . . . . . . . . . . 14 𝑈 ∈ ℂ
248103, 247mulcli 10636 . . . . . . . . . . . . 13 (100 · 𝑈) ∈ ℂ
249246, 248, 226addassi 10639 . . . . . . . . . . . 12 (((𝑅𝑆𝑇 · 1000) + (100 · 𝑈)) + 𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + ((100 · 𝑈) + 𝑃𝑄))
250 dfdec10 12089 . . . . . . . . . . . . . . 15 𝑅𝑆𝑇𝑈 = ((10 · 𝑅𝑆𝑇) + 𝑈)
251250oveq2i 7156 . . . . . . . . . . . . . 14 (100 · 𝑅𝑆𝑇𝑈) = (100 · ((10 · 𝑅𝑆𝑇) + 𝑈))
25224, 140mulcli 10636 . . . . . . . . . . . . . . 15 (10 · 𝑅𝑆𝑇) ∈ ℂ
253103, 252, 247adddii 10641 . . . . . . . . . . . . . 14 (100 · ((10 · 𝑅𝑆𝑇) + 𝑈)) = ((100 · (10 · 𝑅𝑆𝑇)) + (100 · 𝑈))
254140, 177mulcomi 10637 . . . . . . . . . . . . . . . 16 (𝑅𝑆𝑇 · 1000) = (1000 · 𝑅𝑆𝑇)
25524, 103mulcomi 10637 . . . . . . . . . . . . . . . . . 18 (10 · 100) = (100 · 10)
256255, 195eqtr3i 2843 . . . . . . . . . . . . . . . . 17 (100 · 10) = 1000
257256oveq1i 7155 . . . . . . . . . . . . . . . 16 ((100 · 10) · 𝑅𝑆𝑇) = (1000 · 𝑅𝑆𝑇)
258103, 24, 140mulassi 10640 . . . . . . . . . . . . . . . 16 ((100 · 10) · 𝑅𝑆𝑇) = (100 · (10 · 𝑅𝑆𝑇))
259254, 257, 2583eqtr2ri 2848 . . . . . . . . . . . . . . 15 (100 · (10 · 𝑅𝑆𝑇)) = (𝑅𝑆𝑇 · 1000)
260259oveq1i 7155 . . . . . . . . . . . . . 14 ((100 · (10 · 𝑅𝑆𝑇)) + (100 · 𝑈)) = ((𝑅𝑆𝑇 · 1000) + (100 · 𝑈))
261251, 253, 2603eqtri 2845 . . . . . . . . . . . . 13 (100 · 𝑅𝑆𝑇𝑈) = ((𝑅𝑆𝑇 · 1000) + (100 · 𝑈))
262261oveq1i 7155 . . . . . . . . . . . 12 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) = (((𝑅𝑆𝑇 · 1000) + (100 · 𝑈)) + 𝑃𝑄)
263235, 62, 64dfdec100 30473 . . . . . . . . . . . . 13 𝑈𝑃𝑄 = ((100 · 𝑈) + 𝑃𝑄)
264263oveq2i 7156 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + ((100 · 𝑈) + 𝑃𝑄))
265249, 262, 2643eqtr4i 2851 . . . . . . . . . . 11 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) = ((𝑅𝑆𝑇 · 1000) + 𝑈𝑃𝑄)
266140, 141, 177adddiri 10642 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 + 1) · 1000) = ((𝑅𝑆𝑇 · 1000) + (1 · 1000))
267177mulid2i 10634 . . . . . . . . . . . . 13 (1 · 1000) = 1000
268267oveq2i 7156 . . . . . . . . . . . 12 ((𝑅𝑆𝑇 · 1000) + (1 · 1000)) = ((𝑅𝑆𝑇 · 1000) + 1000)
269266, 268eqtri 2841 . . . . . . . . . . 11 ((𝑅𝑆𝑇 + 1) · 1000) = ((𝑅𝑆𝑇 · 1000) + 1000)
270245, 265, 2693brtr4i 5087 . . . . . . . . . 10 ((100 · 𝑅𝑆𝑇𝑈) + 𝑃𝑄) < ((𝑅𝑆𝑇 + 1) · 1000)
271234, 270eqbrtri 5078 . . . . . . . . 9 ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) < ((𝑅𝑆𝑇 + 1) · 1000)
272223, 214posdifi 11178 . . . . . . . . 9 (((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)) < ((𝑅𝑆𝑇 + 1) · 1000) ↔ 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄))))
273271, 272mpbi 231 . . . . . . . 8 0 < (((𝑅𝑆𝑇 + 1) · 1000) − ((100 · 𝐿𝑀𝑁) + ((100 · 𝑂) + 𝑃𝑄)))
274 elrp 12379 . . . . . . . 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 12413 . . . . . . 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 5078 . . . . 5 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000)
2793, 4deccl 12101 . . . . . . . . 9 𝐴𝐵𝐶 ∈ ℕ0
280279, 5deccl 12101 . . . . . . . 8 𝐴𝐵𝐶𝐷 ∈ ℕ0
281280nn0rei 11896 . . . . . . 7 𝐴𝐵𝐶𝐷 ∈ ℝ
2829, 10deccl 12101 . . . . . . . . 9 𝐸𝐹𝐺 ∈ ℕ0
283282, 11deccl 12101 . . . . . . . 8 𝐸𝐹𝐺𝐻 ∈ ℕ0
284283nn0rei 11896 . . . . . . 7 𝐸𝐹𝐺𝐻 ∈ ℝ
285281, 284remulcli 10645 . . . . . 6 (𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) ∈ ℝ
28623decnncl2 12110 . . . . . . . . 9 100 ∈ ℕ
287286decnncl2 12110 . . . . . . . 8 1000 ∈ ℕ
288287nngt0i 11664 . . . . . . 7 0 < 1000
289209, 288pm3.2i 471 . . . . . 6 (1000 ∈ ℝ ∧ 0 < 1000)
290 ltdiv1 11492 . . . . . 6 (((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) ∈ ℝ ∧ (𝑊𝑋𝑌𝑍 · 1000) ∈ ℝ ∧ (1000 ∈ ℝ ∧ 0 < 1000)) → ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000) ↔ ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000)))
291285, 210, 289, 290mp3an 1452 . . . . 5 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) < (𝑊𝑋𝑌𝑍 · 1000) ↔ ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000))
292278, 291mpbi 231 . . . 4 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) < ((𝑊𝑋𝑌𝑍 · 1000) / 1000)
293280nn0cni 11897 . . . . . 6 𝐴𝐵𝐶𝐷 ∈ ℂ
294283nn0cni 11897 . . . . . 6 𝐸𝐹𝐺𝐻 ∈ ℂ
295209, 288gt0ne0ii 11164 . . . . . 6 1000 ≠ 0
296293, 294, 177, 295div23i 11386 . . . . 5 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴𝐵𝐶𝐷 / 1000) · 𝐸𝐹𝐺𝐻)
2971, 2, 4, 48dpmul1000 30502 . . . . . . . 8 ((𝐴.𝐵𝐶𝐷) · 1000) = 𝐴𝐵𝐶𝐷
298297oveq1i 7155 . . . . . . 7 (((𝐴.𝐵𝐶𝐷) · 1000) / 1000) = (𝐴𝐵𝐶𝐷 / 1000)
2994nn0rei 11896 . . . . . . . . . . . 12 𝐶 ∈ ℝ
300 dp2cl 30483 . . . . . . . . . . . 12 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → 𝐶𝐷 ∈ ℝ)
301299, 48, 300mp2an 688 . . . . . . . . . . 11 𝐶𝐷 ∈ ℝ
302 dp2cl 30483 . . . . . . . . . . 11 ((𝐵 ∈ ℝ ∧ 𝐶𝐷 ∈ ℝ) → 𝐵𝐶𝐷 ∈ ℝ)
30319, 301, 302mp2an 688 . . . . . . . . . 10 𝐵𝐶𝐷 ∈ ℝ
304 dpcl 30494 . . . . . . . . . 10 ((𝐴 ∈ ℕ0𝐵𝐶𝐷 ∈ ℝ) → (𝐴.𝐵𝐶𝐷) ∈ ℝ)
3051, 303, 304mp2an 688 . . . . . . . . 9 (𝐴.𝐵𝐶𝐷) ∈ ℝ
306305recni 10643 . . . . . . . 8 (𝐴.𝐵𝐶𝐷) ∈ ℂ
307306, 177, 295divcan4i 11375 . . . . . . 7 (((𝐴.𝐵𝐶𝐷) · 1000) / 1000) = (𝐴.𝐵𝐶𝐷)
308298, 307eqtr3i 2843 . . . . . 6 (𝐴𝐵𝐶𝐷 / 1000) = (𝐴.𝐵𝐶𝐷)
309308oveq1i 7155 . . . . 5 ((𝐴𝐵𝐶𝐷 / 1000) · 𝐸𝐹𝐺𝐻) = ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻)
310296, 309eqtri 2841 . . . 4 ((𝐴𝐵𝐶𝐷 · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻)
311175, 177, 295divcan4i 11375 . . . 4 ((𝑊𝑋𝑌𝑍 · 1000) / 1000) = 𝑊𝑋𝑌𝑍
312292, 310, 3113brtr3i 5086 . . 3 ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍
313305, 284remulcli 10645 . . . 4 ((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) ∈ ℝ
314 ltdiv1 11492 . . . 4 ((((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) ∈ ℝ ∧ 𝑊𝑋𝑌𝑍 ∈ ℝ ∧ (1000 ∈ ℝ ∧ 0 < 1000)) → (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍 ↔ (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000)))
315313, 208, 289, 314mp3an 1452 . . 3 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) < 𝑊𝑋𝑌𝑍 ↔ (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000))
316312, 315mpbi 231 . 2 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) < (𝑊𝑋𝑌𝑍 / 1000)
317306, 294, 177, 295divassi 11384 . . 3 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · (𝐸𝐹𝐺𝐻 / 1000))
3187, 8, 10, 52dpmul1000 30502 . . . . . 6 ((𝐸.𝐹𝐺𝐻) · 1000) = 𝐸𝐹𝐺𝐻
319318oveq1i 7155 . . . . 5 (((𝐸.𝐹𝐺𝐻) · 1000) / 1000) = (𝐸𝐹𝐺𝐻 / 1000)
32010nn0rei 11896 . . . . . . . . . 10 𝐺 ∈ ℝ
321 dp2cl 30483 . . . . . . . . . 10 ((𝐺 ∈ ℝ ∧ 𝐻 ∈ ℝ) → 𝐺𝐻 ∈ ℝ)
322320, 52, 321mp2an 688 . . . . . . . . 9 𝐺𝐻 ∈ ℝ
323 dp2cl 30483 . . . . . . . . 9 ((𝐹 ∈ ℝ ∧ 𝐺𝐻 ∈ ℝ) → 𝐹𝐺𝐻 ∈ ℝ)
32425, 322, 323mp2an 688 . . . . . . . 8 𝐹𝐺𝐻 ∈ ℝ
325 dpcl 30494 . . . . . . . 8 ((𝐸 ∈ ℕ0𝐹𝐺𝐻 ∈ ℝ) → (𝐸.𝐹𝐺𝐻) ∈ ℝ)
3267, 324, 325mp2an 688 . . . . . . 7 (𝐸.𝐹𝐺𝐻) ∈ ℝ
327326recni 10643 . . . . . 6 (𝐸.𝐹𝐺𝐻) ∈ ℂ
328327, 177, 295divcan4i 11375 . . . . 5 (((𝐸.𝐹𝐺𝐻) · 1000) / 1000) = (𝐸.𝐹𝐺𝐻)
329319, 328eqtr3i 2843 . . . 4 (𝐸𝐹𝐺𝐻 / 1000) = (𝐸.𝐹𝐺𝐻)
330329oveq2i 7156 . . 3 ((𝐴.𝐵𝐶𝐷) · (𝐸𝐹𝐺𝐻 / 1000)) = ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻))
331317, 330eqtri 2841 . 2 (((𝐴.𝐵𝐶𝐷) · 𝐸𝐹𝐺𝐻) / 1000) = ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻))
332173nn0rei 11896 . . . . 5 𝑍 ∈ ℝ
333168, 169, 171, 332dpmul1000 30502 . . . 4 ((𝑊.𝑋𝑌𝑍) · 1000) = 𝑊𝑋𝑌𝑍
334333oveq1i 7155 . . 3 (((𝑊.𝑋𝑌𝑍) · 1000) / 1000) = (𝑊𝑋𝑌𝑍 / 1000)
335169nn0rei 11896 . . . . . . 7 𝑋 ∈ ℝ
336171nn0rei 11896 . . . . . . . 8 𝑌 ∈ ℝ
337 dp2cl 30483 . . . . . . . 8 ((𝑌 ∈ ℝ ∧ 𝑍 ∈ ℝ) → 𝑌𝑍 ∈ ℝ)
338336, 332, 337mp2an 688 . . . . . . 7 𝑌𝑍 ∈ ℝ
339 dp2cl 30483 . . . . . . 7 ((𝑋 ∈ ℝ ∧ 𝑌𝑍 ∈ ℝ) → 𝑋𝑌𝑍 ∈ ℝ)
340335, 338, 339mp2an 688 . . . . . 6 𝑋𝑌𝑍 ∈ ℝ
341 dpcl 30494 . . . . . 6 ((𝑊 ∈ ℕ0𝑋𝑌𝑍 ∈ ℝ) → (𝑊.𝑋𝑌𝑍) ∈ ℝ)
342168, 340, 341mp2an 688 . . . . 5 (𝑊.𝑋𝑌𝑍) ∈ ℝ
343342recni 10643 . . . 4 (𝑊.𝑋𝑌𝑍) ∈ ℂ
344343, 177, 295divcan4i 11375 . . 3 (((𝑊.𝑋𝑌𝑍) · 1000) / 1000) = (𝑊.𝑋𝑌𝑍)
345334, 344eqtr3i 2843 . 2 (𝑊𝑋𝑌𝑍 / 1000) = (𝑊.𝑋𝑌𝑍)
346316, 331, 3453brtr3i 5086 1 ((𝐴.𝐵𝐶𝐷) · (𝐸.𝐹𝐺𝐻)) < (𝑊.𝑋𝑌𝑍)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1528  wcel 2105   class class class wbr 5057  (class class class)co 7145  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530   < clt 10663  cmin 10858   / cdiv 11285  2c2 11680  0cn0 11885  cdc 12086  +crp 12377  cexp 13417  cdp2 30474  .cdp 30491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-rp 12378  df-seq 13358  df-exp 13418  df-dp2 30475  df-dp 30492
This theorem is referenced by:  hgt750lem2  31822
  Copyright terms: Public domain W3C validator