2sqlem6 - Intuitionistic Logic Explorer

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

Theorem 2sqlem6 15672

Description: Lemma for 2sq . 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 4055	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 1))
5	4	imbi1d 231	. . . . . 6 ⊢ (𝑥 = 1 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆)))
6	5	ralbidv 2507	. . . . 5 ⊢ (𝑥 = 1 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆)))
7		oveq2 5965	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑚 · 𝑥) = (𝑚 · 1))
8	7	eleq1d 2275	. . . . . . 7 ⊢ (𝑥 = 1 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 1) ∈ 𝑆))
9	8	imbi1d 231	. . . . . 6 ⊢ (𝑥 = 1 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
10	9	ralbidv 2507	. . . . 5 ⊢ (𝑥 = 1 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
11	6, 10	imbi12d 234	. . . 4 ⊢ (𝑥 = 1 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
12		breq2 4055	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑦))
13	12	imbi1d 231	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆)))
14	13	ralbidv 2507	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆)))
15		oveq2 5965	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑚 · 𝑥) = (𝑚 · 𝑦))
16	15	eleq1d 2275	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝑦) ∈ 𝑆))
17	16	imbi1d 231	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
18	17	ralbidv 2507	. . . . 5 ⊢ (𝑥 = 𝑦 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
19	14, 18	imbi12d 234	. . . 4 ⊢ (𝑥 = 𝑦 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
20		breq2 4055	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝑧))
21	20	imbi1d 231	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
22	21	ralbidv 2507	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
23		oveq2 5965	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑚 · 𝑥) = (𝑚 · 𝑧))
24	23	eleq1d 2275	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝑧) ∈ 𝑆))
25	24	imbi1d 231	. . . . . 6 ⊢ (𝑥 = 𝑧 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
26	25	ralbidv 2507	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
27	22, 26	imbi12d 234	. . . 4 ⊢ (𝑥 = 𝑧 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
28		breq2 4055	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ (𝑦 · 𝑧)))
29	28	imbi1d 231	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)))
30	29	ralbidv 2507	. . . . 5 ⊢ (𝑥 = (𝑦 · 𝑧) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)))
31		oveq2 5965	. . . . . . . 8 ⊢ (𝑥 = (𝑦 · 𝑧) → (𝑚 · 𝑥) = (𝑚 · (𝑦 · 𝑧)))
32	31	eleq1d 2275	. . . . . . 7 ⊢ (𝑥 = (𝑦 · 𝑧) → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · (𝑦 · 𝑧)) ∈ 𝑆))
33	32	imbi1d 231	. . . . . 6 ⊢ (𝑥 = (𝑦 · 𝑧) → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
34	33	ralbidv 2507	. . . . 5 ⊢ (𝑥 = (𝑦 · 𝑧) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
35	30, 34	imbi12d 234	. . . 4 ⊢ (𝑥 = (𝑦 · 𝑧) → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
36		breq2 4055	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝐵))
37	36	imbi1d 231	. . . . . 6 ⊢ (𝑥 = 𝐵 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)))
38	37	ralbidv 2507	. . . . 5 ⊢ (𝑥 = 𝐵 → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)))
39		oveq2 5965	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝑚 · 𝑥) = (𝑚 · 𝐵))
40	39	eleq1d 2275	. . . . . . 7 ⊢ (𝑥 = 𝐵 → ((𝑚 · 𝑥) ∈ 𝑆 ↔ (𝑚 · 𝐵) ∈ 𝑆))
41	40	imbi1d 231	. . . . . 6 ⊢ (𝑥 = 𝐵 → (((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
42	41	ralbidv 2507	. . . . 5 ⊢ (𝑥 = 𝐵 → (∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
43	38, 42	imbi12d 234	. . . 4 ⊢ (𝑥 = 𝐵 → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
44		nncn 9064	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
45	44	mulridd 8109	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ → (𝑚 · 1) = 𝑚)
46	45	eleq1d 2275	. . . . . . 7 ⊢ (𝑚 ∈ ℕ → ((𝑚 · 1) ∈ 𝑆 ↔ 𝑚 ∈ 𝑆))
47	46	biimpd 144	. . . . . 6 ⊢ (𝑚 ∈ ℕ → ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))
48	47	rgen 2560	. . . . 5 ⊢ ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆)
49	48	a1i 9	. . . 4 ⊢ (∀𝑝 ∈ ℙ (𝑝 ∥ 1 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 1) ∈ 𝑆 → 𝑚 ∈ 𝑆))
50		breq1 4054	. . . . . . 7 ⊢ (𝑝 = 𝑥 → (𝑝 ∥ 𝑥 ↔ 𝑥 ∥ 𝑥))
51		eleq1 2269	. . . . . . 7 ⊢ (𝑝 = 𝑥 → (𝑝 ∈ 𝑆 ↔ 𝑥 ∈ 𝑆))
52	50, 51	imbi12d 234	. . . . . 6 ⊢ (𝑝 = 𝑥 → ((𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) ↔ (𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆)))
53	52	rspcv 2877	. . . . 5 ⊢ (𝑥 ∈ ℙ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → (𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆)))
54		prmz 12508	. . . . . . 7 ⊢ (𝑥 ∈ ℙ → 𝑥 ∈ ℤ)
55		iddvds 12190	. . . . . . 7 ⊢ (𝑥 ∈ ℤ → 𝑥 ∥ 𝑥)
56	54, 55	syl 14	. . . . . 6 ⊢ (𝑥 ∈ ℙ → 𝑥 ∥ 𝑥)
57		2sq.1	. . . . . . . . . 10 ⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))
58		simprl 529	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑚 ∈ ℕ)
59		simpll 527	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑥 ∈ ℙ)
60		simprr 531	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → (𝑚 · 𝑥) ∈ 𝑆)
61		simplr 528	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑥 ∈ 𝑆)
62	57, 58, 59, 60, 61	2sqlem5 15671	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ (𝑚 ∈ ℕ ∧ (𝑚 · 𝑥) ∈ 𝑆)) → 𝑚 ∈ 𝑆)
63	62	expr 375	. . . . . . . 8 ⊢ (((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))
64	63	ralrimiva 2580	. . . . . . 7 ⊢ ((𝑥 ∈ ℙ ∧ 𝑥 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆))
65	64	ex 115	. . . . . 6 ⊢ (𝑥 ∈ ℙ → (𝑥 ∈ 𝑆 → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
66	56, 65	embantd 56	. . . . 5 ⊢ (𝑥 ∈ ℙ → ((𝑥 ∥ 𝑥 → 𝑥 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
67	53, 66	syld 45	. . . 4 ⊢ (𝑥 ∈ ℙ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑥 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑥) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
68		anim12 344	. . . . 5 ⊢ (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ∧ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
69		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
70		eluzelz 9677	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (ℤ_≥‘2) → 𝑦 ∈ ℤ)
71	70	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑦 ∈ ℤ)
72		eluzelz 9677	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℤ)
73	72	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → 𝑧 ∈ ℤ)
74		euclemma 12543	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑝 ∥ (𝑦 · 𝑧) ↔ (𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧)))
75	69, 71, 73, 74	syl3anc 1250	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝑦 · 𝑧) ↔ (𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧)))
76	75	imbi1d 231	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧) → 𝑝 ∈ 𝑆)))
77		jaob 712	. . . . . . . . . . . 12 ⊢ (((𝑝 ∥ 𝑦 ∨ 𝑝 ∥ 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
78	76, 77	bitrdi 196	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
79	78	ralbidva 2503	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ ∀𝑝 ∈ ℙ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
80		r19.26 2633	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ ℙ ((𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
81	79, 80	bitrdi 196	. . . . . . . . 9 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) ↔ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆))))
82	81	biimpa 296	. . . . . . . 8 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)))
83		oveq1 5964	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑚 · 𝑦) = (𝑛 · 𝑦))
84	83	eleq1d 2275	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑚 · 𝑦) ∈ 𝑆 ↔ (𝑛 · 𝑦) ∈ 𝑆))
85		eleq1 2269	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑆 ↔ 𝑛 ∈ 𝑆))
86	84, 85	imbi12d 234	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)))
87	86	cbvralvw 2743	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆))
88	44	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
89		uzssz 9688	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘2) ⊆ ℤ
90		zsscn 9400	. . . . . . . . . . . . . . . . 17 ⊢ ℤ ⊆ ℂ
91	89, 90	sstri 3206	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘2) ⊆ ℂ
92		simpll 527	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → 𝑦 ∈ (ℤ_≥‘2))
93	92	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈ (ℤ_≥‘2))
94	91, 93	sselid 3195	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑦 ∈ ℂ)
95		simplr 528	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → 𝑧 ∈ (ℤ_≥‘2))
96	95	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ (ℤ_≥‘2))
97	91, 96	sselid 3195	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℂ)
98		mul32 8222	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑧) = ((𝑚 · 𝑧) · 𝑦))
99		mulass 8076	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑦) · 𝑧) = (𝑚 · (𝑦 · 𝑧)))
100	98, 99	eqtr3d 2241	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑧) · 𝑦) = (𝑚 · (𝑦 · 𝑧)))
101	88, 94, 97, 100	syl3anc 1250	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ((𝑚 · 𝑧) · 𝑦) = (𝑚 · (𝑦 · 𝑧)))
102	101	eleq1d 2275	. . . . . . . . . . . . 13 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 ↔ (𝑚 · (𝑦 · 𝑧)) ∈ 𝑆))
103		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
104		eluz2nn 9707	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (ℤ_≥‘2) → 𝑧 ∈ ℕ)
105	96, 104	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℕ)
106	103, 105	nnmulcld 9105	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑧) ∈ ℕ)
107		simplr 528	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆))
108		oveq1 5964	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑚 · 𝑧) → (𝑛 · 𝑦) = ((𝑚 · 𝑧) · 𝑦))
109	108	eleq1d 2275	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 · 𝑧) → ((𝑛 · 𝑦) ∈ 𝑆 ↔ ((𝑚 · 𝑧) · 𝑦) ∈ 𝑆))
110		eleq1 2269	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑚 · 𝑧) → (𝑛 ∈ 𝑆 ↔ (𝑚 · 𝑧) ∈ 𝑆))
111	109, 110	imbi12d 234	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑚 · 𝑧) → (((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆) ↔ (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆)))
112	111	rspcv 2877	. . . . . . . . . . . . . 14 ⊢ ((𝑚 · 𝑧) ∈ ℕ → (∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆)))
113	106, 107, 112	sylc 62	. . . . . . . . . . . . 13 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) · 𝑦) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆))
114	102, 113	sylbird 170	. . . . . . . . . . . 12 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → (𝑚 · 𝑧) ∈ 𝑆))
115	114	imim1d 75	. . . . . . . . . . 11 ⊢ (((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) ∧ 𝑚 ∈ ℕ) → (((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
116	115	ralimdva 2574	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑛 ∈ ℕ ((𝑛 · 𝑦) ∈ 𝑆 → 𝑛 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
117	87, 116	sylan2b 287	. . . . . . . . 9 ⊢ ((((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
118	117	expimpd 363	. . . . . . . 8 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → ((∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆)) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
119	82, 118	embantd 56	. . . . . . 7 ⊢ (((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
120	119	ex 115	. . . . . 6 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
121	120	com23 78	. . . . 5 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆)) → (∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆) ∧ ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
122	68, 121	syl5 32	. . . 4 ⊢ ((𝑦 ∈ (ℤ_≥‘2) ∧ 𝑧 ∈ (ℤ_≥‘2)) → (((∀𝑝 ∈ ℙ (𝑝 ∥ 𝑦 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑦) ∈ 𝑆 → 𝑚 ∈ 𝑆)) ∧ (∀𝑝 ∈ ℙ (𝑝 ∥ 𝑧 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝑧) ∈ 𝑆 → 𝑚 ∈ 𝑆))) → (∀𝑝 ∈ ℙ (𝑝 ∥ (𝑦 · 𝑧) → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · (𝑦 · 𝑧)) ∈ 𝑆 → 𝑚 ∈ 𝑆))))
123	11, 19, 27, 35, 43, 49, 67, 122	prmind 12518	. . 3 ⊢ (𝐵 ∈ ℕ → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆) → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆)))
124	2, 3, 123	sylc 62	. 2 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆))
125		2sqlem6.4	. 2 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑆)
126		oveq1 5964	. . . . 5 ⊢ (𝑚 = 𝐴 → (𝑚 · 𝐵) = (𝐴 · 𝐵))
127	126	eleq1d 2275	. . . 4 ⊢ (𝑚 = 𝐴 → ((𝑚 · 𝐵) ∈ 𝑆 ↔ (𝐴 · 𝐵) ∈ 𝑆))
128		eleq1 2269	. . . 4 ⊢ (𝑚 = 𝐴 → (𝑚 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆))
129	127, 128	imbi12d 234	. . 3 ⊢ (𝑚 = 𝐴 → (((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆) ↔ ((𝐴 · 𝐵) ∈ 𝑆 → 𝐴 ∈ 𝑆)))
130	129	rspcv 2877	. 2 ⊢ (𝐴 ∈ ℕ → (∀𝑚 ∈ ℕ ((𝑚 · 𝐵) ∈ 𝑆 → 𝑚 ∈ 𝑆) → ((𝐴 · 𝐵) ∈ 𝑆 → 𝐴 ∈ 𝑆)))
131	1, 124, 125, 130	syl3c 63	1 ⊢ (𝜑 → 𝐴 ∈ 𝑆)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 710 ∧ w3a 981 = wceq 1373 ∈ wcel 2177 ∀wral 2485 class class class wbr 4051 ↦ cmpt 4113 ran crn 4684 ‘cfv 5280 (class class class)co 5957 ℂcc 7943 1c1 7946 · cmul 7950 ℕcn 9056 2c2 9107 ℤcz 9392 ℤ_≥cuz 9668 ↑cexp 10705 abscabs 11383 ∥ cdvds 12173 ℙcprime 12504 ℤ[i]cgz 12767

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4167 ax-sep 4170 ax-nul 4178 ax-pow 4226 ax-pr 4261 ax-un 4488 ax-setind 4593 ax-iinf 4644 ax-cnex 8036 ax-resscn 8037 ax-1cn 8038 ax-1re 8039 ax-icn 8040 ax-addcl 8041 ax-addrcl 8042 ax-mulcl 8043 ax-mulrcl 8044 ax-addcom 8045 ax-mulcom 8046 ax-addass 8047 ax-mulass 8048 ax-distr 8049 ax-i2m1 8050 ax-0lt1 8051 ax-1rid 8052 ax-0id 8053 ax-rnegex 8054 ax-precex 8055 ax-cnre 8056 ax-pre-ltirr 8057 ax-pre-ltwlin 8058 ax-pre-lttrn 8059 ax-pre-apti 8060 ax-pre-ltadd 8061 ax-pre-mulgt0 8062 ax-pre-mulext 8063 ax-arch 8064 ax-caucvg 8065

This theorem depends on definitions: df-bi 117 df-stab 833 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-if 3576 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3857 df-int 3892 df-iun 3935 df-br 4052 df-opab 4114 df-mpt 4115 df-tr 4151 df-id 4348 df-po 4351 df-iso 4352 df-iord 4421 df-on 4423 df-ilim 4424 df-suc 4426 df-iom 4647 df-xp 4689 df-rel 4690 df-cnv 4691 df-co 4692 df-dm 4693 df-rn 4694 df-res 4695 df-ima 4696 df-iota 5241 df-fun 5282 df-fn 5283 df-f 5284 df-f1 5285 df-fo 5286 df-f1o 5287 df-fv 5288 df-riota 5912 df-ov 5960 df-oprab 5961 df-mpo 5962 df-1st 6239 df-2nd 6240 df-recs 6404 df-frec 6490 df-1o 6515 df-2o 6516 df-er 6633 df-en 6841 df-sup 7101 df-pnf 8129 df-mnf 8130 df-xr 8131 df-ltxr 8132 df-le 8133 df-sub 8265 df-neg 8266 df-reap 8668 df-ap 8675 df-div 8766 df-inn 9057 df-2 9115 df-3 9116 df-4 9117 df-n0 9316 df-z 9393 df-uz 9669 df-q 9761 df-rp 9796 df-fz 10151 df-fzo 10285 df-fl 10435 df-mod 10490 df-seqfrec 10615 df-exp 10706 df-cj 11228 df-re 11229 df-im 11230 df-rsqrt 11384 df-abs 11385 df-dvds 12174 df-gcd 12350 df-prm 12505 df-gz 12768

This theorem is referenced by: 2sqlem8 15675

W3C validator