![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3dec | GIF version |
Description: A "decimal constructor" which is used to build up "decimal integers" or "numeric terms" in base 10 with 3 "digits". (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
Ref | Expression |
---|---|
3dec.a | ⊢ 𝐴 ∈ ℕ0 |
3dec.b | ⊢ 𝐵 ∈ ℕ0 |
Ref | Expression |
---|---|
3dec | ⊢ ;;𝐴𝐵𝐶 = ((((;10↑2) · 𝐴) + (;10 · 𝐵)) + 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfdec10 9454 | . 2 ⊢ ;;𝐴𝐵𝐶 = ((;10 · ;𝐴𝐵) + 𝐶) | |
2 | dfdec10 9454 | . . . . . 6 ⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵) | |
3 | 2 | oveq2i 5930 | . . . . 5 ⊢ (;10 · ;𝐴𝐵) = (;10 · ((;10 · 𝐴) + 𝐵)) |
4 | 1nn 8995 | . . . . . . . 8 ⊢ 1 ∈ ℕ | |
5 | 4 | decnncl2 9474 | . . . . . . 7 ⊢ ;10 ∈ ℕ |
6 | 5 | nncni 8994 | . . . . . 6 ⊢ ;10 ∈ ℂ |
7 | 3dec.a | . . . . . . . 8 ⊢ 𝐴 ∈ ℕ0 | |
8 | 7 | nn0cni 9255 | . . . . . . 7 ⊢ 𝐴 ∈ ℂ |
9 | 6, 8 | mulcli 8026 | . . . . . 6 ⊢ (;10 · 𝐴) ∈ ℂ |
10 | 3dec.b | . . . . . . 7 ⊢ 𝐵 ∈ ℕ0 | |
11 | 10 | nn0cni 9255 | . . . . . 6 ⊢ 𝐵 ∈ ℂ |
12 | 6, 9, 11 | adddii 8031 | . . . . 5 ⊢ (;10 · ((;10 · 𝐴) + 𝐵)) = ((;10 · (;10 · 𝐴)) + (;10 · 𝐵)) |
13 | 3, 12 | eqtri 2214 | . . . 4 ⊢ (;10 · ;𝐴𝐵) = ((;10 · (;10 · 𝐴)) + (;10 · 𝐵)) |
14 | 6, 6, 8 | mulassi 8030 | . . . . . . 7 ⊢ ((;10 · ;10) · 𝐴) = (;10 · (;10 · 𝐴)) |
15 | 14 | eqcomi 2197 | . . . . . 6 ⊢ (;10 · (;10 · 𝐴)) = ((;10 · ;10) · 𝐴) |
16 | 6 | sqvali 10693 | . . . . . . . 8 ⊢ (;10↑2) = (;10 · ;10) |
17 | 16 | eqcomi 2197 | . . . . . . 7 ⊢ (;10 · ;10) = (;10↑2) |
18 | 17 | oveq1i 5929 | . . . . . 6 ⊢ ((;10 · ;10) · 𝐴) = ((;10↑2) · 𝐴) |
19 | 15, 18 | eqtri 2214 | . . . . 5 ⊢ (;10 · (;10 · 𝐴)) = ((;10↑2) · 𝐴) |
20 | 19 | oveq1i 5929 | . . . 4 ⊢ ((;10 · (;10 · 𝐴)) + (;10 · 𝐵)) = (((;10↑2) · 𝐴) + (;10 · 𝐵)) |
21 | 13, 20 | eqtri 2214 | . . 3 ⊢ (;10 · ;𝐴𝐵) = (((;10↑2) · 𝐴) + (;10 · 𝐵)) |
22 | 21 | oveq1i 5929 | . 2 ⊢ ((;10 · ;𝐴𝐵) + 𝐶) = ((((;10↑2) · 𝐴) + (;10 · 𝐵)) + 𝐶) |
23 | 1, 22 | eqtri 2214 | 1 ⊢ ;;𝐴𝐵𝐶 = ((((;10↑2) · 𝐴) + (;10 · 𝐵)) + 𝐶) |
Colors of variables: wff set class |
Syntax hints: = wceq 1364 ∈ wcel 2164 (class class class)co 5919 0cc0 7874 1c1 7875 + caddc 7877 · cmul 7879 2c2 9035 ℕ0cn0 9243 ;cdc 9451 ↑cexp 10612 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4145 ax-sep 4148 ax-nul 4156 ax-pow 4204 ax-pr 4239 ax-un 4465 ax-setind 4570 ax-iinf 4621 ax-cnex 7965 ax-resscn 7966 ax-1cn 7967 ax-1re 7968 ax-icn 7969 ax-addcl 7970 ax-addrcl 7971 ax-mulcl 7972 ax-mulrcl 7973 ax-addcom 7974 ax-mulcom 7975 ax-addass 7976 ax-mulass 7977 ax-distr 7978 ax-i2m1 7979 ax-0lt1 7980 ax-1rid 7981 ax-0id 7982 ax-rnegex 7983 ax-precex 7984 ax-cnre 7985 ax-pre-ltirr 7986 ax-pre-ltwlin 7987 ax-pre-lttrn 7988 ax-pre-apti 7989 ax-pre-ltadd 7990 ax-pre-mulgt0 7991 ax-pre-mulext 7992 |
This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2987 df-csb 3082 df-dif 3156 df-un 3158 df-in 3160 df-ss 3167 df-nul 3448 df-if 3559 df-pw 3604 df-sn 3625 df-pr 3626 df-op 3628 df-uni 3837 df-int 3872 df-iun 3915 df-br 4031 df-opab 4092 df-mpt 4093 df-tr 4129 df-id 4325 df-po 4328 df-iso 4329 df-iord 4398 df-on 4400 df-ilim 4401 df-suc 4403 df-iom 4624 df-xp 4666 df-rel 4667 df-cnv 4668 df-co 4669 df-dm 4670 df-rn 4671 df-res 4672 df-ima 4673 df-iota 5216 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-riota 5874 df-ov 5922 df-oprab 5923 df-mpo 5924 df-1st 6195 df-2nd 6196 df-recs 6360 df-frec 6446 df-pnf 8058 df-mnf 8059 df-xr 8060 df-ltxr 8061 df-le 8062 df-sub 8194 df-neg 8195 df-reap 8596 df-ap 8603 df-div 8694 df-inn 8985 df-2 9043 df-3 9044 df-4 9045 df-5 9046 df-6 9047 df-7 9048 df-8 9049 df-9 9050 df-n0 9244 df-z 9321 df-dec 9452 df-uz 9596 df-seqfrec 10522 df-exp 10613 |
This theorem is referenced by: 3dvds2dec 12010 |
Copyright terms: Public domain | W3C validator |