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 42407

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 12426	. . . . . . . 8 ⊢ (𝐴 · 𝐴) ∈ ℕ₀
3		0nn0 12403	. . . . . . . 8 ⊢ 0 ∈ ℕ₀
4	2, 3	deccl 12609	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)0 ∈ ℕ₀
5	4, 3	deccl 12609	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)00 ∈ ℕ₀
6	5	nn0cni 12400	. . . . 5 ⊢ ;;(𝐴 · 𝐴)00 ∈ ℂ
7		sqdeccom12.b	. . . . . . . . 9 ⊢ 𝐵 ∈ ℕ₀
8	7, 7	nn0mulcli 12426	. . . . . . . 8 ⊢ (𝐵 · 𝐵) ∈ ℕ₀
9	8, 3	deccl 12609	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)0 ∈ ℕ₀
10	9, 3	deccl 12609	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)00 ∈ ℕ₀
11	10	nn0cni 12400	. . . . 5 ⊢ ;;(𝐵 · 𝐵)00 ∈ ℂ
12	1	nn0cni 12400	. . . . . 6 ⊢ 𝐴 ∈ ℂ
13	12, 12	mulcli 11126	. . . . 5 ⊢ (𝐴 · 𝐴) ∈ ℂ
14	7	nn0cni 12400	. . . . . 6 ⊢ 𝐵 ∈ ℂ
15	14, 14	mulcli 11126	. . . . 5 ⊢ (𝐵 · 𝐵) ∈ ℂ
16		subadd4 11412	. . . . 5 ⊢ (((;;(𝐴 · 𝐴)00 ∈ ℂ ∧ ;;(𝐵 · 𝐵)00 ∈ ℂ) ∧ ((𝐴 · 𝐴) ∈ ℂ ∧ (𝐵 · 𝐵) ∈ ℂ)) → ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴))))
17	6, 11, 13, 15, 16	mp4an 693	. . . 4 ⊢ ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴)))
18		eqid 2733	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)00 = ;;(𝐴 · 𝐴)00
19	15	addlidi 11308	. . . . . 6 ⊢ (0 + (𝐵 · 𝐵)) = (𝐵 · 𝐵)
20	4, 3, 8, 18, 19	decaddi 12654	. . . . 5 ⊢ (;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) = ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)
21		eqid 2733	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)00 = ;;(𝐵 · 𝐵)00
22	13	addlidi 11308	. . . . . 6 ⊢ (0 + (𝐴 · 𝐴)) = (𝐴 · 𝐴)
23	9, 3, 2, 21, 22	decaddi 12654	. . . . 5 ⊢ (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴)) = ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)
24	20, 23	oveq12i 7364	. . . 4 ⊢ ((;;(𝐴 · 𝐴)00 + (𝐵 · 𝐵)) − (;;(𝐵 · 𝐵)00 + (𝐴 · 𝐴))) = (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴))
25	17, 24	eqtr2i 2757	. . 3 ⊢ (;;(𝐴 · 𝐴)0(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
26		eqid 2733	. . . . 5 ⊢ ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
27	7, 1	nn0mulcli 12426	. . . . . . . 8 ⊢ (𝐵 · 𝐴) ∈ ℕ₀
28	1, 7, 27	numcl 12607	. . . . . . 7 ⊢ ((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
29	2, 28	deccl 12609	. . . . . 6 ⊢ ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
30		eqid 2733	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) = ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵)
31		eqid 2733	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) = ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)
32		eqid 2733	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))
33		eqid 2733	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)0 = ;(𝐵 · 𝐵)0
34	13, 15	addcomi 11311	. . . . . . 7 ⊢ ((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ((𝐵 · 𝐵) + (𝐴 · 𝐴))
35		eqid 2733	. . . . . . 7 ⊢ (((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0) = (((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
36	2, 28, 8, 3, 32, 33, 34, 35	decadd 12648	. . . . . 6 ⊢ (;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴)) + ;(𝐵 · 𝐵)0) = ;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
37	15, 13	addcomi 11311	. . . . . 6 ⊢ ((𝐵 · 𝐵) + (𝐴 · 𝐴)) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))
38	29, 8, 9, 2, 30, 31, 36, 37	decadd 12648	. . . . 5 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
39	8, 28	deccl 12609	. . . . . 6 ⊢ ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) ∈ ℕ₀
40		eqid 2733	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) = ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)
41		eqid 2733	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) = ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)
42		eqid 2733	. . . . . . 7 ⊢ ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))
43		eqid 2733	. . . . . . 7 ⊢ ;(𝐴 · 𝐴)0 = ;(𝐴 · 𝐴)0
44		eqid 2733	. . . . . . 7 ⊢ ((𝐵 · 𝐵) + (𝐴 · 𝐴)) = ((𝐵 · 𝐵) + (𝐴 · 𝐴))
45	8, 28, 2, 3, 42, 43, 44, 35	decadd 12648	. . . . . 6 ⊢ (;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴)) + ;(𝐴 · 𝐴)0) = ;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)
46		eqid 2733	. . . . . 6 ⊢ ((𝐴 · 𝐴) + (𝐵 · 𝐵)) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))
47	39, 2, 4, 8, 40, 41, 45, 46	decadd 12648	. . . . 5 ⊢ (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵)) = ;;((𝐵 · 𝐵) + (𝐴 · 𝐴))(((𝐴 · 𝐵) + (𝐵 · 𝐴)) + 0)((𝐴 · 𝐴) + (𝐵 · 𝐵))
48	26, 38, 47	3eqtr4i 2766	. . . 4 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) + ;;(𝐵 · 𝐵)0(𝐴 · 𝐴)) = (;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) + ;;(𝐴 · 𝐴)0(𝐵 · 𝐵))
49	29, 8	deccl 12609	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℕ₀
50	49	nn0cni 12400	. . . . 5 ⊢ ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) ∈ ℂ
51	9, 2	deccl 12609	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℕ₀
52	51	nn0cni 12400	. . . . 5 ⊢ ;;(𝐵 · 𝐵)0(𝐴 · 𝐴) ∈ ℂ
53	39, 2	deccl 12609	. . . . . 6 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℕ₀
54	53	nn0cni 12400	. . . . 5 ⊢ ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴) ∈ ℂ
55	4, 8	deccl 12609	. . . . . 6 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℕ₀
56	55	nn0cni 12400	. . . . 5 ⊢ ;;(𝐴 · 𝐴)0(𝐵 · 𝐵) ∈ ℂ
57		addsubeq4com 42398	. . . . 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 12612	. . . . . . 7 ⊢ ;10 ∈ ℕ₀
61	60, 3	deccl 12609	. . . . . 6 ⊢ ;;100 ∈ ℕ₀
62	61	nn0cni 12400	. . . . 5 ⊢ ;;100 ∈ ℂ
63		ax-1cn 11071	. . . . 5 ⊢ 1 ∈ ℂ
64	13, 15	subcli 11444	. . . . 5 ⊢ ((𝐴 · 𝐴) − (𝐵 · 𝐵)) ∈ ℂ
65	62, 63, 64	subdiri 11574	. . . 4 ⊢ ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) − (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))))
66	62, 13, 15	subdii 11573	. . . . . 6 ⊢ (;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 · (𝐴 · 𝐴)) − (;;100 · (𝐵 · 𝐵)))
67		eqid 2733	. . . . . . . 8 ⊢ ;;100 = ;;100
68	2	dec0u 12615	. . . . . . . 8 ⊢ (;10 · (𝐴 · 𝐴)) = ;(𝐴 · 𝐴)0
69	13	mul02i 11309	. . . . . . . 8 ⊢ (0 · (𝐴 · 𝐴)) = 0
70	2, 60, 3, 67, 68, 69	decmul1 12658	. . . . . . 7 ⊢ (;;100 · (𝐴 · 𝐴)) = ;;(𝐴 · 𝐴)00
71	8	dec0u 12615	. . . . . . . 8 ⊢ (;10 · (𝐵 · 𝐵)) = ;(𝐵 · 𝐵)0
72	15	mul02i 11309	. . . . . . . 8 ⊢ (0 · (𝐵 · 𝐵)) = 0
73	8, 60, 3, 67, 71, 72	decmul1 12658	. . . . . . 7 ⊢ (;;100 · (𝐵 · 𝐵)) = ;;(𝐵 · 𝐵)00
74	70, 73	oveq12i 7364	. . . . . 6 ⊢ ((;;100 · (𝐴 · 𝐴)) − (;;100 · (𝐵 · 𝐵))) = (;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00)
75	66, 74	eqtri 2756	. . . . 5 ⊢ (;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = (;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00)
76	64	mullidi 11124	. . . . 5 ⊢ (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((𝐴 · 𝐴) − (𝐵 · 𝐵))
77	75, 76	oveq12i 7364	. . . 4 ⊢ ((;;100 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) − (1 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
78	65, 77	eqtri 2756	. . 3 ⊢ ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;(𝐴 · 𝐴)00 − ;;(𝐵 · 𝐵)00) − ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
79	25, 59, 78	3eqtr4i 2766	. 2 ⊢ (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)) = ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
80		eqid 2733	. . . 4 ⊢ (𝐴 · 𝐴) = (𝐴 · 𝐴)
81		eqid 2733	. . . 4 ⊢ ((𝐴 · 𝐵) + (𝐵 · 𝐴)) = ((𝐴 · 𝐵) + (𝐵 · 𝐴))
82		eqid 2733	. . . 4 ⊢ (𝐵 · 𝐵) = (𝐵 · 𝐵)
83	1, 7, 1, 7, 80, 81, 82	decpmulnc 42405	. . 3 ⊢ (;𝐴𝐵 · ;𝐴𝐵) = ;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵)
84	14, 12	mulcli 11126	. . . . 5 ⊢ (𝐵 · 𝐴) ∈ ℂ
85	12, 14	mulcli 11126	. . . . 5 ⊢ (𝐴 · 𝐵) ∈ ℂ
86	84, 85	addcomi 11311	. . . 4 ⊢ ((𝐵 · 𝐴) + (𝐴 · 𝐵)) = ((𝐴 · 𝐵) + (𝐵 · 𝐴))
87	7, 1, 7, 1, 82, 86, 80	decpmulnc 42405	. . 3 ⊢ (;𝐵𝐴 · ;𝐵𝐴) = ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴)
88	83, 87	oveq12i 7364	. 2 ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;;(𝐴 · 𝐴)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐵 · 𝐵) − ;;(𝐵 · 𝐵)((𝐴 · 𝐵) + (𝐵 · 𝐴))(𝐴 · 𝐴))
89		9nn0 12412	. . . . . 6 ⊢ 9 ∈ ℕ₀
90	89, 89	deccl 12609	. . . . 5 ⊢ ;99 ∈ ℕ₀
91	90	nn0cni 12400	. . . 4 ⊢ ;99 ∈ ℂ
92		9p1e10 12596	. . . . . 6 ⊢ (9 + 1) = ;10
93		eqid 2733	. . . . . 6 ⊢ ;99 = ;99
94	89, 92, 93	decsucc 12635	. . . . 5 ⊢ (;99 + 1) = ;;100
95	91, 63, 94	addcomli 11312	. . . 4 ⊢ (1 + ;99) = ;;100
96	63, 91, 95	mvlladdi 11386	. . 3 ⊢ ;99 = (;;100 − 1)
97	96	oveq1i 7362	. 2 ⊢ (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) = ((;;100 − 1) · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))
98	79, 88, 97	3eqtr4i 2766	1 ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵)))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 = wceq 1541 ∈ wcel 2113 (class class class)co 7352 ℂcc 11011 0cc0 11013 1c1 11014 + caddc 11016 · cmul 11018 − cmin 11351 9c9 12194 ℕ₀cn0 12388 cdc 12594

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 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-iun 4943 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 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 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-pnf 11155 df-mnf 11156 df-ltxr 11158 df-sub 11353 df-nn 12133 df-2 12195 df-3 12196 df-4 12197 df-5 12198 df-6 12199 df-7 12200 df-8 12201 df-9 12202 df-n0 12389 df-dec 12595

This theorem is referenced by: sq3deccom12 42408

W3C validator