Proof of Theorem ex-decpmul
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2nn0 12543 | . . 3
⊢ 2 ∈
ℕ0 | 
| 2 |  | 3nn0 12544 | . . 3
⊢ 3 ∈
ℕ0 | 
| 3 | 1, 2 | deccl 12748 | . 2
⊢ ;23 ∈
ℕ0 | 
| 4 |  | 5nn0 12546 | . 2
⊢ 5 ∈
ℕ0 | 
| 5 |  | 7nn0 12548 | . . 3
⊢ 7 ∈
ℕ0 | 
| 6 |  | 1nn0 12542 | . . 3
⊢ 1 ∈
ℕ0 | 
| 7 | 5, 6 | deccl 12748 | . 2
⊢ ;71 ∈
ℕ0 | 
| 8 |  | eqid 2737 | . . 3
⊢ ;71 = ;71 | 
| 9 |  | 6nn0 12547 | . . . . 5
⊢ 6 ∈
ℕ0 | 
| 10 | 6, 9 | deccl 12748 | . . . 4
⊢ ;16 ∈
ℕ0 | 
| 11 |  | eqid 2737 | . . . . 5
⊢ ;23 = ;23 | 
| 12 |  | 4nn0 12545 | . . . . . 6
⊢ 4 ∈
ℕ0 | 
| 13 |  | 7cn 12360 | . . . . . . 7
⊢ 7 ∈
ℂ | 
| 14 |  | 2cn 12341 | . . . . . . 7
⊢ 2 ∈
ℂ | 
| 15 |  | 7t2e14 12842 | . . . . . . 7
⊢ (7
· 2) = ;14 | 
| 16 | 13, 14, 15 | mulcomli 11270 | . . . . . 6
⊢ (2
· 7) = ;14 | 
| 17 |  | 4p2e6 12419 | . . . . . 6
⊢ (4 + 2) =
6 | 
| 18 | 6, 12, 1, 16, 17 | decaddi 12793 | . . . . 5
⊢ ((2
· 7) + 2) = ;16 | 
| 19 |  | 3cn 12347 | . . . . . 6
⊢ 3 ∈
ℂ | 
| 20 |  | 7t3e21 12843 | . . . . . 6
⊢ (7
· 3) = ;21 | 
| 21 | 13, 19, 20 | mulcomli 11270 | . . . . 5
⊢ (3
· 7) = ;21 | 
| 22 | 5, 1, 2, 11, 6, 1,
18, 21 | decmul1c 12798 | . . . 4
⊢ (;23 · 7) = ;;161 | 
| 23 |  | 1p2e3 12409 | . . . 4
⊢ (1 + 2) =
3 | 
| 24 | 10, 6, 1, 22, 23 | decaddi 12793 | . . 3
⊢ ((;23 · 7) + 2) = ;;163 | 
| 25 | 3 | nn0cni 12538 | . . . 4
⊢ ;23 ∈ ℂ | 
| 26 | 25 | mulridi 11265 | . . 3
⊢ (;23 · 1) = ;23 | 
| 27 | 3, 5, 6, 8, 2, 1, 24, 26 | decmul2c 12799 | . 2
⊢ (;23 · ;71) = ;;;1633 | 
| 28 | 2, 4 | deccl 12748 | . . 3
⊢ ;35 ∈
ℕ0 | 
| 29 | 7 | nn0cni 12538 | . . . 4
⊢ ;71 ∈ ℂ | 
| 30 |  | 5cn 12354 | . . . 4
⊢ 5 ∈
ℂ | 
| 31 |  | 7t5e35 12845 | . . . . 5
⊢ (7
· 5) = ;35 | 
| 32 | 30 | mullidi 11266 | . . . . 5
⊢ (1
· 5) = 5 | 
| 33 | 4, 5, 6, 8, 31, 32 | decmul1 12797 | . . . 4
⊢ (;71 · 5) = ;;355 | 
| 34 | 29, 30, 33 | mulcomli 11270 | . . 3
⊢ (5
· ;71) = ;;355 | 
| 35 | 28 | nn0cni 12538 | . . . 4
⊢ ;35 ∈ ℂ | 
| 36 |  | eqid 2737 | . . . . 5
⊢ ;35 = ;35 | 
| 37 |  | 5p2e7 12422 | . . . . 5
⊢ (5 + 2) =
7 | 
| 38 | 2, 4, 1, 36, 37 | decaddi 12793 | . . . 4
⊢ (;35 + 2) = ;37 | 
| 39 | 35, 14, 38 | addcomli 11453 | . . 3
⊢ (2 +
;35) = ;37 | 
| 40 |  | 5p3e8 12423 | . . . 4
⊢ (5 + 3) =
8 | 
| 41 | 30, 19, 40 | addcomli 11453 | . . 3
⊢ (3 + 5) =
8 | 
| 42 | 1, 2, 28, 4, 26, 34, 39, 41 | decadd 12787 | . 2
⊢ ((;23 · 1) + (5 · ;71)) = ;;378 | 
| 43 | 30 | mulridi 11265 | . . 3
⊢ (5
· 1) = 5 | 
| 44 | 4 | dec0h 12755 | . . 3
⊢ 5 = ;05 | 
| 45 | 43, 44 | eqtri 2765 | . 2
⊢ (5
· 1) = ;05 | 
| 46 | 10, 2 | deccl 12748 | . . . 4
⊢ ;;163 ∈ ℕ0 | 
| 47 | 46, 2 | deccl 12748 | . . 3
⊢ ;;;1633
∈ ℕ0 | 
| 48 |  | 0nn0 12541 | . . 3
⊢ 0 ∈
ℕ0 | 
| 49 | 2, 5 | deccl 12748 | . . 3
⊢ ;37 ∈
ℕ0 | 
| 50 |  | 8nn0 12549 | . . 3
⊢ 8 ∈
ℕ0 | 
| 51 |  | eqid 2737 | . . 3
⊢ ;;;;16330 = ;;;;16330 | 
| 52 |  | eqid 2737 | . . 3
⊢ ;;378 = ;;378 | 
| 53 |  | eqid 2737 | . . . 4
⊢ ;;;1633 =
;;;1633 | 
| 54 |  | eqid 2737 | . . . 4
⊢ ;37 = ;37 | 
| 55 |  | eqid 2737 | . . . . . 6
⊢ ;;163 = ;;163 | 
| 56 |  | 3p3e6 12418 | . . . . . 6
⊢ (3 + 3) =
6 | 
| 57 | 10, 2, 2, 55, 56 | decaddi 12793 | . . . . 5
⊢ (;;163 + 3) = ;;166 | 
| 58 |  | 6p1e7 12414 | . . . . 5
⊢ (6 + 1) =
7 | 
| 59 | 10, 9, 6, 57, 58 | decaddi 12793 | . . . 4
⊢ ((;;163 + 3) + 1) = ;;167 | 
| 60 |  | 7p3e10 12808 | . . . . 5
⊢ (7 + 3) =
;10 | 
| 61 | 13, 19, 60 | addcomli 11453 | . . . 4
⊢ (3 + 7) =
;10 | 
| 62 | 46, 2, 2, 5, 53, 54, 59, 61 | decaddc2 12789 | . . 3
⊢ (;;;1633 +
;37) = ;;;1670 | 
| 63 |  | 8cn 12363 | . . . 4
⊢ 8 ∈
ℂ | 
| 64 | 63 | addlidi 11449 | . . 3
⊢ (0 + 8) =
8 | 
| 65 | 47, 48, 49, 50, 51, 52, 62, 64 | decadd 12787 | . 2
⊢ (;;;;16330 + ;;378) =
;;;;16708 | 
| 66 | 3, 4, 7, 6, 27, 42, 45, 65, 48, 4 | decpmul 42323 | 1
⊢ (;;235 · ;;711) =
;;;;;167085 |