2sqreunnltlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 2sqreunnltlem		Structured version Visualization version GIF version

Theorem 2sqreunnltlem 27580

Description: Lemma for 2sqreunnlt 27590. (Contributed by AV, 4-Jun-2023.) Specialization to different integers, proposed by GL. (Revised by AV, 11-Jun-2023.)

**Assertion**
Ref	Expression
2sqreunnltlem	⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))

Distinct variable group: 𝑃,𝑎,𝑏

**Proof of Theorem 2sqreunnltlem**
Step	Hyp	Ref	Expression
1		2sqreunnlem1 27579	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
2		oveq1 7418	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑎 → (𝑏↑2) = (𝑎↑2))
3	2	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑎 → ((𝑎↑2) + (𝑏↑2)) = ((𝑎↑2) + (𝑎↑2)))
4	3	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ)) → ((𝑎↑2) + (𝑏↑2)) = ((𝑎↑2) + (𝑎↑2)))
5		nncn 12241	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℂ)
6	5	sqcld 14180	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ ℕ → (𝑎↑2) ∈ ℂ)
7		2times 12376	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎↑2) ∈ ℂ → (2 · (𝑎↑2)) = ((𝑎↑2) + (𝑎↑2)))
8	7	eqcomd 2775	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎↑2) ∈ ℂ → ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2)))
9	6, 8	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℕ → ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2)))
10	9	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) → ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2)))
11	10	ad2antrl 740	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ)) → ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2)))
12	4, 11	eqtrd 2804	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ)) → ((𝑎↑2) + (𝑏↑2)) = (2 · (𝑎↑2)))
13	12	eqeq1d 2771	. . . . . . . . . . 11 ⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ)) → (((𝑎↑2) + (𝑏↑2)) = 𝑃 ↔ (2 · (𝑎↑2)) = 𝑃))
14		oveq1 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 = (2 · (𝑎↑2)) → (𝑃 mod 4) = ((2 · (𝑎↑2)) mod 4))
15	14	eqeq1d 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 = (2 · (𝑎↑2)) → ((𝑃 mod 4) = 1 ↔ ((2 · (𝑎↑2)) mod 4) = 1))
16		eleq1 2857	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 = (2 · (𝑎↑2)) → (𝑃 ∈ ℙ ↔ (2 · (𝑎↑2)) ∈ ℙ))
17	15, 16	anbi12d 643	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 = (2 · (𝑎↑2)) → (((𝑃 mod 4) = 1 ∧ 𝑃 ∈ ℙ) ↔ (((2 · (𝑎↑2)) mod 4) = 1 ∧ (2 · (𝑎↑2)) ∈ ℙ)))
18		nnz 12612	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℤ)
19		2nn0 12521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℕ₀
20		zexpcl 14112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ ℤ ∧ 2 ∈ ℕ₀) → (𝑎↑2) ∈ ℤ)
21	18, 19, 20	sylancl 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ ℕ → (𝑎↑2) ∈ ℤ)
22		2mulprm 16751	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎↑2) ∈ ℤ → ((2 · (𝑎↑2)) ∈ ℙ ↔ (𝑎↑2) = 1))
23	21, 22	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℕ → ((2 · (𝑎↑2)) ∈ ℙ ↔ (𝑎↑2) = 1))
24		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎↑2) = 1 → (2 · (𝑎↑2)) = (2 · 1))
25		2t1e2 12403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (2 · 1) = 2
26	24, 25	eqtrdi 2820	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎↑2) = 1 → (2 · (𝑎↑2)) = 2)
27	26	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎↑2) = 1 → ((2 · (𝑎↑2)) mod 4) = (2 mod 4))
28		2re 12315	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℝ
29		4nn 12324	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ∈ ℕ
30		nnrp 13028	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (4 ∈ ℕ → 4 ∈ ℝ⁺)
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 4 ∈ ℝ⁺
32		0le2 12343	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ≤ 2
33		2lt4 12418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 < 4
34		modid 13929	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2 ∈ ℝ ∧ 4 ∈ ℝ⁺) ∧ (0 ≤ 2 ∧ 2 < 4)) → (2 mod 4) = 2)
35	28, 31, 32, 33, 34	mp4an 705	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 mod 4) = 2
36	27, 35	eqtrdi 2820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎↑2) = 1 → ((2 · (𝑎↑2)) mod 4) = 2)
37	36	eqeq1d 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎↑2) = 1 → (((2 · (𝑎↑2)) mod 4) = 1 ↔ 2 = 1))
38		1ne2 12451	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ≠ 2
39		eqcom 2776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 = 1 ↔ 1 = 2)
40		eqneqall 2975	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1 = 2 → (1 ≠ 2 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
41	40	com12 33	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 ≠ 2 → (1 = 2 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
42	39, 41	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1 ≠ 2 → (2 = 1 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
43	38, 42	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 = 1 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))
44	37, 43	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎↑2) = 1 → (((2 · (𝑎↑2)) mod 4) = 1 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
45	23, 44	biimtrdi 256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ ℕ → ((2 · (𝑎↑2)) ∈ ℙ → (((2 · (𝑎↑2)) mod 4) = 1 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))))
46	45	impcomd 416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ ℕ → ((((2 · (𝑎↑2)) mod 4) = 1 ∧ (2 · (𝑎↑2)) ∈ ℙ) → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
47	46	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ ((((2 · (𝑎↑2)) mod 4) = 1 ∧ (2 · (𝑎↑2)) ∈ ℙ) → (𝑎 ∈ ℕ → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
48	17, 47	biimtrdi 256	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 = (2 · (𝑎↑2)) → (((𝑃 mod 4) = 1 ∧ 𝑃 ∈ ℙ) → (𝑎 ∈ ℕ → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))))
49	48	expd 420	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 = (2 · (𝑎↑2)) → ((𝑃 mod 4) = 1 → (𝑃 ∈ ℙ → (𝑎 ∈ ℕ → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))))
50	49	com34 92	. . . . . . . . . . . . . . 15 ⊢ (𝑃 = (2 · (𝑎↑2)) → ((𝑃 mod 4) = 1 → (𝑎 ∈ ℕ → (𝑃 ∈ ℙ → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))))
51	50	eqcoms 2777	. . . . . . . . . . . . . 14 ⊢ ((2 · (𝑎↑2)) = 𝑃 → ((𝑃 mod 4) = 1 → (𝑎 ∈ ℕ → (𝑃 ∈ ℙ → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))))
52	51	com14 97	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 → (𝑎 ∈ ℕ → ((2 · (𝑎↑2)) = 𝑃 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))))
53	52	imp31 422	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) → ((2 · (𝑎↑2)) = 𝑃 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
54	53	ad2antrl 740	. . . . . . . . . . 11 ⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ)) → ((2 · (𝑎↑2)) = 𝑃 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
55	13, 54	sylbid 243	. . . . . . . . . 10 ⊢ ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ)) → (((𝑎↑2) + (𝑏↑2)) = 𝑃 → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
56	55	expimpd 458	. . . . . . . . 9 ⊢ (𝑏 = 𝑎 → (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
57		2a1 29	. . . . . . . . 9 ⊢ (𝑏 ≠ 𝑎 → (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎)))
58	56, 57	pm2.61ine 3047	. . . . . . . 8 ⊢ (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎 ≤ 𝑏 → 𝑏 ≠ 𝑎))
59	58	pm4.71d 570	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎 ≤ 𝑏 ↔ (𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎)))
60		nnre 12240	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℝ)
61	60	adantl 486	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) → 𝑎 ∈ ℝ)
62		nnre 12240	. . . . . . . . . 10 ⊢ (𝑏 ∈ ℕ → 𝑏 ∈ ℝ)
63		ltlen 11311	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 < 𝑏 ↔ (𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎)))
64	61, 62, 63	syl2an 607	. . . . . . . . 9 ⊢ ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ) → (𝑎 < 𝑏 ↔ (𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎)))
65	64	bibi2d 345	. . . . . . . 8 ⊢ ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ) → ((𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏) ↔ (𝑎 ≤ 𝑏 ↔ (𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎))))
66	65	adantr 485	. . . . . . 7 ⊢ (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ((𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏) ↔ (𝑎 ≤ 𝑏 ↔ (𝑎 ≤ 𝑏 ∧ 𝑏 ≠ 𝑎))))
67	59, 66	mpbird 260	. . . . . 6 ⊢ (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏))
68	67	ex 417	. . . . 5 ⊢ ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ) → (((𝑎↑2) + (𝑏↑2)) = 𝑃 → (𝑎 ≤ 𝑏 ↔ 𝑎 < 𝑏)))
69	68	pm5.32rd 588	. . . 4 ⊢ ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) ∧ 𝑏 ∈ ℕ) → ((𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
70	69	reubidva 3389	. . 3 ⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ) → (∃!𝑏 ∈ ℕ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
71	70	reubidva 3389	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
72	1, 71	mpbid 235	1 ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∃!wreu 3373 class class class wbr 5111 (class class class)co 7411 ℂcc 11098 ℝcr 11099 0cc0 11100 1c1 11101 + caddc 11103 · cmul 11105 < clt 11243 ≤ cle 11244 ℕcn 12233 2c2 12295 4c4 12297 ℕ₀cn0 12504 ℤcz 12591 ℝ⁺crp 13016 mod cmo 13902 ↑cexp 14097 ℙcprime 16729

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178 ax-addf 11179 ax-mulf 11180

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-ofr 7676 df-om 7863 df-1st 7986 df-2nd 7987 df-supp 8157 df-tpos 8222 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-2o 8454 df-oadd 8457 df-er 8694 df-ec 8696 df-qs 8700 df-map 8826 df-pm 8827 df-ixp 8896 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fsupp 9322 df-sup 9402 df-inf 9403 df-oi 9472 df-dju 9887 df-card 9925 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12505 df-xnn0 12578 df-z 12592 df-dec 12712 df-uz 12863 df-q 12973 df-rp 13017 df-fz 13536 df-fzo 13683 df-fl 13825 df-mod 13903 df-seq 14038 df-exp 14098 df-hash 14367 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287 df-dvds 16311 df-gcd 16553 df-prm 16730 df-phi 16825 df-pc 16897 df-gz 16990 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-mulr 17324 df-starv 17325 df-sca 17326 df-vsca 17327 df-ip 17328 df-tset 17329 df-ple 17330 df-ds 17332 df-unif 17333 df-hom 17334 df-cco 17335 df-0g 17494 df-gsum 17495 df-prds 17500 df-pws 17502 df-imas 17562 df-qus 17563 df-mre 17638 df-mrc 17639 df-acs 17641 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-mhm 18841 df-submnd 18842 df-grp 19003 df-minusg 19004 df-sbg 19005 df-mulg 19134 df-subg 19189 df-nsg 19190 df-eqg 19191 df-ghm 19284 df-cntz 19387 df-cmn 19852 df-abl 19853 df-mgp 20217 df-rng 20231 df-ur 20264 df-srg 20269 df-ring 20317 df-cring 20318 df-oppr 20419 df-dvdsr 20439 df-unit 20440 df-invr 20470 df-dvr 20483 df-rhm 20554 df-nzr 20596 df-subrng 20631 df-subrg 20655 df-rlreg 20779 df-domn 20780 df-idom 20781 df-drng 20815 df-field 20816 df-lmod 20961 df-lss 21031 df-lsp 21071 df-sra 21272 df-rgmod 21273 df-lidl 21310 df-rsp 21311 df-2idl 21360 df-cnfld 21492 df-zring 21566 df-zrh 21622 df-zn 21625 df-assa 21972 df-asp 21973 df-ascl 21974 df-psr 22028 df-mvr 22029 df-mpl 22030 df-opsr 22032 df-evls 22194 df-evl 22195 df-psr1 22309 df-vr1 22310 df-ply1 22311 df-coe1 22312 df-evl1 22445 df-mdeg 26181 df-deg1 26182 df-mon1 26257 df-uc1p 26258 df-q1p 26259 df-r1p 26260 df-lgs 27425

This theorem is referenced by: 2sqreunnltblem 27581 2sqreunnlt 27590

W3C validator