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 42846

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 12509	. . . . . . . 8 ⊢ (𝐴 · 𝐴) ∈ ℕ₀
3		0nn0 12486	. . . . . . . 8 ⊢ 0 ∈ ℕ₀
4	2, 3	deccl 12693	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)0 ∈ ℕ₀
5	4, 3	deccl 12693	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)00 ∈ ℕ₀
6	5	nn0cni 12483	. . . . 5 ⊢ ;;(𝐴 · 𝐴)00 ∈ ℂ
7		sqdeccom12.b	. . . . . . . . 9 ⊢ 𝐵 ∈ ℕ₀
8	7, 7	nn0mulcli 12509	. . . . . . . 8 ⊢ (𝐵 · 𝐵) ∈ ℕ₀
9	8, 3	deccl 12693	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)0 ∈ ℕ₀
10	9, 3	deccl 12693	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)00 ∈ ℕ₀
11	10	nn0cni 12483	. . . . 5 ⊢ ;;(𝐵 · 𝐵)00 ∈ ℂ
12	1	nn0cni 12483	. . . . . 6 ⊢ 𝐴 ∈ ℂ
13	12, 12	mulcli 11179	. . . . 5 ⊢ (𝐴 · 𝐴) ∈ ℂ
14	7	nn0cni 12483	. . . . . 6 ⊢ 𝐵 ∈ ℂ
15	14, 14	mulcli 11179	. . . . 5 ⊢ (𝐵 · 𝐵) ∈ ℂ
16		subadd4 11465	. . . . 5 ⊢ (((;;(𝐴 · 𝐴)00 ∈ ℂ ∧ ;;(𝐵 · 𝐵)00 ∈ ℂ) ∧ ((𝐴 · 𝐴) ∈ ℂ ∧ (𝐵 · 𝐵) ∈ ℂ)) → ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴))))
17	6, 11, 13, 15, 16	mp4an 701	. . . 4 ⊢ ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴)))
18		eqid 2756	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)00 = ;;(𝐴 · 𝐴)00
19	15	addlidi 11361	. . . . . 6 ⊢ (0 + (𝐵 · 𝐵)) = (𝐵 · 𝐵)
20	4, 3, 8, 18, 19	decaddi 12743	. . . . 5 ⊢ (;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) = ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)
21		eqid 2756	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)00 = ;;(𝐵 · 𝐵)00
22	13	addlidi 11361	. . . . . 6 ⊢ (0 + (𝐴 · 𝐴)) = (𝐴 · 𝐴)
23	9, 3, 2, 21, 22	decaddi 12743	. . . . 5 ⊢ (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴)) = ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)
24	20, 23	oveq12i 7397	. . . 4 ⊢ ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴))) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))
25	17, 24	eqtr2i 2780	. . 3 ⊢ (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
26		eqid 2756	. . . . 5 ⊢ ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
27	7, 1	nn0mulcli 12509	. . . . . . . 8 ⊢ (𝐵 · 𝐴) ∈ ℕ₀
28	1, 7, 27	numcl 12691	. . . . . . 7 ⊢ ((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
29	2, 28	deccl 12693	. . . . . 6 ⊢ ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
30		eqid 2756	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) = ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵)
31		eqid 2756	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) = ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)
32		eqid 2756	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))
33		eqid 2756	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)0 = ;(𝐵 · 𝐵)0
34	13, 15	addcomi 11364	. . . . . . 7 ⊢ ((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ((𝐵 · 𝐵) + (𝐴 · 𝐴))
35		eqid 2756	. . . . . . 7 ⊢ (((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0) = (((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
36	2, 28, 8, 3, 32, 33, 34, 35	decadd 12737	. . . . . 6 ⊢ (;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) + ;(𝐵 · 𝐵)0) = ;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
37	15, 13	addcomi 11364	. . . . . 6 ⊢ ((𝐵 · 𝐵) + (𝐴 · 𝐴)) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))
38	29, 8, 9, 2, 30, 31, 36, 37	decadd 12737	. . . . 5 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
39	8, 28	deccl 12693	. . . . . 6 ⊢ ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
40		eqid 2756	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) = ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)
41		eqid 2756	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) = ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)
42		eqid 2756	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))
43		eqid 2756	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)0 = ;(𝐴 · 𝐴)0
44		eqid 2756	. . . . . . 7 ⊢ ((𝐵 · 𝐵) + (𝐴 · 𝐴)) = ((𝐵 · 𝐵) + (𝐴 · 𝐴))
45	8, 28, 2, 3, 42, 43, 44, 35	decadd 12737	. . . . . 6 ⊢ (;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) + ;(𝐴 · 𝐴)0) = ;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
46		eqid 2756	. . . . . 6 ⊢ ((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))
47	39, 2, 4, 8, 40, 41, 45, 46	decadd 12737	. . . . 5 ⊢ (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
48	26, 38, 47	3eqtr4i 2789	. . . 4 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵))
49	29, 8	deccl 12693	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℕ₀
50	49	nn0cni 12483	. . . . 5 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℂ
51	9, 2	deccl 12693	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℕ₀
52	51	nn0cni 12483	. . . . 5 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℂ
53	39, 2	deccl 12693	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℕ₀
54	53	nn0cni 12483	. . . . 5 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℂ
55	4, 8	deccl 12693	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℕ₀
56	55	nn0cni 12483	. . . . 5 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℂ
57		addsubeq4com 42837	. . . . 5 ⊢ (((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℂ ∧ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℂ) ∧ (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℂ ∧ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℂ)) → ((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) ↔ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))))
58	50, 52, 54, 56, 57	mp4an 701	. . . 4 ⊢ ((;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) ↔ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)))
59	48, 58	mpbi 232	. . 3 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))
60		10nn0 12700	. . . . . . 7 ⊢ ;10 ∈ ℕ₀
61	60, 3	deccl 12693	. . . . . 6 ⊢ ;;100 ∈ ℕ₀
62	61	nn0cni 12483	. . . . 5 ⊢ ;;100 ∈ ℂ
63		ax-1cn 11121	. . . . 5 ⊢ 1 ∈ ℂ
64	13, 15	subcli 11497	. . . . 5 ⊢ ((𝐴 · 𝐴) − (𝐵 · 𝐵)) ∈ ℂ
65	62, 63, 64	subdiri 11627	. . . 4 ⊢ ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) − (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))))
66	62, 13, 15	subdii 11626	. . . . . 6 ⊢ (;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 · (𝐴 · 𝐴)) − (;;100 · (𝐵 · 𝐵)))
67		eqid 2756	. . . . . . . 8 ⊢ ;;100 = ;;100
68	2	dec0u 12704	. . . . . . . 8 ⊢ (;10 · (𝐴 · 𝐴)) = ;(𝐴 · 𝐴)0
69	13	mul02i 11362	. . . . . . . 8 ⊢ (0 · (𝐴 · 𝐴)) = 0
70	2, 60, 3, 67, 68, 69	decmul1 12747	. . . . . . 7 ⊢ (;;100 · (𝐴 · 𝐴)) = ;;(𝐴 · 𝐴)00
71	8	dec0u 12704	. . . . . . . 8 ⊢ (;10 · (𝐵 · 𝐵)) = ;(𝐵 · 𝐵)0
72	15	mul02i 11362	. . . . . . . 8 ⊢ (0 · (𝐵 · 𝐵)) = 0
73	8, 60, 3, 67, 71, 72	decmul1 12747	. . . . . . 7 ⊢ (;;100 · (𝐵 · 𝐵)) = ;;(𝐵 · 𝐵)00
74	70, 73	oveq12i 7397	. . . . . 6 ⊢ ((;;100 · (𝐴 · 𝐴)) − (;;100 · (𝐵 · 𝐵))) = (;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00)
75	66, 74	eqtri 2779	. . . . 5 ⊢ (;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = (;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00)
76	64	mullidi 11177	. . . . 5 ⊢ (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((𝐴 · 𝐴) − (𝐵 · 𝐵))
77	75, 76	oveq12i 7397	. . . 4 ⊢ ((;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) − (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
78	65, 77	eqtri 2779	. . 3 ⊢ ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
79	25, 59, 78	3eqtr4i 2789	. 2 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
80		eqid 2756	. . . 4 ⊢ (𝐴 · 𝐴) = (𝐴 · 𝐴)
81		eqid 2756	. . . 4 ⊢ ((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ((𝐴 · 𝐵) + (𝐵 · 𝐴))
82		eqid 2756	. . . 4 ⊢ (𝐵 · 𝐵) = (𝐵 · 𝐵)
83	1, 7, 1, 7, 80, 81, 82	decpmulnc 42844	. . 3 ⊢ (;𝐴𝐵 · ;𝐴𝐵) = ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵)
84	14, 12	mulcli 11179	. . . . 5 ⊢ (𝐵 · 𝐴) ∈ ℂ
85	12, 14	mulcli 11179	. . . . 5 ⊢ (𝐴 · 𝐵) ∈ ℂ
86	84, 85	addcomi 11364	. . . 4 ⊢ ((𝐵 · 𝐴) + (𝐴 · 𝐵)) = ((𝐴 · 𝐵) + (𝐵 · 𝐴))
87	7, 1, 7, 1, 82, 86, 80	decpmulnc 42844	. . 3 ⊢ (;𝐵𝐴 · ;𝐵𝐴) = ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)
88	83, 87	oveq12i 7397	. 2 ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴))
89		9nn0 12495	. . . . . 6 ⊢ 9 ∈ ℕ₀
90	89, 89	deccl 12693	. . . . 5 ⊢ ;99 ∈ ℕ₀
91	90	nn0cni 12483	. . . 4 ⊢ ;99 ∈ ℂ
92		9p1e10 12680	. . . . . 6 ⊢ (9 + 1) = ;10
93		eqid 2756	. . . . . 6 ⊢ ;99 = ;99
94	89, 92, 93	decsucc 12724	. . . . 5 ⊢ (;99 + 1) = ;;100
95	91, 63, 94	addcomli 11365	. . . 4 ⊢ (1 + ;99) = ;;100
96	63, 91, 95	mvlladdi 11439	. . 3 ⊢ ;99 = (;;100 − 1)
97	96	oveq1i 7395	. 2 ⊢ (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
98	79, 88, 97	3eqtr4i 2789	1 ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 = wceq 1554 ∈ wcel 2136 (class class class)co 7385 ℂcc 11061 0cc0 11063 1c1 11064 + caddc 11066 · cmul 11068 − cmin 11404 9c9 12269 ℕ₀cn0 12471 cdc 12678

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1809 ax-4 1823 ax-5 1924 ax-6 1981 ax-7 2022 ax-8 2138 ax-9 2146 ax-10 2169 ax-11 2185 ax-12 2206 ax-ext 2728 ax-sep 5240 ax-nul 5250 ax-pow 5316 ax-pr 5384 ax-un 7707 ax-resscn 11120 ax-1cn 11121 ax-icn 11122 ax-addcl 11123 ax-addrcl 11124 ax-mulcl 11125 ax-mulrcl 11126 ax-mulcom 11127 ax-addass 11128 ax-mulass 11129 ax-distr 11130 ax-i2m1 11131 ax-1ne0 11132 ax-1rid 11133 ax-rnegex 11134 ax-rrecex 11135 ax-cnre 11136 ax-pre-lttri 11137 ax-pre-lttrn 11138 ax-pre-ltadd 11139

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1557 df-fal 1567 df-ex 1794 df-nf 1798 df-sb 2085 df-mo 2560 df-eu 2590 df-clab 2735 df-cleq 2748 df-clel 2831 df-nfc 2905 df-ne 2952 df-nel 3056 df-ral 3071 df-rex 3081 df-reu 3362 df-rab 3409 df-v 3450 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4281 df-if 4475 df-pw 4551 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-iun 4945 df-br 5095 df-opab 5157 df-mpt 5176 df-tr 5202 df-id 5535 df-eprel 5540 df-po 5548 df-so 5549 df-fr 5593 df-we 5595 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6466 df-fun 6512 df-fn 6513 df-f 6514 df-f1 6515 df-fo 6516 df-f1o 6517 df-fv 6518 df-riota 7342 df-ov 7388 df-oprab 7389 df-mpo 7390 df-om 7836 df-2nd 7960 df-frecs 8250 df-wrecs 8281 df-recs 8330 df-rdg 8369 df-er 8666 df-en 8917 df-dom 8918 df-sdom 8919 df-pnf 11208 df-mnf 11209 df-ltxr 11211 df-sub 11406 df-nn 12201 df-2 12270 df-3 12271 df-4 12272 df-5 12273 df-6 12274 df-7 12275 df-8 12276 df-9 12277 df-n0 12472 df-dec 12679

This theorem is referenced by: sq3deccom12 42847

W3C validator