2sqlem6 - Metamath Proof Explorer

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

Theorem 2sqlem6 27587

Description: Lemma for 2sq 27594. If a number that is a sum of two squares is divisible by a number whose prime divisors are all sums of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.)

**Hypotheses**
Ref	Expression
2sq.1	⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
2sqlem6.1	⊢ (𝜑 → 𝐴 ∈ ℕ)
2sqlem6.2	⊢ (𝜑 → 𝐵 ∈ ℕ)
2sqlem6.3	⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆))
2sqlem6.4	⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑆)

**Assertion**
Ref	Expression
2sqlem6	⊢ (𝜑 → 𝐴 ∈ 𝑆)

Distinct variable groups: 𝑤,𝑝 𝜑,𝑝 𝐵,𝑝 𝑆,𝑝 Allowed substitution hints: 𝜑(𝑤) 𝐴(𝑤,𝑝) 𝐵(𝑤) 𝑆(𝑤)

Proof of Theorem 2sqlem6 Dummy variables 𝑛 𝑥 𝑦 𝑧 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2sqlem6.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		2sqlem6.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℕ)
3		2sqlem6.3	. . 3 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆))
4		breq2 5113	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 1))
5	4	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆)))
6	5	ralbidv 3188	. . . . 5 ⊢ (𝑥 = 1 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆)))
7		oveq2 7418	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑚 · 𝑥) = (𝑚 · 1))
8	7	eleq1d 2848	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 1) ∈ 𝑆))
9	8	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 1 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
10	9	ralbidv 3188	. . . . 5 ⊢ (𝑥 = 1 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
11	6, 10	imbi12d 347	. . . 4 ⊢ (𝑥 = 1 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
12		breq2 5113	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑦))
13	12	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆)))
14	13	ralbidv 3188	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆)))
15		oveq2 7418	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑚 · 𝑥) = (𝑚 · 𝑦))
16	15	eleq1d 2848	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝑦) ∈ 𝑆))
17	16	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
18	17	ralbidv 3188	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
19	14, 18	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝑦 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
20		breq2 5113	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑧))
21	20	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
22	21	ralbidv 3188	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
23		oveq2 7418	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑚 · 𝑥) = (𝑚 · 𝑧))
24	23	eleq1d 2848	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝑧) ∈ 𝑆))
25	24	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑧 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
26	25	ralbidv 3188	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
27	22, 26	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝑧 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
28		breq2 5113	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ (𝑦 · 𝑧)))
29	28	imbi1d 344	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)))
30	29	ralbidv 3188	. . . . 5 ⊢ (𝑥 = (𝑦 · 𝑧) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)))
31		oveq2 7418	. . . . . . . 8 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑚 · 𝑥) = (𝑚 · (𝑦 · 𝑧)))
32	31	eleq1d 2848	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · (𝑦 · 𝑧)) ∈ 𝑆))
33	32	imbi1d 344	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
34	33	ralbidv 3188	. . . . 5 ⊢ (𝑥 = (𝑦 · 𝑧) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
35	30, 34	imbi12d 347	. . . 4 ⊢ (𝑥 = (𝑦 · 𝑧) → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
36		breq2 5113	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝐵))
37	36	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝐵 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)))
38	37	ralbidv 3188	. . . . 5 ⊢ (𝑥 = 𝐵 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)))
39		oveq2 7418	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝑚 · 𝑥) = (𝑚 · 𝐵))
40	39	eleq1d 2848	. . . . . . 7 ⊢ (𝑥 = 𝐵 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝐵) ∈ 𝑆))
41	40	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝐵 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
42	41	ralbidv 3188	. . . . 5 ⊢ (𝑥 = 𝐵 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
43	38, 42	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝐵 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
44		nncn 12236	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
45	44	mulridd 11221	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ → (𝑚 · 1) = 𝑚)
46	45	eleq1d 2848	. . . . . . 7 ⊢ (𝑚 ∈ ℕ → ((𝑚 · 1) ∈ 𝑆 ↔ 𝑚 ∈ 𝑆))
47	46	biimpd 232	. . . . . 6 ⊢ (𝑚 ∈ ℕ → ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))
48	47	rgen 3081	. . . . 5 ⊢ ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)
49	48	a1i 11	. . . 4 ⊢ (∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))
50		breq1 5112	. . . . . . 7 ⊢ (𝑝 = 𝑥 → (𝑝 ∥ 𝑥 ↔ 𝑥 ∥ 𝑥))
51		eleq1 2851	. . . . . . 7 ⊢ (𝑝 = 𝑥 → (𝑝 ∈ 𝑆 ↔ 𝑥 ∈ 𝑆))
52	50, 51	imbi12d 347	. . . . . 6 ⊢ (𝑝 = 𝑥 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆)))
53	52	rspcv 3577	. . . . 5 ⊢ (𝑥 ∈ ℙ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → (𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆)))
54		prmz 16728	. . . . . . 7 ⊢ (𝑥 ∈ ℙ → 𝑥 ∈ ℤ)
55		iddvds 16322	. . . . . . 7 ⊢ (𝑥 ∈ ℤ → 𝑥 ∥ 𝑥)
56	54, 55	syl 18	. . . . . 6 ⊢ (𝑥 ∈ ℙ → 𝑥 ∥ 𝑥)
57		2sq.1	. . . . . . . . . 10 ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
58		simprl 782	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑚 ∈ ℕ)
59		simpll 778	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑥 ∈ ℙ)
60		simprr 784	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → (𝑚 · 𝑥) ∈ 𝑆)
61		simplr 780	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑥 ∈ 𝑆)
62	57, 58, 59, 60, 61	2sqlem5 27586	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑚 ∈ 𝑆)
63	62	expr 461	. . . . . . . 8 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))
64	63	ralrimiva 3157	. . . . . . 7 ⊢ ((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))
65	64	ex 417	. . . . . 6 ⊢ (𝑥 ∈ ℙ → (𝑥 ∈ 𝑆 → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
66	56, 65	embantd 60	. . . . 5 ⊢ (𝑥 ∈ ℙ → ((𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
67	53, 66	syld 48	. . . 4 ⊢ (𝑥 ∈ ℙ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
68		anim12 820	. . . . 5 ⊢ (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ∧ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
69		simpr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
70		eluzelz 12867	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℤ)
71	70	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑦 ∈ ℤ)
72		eluzelz 12867	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℤ)
73	72	ad2antlr 739	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑧 ∈ ℤ)
74		euclemma 16767	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑝 ∥ (𝑦 · 𝑧) ↔ (𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧)))
75	69, 71, 73, 74	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝑦 · 𝑧) ↔ (𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧)))
76	75	imbi1d 344	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧) → 𝑝 ∈ 𝑆)))
77		jaob 976	. . . . . . . . . . . 12 ⊢ (((𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
78	76, 77	bitrdi 290	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
79	78	ralbidva 3186	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
80		r19.26 3125	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ ℙ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
81	79, 80	bitrdi 290	. . . . . . . . 9 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
82	81	biimpa 481	. . . . . . . 8 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
83		oveq1 7417	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑚 · 𝑦) = (𝑛 · 𝑦))
84	83	eleq1d 2848	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑚 · 𝑦) ∈ 𝑆 ↔ (𝑛 · 𝑦) ∈ 𝑆))
85		eleq1 2851	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑆 ↔ 𝑛 ∈ 𝑆))
86	84, 85	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)))
87	86	cbvralvw 3243	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆))
88	44	adantl 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
89		uzssz 12878	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘2) ⊆ ℤ
90		zsscn 12594	. . . . . . . . . . . . . . . . 17 ⊢ ℤ ⊆ ℂ
91	89, 90	sstri 3946	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘2) ⊆ ℂ
92		simpll 778	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → 𝑦 ∈ (ℤ_≥‘2))
93	92	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈ (ℤ_≥‘2))
94	91, 93	sselid 3935	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈ ℂ)
95		simplr 780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → 𝑧 ∈ (ℤ_≥‘2))
96	95	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ (ℤ_≥‘2))
97	91, 96	sselid 3935	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℂ)
98		mul32 11371	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑧) = ((𝑚 · 𝑧) · 𝑦))
99		mulass 11183	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑧) = (𝑚 · (𝑦 · 𝑧)))
100	98, 99	eqtr3d 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑧) · 𝑦) = (𝑚 · (𝑦 · 𝑧)))
101	88, 94, 97, 100	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑧) · 𝑦) = (𝑚 · (𝑦 · 𝑧)))
102	101	eleq1d 2848	. . . . . . . . . . . . 13 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 ↔ (𝑚 · (𝑦 · 𝑧)) ∈ 𝑆))
103		simpr 489	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
104		eluz2nn 12907	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℕ)
105	96, 104	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℕ)
106	103, 105	nnmulcld 12284	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑧) ∈ ℕ)
107		simplr 780	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆))
108		oveq1 7417	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑚 · 𝑧) → (𝑛 · 𝑦) = ((𝑚 · 𝑧) · 𝑦))
109	108	eleq1d 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 · 𝑧) → ((𝑛 · 𝑦) ∈ 𝑆 ↔ ((𝑚 · 𝑧) · 𝑦) ∈ 𝑆))
110		eleq1 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 · 𝑧) → (𝑛 ∈ 𝑆 ↔ (𝑚 · 𝑧) ∈ 𝑆))
111	109, 110	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑚 · 𝑧) → (((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆) ↔ (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆)))
112	111	rspcv 3577	. . . . . . . . . . . . . 14 ⊢ ((𝑚 · 𝑧) ∈ ℕ → (∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆)))
113	106, 107, 112	sylc 66	. . . . . . . . . . . . 13 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆))
114	102, 113	sylbird 263	. . . . . . . . . . . 12 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆))
115	114	imim1d 83	. . . . . . . . . . 11 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
116	115	ralimdva 3177	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
117	87, 116	sylan2b 605	. . . . . . . . 9 ⊢ ((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
118	117	expimpd 458	. . . . . . . 8 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → ((∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
119	82, 118	embantd 60	. . . . . . 7 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
120	119	ex 417	. . . . . 6 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
121	120	com23 87	. . . . 5 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
122	68, 121	syl5 35	. . . 4 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ∧ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
123	11, 19, 27, 35, 43, 49, 67, 122	prmind 16739	. . 3 ⊢ (𝐵 ∈ ℕ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
124	2, 3, 123	sylc 66	. 2 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))
125		2sqlem6.4	. 2 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑆)
126		oveq1 7417	. . . . 5 ⊢ (𝑚 = 𝐴 → (𝑚 · 𝐵) = (𝐴 · 𝐵))
127	126	eleq1d 2848	. . . 4 ⊢ (𝑚 = 𝐴 → ((𝑚 · 𝐵) ∈ 𝑆 ↔ (𝐴 · 𝐵) ∈ 𝑆))
128		eleq1 2851	. . . 4 ⊢ (𝑚 = 𝐴 → (𝑚 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆))
129	127, 128	imbi12d 347	. . 3 ⊢ (𝑚 = 𝐴 → (((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝐴 · 𝐵) ∈ 𝑆 → 𝐴 ∈ 𝑆)))
130	129	rspcv 3577	. 2 ⊢ (𝐴 ∈ ℕ → (∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ((𝐴 · 𝐵) ∈ 𝑆 → 𝐴 ∈ 𝑆)))
131	1, 124, 125, 130	syl3c 67	1 ⊢ (𝜑 → 𝐴 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ∀wral 3079 class class class wbr 5109 ↦ cmpt 5192 ran crn 5662 ‘cfv 6536 (class class class)co 7410 ℂcc 11093 1c1 11096 · cmul 11100 ℕcn 12228 2c2 12290 ℤcz 12586 ℤ_≥cuz 12857 ↑cexp 14093 abscabs 15281 ∥ cdvds 16305 ℙcprime 16724 ℤ[i]cgz 16984

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172 ax-pre-sup 11173

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9398 df-inf 9399 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-div 11867 df-nn 12229 df-2 12298 df-3 12299 df-n0 12500 df-z 12587 df-uz 12858 df-rp 13012 df-fz 13531 df-fl 13821 df-mod 13899 df-seq 14034 df-exp 14094 df-cj 15146 df-re 15147 df-im 15148 df-sqrt 15282 df-abs 15283 df-dvds 16306 df-gcd 16548 df-prm 16725 df-gz 16985

This theorem is referenced by: 2sqlem8 27590

W3C validator