2sqlem4 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 2sqlem4		GIF version

Theorem 2sqlem4 14761

Description: Lemma for 2sqlem5 14762. (Contributed by Mario Carneiro, 20-Jun-2015.)

**Hypotheses**
Ref	Expression
2sq.1	⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
2sqlem5.1	⊢ (𝜑 → 𝑁 ∈ ℕ)
2sqlem5.2	⊢ (𝜑 → 𝑃 ∈ ℙ)
2sqlem4.3	⊢ (𝜑 → 𝐴 ∈ ℤ)
2sqlem4.4	⊢ (𝜑 → 𝐵 ∈ ℤ)
2sqlem4.5	⊢ (𝜑 → 𝐶 ∈ ℤ)
2sqlem4.6	⊢ (𝜑 → 𝐷 ∈ ℤ)
2sqlem4.7	⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2)))
2sqlem4.8	⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2)))

**Assertion**
Ref	Expression
2sqlem4	⊢ (𝜑 → 𝑁 ∈ 𝑆)

**Proof of Theorem 2sqlem4**
Step	Hyp	Ref	Expression
1		2sq.1	. . 3 ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
2		2sqlem5.1	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
3	2	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) → 𝑁 ∈ ℕ)
4		2sqlem5.2	. . . 4 ⊢ (𝜑 → 𝑃 ∈ ℙ)
5	4	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) → 𝑃 ∈ ℙ)
6		2sqlem4.3	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℤ)
7	6	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) → 𝐴 ∈ ℤ)
8		2sqlem4.4	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℤ)
9	8	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) → 𝐵 ∈ ℤ)
10		2sqlem4.5	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℤ)
11	10	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) → 𝐶 ∈ ℤ)
12		2sqlem4.6	. . . 4 ⊢ (𝜑 → 𝐷 ∈ ℤ)
13	12	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) → 𝐷 ∈ ℤ)
14		2sqlem4.7	. . . 4 ⊢ (𝜑 → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2)))
15	14	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) → (𝑁 · 𝑃) = ((𝐴↑2) + (𝐵↑2)))
16		2sqlem4.8	. . . 4 ⊢ (𝜑 → 𝑃 = ((𝐶↑2) + (𝐷↑2)))
17	16	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) → 𝑃 = ((𝐶↑2) + (𝐷↑2)))
18		simpr 110	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) → 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷)))
19	1, 3, 5, 7, 9, 11, 13, 15, 17, 18	2sqlem3 14760	. 2 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷))) → 𝑁 ∈ 𝑆)
20	2	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))) → 𝑁 ∈ ℕ)
21	4	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))) → 𝑃 ∈ ℙ)
22	6	znegcld 9391	. . . 4 ⊢ (𝜑 → -𝐴 ∈ ℤ)
23	22	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))) → -𝐴 ∈ ℤ)
24	8	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))) → 𝐵 ∈ ℤ)
25	10	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))) → 𝐶 ∈ ℤ)
26	12	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))) → 𝐷 ∈ ℤ)
27	6	zcnd 9390	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
28		sqneg 10593	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2))
29	27, 28	syl 14	. . . . . 6 ⊢ (𝜑 → (-𝐴↑2) = (𝐴↑2))
30	29	oveq1d 5903	. . . . 5 ⊢ (𝜑 → ((-𝐴↑2) + (𝐵↑2)) = ((𝐴↑2) + (𝐵↑2)))
31	14, 30	eqtr4d 2223	. . . 4 ⊢ (𝜑 → (𝑁 · 𝑃) = ((-𝐴↑2) + (𝐵↑2)))
32	31	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))) → (𝑁 · 𝑃) = ((-𝐴↑2) + (𝐵↑2)))
33	16	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))) → 𝑃 = ((𝐶↑2) + (𝐷↑2)))
34	12	zcnd 9390	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℂ)
35	27, 34	mulneg1d 8382	. . . . . . 7 ⊢ (𝜑 → (-𝐴 · 𝐷) = -(𝐴 · 𝐷))
36	35	oveq2d 5904	. . . . . 6 ⊢ (𝜑 → ((𝐶 · 𝐵) + (-𝐴 · 𝐷)) = ((𝐶 · 𝐵) + -(𝐴 · 𝐷)))
37	10, 8	zmulcld 9395	. . . . . . . 8 ⊢ (𝜑 → (𝐶 · 𝐵) ∈ ℤ)
38	37	zcnd 9390	. . . . . . 7 ⊢ (𝜑 → (𝐶 · 𝐵) ∈ ℂ)
39	6, 12	zmulcld 9395	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℤ)
40	39	zcnd 9390	. . . . . . 7 ⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
41	38, 40	negsubd 8288	. . . . . 6 ⊢ (𝜑 → ((𝐶 · 𝐵) + -(𝐴 · 𝐷)) = ((𝐶 · 𝐵) − (𝐴 · 𝐷)))
42	36, 41	eqtrd 2220	. . . . 5 ⊢ (𝜑 → ((𝐶 · 𝐵) + (-𝐴 · 𝐷)) = ((𝐶 · 𝐵) − (𝐴 · 𝐷)))
43	42	breq2d 4027	. . . 4 ⊢ (𝜑 → (𝑃 ∥ ((𝐶 · 𝐵) + (-𝐴 · 𝐷)) ↔ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))))
44	43	biimpar 297	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))) → 𝑃 ∥ ((𝐶 · 𝐵) + (-𝐴 · 𝐷)))
45	1, 20, 21, 23, 24, 25, 26, 32, 33, 44	2sqlem3 14760	. 2 ⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))) → 𝑁 ∈ 𝑆)
46		prmz 12125	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
47	4, 46	syl 14	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ ℤ)
48		zsqcl 10605	. . . . . . . 8 ⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈ ℤ)
49	10, 48	syl 14	. . . . . . 7 ⊢ (𝜑 → (𝐶↑2) ∈ ℤ)
50	2	nnzd 9388	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ)
51	49, 50	zmulcld 9395	. . . . . 6 ⊢ (𝜑 → ((𝐶↑2) · 𝑁) ∈ ℤ)
52		zsqcl 10605	. . . . . . 7 ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
53	6, 52	syl 14	. . . . . 6 ⊢ (𝜑 → (𝐴↑2) ∈ ℤ)
54	51, 53	zsubcld 9394	. . . . 5 ⊢ (𝜑 → (((𝐶↑2) · 𝑁) − (𝐴↑2)) ∈ ℤ)
55		dvdsmul1 11834	. . . . 5 ⊢ ((𝑃 ∈ ℤ ∧ (((𝐶↑2) · 𝑁) − (𝐴↑2)) ∈ ℤ) → 𝑃 ∥ (𝑃 · (((𝐶↑2) · 𝑁) − (𝐴↑2))))
56	47, 54, 55	syl2anc 411	. . . 4 ⊢ (𝜑 → 𝑃 ∥ (𝑃 · (((𝐶↑2) · 𝑁) − (𝐴↑2))))
57	10, 6	zmulcld 9395	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · 𝐴) ∈ ℤ)
58	57	zcnd 9390	. . . . . . . 8 ⊢ (𝜑 → (𝐶 · 𝐴) ∈ ℂ)
59	58	sqcld 10666	. . . . . . 7 ⊢ (𝜑 → ((𝐶 · 𝐴)↑2) ∈ ℂ)
60	38	sqcld 10666	. . . . . . 7 ⊢ (𝜑 → ((𝐶 · 𝐵)↑2) ∈ ℂ)
61	40	sqcld 10666	. . . . . . 7 ⊢ (𝜑 → ((𝐴 · 𝐷)↑2) ∈ ℂ)
62	59, 60, 61	pnpcand 8319	. . . . . 6 ⊢ (𝜑 → ((((𝐶 · 𝐴)↑2) + ((𝐶 · 𝐵)↑2)) − (((𝐶 · 𝐴)↑2) + ((𝐴 · 𝐷)↑2))) = (((𝐶 · 𝐵)↑2) − ((𝐴 · 𝐷)↑2)))
63	10	zcnd 9390	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
64	63, 27	sqmuld 10680	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 · 𝐴)↑2) = ((𝐶↑2) · (𝐴↑2)))
65	8	zcnd 9390	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
66	63, 65	sqmuld 10680	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 · 𝐵)↑2) = ((𝐶↑2) · (𝐵↑2)))
67	64, 66	oveq12d 5906	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 · 𝐴)↑2) + ((𝐶 · 𝐵)↑2)) = (((𝐶↑2) · (𝐴↑2)) + ((𝐶↑2) · (𝐵↑2))))
68	63	sqcld 10666	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
69	53	zcnd 9390	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
70	65	sqcld 10666	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
71	68, 69, 70	adddid 7996	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑2) · ((𝐴↑2) + (𝐵↑2))) = (((𝐶↑2) · (𝐴↑2)) + ((𝐶↑2) · (𝐵↑2))))
72	67, 71	eqtr4d 2223	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 · 𝐴)↑2) + ((𝐶 · 𝐵)↑2)) = ((𝐶↑2) · ((𝐴↑2) + (𝐵↑2))))
73	2	nncnd 8947	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
74	47	zcnd 9390	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℂ)
75	73, 74	mulcomd 7993	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 · 𝑃) = (𝑃 · 𝑁))
76	14, 75	eqtr3d 2222	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝑃 · 𝑁))
77	76	oveq2d 5904	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑2) · ((𝐴↑2) + (𝐵↑2))) = ((𝐶↑2) · (𝑃 · 𝑁)))
78	68, 74, 73	mul12d 8123	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑2) · (𝑃 · 𝑁)) = (𝑃 · ((𝐶↑2) · 𝑁)))
79	77, 78	eqtrd 2220	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶↑2) · ((𝐴↑2) + (𝐵↑2))) = (𝑃 · ((𝐶↑2) · 𝑁)))
80	72, 79	eqtrd 2220	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 · 𝐴)↑2) + ((𝐶 · 𝐵)↑2)) = (𝑃 · ((𝐶↑2) · 𝑁)))
81	27, 34	sqmuld 10680	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 · 𝐷)↑2) = ((𝐴↑2) · (𝐷↑2)))
82	34	sqcld 10666	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
83	69, 82	mulcomd 7993	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴↑2) · (𝐷↑2)) = ((𝐷↑2) · (𝐴↑2)))
84	81, 83	eqtrd 2220	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷)↑2) = ((𝐷↑2) · (𝐴↑2)))
85	64, 84	oveq12d 5906	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶 · 𝐴)↑2) + ((𝐴 · 𝐷)↑2)) = (((𝐶↑2) · (𝐴↑2)) + ((𝐷↑2) · (𝐴↑2))))
86	49	zcnd 9390	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
87	86, 82, 69	adddird 7997	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) · (𝐴↑2)) = (((𝐶↑2) · (𝐴↑2)) + ((𝐷↑2) · (𝐴↑2))))
88	85, 87	eqtr4d 2223	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶 · 𝐴)↑2) + ((𝐴 · 𝐷)↑2)) = (((𝐶↑2) + (𝐷↑2)) · (𝐴↑2)))
89	16	oveq1d 5903	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 · (𝐴↑2)) = (((𝐶↑2) + (𝐷↑2)) · (𝐴↑2)))
90	88, 89	eqtr4d 2223	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 · 𝐴)↑2) + ((𝐴 · 𝐷)↑2)) = (𝑃 · (𝐴↑2)))
91	80, 90	oveq12d 5906	. . . . . . 7 ⊢ (𝜑 → ((((𝐶 · 𝐴)↑2) + ((𝐶 · 𝐵)↑2)) − (((𝐶 · 𝐴)↑2) + ((𝐴 · 𝐷)↑2))) = ((𝑃 · ((𝐶↑2) · 𝑁)) − (𝑃 · (𝐴↑2))))
92	51	zcnd 9390	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑2) · 𝑁) ∈ ℂ)
93	74, 92, 69	subdid 8385	. . . . . . 7 ⊢ (𝜑 → (𝑃 · (((𝐶↑2) · 𝑁) − (𝐴↑2))) = ((𝑃 · ((𝐶↑2) · 𝑁)) − (𝑃 · (𝐴↑2))))
94	91, 93	eqtr4d 2223	. . . . . 6 ⊢ (𝜑 → ((((𝐶 · 𝐴)↑2) + ((𝐶 · 𝐵)↑2)) − (((𝐶 · 𝐴)↑2) + ((𝐴 · 𝐷)↑2))) = (𝑃 · (((𝐶↑2) · 𝑁) − (𝐴↑2))))
95	62, 94	eqtr3d 2222	. . . . 5 ⊢ (𝜑 → (((𝐶 · 𝐵)↑2) − ((𝐴 · 𝐷)↑2)) = (𝑃 · (((𝐶↑2) · 𝑁) − (𝐴↑2))))
96		subsq 10641	. . . . . 6 ⊢ (((𝐶 · 𝐵) ∈ ℂ ∧ (𝐴 · 𝐷) ∈ ℂ) → (((𝐶 · 𝐵)↑2) − ((𝐴 · 𝐷)↑2)) = (((𝐶 · 𝐵) + (𝐴 · 𝐷)) · ((𝐶 · 𝐵) − (𝐴 · 𝐷))))
97	38, 40, 96	syl2anc 411	. . . . 5 ⊢ (𝜑 → (((𝐶 · 𝐵)↑2) − ((𝐴 · 𝐷)↑2)) = (((𝐶 · 𝐵) + (𝐴 · 𝐷)) · ((𝐶 · 𝐵) − (𝐴 · 𝐷))))
98	95, 97	eqtr3d 2222	. . . 4 ⊢ (𝜑 → (𝑃 · (((𝐶↑2) · 𝑁) − (𝐴↑2))) = (((𝐶 · 𝐵) + (𝐴 · 𝐷)) · ((𝐶 · 𝐵) − (𝐴 · 𝐷))))
99	56, 98	breqtrd 4041	. . 3 ⊢ (𝜑 → 𝑃 ∥ (((𝐶 · 𝐵) + (𝐴 · 𝐷)) · ((𝐶 · 𝐵) − (𝐴 · 𝐷))))
100	37, 39	zaddcld 9393	. . . 4 ⊢ (𝜑 → ((𝐶 · 𝐵) + (𝐴 · 𝐷)) ∈ ℤ)
101	37, 39	zsubcld 9394	. . . 4 ⊢ (𝜑 → ((𝐶 · 𝐵) − (𝐴 · 𝐷)) ∈ ℤ)
102		euclemma 12160	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ ((𝐶 · 𝐵) + (𝐴 · 𝐷)) ∈ ℤ ∧ ((𝐶 · 𝐵) − (𝐴 · 𝐷)) ∈ ℤ) → (𝑃 ∥ (((𝐶 · 𝐵) + (𝐴 · 𝐷)) · ((𝐶 · 𝐵) − (𝐴 · 𝐷))) ↔ (𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷)) ∨ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷)))))
103	4, 100, 101, 102	syl3anc 1248	. . 3 ⊢ (𝜑 → (𝑃 ∥ (((𝐶 · 𝐵) + (𝐴 · 𝐷)) · ((𝐶 · 𝐵) − (𝐴 · 𝐷))) ↔ (𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷)) ∨ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷)))))
104	99, 103	mpbid 147	. 2 ⊢ (𝜑 → (𝑃 ∥ ((𝐶 · 𝐵) + (𝐴 · 𝐷)) ∨ 𝑃 ∥ ((𝐶 · 𝐵) − (𝐴 · 𝐷))))
105	19, 45, 104	mpjaodan 799	1 ⊢ (𝜑 → 𝑁 ∈ 𝑆)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 = wceq 1363 ∈ wcel 2158 class class class wbr 4015 ↦ cmpt 4076 ran crn 4639 ‘cfv 5228 (class class class)co 5888 ℂcc 7823 + caddc 7828 · cmul 7830 − cmin 8142 -cneg 8143 ℕcn 8933 2c2 8984 ℤcz 9267 ↑cexp 10533 abscabs 11020 ∥ cdvds 11808 ℙcprime 12121 ℤ[i]cgz 12381

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-coll 4130 ax-sep 4133 ax-nul 4141 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-setind 4548 ax-iinf 4599 ax-cnex 7916 ax-resscn 7917 ax-1cn 7918 ax-1re 7919 ax-icn 7920 ax-addcl 7921 ax-addrcl 7922 ax-mulcl 7923 ax-mulrcl 7924 ax-addcom 7925 ax-mulcom 7926 ax-addass 7927 ax-mulass 7928 ax-distr 7929 ax-i2m1 7930 ax-0lt1 7931 ax-1rid 7932 ax-0id 7933 ax-rnegex 7934 ax-precex 7935 ax-cnre 7936 ax-pre-ltirr 7937 ax-pre-ltwlin 7938 ax-pre-lttrn 7939 ax-pre-apti 7940 ax-pre-ltadd 7941 ax-pre-mulgt0 7942 ax-pre-mulext 7943 ax-arch 7944 ax-caucvg 7945

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ne 2358 df-nel 2453 df-ral 2470 df-rex 2471 df-reu 2472 df-rmo 2473 df-rab 2474 df-v 2751 df-sbc 2975 df-csb 3070 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-nul 3435 df-if 3547 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-int 3857 df-iun 3900 df-br 4016 df-opab 4077 df-mpt 4078 df-tr 4114 df-id 4305 df-po 4308 df-iso 4309 df-iord 4378 df-on 4380 df-ilim 4381 df-suc 4383 df-iom 4602 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-rn 4649 df-res 4650 df-ima 4651 df-iota 5190 df-fun 5230 df-fn 5231 df-f 5232 df-f1 5233 df-fo 5234 df-f1o 5235 df-fv 5236 df-riota 5844 df-ov 5891 df-oprab 5892 df-mpo 5893 df-1st 6155 df-2nd 6156 df-recs 6320 df-frec 6406 df-1o 6431 df-2o 6432 df-er 6549 df-en 6755 df-sup 6997 df-pnf 8008 df-mnf 8009 df-xr 8010 df-ltxr 8011 df-le 8012 df-sub 8144 df-neg 8145 df-reap 8546 df-ap 8553 df-div 8644 df-inn 8934 df-2 8992 df-3 8993 df-4 8994 df-n0 9191 df-z 9268 df-uz 9543 df-q 9634 df-rp 9668 df-fz 10023 df-fzo 10157 df-fl 10284 df-mod 10337 df-seqfrec 10460 df-exp 10534 df-cj 10865 df-re 10866 df-im 10867 df-rsqrt 11021 df-abs 11022 df-dvds 11809 df-gcd 11958 df-prm 12122 df-gz 12382

This theorem is referenced by: 2sqlem5 14762

W3C validator