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 42282

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 12422	. . . . . . . 8 ⊢ (𝐴 · 𝐴) ∈ ℕ₀
3		0nn0 12399	. . . . . . . 8 ⊢ 0 ∈ ℕ₀
4	2, 3	deccl 12606	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)0 ∈ ℕ₀
5	4, 3	deccl 12606	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)00 ∈ ℕ₀
6	5	nn0cni 12396	. . . . 5 ⊢ ;;(𝐴 · 𝐴)00 ∈ ℂ
7		sqdeccom12.b	. . . . . . . . 9 ⊢ 𝐵 ∈ ℕ₀
8	7, 7	nn0mulcli 12422	. . . . . . . 8 ⊢ (𝐵 · 𝐵) ∈ ℕ₀
9	8, 3	deccl 12606	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)0 ∈ ℕ₀
10	9, 3	deccl 12606	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)00 ∈ ℕ₀
11	10	nn0cni 12396	. . . . 5 ⊢ ;;(𝐵 · 𝐵)00 ∈ ℂ
12	1	nn0cni 12396	. . . . . 6 ⊢ 𝐴 ∈ ℂ
13	12, 12	mulcli 11122	. . . . 5 ⊢ (𝐴 · 𝐴) ∈ ℂ
14	7	nn0cni 12396	. . . . . 6 ⊢ 𝐵 ∈ ℂ
15	14, 14	mulcli 11122	. . . . 5 ⊢ (𝐵 · 𝐵) ∈ ℂ
16		subadd4 11408	. . . . 5 ⊢ (((;;(𝐴 · 𝐴)00 ∈ ℂ ∧ ;;(𝐵 · 𝐵)00 ∈ ℂ) ∧ ((𝐴 · 𝐴) ∈ ℂ ∧ (𝐵 · 𝐵) ∈ ℂ)) → ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴))))
17	6, 11, 13, 15, 16	mp4an 693	. . . 4 ⊢ ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴)))
18		eqid 2729	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)00 = ;;(𝐴 · 𝐴)00
19	15	addlidi 11304	. . . . . 6 ⊢ (0 + (𝐵 · 𝐵)) = (𝐵 · 𝐵)
20	4, 3, 8, 18, 19	decaddi 12651	. . . . 5 ⊢ (;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) = ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)
21		eqid 2729	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)00 = ;;(𝐵 · 𝐵)00
22	13	addlidi 11304	. . . . . 6 ⊢ (0 + (𝐴 · 𝐴)) = (𝐴 · 𝐴)
23	9, 3, 2, 21, 22	decaddi 12651	. . . . 5 ⊢ (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴)) = ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)
24	20, 23	oveq12i 7361	. . . 4 ⊢ ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴))) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))
25	17, 24	eqtr2i 2753	. . 3 ⊢ (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
26		eqid 2729	. . . . 5 ⊢ ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
27	7, 1	nn0mulcli 12422	. . . . . . . 8 ⊢ (𝐵 · 𝐴) ∈ ℕ₀
28	1, 7, 27	numcl 12604	. . . . . . 7 ⊢ ((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
29	2, 28	deccl 12606	. . . . . 6 ⊢ ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
30		eqid 2729	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) = ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵)
31		eqid 2729	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) = ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)
32		eqid 2729	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))
33		eqid 2729	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)0 = ;(𝐵 · 𝐵)0
34	13, 15	addcomi 11307	. . . . . . 7 ⊢ ((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ((𝐵 · 𝐵) + (𝐴 · 𝐴))
35		eqid 2729	. . . . . . 7 ⊢ (((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0) = (((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
36	2, 28, 8, 3, 32, 33, 34, 35	decadd 12645	. . . . . 6 ⊢ (;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) + ;(𝐵 · 𝐵)0) = ;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
37	15, 13	addcomi 11307	. . . . . 6 ⊢ ((𝐵 · 𝐵) + (𝐴 · 𝐴)) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))
38	29, 8, 9, 2, 30, 31, 36, 37	decadd 12645	. . . . 5 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
39	8, 28	deccl 12606	. . . . . 6 ⊢ ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
40		eqid 2729	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) = ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)
41		eqid 2729	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) = ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)
42		eqid 2729	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))
43		eqid 2729	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)0 = ;(𝐴 · 𝐴)0
44		eqid 2729	. . . . . . 7 ⊢ ((𝐵 · 𝐵) + (𝐴 · 𝐴)) = ((𝐵 · 𝐵) + (𝐴 · 𝐴))
45	8, 28, 2, 3, 42, 43, 44, 35	decadd 12645	. . . . . 6 ⊢ (;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) + ;(𝐴 · 𝐴)0) = ;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
46		eqid 2729	. . . . . 6 ⊢ ((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))
47	39, 2, 4, 8, 40, 41, 45, 46	decadd 12645	. . . . 5 ⊢ (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
48	26, 38, 47	3eqtr4i 2762	. . . 4 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵))
49	29, 8	deccl 12606	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℕ₀
50	49	nn0cni 12396	. . . . 5 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℂ
51	9, 2	deccl 12606	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℕ₀
52	51	nn0cni 12396	. . . . 5 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℂ
53	39, 2	deccl 12606	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℕ₀
54	53	nn0cni 12396	. . . . 5 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℂ
55	4, 8	deccl 12606	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℕ₀
56	55	nn0cni 12396	. . . . 5 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℂ
57		addsubeq4com 42273	. . . . 5 ⊢ (((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℂ ∧ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℂ) ∧ (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℂ ∧ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℂ)) → ((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) ↔ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))))
58	50, 52, 54, 56, 57	mp4an 693	. . . 4 ⊢ ((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) ↔ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)))
59	48, 58	mpbi 230	. . 3 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))
60		10nn0 12609	. . . . . . 7 ⊢ ;10 ∈ ℕ₀
61	60, 3	deccl 12606	. . . . . 6 ⊢ ;;100 ∈ ℕ₀
62	61	nn0cni 12396	. . . . 5 ⊢ ;;100 ∈ ℂ
63		ax-1cn 11067	. . . . 5 ⊢ 1 ∈ ℂ
64	13, 15	subcli 11440	. . . . 5 ⊢ ((𝐴 · 𝐴) − (𝐵 · 𝐵)) ∈ ℂ
65	62, 63, 64	subdiri 11570	. . . 4 ⊢ ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) − (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))))
66	62, 13, 15	subdii 11569	. . . . . 6 ⊢ (;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 · (𝐴 · 𝐴)) − (;;100 · (𝐵 · 𝐵)))
67		eqid 2729	. . . . . . . 8 ⊢ ;;100 = ;;100
68	2	dec0u 12612	. . . . . . . 8 ⊢ (;10 · (𝐴 · 𝐴)) = ;(𝐴 · 𝐴)0
69	13	mul02i 11305	. . . . . . . 8 ⊢ (0 · (𝐴 · 𝐴)) = 0
70	2, 60, 3, 67, 68, 69	decmul1 12655	. . . . . . 7 ⊢ (;;100 · (𝐴 · 𝐴)) = ;;(𝐴 · 𝐴)00
71	8	dec0u 12612	. . . . . . . 8 ⊢ (;10 · (𝐵 · 𝐵)) = ;(𝐵 · 𝐵)0
72	15	mul02i 11305	. . . . . . . 8 ⊢ (0 · (𝐵 · 𝐵)) = 0
73	8, 60, 3, 67, 71, 72	decmul1 12655	. . . . . . 7 ⊢ (;;100 · (𝐵 · 𝐵)) = ;;(𝐵 · 𝐵)00
74	70, 73	oveq12i 7361	. . . . . 6 ⊢ ((;;100 · (𝐴 · 𝐴)) − (;;100 · (𝐵 · 𝐵))) = (;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00)
75	66, 74	eqtri 2752	. . . . 5 ⊢ (;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = (;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00)
76	64	mullidi 11120	. . . . 5 ⊢ (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((𝐴 · 𝐴) − (𝐵 · 𝐵))
77	75, 76	oveq12i 7361	. . . 4 ⊢ ((;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) − (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
78	65, 77	eqtri 2752	. . 3 ⊢ ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
79	25, 59, 78	3eqtr4i 2762	. 2 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
80		eqid 2729	. . . 4 ⊢ (𝐴 · 𝐴) = (𝐴 · 𝐴)
81		eqid 2729	. . . 4 ⊢ ((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ((𝐴 · 𝐵) + (𝐵 · 𝐴))
82		eqid 2729	. . . 4 ⊢ (𝐵 · 𝐵) = (𝐵 · 𝐵)
83	1, 7, 1, 7, 80, 81, 82	decpmulnc 42280	. . 3 ⊢ (;𝐴𝐵 · ;𝐴𝐵) = ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵)
84	14, 12	mulcli 11122	. . . . 5 ⊢ (𝐵 · 𝐴) ∈ ℂ
85	12, 14	mulcli 11122	. . . . 5 ⊢ (𝐴 · 𝐵) ∈ ℂ
86	84, 85	addcomi 11307	. . . 4 ⊢ ((𝐵 · 𝐴) + (𝐴 · 𝐵)) = ((𝐴 · 𝐵) + (𝐵 · 𝐴))
87	7, 1, 7, 1, 82, 86, 80	decpmulnc 42280	. . 3 ⊢ (;𝐵𝐴 · ;𝐵𝐴) = ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)
88	83, 87	oveq12i 7361	. 2 ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴))
89		9nn0 12408	. . . . . 6 ⊢ 9 ∈ ℕ₀
90	89, 89	deccl 12606	. . . . 5 ⊢ ;99 ∈ ℕ₀
91	90	nn0cni 12396	. . . 4 ⊢ ;99 ∈ ℂ
92		9p1e10 12593	. . . . . 6 ⊢ (9 + 1) = ;10
93		eqid 2729	. . . . . 6 ⊢ ;99 = ;99
94	89, 92, 93	decsucc 12632	. . . . 5 ⊢ (;99 + 1) = ;;100
95	91, 63, 94	addcomli 11308	. . . 4 ⊢ (1 + ;99) = ;;100
96	63, 91, 95	mvlladdi 11382	. . 3 ⊢ ;99 = (;;100 − 1)
97	96	oveq1i 7359	. 2 ⊢ (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
98	79, 88, 97	3eqtr4i 2762	1 ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 = wceq 1540 ∈ wcel 2109 (class class class)co 7349 ℂcc 11007 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 − cmin 11347 9c9 12190 ℕ₀cn0 12384 cdc 12591

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-pnf 11151 df-mnf 11152 df-ltxr 11154 df-sub 11349 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-dec 12592

This theorem is referenced by: sq3deccom12 42283

W3C validator