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 42905

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 12530	. . . . . . . 8 ⊢ (𝐴 · 𝐴) ∈ ℕ₀
3		0nn0 12507	. . . . . . . 8 ⊢ 0 ∈ ℕ₀
4	2, 3	deccl 12714	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)0 ∈ ℕ₀
5	4, 3	deccl 12714	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)00 ∈ ℕ₀
6	5	nn0cni 12504	. . . . 5 ⊢ ;;(𝐴 · 𝐴)00 ∈ ℂ
7		sqdeccom12.b	. . . . . . . . 9 ⊢ 𝐵 ∈ ℕ₀
8	7, 7	nn0mulcli 12530	. . . . . . . 8 ⊢ (𝐵 · 𝐵) ∈ ℕ₀
9	8, 3	deccl 12714	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)0 ∈ ℕ₀
10	9, 3	deccl 12714	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)00 ∈ ℕ₀
11	10	nn0cni 12504	. . . . 5 ⊢ ;;(𝐵 · 𝐵)00 ∈ ℂ
12	1	nn0cni 12504	. . . . . 6 ⊢ 𝐴 ∈ ℂ
13	12, 12	mulcli 11204	. . . . 5 ⊢ (𝐴 · 𝐴) ∈ ℂ
14	7	nn0cni 12504	. . . . . 6 ⊢ 𝐵 ∈ ℂ
15	14, 14	mulcli 11204	. . . . 5 ⊢ (𝐵 · 𝐵) ∈ ℂ
16		subadd4 11490	. . . . 5 ⊢ (((;;(𝐴 · 𝐴)00 ∈ ℂ ∧ ;;(𝐵 · 𝐵)00 ∈ ℂ) ∧ ((𝐴 · 𝐴) ∈ ℂ ∧ (𝐵 · 𝐵) ∈ ℂ)) → ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴))))
17	6, 11, 13, 15, 16	mp4an 705	. . . 4 ⊢ ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴)))
18		eqid 2765	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)00 = ;;(𝐴 · 𝐴)00
19	15	addlidi 11386	. . . . . 6 ⊢ (0 + (𝐵 · 𝐵)) = (𝐵 · 𝐵)
20	4, 3, 8, 18, 19	decaddi 12764	. . . . 5 ⊢ (;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) = ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)
21		eqid 2765	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)00 = ;;(𝐵 · 𝐵)00
22	13	addlidi 11386	. . . . . 6 ⊢ (0 + (𝐴 · 𝐴)) = (𝐴 · 𝐴)
23	9, 3, 2, 21, 22	decaddi 12764	. . . . 5 ⊢ (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴)) = ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)
24	20, 23	oveq12i 7412	. . . 4 ⊢ ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴))) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))
25	17, 24	eqtr2i 2789	. . 3 ⊢ (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
26		eqid 2765	. . . . 5 ⊢ ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
27	7, 1	nn0mulcli 12530	. . . . . . . 8 ⊢ (𝐵 · 𝐴) ∈ ℕ₀
28	1, 7, 27	numcl 12712	. . . . . . 7 ⊢ ((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
29	2, 28	deccl 12714	. . . . . 6 ⊢ ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
30		eqid 2765	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) = ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵)
31		eqid 2765	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) = ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)
32		eqid 2765	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))
33		eqid 2765	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)0 = ;(𝐵 · 𝐵)0
34	13, 15	addcomi 11389	. . . . . . 7 ⊢ ((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ((𝐵 · 𝐵) + (𝐴 · 𝐴))
35		eqid 2765	. . . . . . 7 ⊢ (((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0) = (((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
36	2, 28, 8, 3, 32, 33, 34, 35	decadd 12758	. . . . . 6 ⊢ (;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) + ;(𝐵 · 𝐵)0) = ;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
37	15, 13	addcomi 11389	. . . . . 6 ⊢ ((𝐵 · 𝐵) + (𝐴 · 𝐴)) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))
38	29, 8, 9, 2, 30, 31, 36, 37	decadd 12758	. . . . 5 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
39	8, 28	deccl 12714	. . . . . 6 ⊢ ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
40		eqid 2765	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) = ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)
41		eqid 2765	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) = ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)
42		eqid 2765	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))
43		eqid 2765	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)0 = ;(𝐴 · 𝐴)0
44		eqid 2765	. . . . . . 7 ⊢ ((𝐵 · 𝐵) + (𝐴 · 𝐴)) = ((𝐵 · 𝐵) + (𝐴 · 𝐴))
45	8, 28, 2, 3, 42, 43, 44, 35	decadd 12758	. . . . . 6 ⊢ (;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) + ;(𝐴 · 𝐴)0) = ;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
46		eqid 2765	. . . . . 6 ⊢ ((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))
47	39, 2, 4, 8, 40, 41, 45, 46	decadd 12758	. . . . 5 ⊢ (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
48	26, 38, 47	3eqtr4i 2798	. . . 4 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵))
49	29, 8	deccl 12714	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℕ₀
50	49	nn0cni 12504	. . . . 5 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℂ
51	9, 2	deccl 12714	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℕ₀
52	51	nn0cni 12504	. . . . 5 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℂ
53	39, 2	deccl 12714	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℕ₀
54	53	nn0cni 12504	. . . . 5 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℂ
55	4, 8	deccl 12714	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℕ₀
56	55	nn0cni 12504	. . . . 5 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℂ
57		addsubeq4com 42896	. . . . 5 ⊢ (((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℂ ∧ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℂ) ∧ (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℂ ∧ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℂ)) → ((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) ↔ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))))
58	50, 52, 54, 56, 57	mp4an 705	. . . 4 ⊢ ((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) ↔ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)))
59	48, 58	mpbi 233	. . 3 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))
60		10nn0 12721	. . . . . . 7 ⊢ ;10 ∈ ℕ₀
61	60, 3	deccl 12714	. . . . . 6 ⊢ ;;100 ∈ ℕ₀
62	61	nn0cni 12504	. . . . 5 ⊢ ;;100 ∈ ℂ
63		ax-1cn 11146	. . . . 5 ⊢ 1 ∈ ℂ
64	13, 15	subcli 11522	. . . . 5 ⊢ ((𝐴 · 𝐴) − (𝐵 · 𝐵)) ∈ ℂ
65	62, 63, 64	subdiri 11652	. . . 4 ⊢ ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) − (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))))
66	62, 13, 15	subdii 11651	. . . . . 6 ⊢ (;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 · (𝐴 · 𝐴)) − (;;100 · (𝐵 · 𝐵)))
67		eqid 2765	. . . . . . . 8 ⊢ ;;100 = ;;100
68	2	dec0u 12725	. . . . . . . 8 ⊢ (;10 · (𝐴 · 𝐴)) = ;(𝐴 · 𝐴)0
69	13	mul02i 11387	. . . . . . . 8 ⊢ (0 · (𝐴 · 𝐴)) = 0
70	2, 60, 3, 67, 68, 69	decmul1 12768	. . . . . . 7 ⊢ (;;100 · (𝐴 · 𝐴)) = ;;(𝐴 · 𝐴)00
71	8	dec0u 12725	. . . . . . . 8 ⊢ (;10 · (𝐵 · 𝐵)) = ;(𝐵 · 𝐵)0
72	15	mul02i 11387	. . . . . . . 8 ⊢ (0 · (𝐵 · 𝐵)) = 0
73	8, 60, 3, 67, 71, 72	decmul1 12768	. . . . . . 7 ⊢ (;;100 · (𝐵 · 𝐵)) = ;;(𝐵 · 𝐵)00
74	70, 73	oveq12i 7412	. . . . . 6 ⊢ ((;;100 · (𝐴 · 𝐴)) − (;;100 · (𝐵 · 𝐵))) = (;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00)
75	66, 74	eqtri 2788	. . . . 5 ⊢ (;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = (;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00)
76	64	mullidi 11202	. . . . 5 ⊢ (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((𝐴 · 𝐴) − (𝐵 · 𝐵))
77	75, 76	oveq12i 7412	. . . 4 ⊢ ((;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) − (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
78	65, 77	eqtri 2788	. . 3 ⊢ ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
79	25, 59, 78	3eqtr4i 2798	. 2 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
80		eqid 2765	. . . 4 ⊢ (𝐴 · 𝐴) = (𝐴 · 𝐴)
81		eqid 2765	. . . 4 ⊢ ((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ((𝐴 · 𝐵) + (𝐵 · 𝐴))
82		eqid 2765	. . . 4 ⊢ (𝐵 · 𝐵) = (𝐵 · 𝐵)
83	1, 7, 1, 7, 80, 81, 82	decpmulnc 42903	. . 3 ⊢ (;𝐴𝐵 · ;𝐴𝐵) = ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵)
84	14, 12	mulcli 11204	. . . . 5 ⊢ (𝐵 · 𝐴) ∈ ℂ
85	12, 14	mulcli 11204	. . . . 5 ⊢ (𝐴 · 𝐵) ∈ ℂ
86	84, 85	addcomi 11389	. . . 4 ⊢ ((𝐵 · 𝐴) + (𝐴 · 𝐵)) = ((𝐴 · 𝐵) + (𝐵 · 𝐴))
87	7, 1, 7, 1, 82, 86, 80	decpmulnc 42903	. . 3 ⊢ (;𝐵𝐴 · ;𝐵𝐴) = ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)
88	83, 87	oveq12i 7412	. 2 ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴))
89		9nn0 12516	. . . . . 6 ⊢ 9 ∈ ℕ₀
90	89, 89	deccl 12714	. . . . 5 ⊢ ;99 ∈ ℕ₀
91	90	nn0cni 12504	. . . 4 ⊢ ;99 ∈ ℂ
92		9p1e10 12701	. . . . . 6 ⊢ (9 + 1) = ;10
93		eqid 2765	. . . . . 6 ⊢ ;99 = ;99
94	89, 92, 93	decsucc 12745	. . . . 5 ⊢ (;99 + 1) = ;;100
95	91, 63, 94	addcomli 11390	. . . 4 ⊢ (1 + ;99) = ;;100
96	63, 91, 95	mvlladdi 11464	. . 3 ⊢ ;99 = (;;100 − 1)
97	96	oveq1i 7410	. 2 ⊢ (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
98	79, 88, 97	3eqtr4i 2798	1 ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 209 = wceq 1563 ∈ wcel 2145 (class class class)co 7400 ℂcc 11086 0cc0 11088 1c1 11089 + caddc 11091 · cmul 11093 − cmin 11429 9c9 12290 ℕ₀cn0 12492 cdc 12699

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-pnf 11233 df-mnf 11234 df-ltxr 11236 df-sub 11431 df-nn 12222 df-2 12291 df-3 12292 df-4 12293 df-5 12294 df-6 12295 df-7 12296 df-8 12297 df-9 12298 df-n0 12493 df-dec 12700

This theorem is referenced by: sq3deccom12 42906

W3C validator