Theorem dpadd2 29959

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

Hypotheses

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

Assertion

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

Proof of Theorem dpadd2

Step	Hyp	Ref	Expression
1		dpadd2.g	. . . 4 ⊢ 𝐺 ∈ ℕ0
2		dpadd2.a	. . . . . 6 ⊢ 𝐴 ∈ ℕ0
3	2	nn0rei 11503	. . . . 5 ⊢ 𝐴 ∈ ℝ
4		dpadd2.b	. . . . . 6 ⊢ 𝐵 ∈ ℝ+
5		rpre 12041	. . . . . 6 ⊢ (𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ)
6	4, 5	ax-mp 5	. . . . 5 ⊢ 𝐵 ∈ ℝ
7		dp2cl 29928	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → _𝐴𝐵 ∈ ℝ)
8	3, 6, 7	mp2an 707	. . . 4 ⊢ _𝐴𝐵 ∈ ℝ
9	1, 8	dpval2 29942	. . 3 ⊢ (𝐺._𝐴𝐵) = (𝐺 + (_𝐴𝐵 / ;10))
10		dpadd2.h	. . . 4 ⊢ 𝐻 ∈ ℕ0
11		dpadd2.c	. . . . . 6 ⊢ 𝐶 ∈ ℕ0
12	11	nn0rei 11503	. . . . 5 ⊢ 𝐶 ∈ ℝ
13		dpadd2.d	. . . . . 6 ⊢ 𝐷 ∈ ℝ+
14		rpre 12041	. . . . . 6 ⊢ (𝐷 ∈ ℝ+ → 𝐷 ∈ ℝ)
15	13, 14	ax-mp 5	. . . . 5 ⊢ 𝐷 ∈ ℝ
16		dp2cl 29928	. . . . 5 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → _𝐶𝐷 ∈ ℝ)
17	12, 15, 16	mp2an 707	. . . 4 ⊢ _𝐶𝐷 ∈ ℝ
18	10, 17	dpval2 29942	. . 3 ⊢ (𝐻._𝐶𝐷) = (𝐻 + (_𝐶𝐷 / ;10))
19	9, 18	oveq12i 6803	. 2 ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = ((𝐺 + (_𝐴𝐵 / ;10)) + (𝐻 + (_𝐶𝐷 / ;10)))
20	1	nn0cni 11504	. . 3 ⊢ 𝐺 ∈ ℂ
21	8	recni 10252	. . . 4 ⊢ _𝐴𝐵 ∈ ℂ
22		10nn 11714	. . . . 5 ⊢ ;10 ∈ ℕ
23	22	nncni 11230	. . . 4 ⊢ ;10 ∈ ℂ
24	22	nnne0i 11255	. . . 4 ⊢ ;10 ≠ 0
25	21, 23, 24	divcli 10967	. . 3 ⊢ (_𝐴𝐵 / ;10) ∈ ℂ
26	10	nn0cni 11504	. . 3 ⊢ 𝐻 ∈ ℂ
27	17	recni 10252	. . . 4 ⊢ _𝐶𝐷 ∈ ℂ
28	27, 23, 24	divcli 10967	. . 3 ⊢ (_𝐶𝐷 / ;10) ∈ ℂ
29	20, 25, 26, 28	add4i 10460	. 2 ⊢ ((𝐺 + (_𝐴𝐵 / ;10)) + (𝐻 + (_𝐶𝐷 / ;10))) = ((𝐺 + 𝐻) + ((_𝐴𝐵 / ;10) + (_𝐶𝐷 / ;10)))
30		dpadd2.i	. . . 4 ⊢ (𝐺 + 𝐻) = 𝐼
31	21, 27, 23, 24	divdiri 10982	. . . . 5 ⊢ ((_𝐴𝐵 + _𝐶𝐷) / ;10) = ((_𝐴𝐵 / ;10) + (_𝐶𝐷 / ;10))
32		dpadd2.1	. . . . . . 7 ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)
33		dpval 29938	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = _𝐴𝐵)
34	2, 6, 33	mp2an 707	. . . . . . . 8 ⊢ (𝐴.𝐵) = _𝐴𝐵
35		dpval 29938	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ) → (𝐶.𝐷) = _𝐶𝐷)
36	11, 15, 35	mp2an 707	. . . . . . . 8 ⊢ (𝐶.𝐷) = _𝐶𝐷
37	34, 36	oveq12i 6803	. . . . . . 7 ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (_𝐴𝐵 + _𝐶𝐷)
38		dpadd2.e	. . . . . . . 8 ⊢ 𝐸 ∈ ℕ0
39		dpadd2.f	. . . . . . . . 9 ⊢ 𝐹 ∈ ℝ+
40		rpre 12041	. . . . . . . . 9 ⊢ (𝐹 ∈ ℝ+ → 𝐹 ∈ ℝ)
41	39, 40	ax-mp 5	. . . . . . . 8 ⊢ 𝐹 ∈ ℝ
42		dpval 29938	. . . . . . . 8 ⊢ ((𝐸 ∈ ℕ0 ∧ 𝐹 ∈ ℝ) → (𝐸.𝐹) = _𝐸𝐹)
43	38, 41, 42	mp2an 707	. . . . . . 7 ⊢ (𝐸.𝐹) = _𝐸𝐹
44	32, 37, 43	3eqtr3i 2799	. . . . . 6 ⊢ (_𝐴𝐵 + _𝐶𝐷) = _𝐸𝐹
45	44	oveq1i 6801	. . . . 5 ⊢ ((_𝐴𝐵 + _𝐶𝐷) / ;10) = (_𝐸𝐹 / ;10)
46	31, 45	eqtr3i 2793	. . . 4 ⊢ ((_𝐴𝐵 / ;10) + (_𝐶𝐷 / ;10)) = (_𝐸𝐹 / ;10)
47	30, 46	oveq12i 6803	. . 3 ⊢ ((𝐺 + 𝐻) + ((_𝐴𝐵 / ;10) + (_𝐶𝐷 / ;10))) = (𝐼 + (_𝐸𝐹 / ;10))
48	1, 10	nn0addcli 11530	. . . . 5 ⊢ (𝐺 + 𝐻) ∈ ℕ0
49	30, 48	eqeltrri 2845	. . . 4 ⊢ 𝐼 ∈ ℕ0
50	38	nn0rei 11503	. . . . 5 ⊢ 𝐸 ∈ ℝ
51		dp2cl 29928	. . . . 5 ⊢ ((𝐸 ∈ ℝ ∧ 𝐹 ∈ ℝ) → _𝐸𝐹 ∈ ℝ)
52	50, 41, 51	mp2an 707	. . . 4 ⊢ _𝐸𝐹 ∈ ℝ
53	49, 52	dpval2 29942	. . 3 ⊢ (𝐼._𝐸𝐹) = (𝐼 + (_𝐸𝐹 / ;10))
54	47, 53	eqtr4i 2794	. 2 ⊢ ((𝐺 + 𝐻) + ((_𝐴𝐵 / ;10) + (_𝐶𝐷 / ;10))) = (𝐼._𝐸𝐹)
55	19, 29, 54	3eqtri 2795	1 ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹)

Syntax hints:   = wceq 1629   ∈ wcel 2143  (class class class)co 6791  ℝcr 10135  0cc0 10136  1c1 10137   + caddc 10139   / cdiv 10884  ℕ₀cn0 11492  ;cdc 11693  ℝ⁺crp 12034  _cdp2 29918  .cdp 29936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2145  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749  ax-sep 4911  ax-nul 4919  ax-pow 4970  ax-pr 5033  ax-un 7094  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1070  df-3an 1071  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-eu 2620  df-mo 2621  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ne 2942  df-nel 3045  df-ral 3064  df-rex 3065  df-reu 3066  df-rmo 3067  df-rab 3068  df-v 3350  df-sbc 3585  df-csb 3680  df-dif 3723  df-un 3725  df-in 3727  df-ss 3734  df-pss 3736  df-nul 4061  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4572  df-iun 4653  df-br 4784  df-opab 4844  df-mpt 4861  df-tr 4884  df-id 5156  df-eprel 5161  df-po 5169  df-so 5170  df-fr 5207  df-we 5209  df-xp 5254  df-rel 5255  df-cnv 5256  df-co 5257  df-dm 5258  df-rn 5259  df-res 5260  df-ima 5261  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-om 7211  df-wrecs 7557  df-recs 7619  df-rdg 7657  df-er 7894  df-en 8108  df-dom 8109  df-sdom 8110  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-div 10885  df-nn 11221  df-2 11279  df-3 11280  df-4 11281  df-5 11282  df-6 11283  df-7 11284  df-8 11285  df-9 11286  df-n0 11493  df-dec 11694  df-rp 12035  df-dp2 29919  df-dp 29937

This theorem is referenced by:  hgt750lemd  31067