dpadd2 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dpadd2		Structured version Visualization version GIF version

Theorem dpadd2 33458

Description: Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.)

**Hypotheses**
Ref	Expression
dpadd2.a	⊢ 𝐴 ∈ ℕ₀
dpadd2.b	⊢ 𝐵 ∈ ℝ⁺
dpadd2.c	⊢ 𝐶 ∈ ℕ₀
dpadd2.d	⊢ 𝐷 ∈ ℝ⁺
dpadd2.e	⊢ 𝐸 ∈ ℕ₀
dpadd2.f	⊢ 𝐹 ∈ ℝ⁺
dpadd2.g	⊢ 𝐺 ∈ ℕ₀
dpadd2.h	⊢ 𝐻 ∈ ℕ₀
dpadd2.i	⊢ (𝐺 + 𝐻) = 𝐼
dpadd2.1	⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)

**Assertion**
Ref	Expression
dpadd2	⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹)

**Proof of Theorem dpadd2**
Step	Hyp	Ref	Expression
1		dpadd2.g	. . . 4 ⊢ 𝐺 ∈ ℕ₀
2		dpadd2.a	. . . . . 6 ⊢ 𝐴 ∈ ℕ₀
3	2	nn0rei 12598	. . . . 5 ⊢ 𝐴 ∈ ℝ
4		dpadd2.b	. . . . . 6 ⊢ 𝐵 ∈ ℝ⁺
5		rpre 13110	. . . . . 6 ⊢ (𝐵 ∈ ℝ⁺ → 𝐵 ∈ ℝ)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 𝐵 ∈ ℝ
7		dp2cl 33428	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → _𝐴𝐵 ∈ ℝ)
8	3, 6, 7	mp2an 705	. . . 4 ⊢ _𝐴𝐵 ∈ ℝ
9	1, 8	dpval2 33441	. . 3 ⊢ (𝐺._𝐴𝐵) = (𝐺 + (_𝐴𝐵 / ;10))
10		dpadd2.h	. . . 4 ⊢ 𝐻 ∈ ℕ₀
11		dpadd2.c	. . . . . 6 ⊢ 𝐶 ∈ ℕ₀
12	11	nn0rei 12598	. . . . 5 ⊢ 𝐶 ∈ ℝ
13		dpadd2.d	. . . . . 6 ⊢ 𝐷 ∈ ℝ⁺
14		rpre 13110	. . . . . 6 ⊢ (𝐷 ∈ ℝ⁺ → 𝐷 ∈ ℝ)
15	13, 14	ax-mp 5	. . . . 5 ⊢ 𝐷 ∈ ℝ
16		dp2cl 33428	. . . . 5 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → _𝐶𝐷 ∈ ℝ)
17	12, 15, 16	mp2an 705	. . . 4 ⊢ _𝐶𝐷 ∈ ℝ
18	10, 17	dpval2 33441	. . 3 ⊢ (𝐻._𝐶𝐷) = (𝐻 + (_𝐶𝐷 / ;10))
19	9, 18	oveq12i 7424	. 2 ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = ((𝐺 + (_𝐴𝐵 / ;10)) + (𝐻 + (_𝐶𝐷 / ;10)))
20	1	nn0cni 12599	. . 3 ⊢ 𝐺 ∈ ℂ
21	8	recni 11304	. . . 4 ⊢ _𝐴𝐵 ∈ ℂ
22		10nn 12815	. . . . 5 ⊢ ;10 ∈ ℕ
23	22	nncni 12326	. . . 4 ⊢ ;10 ∈ ℂ
24	22	nnne0i 12359	. . . 4 ⊢ ;10 ≠ 0
25	21, 23, 24	divcli 12040	. . 3 ⊢ (_𝐴𝐵 / ;10) ∈ ℂ
26	10	nn0cni 12599	. . 3 ⊢ 𝐻 ∈ ℂ
27	17	recni 11304	. . . 4 ⊢ _𝐶𝐷 ∈ ℂ
28	27, 23, 24	divcli 12040	. . 3 ⊢ (_𝐶𝐷 / ;10) ∈ ℂ
29	20, 25, 26, 28	add4i 11516	. 2 ⊢ ((𝐺 + (_𝐴𝐵 / ;10)) + (𝐻 + (_𝐶𝐷 / ;10))) = ((𝐺 + 𝐻) + ((_𝐴𝐵 / ;10) + (_𝐶𝐷 / ;10)))
30		dpadd2.i	. . . 4 ⊢ (𝐺 + 𝐻) = 𝐼
31	21, 27, 23, 24	divdiri 12055	. . . . 5 ⊢ ((_𝐴𝐵 + _𝐶𝐷) / ;10) = ((_𝐴𝐵 / ;10) + (_𝐶𝐷 / ;10))
32		dpadd2.1	. . . . . . 7 ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)
33		dpval 33438	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = _𝐴𝐵)
34	2, 6, 33	mp2an 705	. . . . . . . 8 ⊢ (𝐴.𝐵) = _𝐴𝐵
35		dpval 33438	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℕ₀ ∧ 𝐷 ∈ ℝ) → (𝐶.𝐷) = _𝐶𝐷)
36	11, 15, 35	mp2an 705	. . . . . . . 8 ⊢ (𝐶.𝐷) = _𝐶𝐷
37	34, 36	oveq12i 7424	. . . . . . 7 ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (_𝐴𝐵 + _𝐶𝐷)
38		dpadd2.e	. . . . . . . 8 ⊢ 𝐸 ∈ ℕ₀
39		dpadd2.f	. . . . . . . . 9 ⊢ 𝐹 ∈ ℝ⁺
40		rpre 13110	. . . . . . . . 9 ⊢ (𝐹 ∈ ℝ⁺ → 𝐹 ∈ ℝ)
41	39, 40	ax-mp 5	. . . . . . . 8 ⊢ 𝐹 ∈ ℝ
42		dpval 33438	. . . . . . . 8 ⊢ ((𝐸 ∈ ℕ₀ ∧ 𝐹 ∈ ℝ) → (𝐸.𝐹) = _𝐸𝐹)
43	38, 41, 42	mp2an 705	. . . . . . 7 ⊢ (𝐸.𝐹) = _𝐸𝐹
44	32, 37, 43	3eqtr3i 2792	. . . . . 6 ⊢ (_𝐴𝐵 + _𝐶𝐷) = _𝐸𝐹
45	44	oveq1i 7422	. . . . 5 ⊢ ((_𝐴𝐵 + _𝐶𝐷) / ;10) = (_𝐸𝐹 / ;10)
46	31, 45	eqtr3i 2786	. . . 4 ⊢ ((_𝐴𝐵 / ;10) + (_𝐶𝐷 / ;10)) = (_𝐸𝐹 / ;10)
47	30, 46	oveq12i 7424	. . 3 ⊢ ((𝐺 + 𝐻) + ((_𝐴𝐵 / ;10) + (_𝐶𝐷 / ;10))) = (𝐼 + (_𝐸𝐹 / ;10))
48	1, 10	nn0addcli 12624	. . . . 5 ⊢ (𝐺 + 𝐻) ∈ ℕ₀
49	30, 48	eqeltrri 2858	. . . 4 ⊢ 𝐼 ∈ ℕ₀
50	38	nn0rei 12598	. . . . 5 ⊢ 𝐸 ∈ ℝ
51		dp2cl 33428	. . . . 5 ⊢ ((𝐸 ∈ ℝ ∧ 𝐹 ∈ ℝ) → _𝐸𝐹 ∈ ℝ)
52	50, 41, 51	mp2an 705	. . . 4 ⊢ _𝐸𝐹 ∈ ℝ
53	49, 52	dpval2 33441	. . 3 ⊢ (𝐼._𝐸𝐹) = (𝐼 + (_𝐸𝐹 / ;10))
54	47, 53	eqtr4i 2787	. 2 ⊢ ((𝐺 + 𝐻) + ((_𝐴𝐵 / ;10) + (_𝐶𝐷 / ;10))) = (𝐼._𝐸𝐹)
55	19, 29, 54	3eqtri 2788	1 ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹)

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1570 ∈ wcel 2145 (class class class)co 7412 ℝcr 11180 0cc0 11181 1c1 11182 + caddc 11184 / cdiv 11954 ℕ₀cn0 12587 cdc 12795 ℝ⁺crp 13101 cdp2 33419 .cdp 33436

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8701 df-en 8958 df-dom 8959 df-sdom 8960 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-5 12389 df-6 12390 df-7 12391 df-8 12392 df-9 12393 df-n0 12588 df-dec 12796 df-rp 13102 df-dp2 33420 df-dp 33437

This theorem is used by: hgt750lemd 35260

W3C validator