Proof of Theorem dpmul4
Step | Hyp | Ref
| Expression |
1 | | dpmul.a |
. . . . . . . . 9
⊢ 𝐴 ∈
ℕ0 |
2 | | dpmul.b |
. . . . . . . . 9
⊢ 𝐵 ∈
ℕ0 |
3 | 1, 2 | deccl 12381 |
. . . . . . . 8
⊢ ;𝐴𝐵 ∈ ℕ0 |
4 | | dpmul.c |
. . . . . . . . 9
⊢ 𝐶 ∈
ℕ0 |
5 | | dpmul.d |
. . . . . . . . 9
⊢ 𝐷 ∈
ℕ0 |
6 | 4, 5 | deccl 12381 |
. . . . . . . 8
⊢ ;𝐶𝐷 ∈ ℕ0 |
7 | | dpmul.e |
. . . . . . . . 9
⊢ 𝐸 ∈
ℕ0 |
8 | | dpmul4.f |
. . . . . . . . 9
⊢ 𝐹 ∈
ℕ0 |
9 | 7, 8 | deccl 12381 |
. . . . . . . 8
⊢ ;𝐸𝐹 ∈ ℕ0 |
10 | | dpmul.g |
. . . . . . . . 9
⊢ 𝐺 ∈
ℕ0 |
11 | | dpmul4.h |
. . . . . . . . 9
⊢ 𝐻 ∈
ℕ0 |
12 | 10, 11 | deccl 12381 |
. . . . . . . 8
⊢ ;𝐺𝐻 ∈ ℕ0 |
13 | | dpmul4.l |
. . . . . . . . . 10
⊢ 𝐿 ∈
ℕ0 |
14 | | dpmul4.m |
. . . . . . . . . 10
⊢ 𝑀 ∈
ℕ0 |
15 | 13, 14 | deccl 12381 |
. . . . . . . . 9
⊢ ;𝐿𝑀 ∈ ℕ0 |
16 | | dpmul4.n |
. . . . . . . . 9
⊢ 𝑁 ∈
ℕ0 |
17 | 15, 16 | deccl 12381 |
. . . . . . . 8
⊢ ;;𝐿𝑀𝑁 ∈ ℕ0 |
18 | | 2nn0 12180 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
19 | 2 | nn0rei 12174 |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈ ℝ |
20 | | dpcl 31067 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℝ)
→ (𝐴.𝐵) ∈ ℝ) |
21 | 1, 19, 20 | mp2an 688 |
. . . . . . . . . . . 12
⊢ (𝐴.𝐵) ∈ ℝ |
22 | 21 | recni 10920 |
. . . . . . . . . . 11
⊢ (𝐴.𝐵) ∈ ℂ |
23 | | 10nn 12382 |
. . . . . . . . . . . 12
⊢ ;10 ∈ ℕ |
24 | 23 | nncni 11913 |
. . . . . . . . . . 11
⊢ ;10 ∈ ℂ |
25 | 8 | nn0rei 12174 |
. . . . . . . . . . . . 13
⊢ 𝐹 ∈ ℝ |
26 | | dpcl 31067 |
. . . . . . . . . . . . 13
⊢ ((𝐸 ∈ ℕ0
∧ 𝐹 ∈ ℝ)
→ (𝐸.𝐹) ∈ ℝ) |
27 | 7, 25, 26 | mp2an 688 |
. . . . . . . . . . . 12
⊢ (𝐸.𝐹) ∈ ℝ |
28 | 27 | recni 10920 |
. . . . . . . . . . 11
⊢ (𝐸.𝐹) ∈ ℂ |
29 | 22, 24, 28, 24 | mul4i 11102 |
. . . . . . . . . 10
⊢ (((𝐴.𝐵) · ;10) · ((𝐸.𝐹) · ;10)) = (((𝐴.𝐵) · (𝐸.𝐹)) · (;10 · ;10)) |
30 | 22, 28 | mulcli 10913 |
. . . . . . . . . . 11
⊢ ((𝐴.𝐵) · (𝐸.𝐹)) ∈ ℂ |
31 | 30, 24, 24 | mulassi 10917 |
. . . . . . . . . 10
⊢ ((((𝐴.𝐵) · (𝐸.𝐹)) · ;10) · ;10) = (((𝐴.𝐵) · (𝐸.𝐹)) · (;10 · ;10)) |
32 | | dpmul4.2 |
. . . . . . . . . . . . 13
⊢ ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼._𝐽𝐾) |
33 | 32 | oveq1i 7265 |
. . . . . . . . . . . 12
⊢ (((𝐴.𝐵) · (𝐸.𝐹)) · ;10) = ((𝐼._𝐽𝐾) · ;10) |
34 | | dpmul4.i |
. . . . . . . . . . . . 13
⊢ 𝐼 ∈
ℕ0 |
35 | | dpmul.j |
. . . . . . . . . . . . 13
⊢ 𝐽 ∈
ℕ0 |
36 | | dpmul.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 ∈
ℕ0 |
37 | 36 | nn0rei 12174 |
. . . . . . . . . . . . 13
⊢ 𝐾 ∈ ℝ |
38 | 34, 35, 37 | dp3mul10 31074 |
. . . . . . . . . . . 12
⊢ ((𝐼._𝐽𝐾) · ;10) = (;𝐼𝐽.𝐾) |
39 | 33, 38 | eqtri 2766 |
. . . . . . . . . . 11
⊢ (((𝐴.𝐵) · (𝐸.𝐹)) · ;10) = (;𝐼𝐽.𝐾) |
40 | 39 | oveq1i 7265 |
. . . . . . . . . 10
⊢ ((((𝐴.𝐵) · (𝐸.𝐹)) · ;10) · ;10) = ((;𝐼𝐽.𝐾) · ;10) |
41 | 29, 31, 40 | 3eqtr2ri 2773 |
. . . . . . . . 9
⊢ ((;𝐼𝐽.𝐾) · ;10) = (((𝐴.𝐵) · ;10) · ((𝐸.𝐹) · ;10)) |
42 | 34, 35 | deccl 12381 |
. . . . . . . . . 10
⊢ ;𝐼𝐽 ∈ ℕ0 |
43 | 42, 37 | dpmul10 31071 |
. . . . . . . . 9
⊢ ((;𝐼𝐽.𝐾) · ;10) = ;;𝐼𝐽𝐾 |
44 | 1, 19 | dpmul10 31071 |
. . . . . . . . . 10
⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵 |
45 | 7, 25 | dpmul10 31071 |
. . . . . . . . . 10
⊢ ((𝐸.𝐹) · ;10) = ;𝐸𝐹 |
46 | 44, 45 | oveq12i 7267 |
. . . . . . . . 9
⊢ (((𝐴.𝐵) · ;10) · ((𝐸.𝐹) · ;10)) = (;𝐴𝐵 · ;𝐸𝐹) |
47 | 41, 43, 46 | 3eqtr3ri 2775 |
. . . . . . . 8
⊢ (;𝐴𝐵 · ;𝐸𝐹) = ;;𝐼𝐽𝐾 |
48 | 5 | nn0rei 12174 |
. . . . . . . . . . . . 13
⊢ 𝐷 ∈ ℝ |
49 | | dpcl 31067 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℕ0
∧ 𝐷 ∈ ℝ)
→ (𝐶.𝐷) ∈ ℝ) |
50 | 4, 48, 49 | mp2an 688 |
. . . . . . . . . . . 12
⊢ (𝐶.𝐷) ∈ ℝ |
51 | 50 | recni 10920 |
. . . . . . . . . . 11
⊢ (𝐶.𝐷) ∈ ℂ |
52 | 11 | nn0rei 12174 |
. . . . . . . . . . . . 13
⊢ 𝐻 ∈ ℝ |
53 | | dpcl 31067 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ ℕ0
∧ 𝐻 ∈ ℝ)
→ (𝐺.𝐻) ∈ ℝ) |
54 | 10, 52, 53 | mp2an 688 |
. . . . . . . . . . . 12
⊢ (𝐺.𝐻) ∈ ℝ |
55 | 54 | recni 10920 |
. . . . . . . . . . 11
⊢ (𝐺.𝐻) ∈ ℂ |
56 | 51, 24, 55, 24 | mul4i 11102 |
. . . . . . . . . 10
⊢ (((𝐶.𝐷) · ;10) · ((𝐺.𝐻) · ;10)) = (((𝐶.𝐷) · (𝐺.𝐻)) · (;10 · ;10)) |
57 | 51, 55 | mulcli 10913 |
. . . . . . . . . . 11
⊢ ((𝐶.𝐷) · (𝐺.𝐻)) ∈ ℂ |
58 | 57, 24, 24 | mulassi 10917 |
. . . . . . . . . 10
⊢ ((((𝐶.𝐷) · (𝐺.𝐻)) · ;10) · ;10) = (((𝐶.𝐷) · (𝐺.𝐻)) · (;10 · ;10)) |
59 | | dpmul4.3 |
. . . . . . . . . . . . 13
⊢ ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂._𝑃𝑄) |
60 | 59 | oveq1i 7265 |
. . . . . . . . . . . 12
⊢ (((𝐶.𝐷) · (𝐺.𝐻)) · ;10) = ((𝑂._𝑃𝑄) · ;10) |
61 | | dpmul4.o |
. . . . . . . . . . . . 13
⊢ 𝑂 ∈
ℕ0 |
62 | | dpmul4.p |
. . . . . . . . . . . . 13
⊢ 𝑃 ∈
ℕ0 |
63 | | dpmul4.q |
. . . . . . . . . . . . . 14
⊢ 𝑄 ∈
ℕ0 |
64 | 63 | nn0rei 12174 |
. . . . . . . . . . . . 13
⊢ 𝑄 ∈ ℝ |
65 | 61, 62, 64 | dp3mul10 31074 |
. . . . . . . . . . . 12
⊢ ((𝑂._𝑃𝑄) · ;10) = (;𝑂𝑃.𝑄) |
66 | 60, 65 | eqtri 2766 |
. . . . . . . . . . 11
⊢ (((𝐶.𝐷) · (𝐺.𝐻)) · ;10) = (;𝑂𝑃.𝑄) |
67 | 66 | oveq1i 7265 |
. . . . . . . . . 10
⊢ ((((𝐶.𝐷) · (𝐺.𝐻)) · ;10) · ;10) = ((;𝑂𝑃.𝑄) · ;10) |
68 | 56, 58, 67 | 3eqtr2ri 2773 |
. . . . . . . . 9
⊢ ((;𝑂𝑃.𝑄) · ;10) = (((𝐶.𝐷) · ;10) · ((𝐺.𝐻) · ;10)) |
69 | 61, 62 | deccl 12381 |
. . . . . . . . . 10
⊢ ;𝑂𝑃 ∈ ℕ0 |
70 | 69, 64 | dpmul10 31071 |
. . . . . . . . 9
⊢ ((;𝑂𝑃.𝑄) · ;10) = ;;𝑂𝑃𝑄 |
71 | 4, 48 | dpmul10 31071 |
. . . . . . . . . 10
⊢ ((𝐶.𝐷) · ;10) = ;𝐶𝐷 |
72 | 10, 52 | dpmul10 31071 |
. . . . . . . . . 10
⊢ ((𝐺.𝐻) · ;10) = ;𝐺𝐻 |
73 | 71, 72 | oveq12i 7267 |
. . . . . . . . 9
⊢ (((𝐶.𝐷) · ;10) · ((𝐺.𝐻) · ;10)) = (;𝐶𝐷 · ;𝐺𝐻) |
74 | 68, 70, 73 | 3eqtr3ri 2775 |
. . . . . . . 8
⊢ (;𝐶𝐷 · ;𝐺𝐻) = ;;𝑂𝑃𝑄 |
75 | 22, 51, 24 | adddiri 10919 |
. . . . . . . . . . . 12
⊢ (((𝐴.𝐵) + (𝐶.𝐷)) · ;10) = (((𝐴.𝐵) · ;10) + ((𝐶.𝐷) · ;10)) |
76 | 44, 71 | oveq12i 7267 |
. . . . . . . . . . . 12
⊢ (((𝐴.𝐵) · ;10) + ((𝐶.𝐷) · ;10)) = (;𝐴𝐵 + ;𝐶𝐷) |
77 | 75, 76 | eqtr2i 2767 |
. . . . . . . . . . 11
⊢ (;𝐴𝐵 + ;𝐶𝐷) = (((𝐴.𝐵) + (𝐶.𝐷)) · ;10) |
78 | 28, 55, 24 | adddiri 10919 |
. . . . . . . . . . . 12
⊢ (((𝐸.𝐹) + (𝐺.𝐻)) · ;10) = (((𝐸.𝐹) · ;10) + ((𝐺.𝐻) · ;10)) |
79 | 45, 72 | oveq12i 7267 |
. . . . . . . . . . . 12
⊢ (((𝐸.𝐹) · ;10) + ((𝐺.𝐻) · ;10)) = (;𝐸𝐹 + ;𝐺𝐻) |
80 | 78, 79 | eqtr2i 2767 |
. . . . . . . . . . 11
⊢ (;𝐸𝐹 + ;𝐺𝐻) = (((𝐸.𝐹) + (𝐺.𝐻)) · ;10) |
81 | 77, 80 | oveq12i 7267 |
. . . . . . . . . 10
⊢ ((;𝐴𝐵 + ;𝐶𝐷) · (;𝐸𝐹 + ;𝐺𝐻)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · ;10) · (((𝐸.𝐹) + (𝐺.𝐻)) · ;10)) |
82 | 22, 51 | addcli 10912 |
. . . . . . . . . . 11
⊢ ((𝐴.𝐵) + (𝐶.𝐷)) ∈ ℂ |
83 | 28, 55 | addcli 10912 |
. . . . . . . . . . 11
⊢ ((𝐸.𝐹) + (𝐺.𝐻)) ∈ ℂ |
84 | 82, 24, 83, 24 | mul4i 11102 |
. . . . . . . . . 10
⊢ ((((𝐴.𝐵) + (𝐶.𝐷)) · ;10) · (((𝐸.𝐹) + (𝐺.𝐻)) · ;10)) = ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (;10 · ;10)) |
85 | | dpmul4.5 |
. . . . . . . . . . 11
⊢ (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄)) |
86 | 85 | oveq1i 7265 |
. . . . . . . . . 10
⊢ ((((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) · (;10 · ;10)) = ((((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄)) · (;10 · ;10)) |
87 | 81, 84, 86 | 3eqtri 2770 |
. . . . . . . . 9
⊢ ((;𝐴𝐵 + ;𝐶𝐷) · (;𝐸𝐹 + ;𝐺𝐻)) = ((((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄)) · (;10 · ;10)) |
88 | | 10nn0 12384 |
. . . . . . . . . . 11
⊢ ;10 ∈
ℕ0 |
89 | 88 | dec0u 12387 |
. . . . . . . . . 10
⊢ (;10 · ;10) = ;;100 |
90 | 89 | oveq2i 7266 |
. . . . . . . . 9
⊢ ((((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄)) · (;10 · ;10)) = ((((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄)) · ;;100) |
91 | 32, 30 | eqeltrri 2836 |
. . . . . . . . . . . 12
⊢ (𝐼._𝐽𝐾) ∈ ℂ |
92 | 14 | nn0rei 12174 |
. . . . . . . . . . . . . . 15
⊢ 𝑀 ∈ ℝ |
93 | 16 | nn0rei 12174 |
. . . . . . . . . . . . . . 15
⊢ 𝑁 ∈ ℝ |
94 | | dp2cl 31056 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → _𝑀𝑁 ∈ ℝ) |
95 | 92, 93, 94 | mp2an 688 |
. . . . . . . . . . . . . 14
⊢ _𝑀𝑁 ∈ ℝ |
96 | | dpcl 31067 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ0
∧ _𝑀𝑁 ∈ ℝ) → (𝐿._𝑀𝑁) ∈ ℝ) |
97 | 13, 95, 96 | mp2an 688 |
. . . . . . . . . . . . 13
⊢ (𝐿._𝑀𝑁) ∈ ℝ |
98 | 97 | recni 10920 |
. . . . . . . . . . . 12
⊢ (𝐿._𝑀𝑁) ∈ ℂ |
99 | 91, 98 | addcli 10912 |
. . . . . . . . . . 11
⊢ ((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) ∈ ℂ |
100 | 59, 57 | eqeltrri 2836 |
. . . . . . . . . . 11
⊢ (𝑂._𝑃𝑄) ∈ ℂ |
101 | | 0nn0 12178 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
102 | 88, 101 | deccl 12381 |
. . . . . . . . . . . 12
⊢ ;;100 ∈ ℕ0 |
103 | 102 | nn0cni 12175 |
. . . . . . . . . . 11
⊢ ;;100 ∈ ℂ |
104 | 99, 100, 103 | adddiri 10919 |
. . . . . . . . . 10
⊢ ((((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄)) · ;;100) =
((((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) · ;;100) +
((𝑂._𝑃𝑄) · ;;100)) |
105 | 91, 98, 103 | adddiri 10919 |
. . . . . . . . . . 11
⊢ (((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) · ;;100) =
(((𝐼._𝐽𝐾) · ;;100) +
((𝐿._𝑀𝑁) · ;;100)) |
106 | 105 | oveq1i 7265 |
. . . . . . . . . 10
⊢ ((((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) · ;;100) +
((𝑂._𝑃𝑄) · ;;100))
= ((((𝐼._𝐽𝐾) · ;;100) +
((𝐿._𝑀𝑁) · ;;100))
+ ((𝑂._𝑃𝑄) · ;;100)) |
107 | 34, 35, 37 | dpmul100 31073 |
. . . . . . . . . . . 12
⊢ ((𝐼._𝐽𝐾) · ;;100) =
;;𝐼𝐽𝐾 |
108 | 13, 14, 93 | dpmul100 31073 |
. . . . . . . . . . . 12
⊢ ((𝐿._𝑀𝑁) · ;;100) =
;;𝐿𝑀𝑁 |
109 | 107, 108 | oveq12i 7267 |
. . . . . . . . . . 11
⊢ (((𝐼._𝐽𝐾) · ;;100) +
((𝐿._𝑀𝑁) · ;;100))
= (;;𝐼𝐽𝐾 + ;;𝐿𝑀𝑁) |
110 | 61, 62, 64 | dpmul100 31073 |
. . . . . . . . . . 11
⊢ ((𝑂._𝑃𝑄) · ;;100) =
;;𝑂𝑃𝑄 |
111 | 109, 110 | oveq12i 7267 |
. . . . . . . . . 10
⊢ ((((𝐼._𝐽𝐾) · ;;100) +
((𝐿._𝑀𝑁) · ;;100))
+ ((𝑂._𝑃𝑄) · ;;100))
= ((;;𝐼𝐽𝐾 + ;;𝐿𝑀𝑁) + ;;𝑂𝑃𝑄) |
112 | 104, 106,
111 | 3eqtri 2770 |
. . . . . . . . 9
⊢ ((((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄)) · ;;100) =
((;;𝐼𝐽𝐾 + ;;𝐿𝑀𝑁) + ;;𝑂𝑃𝑄) |
113 | 87, 90, 112 | 3eqtri 2770 |
. . . . . . . 8
⊢ ((;𝐴𝐵 + ;𝐶𝐷) · (;𝐸𝐹 + ;𝐺𝐻)) = ((;;𝐼𝐽𝐾 + ;;𝐿𝑀𝑁) + ;;𝑂𝑃𝑄) |
114 | | sq10 13906 |
. . . . . . . . . . . 12
⊢ (;10↑2) = ;;100 |
115 | 114 | oveq2i 7266 |
. . . . . . . . . . 11
⊢ (;𝐴𝐵 · (;10↑2)) = (;𝐴𝐵 · ;;100) |
116 | 3 | nn0cni 12175 |
. . . . . . . . . . . 12
⊢ ;𝐴𝐵 ∈ ℂ |
117 | 103, 116 | mulcomi 10914 |
. . . . . . . . . . 11
⊢ (;;100 · ;𝐴𝐵) = (;𝐴𝐵 · ;;100) |
118 | 115, 117 | eqtr4i 2769 |
. . . . . . . . . 10
⊢ (;𝐴𝐵 · (;10↑2)) = (;;100
· ;𝐴𝐵) |
119 | 118 | oveq1i 7265 |
. . . . . . . . 9
⊢ ((;𝐴𝐵 · (;10↑2)) + ;𝐶𝐷) = ((;;100
· ;𝐴𝐵) + ;𝐶𝐷) |
120 | 3, 4, 48 | dfdec100 31046 |
. . . . . . . . 9
⊢ ;;;𝐴𝐵𝐶𝐷 = ((;;100
· ;𝐴𝐵) + ;𝐶𝐷) |
121 | 119, 120 | eqtr4i 2769 |
. . . . . . . 8
⊢ ((;𝐴𝐵 · (;10↑2)) + ;𝐶𝐷) = ;;;𝐴𝐵𝐶𝐷 |
122 | 114 | oveq2i 7266 |
. . . . . . . . . . 11
⊢ (;𝐸𝐹 · (;10↑2)) = (;𝐸𝐹 · ;;100) |
123 | 9 | nn0cni 12175 |
. . . . . . . . . . . 12
⊢ ;𝐸𝐹 ∈ ℂ |
124 | 103, 123 | mulcomi 10914 |
. . . . . . . . . . 11
⊢ (;;100 · ;𝐸𝐹) = (;𝐸𝐹 · ;;100) |
125 | 122, 124 | eqtr4i 2769 |
. . . . . . . . . 10
⊢ (;𝐸𝐹 · (;10↑2)) = (;;100
· ;𝐸𝐹) |
126 | 125 | oveq1i 7265 |
. . . . . . . . 9
⊢ ((;𝐸𝐹 · (;10↑2)) + ;𝐺𝐻) = ((;;100
· ;𝐸𝐹) + ;𝐺𝐻) |
127 | 9, 10, 52 | dfdec100 31046 |
. . . . . . . . 9
⊢ ;;;𝐸𝐹𝐺𝐻 = ((;;100
· ;𝐸𝐹) + ;𝐺𝐻) |
128 | 126, 127 | eqtr4i 2769 |
. . . . . . . 8
⊢ ((;𝐸𝐹 · (;10↑2)) + ;𝐺𝐻) = ;;;𝐸𝐹𝐺𝐻 |
129 | 24 | sqvali 13825 |
. . . . . . . . . . . 12
⊢ (;10↑2) = (;10 · ;10) |
130 | 129 | oveq2i 7266 |
. . . . . . . . . . 11
⊢ (;;𝐼𝐽𝐾 · (;10↑2)) = (;;𝐼𝐽𝐾 · (;10 · ;10)) |
131 | 42, 36 | deccl 12381 |
. . . . . . . . . . . . 13
⊢ ;;𝐼𝐽𝐾 ∈ ℕ0 |
132 | 131 | nn0cni 12175 |
. . . . . . . . . . . 12
⊢ ;;𝐼𝐽𝐾 ∈ ℂ |
133 | 132, 24, 24 | mulassi 10917 |
. . . . . . . . . . 11
⊢ ((;;𝐼𝐽𝐾 · ;10) · ;10) = (;;𝐼𝐽𝐾 · (;10 · ;10)) |
134 | 130, 133 | eqtr4i 2769 |
. . . . . . . . . 10
⊢ (;;𝐼𝐽𝐾 · (;10↑2)) = ((;;𝐼𝐽𝐾 · ;10) · ;10) |
135 | | dpmul4.r |
. . . . . . . . . . . . . . . 16
⊢ 𝑅 ∈
ℕ0 |
136 | | dpmul4.s |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 ∈
ℕ0 |
137 | 135, 136 | deccl 12381 |
. . . . . . . . . . . . . . 15
⊢ ;𝑅𝑆 ∈ ℕ0 |
138 | | dpmul4.t |
. . . . . . . . . . . . . . 15
⊢ 𝑇 ∈
ℕ0 |
139 | 137, 138 | deccl 12381 |
. . . . . . . . . . . . . 14
⊢ ;;𝑅𝑆𝑇 ∈ ℕ0 |
140 | 139 | nn0cni 12175 |
. . . . . . . . . . . . 13
⊢ ;;𝑅𝑆𝑇 ∈ ℂ |
141 | | ax-1cn 10860 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
142 | 140, 141 | addcli 10912 |
. . . . . . . . . . . 12
⊢ (;;𝑅𝑆𝑇 + 1) ∈ ℂ |
143 | 132, 24 | mulcli 10913 |
. . . . . . . . . . . 12
⊢ (;;𝐼𝐽𝐾 · ;10) ∈ ℂ |
144 | 141, 143 | addcomi 11096 |
. . . . . . . . . . . . . . . 16
⊢ (1 +
(;;𝐼𝐽𝐾 · ;10)) = ((;;𝐼𝐽𝐾 · ;10) + 1) |
145 | 24, 132 | mulcomi 10914 |
. . . . . . . . . . . . . . . . . 18
⊢ (;10 · ;;𝐼𝐽𝐾) = (;;𝐼𝐽𝐾 · ;10) |
146 | 131 | dec0u 12387 |
. . . . . . . . . . . . . . . . . 18
⊢ (;10 · ;;𝐼𝐽𝐾) = ;;;𝐼𝐽𝐾0 |
147 | 145, 146 | eqtr3i 2768 |
. . . . . . . . . . . . . . . . 17
⊢ (;;𝐼𝐽𝐾 · ;10) = ;;;𝐼𝐽𝐾0 |
148 | 147 | oveq1i 7265 |
. . . . . . . . . . . . . . . 16
⊢ ((;;𝐼𝐽𝐾 · ;10) + 1) = (;;;𝐼𝐽𝐾0 + 1) |
149 | 141 | addid2i 11093 |
. . . . . . . . . . . . . . . . 17
⊢ (0 + 1) =
1 |
150 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ ;;;𝐼𝐽𝐾0 = ;;;𝐼𝐽𝐾0 |
151 | 131, 101,
149, 150 | decsuc 12397 |
. . . . . . . . . . . . . . . 16
⊢ (;;;𝐼𝐽𝐾0 + 1) = ;;;𝐼𝐽𝐾1 |
152 | 144, 148,
151 | 3eqtri 2770 |
. . . . . . . . . . . . . . 15
⊢ (1 +
(;;𝐼𝐽𝐾 · ;10)) = ;;;𝐼𝐽𝐾1 |
153 | 152 | oveq2i 7266 |
. . . . . . . . . . . . . 14
⊢ (;;𝑅𝑆𝑇 + (1 + (;;𝐼𝐽𝐾 · ;10))) = (;;𝑅𝑆𝑇 + ;;;𝐼𝐽𝐾1) |
154 | 140, 141,
143 | addassi 10916 |
. . . . . . . . . . . . . 14
⊢ ((;;𝑅𝑆𝑇 + 1) + (;;𝐼𝐽𝐾 · ;10)) = (;;𝑅𝑆𝑇 + (1 + (;;𝐼𝐽𝐾 · ;10))) |
155 | | 1nn0 12179 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℕ0 |
156 | 131, 155 | deccl 12381 |
. . . . . . . . . . . . . . . 16
⊢ ;;;𝐼𝐽𝐾1 ∈
ℕ0 |
157 | 156 | nn0cni 12175 |
. . . . . . . . . . . . . . 15
⊢ ;;;𝐼𝐽𝐾1 ∈ ℂ |
158 | 157, 140 | addcomi 11096 |
. . . . . . . . . . . . . 14
⊢ (;;;𝐼𝐽𝐾1 + ;;𝑅𝑆𝑇) = (;;𝑅𝑆𝑇 + ;;;𝐼𝐽𝐾1) |
159 | 153, 154,
158 | 3eqtr4i 2776 |
. . . . . . . . . . . . 13
⊢ ((;;𝑅𝑆𝑇 + 1) + (;;𝐼𝐽𝐾 · ;10)) = (;;;𝐼𝐽𝐾1 + ;;𝑅𝑆𝑇) |
160 | | dpmul4.4 |
. . . . . . . . . . . . 13
⊢ (;;;𝐼𝐽𝐾1 + ;;𝑅𝑆𝑇) = ;;;𝑊𝑋𝑌𝑍 |
161 | 159, 160 | eqtri 2766 |
. . . . . . . . . . . 12
⊢ ((;;𝑅𝑆𝑇 + 1) + (;;𝐼𝐽𝐾 · ;10)) = ;;;𝑊𝑋𝑌𝑍 |
162 | 142, 143,
161 | mvlladdi 11169 |
. . . . . . . . . . 11
⊢ (;;𝐼𝐽𝐾 · ;10) = (;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) |
163 | 162 | oveq1i 7265 |
. . . . . . . . . 10
⊢ ((;;𝐼𝐽𝐾 · ;10) · ;10) = ((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) |
164 | 134, 163 | eqtri 2766 |
. . . . . . . . 9
⊢ (;;𝐼𝐽𝐾 · (;10↑2)) = ((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) |
165 | 164 | oveq1i 7265 |
. . . . . . . 8
⊢ ((;;𝐼𝐽𝐾 · (;10↑2)) + ;;𝐿𝑀𝑁) = (((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) + ;;𝐿𝑀𝑁) |
166 | | eqid 2738 |
. . . . . . . 8
⊢
(((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) + ;;𝐿𝑀𝑁) · (;10↑2)) + ;;𝑂𝑃𝑄) = (((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) + ;;𝐿𝑀𝑁) · (;10↑2)) + ;;𝑂𝑃𝑄) |
167 | 3, 6, 9, 12, 17, 18, 47, 74, 113, 121, 128, 165, 166 | karatsuba 16713 |
. . . . . . 7
⊢ (;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) = (((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) + ;;𝐿𝑀𝑁) · (;10↑2)) + ;;𝑂𝑃𝑄) |
168 | | dpmul4.w |
. . . . . . . . . . . . . . 15
⊢ 𝑊 ∈
ℕ0 |
169 | | dpmul4.x |
. . . . . . . . . . . . . . 15
⊢ 𝑋 ∈
ℕ0 |
170 | 168, 169 | deccl 12381 |
. . . . . . . . . . . . . 14
⊢ ;𝑊𝑋 ∈ ℕ0 |
171 | | dpmul4.y |
. . . . . . . . . . . . . 14
⊢ 𝑌 ∈
ℕ0 |
172 | 170, 171 | deccl 12381 |
. . . . . . . . . . . . 13
⊢ ;;𝑊𝑋𝑌 ∈ ℕ0 |
173 | | dpmul4.z |
. . . . . . . . . . . . 13
⊢ 𝑍 ∈
ℕ0 |
174 | 172, 173 | deccl 12381 |
. . . . . . . . . . . 12
⊢ ;;;𝑊𝑋𝑌𝑍 ∈ ℕ0 |
175 | 174 | nn0cni 12175 |
. . . . . . . . . . 11
⊢ ;;;𝑊𝑋𝑌𝑍 ∈ ℂ |
176 | 102, 101 | deccl 12381 |
. . . . . . . . . . . 12
⊢ ;;;1000
∈ ℕ0 |
177 | 176 | nn0cni 12175 |
. . . . . . . . . . 11
⊢ ;;;1000
∈ ℂ |
178 | 175, 177 | mulcli 10913 |
. . . . . . . . . 10
⊢ (;;;𝑊𝑋𝑌𝑍 · ;;;1000) ∈ ℂ |
179 | 142, 177 | mulcli 10913 |
. . . . . . . . . 10
⊢ ((;;𝑅𝑆𝑇 + 1) · ;;;1000) ∈ ℂ |
180 | 178, 179 | subcli 11227 |
. . . . . . . . 9
⊢ ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − ((;;𝑅𝑆𝑇 + 1) · ;;;1000)) ∈ ℂ |
181 | 17 | nn0cni 12175 |
. . . . . . . . . 10
⊢ ;;𝐿𝑀𝑁 ∈ ℂ |
182 | 103, 181 | mulcli 10913 |
. . . . . . . . 9
⊢ (;;100 · ;;𝐿𝑀𝑁) ∈ ℂ |
183 | 61, 62, 64 | dfdec100 31046 |
. . . . . . . . . 10
⊢ ;;𝑂𝑃𝑄 = ((;;100
· 𝑂) + ;𝑃𝑄) |
184 | 69, 63 | deccl 12381 |
. . . . . . . . . . 11
⊢ ;;𝑂𝑃𝑄 ∈ ℕ0 |
185 | 184 | nn0cni 12175 |
. . . . . . . . . 10
⊢ ;;𝑂𝑃𝑄 ∈ ℂ |
186 | 183, 185 | eqeltrri 2836 |
. . . . . . . . 9
⊢ ((;;100 · 𝑂) + ;𝑃𝑄) ∈ ℂ |
187 | 180, 182,
186 | addassi 10916 |
. . . . . . . 8
⊢ ((((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − ((;;𝑅𝑆𝑇 + 1) · ;;;1000)) + (;;100
· ;;𝐿𝑀𝑁)) + ((;;100
· 𝑂) + ;𝑃𝑄)) = (((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − ((;;𝑅𝑆𝑇 + 1) · ;;;1000)) + ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄))) |
188 | 24 | sqcli 13826 |
. . . . . . . . . . . . 13
⊢ (;10↑2) ∈
ℂ |
189 | 132, 188 | mulcli 10913 |
. . . . . . . . . . . 12
⊢ (;;𝐼𝐽𝐾 · (;10↑2)) ∈ ℂ |
190 | 164, 189 | eqeltrri 2836 |
. . . . . . . . . . 11
⊢ ((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) ∈ ℂ |
191 | 190, 181,
103 | adddiri 10919 |
. . . . . . . . . 10
⊢ ((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) + ;;𝐿𝑀𝑁) · ;;100) =
((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) · ;;100) +
(;;𝐿𝑀𝑁 · ;;100)) |
192 | 114 | oveq2i 7266 |
. . . . . . . . . 10
⊢ ((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) + ;;𝐿𝑀𝑁) · (;10↑2)) = ((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) + ;;𝐿𝑀𝑁) · ;;100) |
193 | 175, 142 | subcli 11227 |
. . . . . . . . . . . . 13
⊢ (;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) ∈ ℂ |
194 | 193, 24, 103 | mulassi 10917 |
. . . . . . . . . . . 12
⊢ (((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) · ;;100) =
((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · (;10 · ;;100)) |
195 | 102 | dec0u 12387 |
. . . . . . . . . . . . 13
⊢ (;10 · ;;100) =
;;;1000 |
196 | 195 | oveq2i 7266 |
. . . . . . . . . . . 12
⊢ ((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · (;10 · ;;100))
= ((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;;;1000) |
197 | 175, 142,
177 | subdiri 11355 |
. . . . . . . . . . . 12
⊢ ((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;;;1000) = ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − ((;;𝑅𝑆𝑇 + 1) · ;;;1000)) |
198 | 194, 196,
197 | 3eqtrri 2771 |
. . . . . . . . . . 11
⊢ ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − ((;;𝑅𝑆𝑇 + 1) · ;;;1000)) = (((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) · ;;100) |
199 | 103, 181 | mulcomi 10914 |
. . . . . . . . . . 11
⊢ (;;100 · ;;𝐿𝑀𝑁) = (;;𝐿𝑀𝑁 · ;;100) |
200 | 198, 199 | oveq12i 7267 |
. . . . . . . . . 10
⊢ (((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − ((;;𝑅𝑆𝑇 + 1) · ;;;1000)) + (;;100
· ;;𝐿𝑀𝑁)) = ((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) · ;;100) +
(;;𝐿𝑀𝑁 · ;;100)) |
201 | 191, 192,
200 | 3eqtr4i 2776 |
. . . . . . . . 9
⊢ ((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) + ;;𝐿𝑀𝑁) · (;10↑2)) = (((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − ((;;𝑅𝑆𝑇 + 1) · ;;;1000)) + (;;100
· ;;𝐿𝑀𝑁)) |
202 | 201, 183 | oveq12i 7267 |
. . . . . . . 8
⊢
(((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) + ;;𝐿𝑀𝑁) · (;10↑2)) + ;;𝑂𝑃𝑄) = ((((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − ((;;𝑅𝑆𝑇 + 1) · ;;;1000)) + (;;100
· ;;𝐿𝑀𝑁)) + ((;;100
· 𝑂) + ;𝑃𝑄)) |
203 | 182, 186 | addcli 10912 |
. . . . . . . . 9
⊢ ((;;100 · ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)) ∈ ℂ |
204 | | subsub 11181 |
. . . . . . . . 9
⊢ (((;;;𝑊𝑋𝑌𝑍 · ;;;1000) ∈ ℂ ∧ ((;;𝑅𝑆𝑇 + 1) · ;;;1000) ∈ ℂ ∧ ((;;100 · ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)) ∈ ℂ) → ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)))) = (((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − ((;;𝑅𝑆𝑇 + 1) · ;;;1000)) + ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)))) |
205 | 178, 179,
203, 204 | mp3an 1459 |
. . . . . . . 8
⊢ ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)))) = (((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − ((;;𝑅𝑆𝑇 + 1) · ;;;1000)) + ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄))) |
206 | 187, 202,
205 | 3eqtr4ri 2777 |
. . . . . . 7
⊢ ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)))) = (((((;;;𝑊𝑋𝑌𝑍 − (;;𝑅𝑆𝑇 + 1)) · ;10) + ;;𝐿𝑀𝑁) · (;10↑2)) + ;;𝑂𝑃𝑄) |
207 | 167, 206 | eqtr4i 2769 |
. . . . . 6
⊢ (;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) = ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)))) |
208 | 174 | nn0rei 12174 |
. . . . . . . 8
⊢ ;;;𝑊𝑋𝑌𝑍 ∈ ℝ |
209 | 176 | nn0rei 12174 |
. . . . . . . 8
⊢ ;;;1000
∈ ℝ |
210 | 208, 209 | remulcli 10922 |
. . . . . . 7
⊢ (;;;𝑊𝑋𝑌𝑍 · ;;;1000) ∈ ℝ |
211 | 139 | nn0rei 12174 |
. . . . . . . . . . 11
⊢ ;;𝑅𝑆𝑇 ∈ ℝ |
212 | | 1re 10906 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
213 | 211, 212 | readdcli 10921 |
. . . . . . . . . 10
⊢ (;;𝑅𝑆𝑇 + 1) ∈ ℝ |
214 | 213, 209 | remulcli 10922 |
. . . . . . . . 9
⊢ ((;;𝑅𝑆𝑇 + 1) · ;;;1000) ∈ ℝ |
215 | 102 | nn0rei 12174 |
. . . . . . . . . . 11
⊢ ;;100 ∈ ℝ |
216 | 17 | nn0rei 12174 |
. . . . . . . . . . 11
⊢ ;;𝐿𝑀𝑁 ∈ ℝ |
217 | 215, 216 | remulcli 10922 |
. . . . . . . . . 10
⊢ (;;100 · ;;𝐿𝑀𝑁) ∈ ℝ |
218 | 61 | nn0rei 12174 |
. . . . . . . . . . . 12
⊢ 𝑂 ∈ ℝ |
219 | 215, 218 | remulcli 10922 |
. . . . . . . . . . 11
⊢ (;;100 · 𝑂) ∈ ℝ |
220 | 62, 63 | deccl 12381 |
. . . . . . . . . . . 12
⊢ ;𝑃𝑄 ∈ ℕ0 |
221 | 220 | nn0rei 12174 |
. . . . . . . . . . 11
⊢ ;𝑃𝑄 ∈ ℝ |
222 | 219, 221 | readdcli 10921 |
. . . . . . . . . 10
⊢ ((;;100 · 𝑂) + ;𝑃𝑄) ∈ ℝ |
223 | 217, 222 | readdcli 10921 |
. . . . . . . . 9
⊢ ((;;100 · ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)) ∈ ℝ |
224 | 214, 223 | resubcli 11213 |
. . . . . . . 8
⊢ (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄))) ∈ ℝ |
225 | 219 | recni 10920 |
. . . . . . . . . . . 12
⊢ (;;100 · 𝑂) ∈ ℂ |
226 | 221 | recni 10920 |
. . . . . . . . . . . 12
⊢ ;𝑃𝑄 ∈ ℂ |
227 | 182, 225,
226 | addassi 10916 |
. . . . . . . . . . 11
⊢ (((;;100 · ;;𝐿𝑀𝑁) + (;;100
· 𝑂)) + ;𝑃𝑄) = ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)) |
228 | 218 | recni 10920 |
. . . . . . . . . . . . . 14
⊢ 𝑂 ∈ ℂ |
229 | 103, 181,
228 | adddii 10918 |
. . . . . . . . . . . . 13
⊢ (;;100 · (;;𝐿𝑀𝑁 + 𝑂)) = ((;;100
· ;;𝐿𝑀𝑁) + (;;100
· 𝑂)) |
230 | | dpmul4.1 |
. . . . . . . . . . . . . 14
⊢ (;;𝐿𝑀𝑁 + 𝑂) = ;;;𝑅𝑆𝑇𝑈 |
231 | 230 | oveq2i 7266 |
. . . . . . . . . . . . 13
⊢ (;;100 · (;;𝐿𝑀𝑁 + 𝑂)) = (;;100
· ;;;𝑅𝑆𝑇𝑈) |
232 | 229, 231 | eqtr3i 2768 |
. . . . . . . . . . . 12
⊢ ((;;100 · ;;𝐿𝑀𝑁) + (;;100
· 𝑂)) = (;;100 · ;;;𝑅𝑆𝑇𝑈) |
233 | 232 | oveq1i 7265 |
. . . . . . . . . . 11
⊢ (((;;100 · ;;𝐿𝑀𝑁) + (;;100
· 𝑂)) + ;𝑃𝑄) = ((;;100
· ;;;𝑅𝑆𝑇𝑈) + ;𝑃𝑄) |
234 | 227, 233 | eqtr3i 2768 |
. . . . . . . . . 10
⊢ ((;;100 · ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)) = ((;;100
· ;;;𝑅𝑆𝑇𝑈) + ;𝑃𝑄) |
235 | | dpmul4.u |
. . . . . . . . . . . . 13
⊢ 𝑈 ∈
ℕ0 |
236 | | dpmul4.a |
. . . . . . . . . . . . 13
⊢ 𝑈 < ;10 |
237 | | dpmul4.b |
. . . . . . . . . . . . 13
⊢ 𝑃 < ;10 |
238 | | dpmul4.c |
. . . . . . . . . . . . 13
⊢ 𝑄 < ;10 |
239 | 235, 88, 62, 101, 63, 101, 236, 237, 238 | 3decltc 12399 |
. . . . . . . . . . . 12
⊢ ;;𝑈𝑃𝑄 < ;;;1000 |
240 | 235, 62 | deccl 12381 |
. . . . . . . . . . . . . . 15
⊢ ;𝑈𝑃 ∈ ℕ0 |
241 | 240, 63 | deccl 12381 |
. . . . . . . . . . . . . 14
⊢ ;;𝑈𝑃𝑄 ∈ ℕ0 |
242 | 241 | nn0rei 12174 |
. . . . . . . . . . . . 13
⊢ ;;𝑈𝑃𝑄 ∈ ℝ |
243 | 211, 209 | remulcli 10922 |
. . . . . . . . . . . . 13
⊢ (;;𝑅𝑆𝑇 · ;;;1000) ∈ ℝ |
244 | 242, 209,
243 | ltadd2i 11036 |
. . . . . . . . . . . 12
⊢ (;;𝑈𝑃𝑄 < ;;;1000 ↔ ((;;𝑅𝑆𝑇 · ;;;1000) + ;;𝑈𝑃𝑄) < ((;;𝑅𝑆𝑇 · ;;;1000) + ;;;1000)) |
245 | 239, 244 | mpbi 229 |
. . . . . . . . . . 11
⊢ ((;;𝑅𝑆𝑇 · ;;;1000) + ;;𝑈𝑃𝑄) < ((;;𝑅𝑆𝑇 · ;;;1000) + ;;;1000) |
246 | 140, 177 | mulcli 10913 |
. . . . . . . . . . . . 13
⊢ (;;𝑅𝑆𝑇 · ;;;1000) ∈ ℂ |
247 | 235 | nn0cni 12175 |
. . . . . . . . . . . . . 14
⊢ 𝑈 ∈ ℂ |
248 | 103, 247 | mulcli 10913 |
. . . . . . . . . . . . 13
⊢ (;;100 · 𝑈) ∈ ℂ |
249 | 246, 248,
226 | addassi 10916 |
. . . . . . . . . . . 12
⊢ (((;;𝑅𝑆𝑇 · ;;;1000) + (;;100
· 𝑈)) + ;𝑃𝑄) = ((;;𝑅𝑆𝑇 · ;;;1000) + ((;;100
· 𝑈) + ;𝑃𝑄)) |
250 | | dfdec10 12369 |
. . . . . . . . . . . . . . 15
⊢ ;;;𝑅𝑆𝑇𝑈 = ((;10 · ;;𝑅𝑆𝑇) + 𝑈) |
251 | 250 | oveq2i 7266 |
. . . . . . . . . . . . . 14
⊢ (;;100 · ;;;𝑅𝑆𝑇𝑈) = (;;100
· ((;10 · ;;𝑅𝑆𝑇) + 𝑈)) |
252 | 24, 140 | mulcli 10913 |
. . . . . . . . . . . . . . 15
⊢ (;10 · ;;𝑅𝑆𝑇) ∈ ℂ |
253 | 103, 252,
247 | adddii 10918 |
. . . . . . . . . . . . . 14
⊢ (;;100 · ((;10 · ;;𝑅𝑆𝑇) + 𝑈)) = ((;;100
· (;10 · ;;𝑅𝑆𝑇)) + (;;100
· 𝑈)) |
254 | 140, 177 | mulcomi 10914 |
. . . . . . . . . . . . . . . 16
⊢ (;;𝑅𝑆𝑇 · ;;;1000) = (;;;1000 · ;;𝑅𝑆𝑇) |
255 | 24, 103 | mulcomi 10914 |
. . . . . . . . . . . . . . . . . 18
⊢ (;10 · ;;100) =
(;;100 · ;10) |
256 | 255, 195 | eqtr3i 2768 |
. . . . . . . . . . . . . . . . 17
⊢ (;;100 · ;10) = ;;;1000 |
257 | 256 | oveq1i 7265 |
. . . . . . . . . . . . . . . 16
⊢ ((;;100 · ;10) · ;;𝑅𝑆𝑇) = (;;;1000 · ;;𝑅𝑆𝑇) |
258 | 103, 24, 140 | mulassi 10917 |
. . . . . . . . . . . . . . . 16
⊢ ((;;100 · ;10) · ;;𝑅𝑆𝑇) = (;;100
· (;10 · ;;𝑅𝑆𝑇)) |
259 | 254, 257,
258 | 3eqtr2ri 2773 |
. . . . . . . . . . . . . . 15
⊢ (;;100 · (;10 · ;;𝑅𝑆𝑇)) = (;;𝑅𝑆𝑇 · ;;;1000) |
260 | 259 | oveq1i 7265 |
. . . . . . . . . . . . . 14
⊢ ((;;100 · (;10 · ;;𝑅𝑆𝑇)) + (;;100
· 𝑈)) = ((;;𝑅𝑆𝑇 · ;;;1000) + (;;100
· 𝑈)) |
261 | 251, 253,
260 | 3eqtri 2770 |
. . . . . . . . . . . . 13
⊢ (;;100 · ;;;𝑅𝑆𝑇𝑈) = ((;;𝑅𝑆𝑇 · ;;;1000) + (;;100
· 𝑈)) |
262 | 261 | oveq1i 7265 |
. . . . . . . . . . . 12
⊢ ((;;100 · ;;;𝑅𝑆𝑇𝑈) + ;𝑃𝑄) = (((;;𝑅𝑆𝑇 · ;;;1000) + (;;100
· 𝑈)) + ;𝑃𝑄) |
263 | 235, 62, 64 | dfdec100 31046 |
. . . . . . . . . . . . 13
⊢ ;;𝑈𝑃𝑄 = ((;;100
· 𝑈) + ;𝑃𝑄) |
264 | 263 | oveq2i 7266 |
. . . . . . . . . . . 12
⊢ ((;;𝑅𝑆𝑇 · ;;;1000) + ;;𝑈𝑃𝑄) = ((;;𝑅𝑆𝑇 · ;;;1000) + ((;;100
· 𝑈) + ;𝑃𝑄)) |
265 | 249, 262,
264 | 3eqtr4i 2776 |
. . . . . . . . . . 11
⊢ ((;;100 · ;;;𝑅𝑆𝑇𝑈) + ;𝑃𝑄) = ((;;𝑅𝑆𝑇 · ;;;1000) + ;;𝑈𝑃𝑄) |
266 | 140, 141,
177 | adddiri 10919 |
. . . . . . . . . . . 12
⊢ ((;;𝑅𝑆𝑇 + 1) · ;;;1000) = ((;;𝑅𝑆𝑇 · ;;;1000) + (1 · ;;;1000)) |
267 | 177 | mulid2i 10911 |
. . . . . . . . . . . . 13
⊢ (1
· ;;;1000)
= ;;;1000 |
268 | 267 | oveq2i 7266 |
. . . . . . . . . . . 12
⊢ ((;;𝑅𝑆𝑇 · ;;;1000) + (1 · ;;;1000)) = ((;;𝑅𝑆𝑇 · ;;;1000) + ;;;1000) |
269 | 266, 268 | eqtri 2766 |
. . . . . . . . . . 11
⊢ ((;;𝑅𝑆𝑇 + 1) · ;;;1000) = ((;;𝑅𝑆𝑇 · ;;;1000) + ;;;1000) |
270 | 245, 265,
269 | 3brtr4i 5100 |
. . . . . . . . . 10
⊢ ((;;100 · ;;;𝑅𝑆𝑇𝑈) + ;𝑃𝑄) < ((;;𝑅𝑆𝑇 + 1) · ;;;1000) |
271 | 234, 270 | eqbrtri 5091 |
. . . . . . . . 9
⊢ ((;;100 · ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)) < ((;;𝑅𝑆𝑇 + 1) · ;;;1000) |
272 | 223, 214 | posdifi 11455 |
. . . . . . . . 9
⊢ (((;;100 · ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)) < ((;;𝑅𝑆𝑇 + 1) · ;;;1000) ↔ 0 < (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)))) |
273 | 271, 272 | mpbi 229 |
. . . . . . . 8
⊢ 0 <
(((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄))) |
274 | | elrp 12661 |
. . . . . . . 8
⊢ ((((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄))) ∈ ℝ+ ↔
((((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄))) ∈ ℝ ∧ 0 < (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄))))) |
275 | 224, 273,
274 | mpbir2an 707 |
. . . . . . 7
⊢ (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄))) ∈
ℝ+ |
276 | | ltsubrp 12695 |
. . . . . . 7
⊢ (((;;;𝑊𝑋𝑌𝑍 · ;;;1000) ∈ ℝ ∧ (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄))) ∈ ℝ+) →
((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)))) < (;;;𝑊𝑋𝑌𝑍 · ;;;1000)) |
277 | 210, 275,
276 | mp2an 688 |
. . . . . 6
⊢ ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) − (((;;𝑅𝑆𝑇 + 1) · ;;;1000) − ((;;100
· ;;𝐿𝑀𝑁) + ((;;100
· 𝑂) + ;𝑃𝑄)))) < (;;;𝑊𝑋𝑌𝑍 · ;;;1000) |
278 | 207, 277 | eqbrtri 5091 |
. . . . 5
⊢ (;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) < (;;;𝑊𝑋𝑌𝑍 · ;;;1000) |
279 | 3, 4 | deccl 12381 |
. . . . . . . . 9
⊢ ;;𝐴𝐵𝐶 ∈ ℕ0 |
280 | 279, 5 | deccl 12381 |
. . . . . . . 8
⊢ ;;;𝐴𝐵𝐶𝐷 ∈ ℕ0 |
281 | 280 | nn0rei 12174 |
. . . . . . 7
⊢ ;;;𝐴𝐵𝐶𝐷 ∈ ℝ |
282 | 9, 10 | deccl 12381 |
. . . . . . . . 9
⊢ ;;𝐸𝐹𝐺 ∈ ℕ0 |
283 | 282, 11 | deccl 12381 |
. . . . . . . 8
⊢ ;;;𝐸𝐹𝐺𝐻 ∈ ℕ0 |
284 | 283 | nn0rei 12174 |
. . . . . . 7
⊢ ;;;𝐸𝐹𝐺𝐻 ∈ ℝ |
285 | 281, 284 | remulcli 10922 |
. . . . . 6
⊢ (;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) ∈ ℝ |
286 | 23 | decnncl2 12390 |
. . . . . . . . 9
⊢ ;;100 ∈ ℕ |
287 | 286 | decnncl2 12390 |
. . . . . . . 8
⊢ ;;;1000
∈ ℕ |
288 | 287 | nngt0i 11942 |
. . . . . . 7
⊢ 0 <
;;;1000 |
289 | 209, 288 | pm3.2i 470 |
. . . . . 6
⊢ (;;;1000
∈ ℝ ∧ 0 < ;;;1000) |
290 | | ltdiv1 11769 |
. . . . . 6
⊢ (((;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) ∈ ℝ ∧ (;;;𝑊𝑋𝑌𝑍 · ;;;1000) ∈ ℝ ∧ (;;;1000
∈ ℝ ∧ 0 < ;;;1000)) → ((;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) < (;;;𝑊𝑋𝑌𝑍 · ;;;1000) ↔ ((;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) / ;;;1000) < ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) / ;;;1000))) |
291 | 285, 210,
289, 290 | mp3an 1459 |
. . . . 5
⊢ ((;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) < (;;;𝑊𝑋𝑌𝑍 · ;;;1000) ↔ ((;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) / ;;;1000) < ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) / ;;;1000)) |
292 | 278, 291 | mpbi 229 |
. . . 4
⊢ ((;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) / ;;;1000) < ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) / ;;;1000) |
293 | 280 | nn0cni 12175 |
. . . . . 6
⊢ ;;;𝐴𝐵𝐶𝐷 ∈ ℂ |
294 | 283 | nn0cni 12175 |
. . . . . 6
⊢ ;;;𝐸𝐹𝐺𝐻 ∈ ℂ |
295 | 209, 288 | gt0ne0ii 11441 |
. . . . . 6
⊢ ;;;1000
≠ 0 |
296 | 293, 294,
177, 295 | div23i 11663 |
. . . . 5
⊢ ((;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) / ;;;1000) = ((;;;𝐴𝐵𝐶𝐷 / ;;;1000) · ;;;𝐸𝐹𝐺𝐻) |
297 | 1, 2, 4, 48 | dpmul1000 31075 |
. . . . . . . 8
⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;1000) = ;;;𝐴𝐵𝐶𝐷 |
298 | 297 | oveq1i 7265 |
. . . . . . 7
⊢ (((𝐴._𝐵_𝐶𝐷) · ;;;1000) / ;;;1000) = (;;;𝐴𝐵𝐶𝐷 / ;;;1000) |
299 | 4 | nn0rei 12174 |
. . . . . . . . . . . 12
⊢ 𝐶 ∈ ℝ |
300 | | dp2cl 31056 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → _𝐶𝐷 ∈ ℝ) |
301 | 299, 48, 300 | mp2an 688 |
. . . . . . . . . . 11
⊢ _𝐶𝐷 ∈ ℝ |
302 | | dp2cl 31056 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ _𝐶𝐷 ∈ ℝ) → _𝐵_𝐶𝐷 ∈ ℝ) |
303 | 19, 301, 302 | mp2an 688 |
. . . . . . . . . 10
⊢ _𝐵_𝐶𝐷 ∈ ℝ |
304 | | dpcl 31067 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ _𝐵_𝐶𝐷 ∈ ℝ) → (𝐴._𝐵_𝐶𝐷) ∈ ℝ) |
305 | 1, 303, 304 | mp2an 688 |
. . . . . . . . 9
⊢ (𝐴._𝐵_𝐶𝐷) ∈ ℝ |
306 | 305 | recni 10920 |
. . . . . . . 8
⊢ (𝐴._𝐵_𝐶𝐷) ∈ ℂ |
307 | 306, 177,
295 | divcan4i 11652 |
. . . . . . 7
⊢ (((𝐴._𝐵_𝐶𝐷) · ;;;1000) / ;;;1000) = (𝐴._𝐵_𝐶𝐷) |
308 | 298, 307 | eqtr3i 2768 |
. . . . . 6
⊢ (;;;𝐴𝐵𝐶𝐷 / ;;;1000) = (𝐴._𝐵_𝐶𝐷) |
309 | 308 | oveq1i 7265 |
. . . . 5
⊢ ((;;;𝐴𝐵𝐶𝐷 / ;;;1000) · ;;;𝐸𝐹𝐺𝐻) = ((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) |
310 | 296, 309 | eqtri 2766 |
. . . 4
⊢ ((;;;𝐴𝐵𝐶𝐷 · ;;;𝐸𝐹𝐺𝐻) / ;;;1000) = ((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) |
311 | 175, 177,
295 | divcan4i 11652 |
. . . 4
⊢ ((;;;𝑊𝑋𝑌𝑍 · ;;;1000) / ;;;1000) = ;;;𝑊𝑋𝑌𝑍 |
312 | 292, 310,
311 | 3brtr3i 5099 |
. . 3
⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) < ;;;𝑊𝑋𝑌𝑍 |
313 | 305, 284 | remulcli 10922 |
. . . 4
⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) ∈ ℝ |
314 | | ltdiv1 11769 |
. . . 4
⊢ ((((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) ∈ ℝ ∧ ;;;𝑊𝑋𝑌𝑍 ∈ ℝ ∧ (;;;1000 ∈ ℝ ∧ 0 < ;;;1000))
→ (((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) < ;;;𝑊𝑋𝑌𝑍 ↔ (((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) / ;;;1000) < (;;;𝑊𝑋𝑌𝑍 / ;;;1000))) |
315 | 313, 208,
289, 314 | mp3an 1459 |
. . 3
⊢ (((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) < ;;;𝑊𝑋𝑌𝑍 ↔ (((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) / ;;;1000) < (;;;𝑊𝑋𝑌𝑍 / ;;;1000)) |
316 | 312, 315 | mpbi 229 |
. 2
⊢ (((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) / ;;;1000) < (;;;𝑊𝑋𝑌𝑍 / ;;;1000) |
317 | 306, 294,
177, 295 | divassi 11661 |
. . 3
⊢ (((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) / ;;;1000) = ((𝐴._𝐵_𝐶𝐷) · (;;;𝐸𝐹𝐺𝐻 / ;;;1000)) |
318 | 7, 8, 10, 52 | dpmul1000 31075 |
. . . . . 6
⊢ ((𝐸._𝐹_𝐺𝐻) · ;;;1000) = ;;;𝐸𝐹𝐺𝐻 |
319 | 318 | oveq1i 7265 |
. . . . 5
⊢ (((𝐸._𝐹_𝐺𝐻) · ;;;1000) / ;;;1000) = (;;;𝐸𝐹𝐺𝐻 / ;;;1000) |
320 | 10 | nn0rei 12174 |
. . . . . . . . . 10
⊢ 𝐺 ∈ ℝ |
321 | | dp2cl 31056 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ ℝ ∧ 𝐻 ∈ ℝ) → _𝐺𝐻 ∈ ℝ) |
322 | 320, 52, 321 | mp2an 688 |
. . . . . . . . 9
⊢ _𝐺𝐻 ∈ ℝ |
323 | | dp2cl 31056 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ℝ ∧ _𝐺𝐻 ∈ ℝ) → _𝐹_𝐺𝐻 ∈ ℝ) |
324 | 25, 322, 323 | mp2an 688 |
. . . . . . . 8
⊢ _𝐹_𝐺𝐻 ∈ ℝ |
325 | | dpcl 31067 |
. . . . . . . 8
⊢ ((𝐸 ∈ ℕ0
∧ _𝐹_𝐺𝐻 ∈ ℝ) → (𝐸._𝐹_𝐺𝐻) ∈ ℝ) |
326 | 7, 324, 325 | mp2an 688 |
. . . . . . 7
⊢ (𝐸._𝐹_𝐺𝐻) ∈ ℝ |
327 | 326 | recni 10920 |
. . . . . 6
⊢ (𝐸._𝐹_𝐺𝐻) ∈ ℂ |
328 | 327, 177,
295 | divcan4i 11652 |
. . . . 5
⊢ (((𝐸._𝐹_𝐺𝐻) · ;;;1000) / ;;;1000) = (𝐸._𝐹_𝐺𝐻) |
329 | 319, 328 | eqtr3i 2768 |
. . . 4
⊢ (;;;𝐸𝐹𝐺𝐻 / ;;;1000) = (𝐸._𝐹_𝐺𝐻) |
330 | 329 | oveq2i 7266 |
. . 3
⊢ ((𝐴._𝐵_𝐶𝐷) · (;;;𝐸𝐹𝐺𝐻 / ;;;1000)) = ((𝐴._𝐵_𝐶𝐷) · (𝐸._𝐹_𝐺𝐻)) |
331 | 317, 330 | eqtri 2766 |
. 2
⊢ (((𝐴._𝐵_𝐶𝐷) · ;;;𝐸𝐹𝐺𝐻) / ;;;1000) = ((𝐴._𝐵_𝐶𝐷) · (𝐸._𝐹_𝐺𝐻)) |
332 | 173 | nn0rei 12174 |
. . . . 5
⊢ 𝑍 ∈ ℝ |
333 | 168, 169,
171, 332 | dpmul1000 31075 |
. . . 4
⊢ ((𝑊._𝑋_𝑌𝑍) · ;;;1000) = ;;;𝑊𝑋𝑌𝑍 |
334 | 333 | oveq1i 7265 |
. . 3
⊢ (((𝑊._𝑋_𝑌𝑍) · ;;;1000) / ;;;1000) = (;;;𝑊𝑋𝑌𝑍 / ;;;1000) |
335 | 169 | nn0rei 12174 |
. . . . . . 7
⊢ 𝑋 ∈ ℝ |
336 | 171 | nn0rei 12174 |
. . . . . . . 8
⊢ 𝑌 ∈ ℝ |
337 | | dp2cl 31056 |
. . . . . . . 8
⊢ ((𝑌 ∈ ℝ ∧ 𝑍 ∈ ℝ) → _𝑌𝑍 ∈ ℝ) |
338 | 336, 332,
337 | mp2an 688 |
. . . . . . 7
⊢ _𝑌𝑍 ∈ ℝ |
339 | | dp2cl 31056 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ _𝑌𝑍 ∈ ℝ) → _𝑋_𝑌𝑍 ∈ ℝ) |
340 | 335, 338,
339 | mp2an 688 |
. . . . . 6
⊢ _𝑋_𝑌𝑍 ∈ ℝ |
341 | | dpcl 31067 |
. . . . . 6
⊢ ((𝑊 ∈ ℕ0
∧ _𝑋_𝑌𝑍 ∈ ℝ) → (𝑊._𝑋_𝑌𝑍) ∈ ℝ) |
342 | 168, 340,
341 | mp2an 688 |
. . . . 5
⊢ (𝑊._𝑋_𝑌𝑍) ∈ ℝ |
343 | 342 | recni 10920 |
. . . 4
⊢ (𝑊._𝑋_𝑌𝑍) ∈ ℂ |
344 | 343, 177,
295 | divcan4i 11652 |
. . 3
⊢ (((𝑊._𝑋_𝑌𝑍) · ;;;1000) / ;;;1000) = (𝑊._𝑋_𝑌𝑍) |
345 | 334, 344 | eqtr3i 2768 |
. 2
⊢ (;;;𝑊𝑋𝑌𝑍 / ;;;1000) = (𝑊._𝑋_𝑌𝑍) |
346 | 316, 331,
345 | 3brtr3i 5099 |
1
⊢ ((𝐴._𝐵_𝐶𝐷) · (𝐸._𝐹_𝐺𝐻)) < (𝑊._𝑋_𝑌𝑍) |