dec0u - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > dec0u		GIF version

Theorem dec0u 9531

Description: Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)

**Hypothesis**
Ref	Expression
dec0u.1	⊢ 𝐴 ∈ ℕ₀

**Assertion**
Ref	Expression
dec0u	⊢ (;10 · 𝐴) = ;𝐴0

**Proof of Theorem dec0u**
Step	Hyp	Ref	Expression
1		10nn0 9528	. . 3 ⊢ ;10 ∈ ℕ₀
2		dec0u.1	. . 3 ⊢ 𝐴 ∈ ℕ₀
3	1, 2	num0u 9521	. 2 ⊢ (;10 · 𝐴) = ((;10 · 𝐴) + 0)
4		dfdec10 9514	. 2 ⊢ ;𝐴0 = ((;10 · 𝐴) + 0)
5	3, 4	eqtr4i 2230	1 ⊢ (;10 · 𝐴) = ;𝐴0

Colors of variables: wff set class

Syntax hints: = wceq 1373 ∈ wcel 2177 (class class class)co 5951 0cc0 7932 1c1 7933 + caddc 7935 · cmul 7937 ℕ₀cn0 9302 cdc 9511

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-14 2180 ax-ext 2188 ax-sep 4166 ax-pow 4222 ax-pr 4257 ax-setind 4589 ax-cnex 8023 ax-resscn 8024 ax-1cn 8025 ax-1re 8026 ax-icn 8027 ax-addcl 8028 ax-addrcl 8029 ax-mulcl 8030 ax-addcom 8032 ax-mulcom 8033 ax-addass 8034 ax-mulass 8035 ax-distr 8036 ax-i2m1 8037 ax-1rid 8039 ax-0id 8040 ax-rnegex 8041 ax-cnre 8043

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-ral 2490 df-rex 2491 df-reu 2492 df-rab 2494 df-v 2775 df-sbc 3000 df-dif 3169 df-un 3171 df-in 3173 df-ss 3180 df-pw 3619 df-sn 3640 df-pr 3641 df-op 3643 df-uni 3853 df-int 3888 df-br 4048 df-opab 4110 df-id 4344 df-xp 4685 df-rel 4686 df-cnv 4687 df-co 4688 df-dm 4689 df-iota 5237 df-fun 5278 df-fv 5284 df-riota 5906 df-ov 5954 df-oprab 5955 df-mpo 5956 df-sub 8252 df-inn 9044 df-2 9102 df-3 9103 df-4 9104 df-5 9105 df-6 9106 df-7 9107 df-8 9108 df-9 9109 df-n0 9303 df-dec 9512

This theorem is referenced by: decmul10add 9579 5t5e25 9613 6t6e36 9618 8t6e48 9629