dec0h - Intuitionistic Logic Explorer

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

Theorem dec0h 9545

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

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

**Assertion**
Ref	Expression
dec0h	⊢ 𝐴 = ;0𝐴

**Proof of Theorem dec0h**
Step	Hyp	Ref	Expression
1		10nn0 9541	. . 3 ⊢ ;10 ∈ ℕ₀
2		dec0u.1	. . 3 ⊢ 𝐴 ∈ ℕ₀
3	1, 2	num0h 9535	. 2 ⊢ 𝐴 = ((;10 · 0) + 𝐴)
4		dfdec10 9527	. 2 ⊢ ;0𝐴 = ((;10 · 0) + 𝐴)
5	3, 4	eqtr4i 2230	1 ⊢ 𝐴 = ;0𝐴

Colors of variables: wff set class

Syntax hints: = wceq 1373 ∈ wcel 2177 (class class class)co 5957 0cc0 7945 1c1 7946 + caddc 7948 · cmul 7950 ℕ₀cn0 9315 cdc 9524

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 4170 ax-pow 4226 ax-pr 4261 ax-setind 4593 ax-cnex 8036 ax-resscn 8037 ax-1cn 8038 ax-1re 8039 ax-icn 8040 ax-addcl 8041 ax-addrcl 8042 ax-mulcl 8043 ax-addcom 8045 ax-mulcom 8046 ax-addass 8047 ax-mulass 8048 ax-distr 8049 ax-i2m1 8050 ax-1rid 8052 ax-0id 8053 ax-rnegex 8054 ax-cnre 8056

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 3003 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3857 df-int 3892 df-br 4052 df-opab 4114 df-id 4348 df-xp 4689 df-rel 4690 df-cnv 4691 df-co 4692 df-dm 4693 df-iota 5241 df-fun 5282 df-fv 5288 df-riota 5912 df-ov 5960 df-oprab 5961 df-mpo 5962 df-sub 8265 df-inn 9057 df-2 9115 df-3 9116 df-4 9117 df-5 9118 df-6 9119 df-7 9120 df-8 9121 df-9 9122 df-n0 9316 df-dec 9525

This theorem is referenced by: declei 9559 decrmanc 9580 decrmac 9581 decaddi 9583 decaddci 9584 decmulnc 9590 dec5dvds2 12811 2exp16 12835