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 25993

Description: Lemma for 2sq 26000. 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 5062	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 1))
5	4	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆)))
6	5	ralbidv 3197	. . . . 5 ⊢ (𝑥 = 1 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆)))
7		oveq2 7158	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑚 · 𝑥) = (𝑚 · 1))
8	7	eleq1d 2897	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 1) ∈ 𝑆))
9	8	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 1 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
10	9	ralbidv 3197	. . . . 5 ⊢ (𝑥 = 1 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
11	6, 10	imbi12d 347	. . . 4 ⊢ (𝑥 = 1 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
12		breq2 5062	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑦))
13	12	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆)))
14	13	ralbidv 3197	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆)))
15		oveq2 7158	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑚 · 𝑥) = (𝑚 · 𝑦))
16	15	eleq1d 2897	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝑦) ∈ 𝑆))
17	16	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
18	17	ralbidv 3197	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
19	14, 18	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝑦 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
20		breq2 5062	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑧))
21	20	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
22	21	ralbidv 3197	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
23		oveq2 7158	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑚 · 𝑥) = (𝑚 · 𝑧))
24	23	eleq1d 2897	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝑧) ∈ 𝑆))
25	24	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑧 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
26	25	ralbidv 3197	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
27	22, 26	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝑧 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
28		breq2 5062	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ (𝑦 · 𝑧)))
29	28	imbi1d 344	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)))
30	29	ralbidv 3197	. . . . 5 ⊢ (𝑥 = (𝑦 · 𝑧) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)))
31		oveq2 7158	. . . . . . . 8 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑚 · 𝑥) = (𝑚 · (𝑦 · 𝑧)))
32	31	eleq1d 2897	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · (𝑦 · 𝑧)) ∈ 𝑆))
33	32	imbi1d 344	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
34	33	ralbidv 3197	. . . . 5 ⊢ (𝑥 = (𝑦 · 𝑧) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
35	30, 34	imbi12d 347	. . . 4 ⊢ (𝑥 = (𝑦 · 𝑧) → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
36		breq2 5062	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝐵))
37	36	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝐵 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)))
38	37	ralbidv 3197	. . . . 5 ⊢ (𝑥 = 𝐵 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)))
39		oveq2 7158	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝑚 · 𝑥) = (𝑚 · 𝐵))
40	39	eleq1d 2897	. . . . . . 7 ⊢ (𝑥 = 𝐵 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝐵) ∈ 𝑆))
41	40	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝐵 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
42	41	ralbidv 3197	. . . . 5 ⊢ (𝑥 = 𝐵 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
43	38, 42	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝐵 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
44		nncn 11640	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
45	44	mulid1d 10652	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ → (𝑚 · 1) = 𝑚)
46	45	eleq1d 2897	. . . . . . 7 ⊢ (𝑚 ∈ ℕ → ((𝑚 · 1) ∈ 𝑆 ↔ 𝑚 ∈ 𝑆))
47	46	biimpd 231	. . . . . 6 ⊢ (𝑚 ∈ ℕ → ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))
48	47	rgen 3148	. . . . 5 ⊢ ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)
49	48	a1i 11	. . . 4 ⊢ (∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))
50		breq1 5061	. . . . . . 7 ⊢ (𝑝 = 𝑥 → (𝑝 ∥ 𝑥 ↔ 𝑥 ∥ 𝑥))
51		eleq1 2900	. . . . . . 7 ⊢ (𝑝 = 𝑥 → (𝑝 ∈ 𝑆 ↔ 𝑥 ∈ 𝑆))
52	50, 51	imbi12d 347	. . . . . 6 ⊢ (𝑝 = 𝑥 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆)))
53	52	rspcv 3617	. . . . 5 ⊢ (𝑥 ∈ ℙ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → (𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆)))
54		prmz 16013	. . . . . . 7 ⊢ (𝑥 ∈ ℙ → 𝑥 ∈ ℤ)
55		iddvds 15617	. . . . . . 7 ⊢ (𝑥 ∈ ℤ → 𝑥 ∥ 𝑥)
56	54, 55	syl 17	. . . . . 6 ⊢ (𝑥 ∈ ℙ → 𝑥 ∥ 𝑥)
57		2sq.1	. . . . . . . . . 10 ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
58		simprl 769	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑚 ∈ ℕ)
59		simpll 765	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑥 ∈ ℙ)
60		simprr 771	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → (𝑚 · 𝑥) ∈ 𝑆)
61		simplr 767	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑥 ∈ 𝑆)
62	57, 58, 59, 60, 61	2sqlem5 25992	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑚 ∈ 𝑆)
63	62	expr 459	. . . . . . . 8 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))
64	63	ralrimiva 3182	. . . . . . 7 ⊢ ((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))
65	64	ex 415	. . . . . 6 ⊢ (𝑥 ∈ ℙ → (𝑥 ∈ 𝑆 → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
66	56, 65	embantd 59	. . . . 5 ⊢ (𝑥 ∈ ℙ → ((𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
67	53, 66	syld 47	. . . 4 ⊢ (𝑥 ∈ ℙ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
68		anim12 807	. . . . 5 ⊢ (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ∧ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
69		simpr 487	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
70		eluzelz 12247	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℤ)
71	70	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑦 ∈ ℤ)
72		eluzelz 12247	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℤ)
73	72	ad2antlr 725	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑧 ∈ ℤ)
74		euclemma 16051	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑝 ∥ (𝑦 · 𝑧) ↔ (𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧)))
75	69, 71, 73, 74	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝑦 · 𝑧) ↔ (𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧)))
76	75	imbi1d 344	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧) → 𝑝 ∈ 𝑆)))
77		jaob 958	. . . . . . . . . . . 12 ⊢ (((𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
78	76, 77	syl6bb 289	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
79	78	ralbidva 3196	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
80		r19.26 3170	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ ℙ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
81	79, 80	syl6bb 289	. . . . . . . . 9 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
82	81	biimpa 479	. . . . . . . 8 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
83		oveq1 7157	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑚 · 𝑦) = (𝑛 · 𝑦))
84	83	eleq1d 2897	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑚 · 𝑦) ∈ 𝑆 ↔ (𝑛 · 𝑦) ∈ 𝑆))
85		eleq1 2900	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑆 ↔ 𝑛 ∈ 𝑆))
86	84, 85	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)))
87	86	cbvralvw 3449	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆))
88	44	adantl 484	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
89		uzssz 12258	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘2) ⊆ ℤ
90		zsscn 11983	. . . . . . . . . . . . . . . . 17 ⊢ ℤ ⊆ ℂ
91	89, 90	sstri 3975	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘2) ⊆ ℂ
92		simpll 765	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → 𝑦 ∈ (ℤ_≥‘2))
93	92	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈ (ℤ_≥‘2))
94	91, 93	sseldi 3964	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈ ℂ)
95		simplr 767	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → 𝑧 ∈ (ℤ_≥‘2))
96	95	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ (ℤ_≥‘2))
97	91, 96	sseldi 3964	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℂ)
98		mul32 10800	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑧) = ((𝑚 · 𝑧) · 𝑦))
99		mulass 10619	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑧) = (𝑚 · (𝑦 · 𝑧)))
100	98, 99	eqtr3d 2858	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑧) · 𝑦) = (𝑚 · (𝑦 · 𝑧)))
101	88, 94, 97, 100	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑧) · 𝑦) = (𝑚 · (𝑦 · 𝑧)))
102	101	eleq1d 2897	. . . . . . . . . . . . 13 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 ↔ (𝑚 · (𝑦 · 𝑧)) ∈ 𝑆))
103		simpr 487	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
104		eluz2nn 12278	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℕ)
105	96, 104	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℕ)
106	103, 105	nnmulcld 11684	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑧) ∈ ℕ)
107		simplr 767	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆))
108		oveq1 7157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑚 · 𝑧) → (𝑛 · 𝑦) = ((𝑚 · 𝑧) · 𝑦))
109	108	eleq1d 2897	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 · 𝑧) → ((𝑛 · 𝑦) ∈ 𝑆 ↔ ((𝑚 · 𝑧) · 𝑦) ∈ 𝑆))
110		eleq1 2900	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 · 𝑧) → (𝑛 ∈ 𝑆 ↔ (𝑚 · 𝑧) ∈ 𝑆))
111	109, 110	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑚 · 𝑧) → (((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆) ↔ (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆)))
112	111	rspcv 3617	. . . . . . . . . . . . . 14 ⊢ ((𝑚 · 𝑧) ∈ ℕ → (∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆)))
113	106, 107, 112	sylc 65	. . . . . . . . . . . . 13 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆))
114	102, 113	sylbird 262	. . . . . . . . . . . 12 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆))
115	114	imim1d 82	. . . . . . . . . . 11 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
116	115	ralimdva 3177	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
117	87, 116	sylan2b 595	. . . . . . . . 9 ⊢ ((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
118	117	expimpd 456	. . . . . . . 8 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → ((∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
119	82, 118	embantd 59	. . . . . . 7 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
120	119	ex 415	. . . . . 6 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
121	120	com23 86	. . . . 5 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
122	68, 121	syl5 34	. . . 4 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ∧ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
123	11, 19, 27, 35, 43, 49, 67, 122	prmind 16024	. . 3 ⊢ (𝐵 ∈ ℕ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
124	2, 3, 123	sylc 65	. 2 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))
125		2sqlem6.4	. 2 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑆)
126		oveq1 7157	. . . . 5 ⊢ (𝑚 = 𝐴 → (𝑚 · 𝐵) = (𝐴 · 𝐵))
127	126	eleq1d 2897	. . . 4 ⊢ (𝑚 = 𝐴 → ((𝑚 · 𝐵) ∈ 𝑆 ↔ (𝐴 · 𝐵) ∈ 𝑆))
128		eleq1 2900	. . . 4 ⊢ (𝑚 = 𝐴 → (𝑚 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆))
129	127, 128	imbi12d 347	. . 3 ⊢ (𝑚 = 𝐴 → (((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝐴 · 𝐵) ∈ 𝑆 → 𝐴 ∈ 𝑆)))
130	129	rspcv 3617	. 2 ⊢ (𝐴 ∈ ℕ → (∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ((𝐴 · 𝐵) ∈ 𝑆 → 𝐴 ∈ 𝑆)))
131	1, 124, 125, 130	syl3c 66	1 ⊢ (𝜑 → 𝐴 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∀wral 3138 class class class wbr 5058 ↦ cmpt 5138 ran crn 5550 ‘cfv 6349 (class class class)co 7150 ℂcc 10529 1c1 10532 · cmul 10536 ℕcn 11632 2c2 11686 ℤcz 11975 ℤ_≥cuz 12237 ↑cexp 13423 abscabs 14587 ∥ cdvds 15601 ℙcprime 16009 ℤ[i]cgz 16259

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-2o 8097 df-er 8283 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-sup 8900 df-inf 8901 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-z 11976 df-uz 12238 df-rp 12384 df-fz 12887 df-fl 13156 df-mod 13232 df-seq 13364 df-exp 13424 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-dvds 15602 df-gcd 15838 df-prm 16010 df-gz 16260

This theorem is referenced by: 2sqlem8 25996

W3C validator