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 27662

Description: Lemma for 2sq 27669. 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 5107	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 1))
5	4	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆)))
6	5	ralbidv 3185	. . . . 5 ⊢ (𝑥 = 1 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆)))
7		oveq2 7422	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑚 · 𝑥) = (𝑚 · 1))
8	7	eleq1d 2845	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 1) ∈ 𝑆))
9	8	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 1 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
10	9	ralbidv 3185	. . . . 5 ⊢ (𝑥 = 1 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
11	6, 10	imbi12d 347	. . . 4 ⊢ (𝑥 = 1 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
12		breq2 5107	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑦))
13	12	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆)))
14	13	ralbidv 3185	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆)))
15		oveq2 7422	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑚 · 𝑥) = (𝑚 · 𝑦))
16	15	eleq1d 2845	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝑦) ∈ 𝑆))
17	16	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
18	17	ralbidv 3185	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
19	14, 18	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝑦 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
20		breq2 5107	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑧))
21	20	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
22	21	ralbidv 3185	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
23		oveq2 7422	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑚 · 𝑥) = (𝑚 · 𝑧))
24	23	eleq1d 2845	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝑧) ∈ 𝑆))
25	24	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝑧 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
26	25	ralbidv 3185	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
27	22, 26	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝑧 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
28		breq2 5107	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ (𝑦 · 𝑧)))
29	28	imbi1d 344	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)))
30	29	ralbidv 3185	. . . . 5 ⊢ (𝑥 = (𝑦 · 𝑧) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)))
31		oveq2 7422	. . . . . . . 8 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑚 · 𝑥) = (𝑚 · (𝑦 · 𝑧)))
32	31	eleq1d 2845	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · (𝑦 · 𝑧)) ∈ 𝑆))
33	32	imbi1d 344	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
34	33	ralbidv 3185	. . . . 5 ⊢ (𝑥 = (𝑦 · 𝑧) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
35	30, 34	imbi12d 347	. . . 4 ⊢ (𝑥 = (𝑦 · 𝑧) → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
36		breq2 5107	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝐵))
37	36	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝐵 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)))
38	37	ralbidv 3185	. . . . 5 ⊢ (𝑥 = 𝐵 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)))
39		oveq2 7422	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝑚 · 𝑥) = (𝑚 · 𝐵))
40	39	eleq1d 2845	. . . . . . 7 ⊢ (𝑥 = 𝐵 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝐵) ∈ 𝑆))
41	40	imbi1d 344	. . . . . 6 ⊢ (𝑥 = 𝐵 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
42	41	ralbidv 3185	. . . . 5 ⊢ (𝑥 = 𝐵 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
43	38, 42	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝐵 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
44		nncn 12268	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
45	44	mulridd 11253	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ → (𝑚 · 1) = 𝑚)
46	45	eleq1d 2845	. . . . . . 7 ⊢ (𝑚 ∈ ℕ → ((𝑚 · 1) ∈ 𝑆 ↔ 𝑚 ∈ 𝑆))
47	46	biimpd 232	. . . . . 6 ⊢ (𝑚 ∈ ℕ → ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))
48	47	rgen 3078	. . . . 5 ⊢ ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)
49	48	a1i 11	. . . 4 ⊢ (∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))
50		breq1 5106	. . . . . . 7 ⊢ (𝑝 = 𝑥 → (𝑝 ∥ 𝑥 ↔ 𝑥 ∥ 𝑥))
51		eleq1 2848	. . . . . . 7 ⊢ (𝑝 = 𝑥 → (𝑝 ∈ 𝑆 ↔ 𝑥 ∈ 𝑆))
52	50, 51	imbi12d 347	. . . . . 6 ⊢ (𝑝 = 𝑥 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆)))
53	52	rspcv 3572	. . . . 5 ⊢ (𝑥 ∈ ℙ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → (𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆)))
54		prmz 16768	. . . . . . 7 ⊢ (𝑥 ∈ ℙ → 𝑥 ∈ ℤ)
55		iddvds 16362	. . . . . . 7 ⊢ (𝑥 ∈ ℤ → 𝑥 ∥ 𝑥)
56	54, 55	syl 18	. . . . . 6 ⊢ (𝑥 ∈ ℙ → 𝑥 ∥ 𝑥)
57		2sq.1	. . . . . . . . . 10 ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
58		simprl 783	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑚 ∈ ℕ)
59		simpll 779	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑥 ∈ ℙ)
60		simprr 785	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → (𝑚 · 𝑥) ∈ 𝑆)
61		simplr 781	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑥 ∈ 𝑆)
62	57, 58, 59, 60, 61	2sqlem5 27661	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑚 ∈ 𝑆)
63	62	expr 462	. . . . . . . 8 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))
64	63	ralrimiva 3154	. . . . . . 7 ⊢ ((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))
65	64	ex 418	. . . . . 6 ⊢ (𝑥 ∈ ℙ → (𝑥 ∈ 𝑆 → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
66	56, 65	embantd 60	. . . . 5 ⊢ (𝑥 ∈ ℙ → ((𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
67	53, 66	syld 48	. . . 4 ⊢ (𝑥 ∈ ℙ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
68		anim12 821	. . . . 5 ⊢ (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ∧ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
69		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
70		eluzelz 12900	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℤ)
71	70	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑦 ∈ ℤ)
72		eluzelz 12900	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℤ)
73	72	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑧 ∈ ℤ)
74		euclemma 16807	. . . . . . . . . . . . . 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 3183	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
80		r19.26 3122	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ ℙ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
81	79, 80	bitrdi 290	. . . . . . . . 9 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
82	81	biimpa 482	. . . . . . . 8 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
83		oveq1 7421	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑚 · 𝑦) = (𝑛 · 𝑦))
84	83	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑚 · 𝑦) ∈ 𝑆 ↔ (𝑛 · 𝑦) ∈ 𝑆))
85		eleq1 2848	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑆 ↔ 𝑛 ∈ 𝑆))
86	84, 85	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)))
87	86	cbvralvw 3240	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆))
88	44	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
89		uzssz 12911	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘2) ⊆ ℤ
90		zsscn 12626	. . . . . . . . . . . . . . . . 17 ⊢ ℤ ⊆ ℂ
91	89, 90	sstri 3940	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘2) ⊆ ℂ
92		simpll 779	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → 𝑦 ∈ (ℤ_≥‘2))
93	92	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈ (ℤ_≥‘2))
94	91, 93	sselid 3929	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈ ℂ)
95		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → 𝑧 ∈ (ℤ_≥‘2))
96	95	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ (ℤ_≥‘2))
97	91, 96	sselid 3929	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℂ)
98		mul32 11403	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑧) = ((𝑚 · 𝑧) · 𝑦))
99		mulass 11215	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑧) = (𝑚 · (𝑦 · 𝑧)))
100	98, 99	eqtr3d 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑧) · 𝑦) = (𝑚 · (𝑦 · 𝑧)))
101	88, 94, 97, 100	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑧) · 𝑦) = (𝑚 · (𝑦 · 𝑧)))
102	101	eleq1d 2845	. . . . . . . . . . . . 13 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 ↔ (𝑚 · (𝑦 · 𝑧)) ∈ 𝑆))
103		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
104		eluz2nn 12940	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℕ)
105	96, 104	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℕ)
106	103, 105	nnmulcld 12316	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑧) ∈ ℕ)
107		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆))
108		oveq1 7421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑚 · 𝑧) → (𝑛 · 𝑦) = ((𝑚 · 𝑧) · 𝑦))
109	108	eleq1d 2845	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 · 𝑧) → ((𝑛 · 𝑦) ∈ 𝑆 ↔ ((𝑚 · 𝑧) · 𝑦) ∈ 𝑆))
110		eleq1 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 · 𝑧) → (𝑛 ∈ 𝑆 ↔ (𝑚 · 𝑧) ∈ 𝑆))
111	109, 110	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑚 · 𝑧) → (((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆) ↔ (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆)))
112	111	rspcv 3572	. . . . . . . . . . . . . 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 3174	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
117	87, 116	sylan2b 606	. . . . . . . . 9 ⊢ ((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
118	117	expimpd 459	. . . . . . . 8 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → ((∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
119	82, 118	embantd 60	. . . . . . 7 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
120	119	ex 418	. . . . . 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 16779	. . 3 ⊢ (𝐵 ∈ ℕ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
124	2, 3, 123	sylc 66	. 2 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))
125		2sqlem6.4	. 2 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑆)
126		oveq1 7421	. . . . 5 ⊢ (𝑚 = 𝐴 → (𝑚 · 𝐵) = (𝐴 · 𝐵))
127	126	eleq1d 2845	. . . 4 ⊢ (𝑚 = 𝐴 → ((𝑚 · 𝐵) ∈ 𝑆 ↔ (𝐴 · 𝐵) ∈ 𝑆))
128		eleq1 2848	. . . 4 ⊢ (𝑚 = 𝐴 → (𝑚 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆))
129	127, 128	imbi12d 347	. . 3 ⊢ (𝑚 = 𝐴 → (((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝐴 · 𝐵) ∈ 𝑆 → 𝐴 ∈ 𝑆)))
130	129	rspcv 3572	. 2 ⊢ (𝐴 ∈ ℕ → (∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ((𝐴 · 𝐵) ∈ 𝑆 → 𝐴 ∈ 𝑆)))
131	1, 124, 125, 130	syl3c 67	1 ⊢ (𝜑 → 𝐴 ∈ 𝑆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3076 class class class wbr 5103 ↦ cmpt 5186 ran crn 5656 ‘cfv 6533 (class class class)co 7414 ℂcc 11125 1c1 11128 · cmul 11132 ℕcn 12260 2c2 12322 ℤcz 12618 ℤ_≥cuz 12890 ↑cexp 14128 abscabs 15324 ∥ cdvds 16345 ℙcprime 16764 ℤ[i]cgz 17024

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8458 df-2o 8459 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-sup 9415 df-inf 9416 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-n0 12532 df-z 12619 df-uz 12891 df-rp 13046 df-fz 13565 df-fl 13856 df-mod 13934 df-seq 14069 df-exp 14129 df-cj 15189 df-re 15190 df-im 15191 df-sqrt 15325 df-abs 15326 df-dvds 16346 df-gcd 16588 df-prm 16765 df-gz 17025

This theorem is used by: 2sqlem8 27665

W3C validator