sqdeccom12 - Mathbox for Steven Nguyen

	Mathbox for Steven Nguyen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sqdeccom12		Structured version Visualization version GIF version

Theorem sqdeccom12 39195

Description: The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.)

**Hypotheses**
Ref	Expression
sqdeccom12.a	⊢ 𝐴 ∈ ℕ₀
sqdeccom12.b	⊢ 𝐵 ∈ ℕ₀

**Assertion**
Ref	Expression
sqdeccom12	⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))

**Proof of Theorem sqdeccom12**
Step	Hyp	Ref	Expression
1		sqdeccom12.a	. . . . . . . . 9 ⊢ 𝐴 ∈ ℕ₀
2	1, 1	nn0mulcli 11936	. . . . . . . 8 ⊢ (𝐴 · 𝐴) ∈ ℕ₀
3		0nn0 11913	. . . . . . . 8 ⊢ 0 ∈ ℕ₀
4	2, 3	deccl 12114	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)0 ∈ ℕ₀
5	4, 3	deccl 12114	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)00 ∈ ℕ₀
6	5	nn0cni 11910	. . . . 5 ⊢ ;;(𝐴 · 𝐴)00 ∈ ℂ
7		sqdeccom12.b	. . . . . . . . 9 ⊢ 𝐵 ∈ ℕ₀
8	7, 7	nn0mulcli 11936	. . . . . . . 8 ⊢ (𝐵 · 𝐵) ∈ ℕ₀
9	8, 3	deccl 12114	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)0 ∈ ℕ₀
10	9, 3	deccl 12114	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)00 ∈ ℕ₀
11	10	nn0cni 11910	. . . . 5 ⊢ ;;(𝐵 · 𝐵)00 ∈ ℂ
12	1	nn0cni 11910	. . . . . 6 ⊢ 𝐴 ∈ ℂ
13	12, 12	mulcli 10648	. . . . 5 ⊢ (𝐴 · 𝐴) ∈ ℂ
14	7	nn0cni 11910	. . . . . 6 ⊢ 𝐵 ∈ ℂ
15	14, 14	mulcli 10648	. . . . 5 ⊢ (𝐵 · 𝐵) ∈ ℂ
16		subadd4 10930	. . . . 5 ⊢ (((;;(𝐴 · 𝐴)00 ∈ ℂ ∧ ;;(𝐵 · 𝐵)00 ∈ ℂ) ∧ ((𝐴 · 𝐴) ∈ ℂ ∧ (𝐵 · 𝐵) ∈ ℂ)) → ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴))))
17	6, 11, 13, 15, 16	mp4an 691	. . . 4 ⊢ ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴)))
18		eqid 2821	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)00 = ;;(𝐴 · 𝐴)00
19	15	addid2i 10828	. . . . . 6 ⊢ (0 + (𝐵 · 𝐵)) = (𝐵 · 𝐵)
20	4, 3, 8, 18, 19	decaddi 12159	. . . . 5 ⊢ (;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) = ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)
21		eqid 2821	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)00 = ;;(𝐵 · 𝐵)00
22	13	addid2i 10828	. . . . . 6 ⊢ (0 + (𝐴 · 𝐴)) = (𝐴 · 𝐴)
23	9, 3, 2, 21, 22	decaddi 12159	. . . . 5 ⊢ (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴)) = ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)
24	20, 23	oveq12i 7168	. . . 4 ⊢ ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴))) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))
25	17, 24	eqtr2i 2845	. . 3 ⊢ (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
26		eqid 2821	. . . . 5 ⊢ ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
27	7, 1	nn0mulcli 11936	. . . . . . . 8 ⊢ (𝐵 · 𝐴) ∈ ℕ₀
28	1, 7, 27	numcl 12112	. . . . . . 7 ⊢ ((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
29	2, 28	deccl 12114	. . . . . 6 ⊢ ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
30		eqid 2821	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) = ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵)
31		eqid 2821	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) = ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)
32		eqid 2821	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))
33		eqid 2821	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)0 = ;(𝐵 · 𝐵)0
34	13, 15	addcomi 10831	. . . . . . 7 ⊢ ((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ((𝐵 · 𝐵) + (𝐴 · 𝐴))
35		eqid 2821	. . . . . . 7 ⊢ (((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0) = (((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
36	2, 28, 8, 3, 32, 33, 34, 35	decadd 12153	. . . . . 6 ⊢ (;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) + ;(𝐵 · 𝐵)0) = ;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
37	15, 13	addcomi 10831	. . . . . 6 ⊢ ((𝐵 · 𝐵) + (𝐴 · 𝐴)) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))
38	29, 8, 9, 2, 30, 31, 36, 37	decadd 12153	. . . . 5 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
39	8, 28	deccl 12114	. . . . . 6 ⊢ ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
40		eqid 2821	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) = ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)
41		eqid 2821	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) = ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)
42		eqid 2821	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))
43		eqid 2821	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)0 = ;(𝐴 · 𝐴)0
44		eqid 2821	. . . . . . 7 ⊢ ((𝐵 · 𝐵) + (𝐴 · 𝐴)) = ((𝐵 · 𝐵) + (𝐴 · 𝐴))
45	8, 28, 2, 3, 42, 43, 44, 35	decadd 12153	. . . . . 6 ⊢ (;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) + ;(𝐴 · 𝐴)0) = ;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
46		eqid 2821	. . . . . 6 ⊢ ((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))
47	39, 2, 4, 8, 40, 41, 45, 46	decadd 12153	. . . . 5 ⊢ (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
48	26, 38, 47	3eqtr4i 2854	. . . 4 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵))
49	29, 8	deccl 12114	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℕ₀
50	49	nn0cni 11910	. . . . 5 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℂ
51	9, 2	deccl 12114	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℕ₀
52	51	nn0cni 11910	. . . . 5 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℂ
53	39, 2	deccl 12114	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℕ₀
54	53	nn0cni 11910	. . . . 5 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℂ
55	4, 8	deccl 12114	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℕ₀
56	55	nn0cni 11910	. . . . 5 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℂ
57		addsubeq4com 39186	. . . . 5 ⊢ (((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℂ ∧ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℂ) ∧ (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℂ ∧ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℂ)) → ((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) ↔ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))))
58	50, 52, 54, 56, 57	mp4an 691	. . . 4 ⊢ ((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) ↔ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)))
59	48, 58	mpbi 232	. . 3 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))
60		10nn0 12117	. . . . . . 7 ⊢ ;10 ∈ ℕ₀
61	60, 3	deccl 12114	. . . . . 6 ⊢ ;;100 ∈ ℕ₀
62	61	nn0cni 11910	. . . . 5 ⊢ ;;100 ∈ ℂ
63		ax-1cn 10595	. . . . 5 ⊢ 1 ∈ ℂ
64	13, 15	subcli 10962	. . . . 5 ⊢ ((𝐴 · 𝐴) − (𝐵 · 𝐵)) ∈ ℂ
65	62, 63, 64	subdiri 11090	. . . 4 ⊢ ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) − (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))))
66	62, 13, 15	subdii 11089	. . . . . 6 ⊢ (;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 · (𝐴 · 𝐴)) − (;;100 · (𝐵 · 𝐵)))
67		eqid 2821	. . . . . . . 8 ⊢ ;;100 = ;;100
68	2	dec0u 12120	. . . . . . . 8 ⊢ (;10 · (𝐴 · 𝐴)) = ;(𝐴 · 𝐴)0
69	13	mul02i 10829	. . . . . . . 8 ⊢ (0 · (𝐴 · 𝐴)) = 0
70	2, 60, 3, 67, 68, 69	decmul1 12163	. . . . . . 7 ⊢ (;;100 · (𝐴 · 𝐴)) = ;;(𝐴 · 𝐴)00
71	8	dec0u 12120	. . . . . . . 8 ⊢ (;10 · (𝐵 · 𝐵)) = ;(𝐵 · 𝐵)0
72	15	mul02i 10829	. . . . . . . 8 ⊢ (0 · (𝐵 · 𝐵)) = 0
73	8, 60, 3, 67, 71, 72	decmul1 12163	. . . . . . 7 ⊢ (;;100 · (𝐵 · 𝐵)) = ;;(𝐵 · 𝐵)00
74	70, 73	oveq12i 7168	. . . . . 6 ⊢ ((;;100 · (𝐴 · 𝐴)) − (;;100 · (𝐵 · 𝐵))) = (;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00)
75	66, 74	eqtri 2844	. . . . 5 ⊢ (;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = (;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00)
76	64	mulid2i 10646	. . . . 5 ⊢ (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((𝐴 · 𝐴) − (𝐵 · 𝐵))
77	75, 76	oveq12i 7168	. . . 4 ⊢ ((;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) − (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
78	65, 77	eqtri 2844	. . 3 ⊢ ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
79	25, 59, 78	3eqtr4i 2854	. 2 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
80		eqid 2821	. . . 4 ⊢ (𝐴 · 𝐴) = (𝐴 · 𝐴)
81		eqid 2821	. . . 4 ⊢ ((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ((𝐴 · 𝐵) + (𝐵 · 𝐴))
82		eqid 2821	. . . 4 ⊢ (𝐵 · 𝐵) = (𝐵 · 𝐵)
83	1, 7, 1, 7, 80, 81, 82	decpmulnc 39193	. . 3 ⊢ (;𝐴𝐵 · ;𝐴𝐵) = ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵)
84	14, 12	mulcli 10648	. . . . 5 ⊢ (𝐵 · 𝐴) ∈ ℂ
85	12, 14	mulcli 10648	. . . . 5 ⊢ (𝐴 · 𝐵) ∈ ℂ
86	84, 85	addcomi 10831	. . . 4 ⊢ ((𝐵 · 𝐴) + (𝐴 · 𝐵)) = ((𝐴 · 𝐵) + (𝐵 · 𝐴))
87	7, 1, 7, 1, 82, 86, 80	decpmulnc 39193	. . 3 ⊢ (;𝐵𝐴 · ;𝐵𝐴) = ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)
88	83, 87	oveq12i 7168	. 2 ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴))
89		9nn0 11922	. . . . . 6 ⊢ 9 ∈ ℕ₀
90	89, 89	deccl 12114	. . . . 5 ⊢ ;99 ∈ ℕ₀
91	90	nn0cni 11910	. . . 4 ⊢ ;99 ∈ ℂ
92		9p1e10 12101	. . . . . 6 ⊢ (9 + 1) = ;10
93		eqid 2821	. . . . . 6 ⊢ ;99 = ;99
94	89, 92, 93	decsucc 12140	. . . . 5 ⊢ (;99 + 1) = ;;100
95	91, 63, 94	addcomli 10832	. . . 4 ⊢ (1 + ;99) = ;;100
96	63, 91, 95	mvlladdi 10904	. . 3 ⊢ ;99 = (;;100 − 1)
97	96	oveq1i 7166	. 2 ⊢ (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
98	79, 88, 97	3eqtr4i 2854	1 ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 = wceq 1537 ∈ wcel 2114 (class class class)co 7156 ℂcc 10535 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 − cmin 10870 9c9 11700 ℕ₀cn0 11898 cdc 12099

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-er 8289 df-en 8510 df-dom 8511 df-sdom 8512 df-pnf 10677 df-mnf 10678 df-ltxr 10680 df-sub 10872 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-dec 12100

This theorem is referenced by: sq3deccom12 39196

W3C validator