2sqlem6

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)

	Ref	Expression
Hypotheses	2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
	2sqlem6.1	$⊢ φ \to A \in ℕ$
	2sqlem6.2	$⊢ φ \to B \in ℕ$
	2sqlem6.3	$⊢ φ \to \forall p \in ℙ (p ∥ B \to p \in S)$
	2sqlem6.4	$⊢ φ \to A B \in S$
Assertion	2sqlem6	$⊢ φ \to A \in S$

Proof

Step	Hyp	Ref	Expression
1		2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
2		2sqlem6.1	$⊢ φ \to A \in ℕ$
3		2sqlem6.2	$⊢ φ \to B \in ℕ$
4		2sqlem6.3	$⊢ φ \to \forall p \in ℙ (p ∥ B \to p \in S)$
5		2sqlem6.4	$⊢ φ \to A B \in S$
6		breq2	$⊢ x = 1 \to (p ∥ x \leftrightarrow p ∥ 1)$
7	6	imbi1d	$⊢ x = 1 \to ((p ∥ x \to p \in S) \leftrightarrow (p ∥ 1 \to p \in S))$
8	7	ralbidv	$⊢ x = 1 \to (\forall p \in ℙ (p ∥ x \to p \in S) \leftrightarrow \forall p \in ℙ (p ∥ 1 \to p \in S))$
9		oveq2	$⊢ x = 1 \to m x = m \cdot 1$
10	9	eleq1d	$⊢ x = 1 \to (m x \in S \leftrightarrow m \cdot 1 \in S)$
11	10	imbi1d	$⊢ x = 1 \to ((m x \in S \to m \in S) \leftrightarrow (m \cdot 1 \in S \to m \in S))$
12	11	ralbidv	$⊢ x = 1 \to (\forall m \in ℕ (m x \in S \to m \in S) \leftrightarrow \forall m \in ℕ (m \cdot 1 \in S \to m \in S))$
13	8 12	imbi12d	$⊢ x = 1 \to ((\forall p \in ℙ (p ∥ x \to p \in S) \to \forall m \in ℕ (m x \in S \to m \in S)) \leftrightarrow (\forall p \in ℙ (p ∥ 1 \to p \in S) \to \forall m \in ℕ (m \cdot 1 \in S \to m \in S)))$
14		breq2	$⊢ x = y \to (p ∥ x \leftrightarrow p ∥ y)$
15	14	imbi1d	$⊢ x = y \to ((p ∥ x \to p \in S) \leftrightarrow (p ∥ y \to p \in S))$
16	15	ralbidv	$⊢ x = y \to (\forall p \in ℙ (p ∥ x \to p \in S) \leftrightarrow \forall p \in ℙ (p ∥ y \to p \in S))$
17		oveq2	$⊢ x = y \to m x = m y$
18	17	eleq1d	$⊢ x = y \to (m x \in S \leftrightarrow m y \in S)$
19	18	imbi1d	$⊢ x = y \to ((m x \in S \to m \in S) \leftrightarrow (m y \in S \to m \in S))$
20	19	ralbidv	$⊢ x = y \to (\forall m \in ℕ (m x \in S \to m \in S) \leftrightarrow \forall m \in ℕ (m y \in S \to m \in S))$
21	16 20	imbi12d	$⊢ x = y \to ((\forall p \in ℙ (p ∥ x \to p \in S) \to \forall m \in ℕ (m x \in S \to m \in S)) \leftrightarrow (\forall p \in ℙ (p ∥ y \to p \in S) \to \forall m \in ℕ (m y \in S \to m \in S)))$
22		breq2	$⊢ x = z \to (p ∥ x \leftrightarrow p ∥ z)$
23	22	imbi1d	$⊢ x = z \to ((p ∥ x \to p \in S) \leftrightarrow (p ∥ z \to p \in S))$
24	23	ralbidv	$⊢ x = z \to (\forall p \in ℙ (p ∥ x \to p \in S) \leftrightarrow \forall p \in ℙ (p ∥ z \to p \in S))$
25		oveq2	$⊢ x = z \to m x = m z$
26	25	eleq1d	$⊢ x = z \to (m x \in S \leftrightarrow m z \in S)$
27	26	imbi1d	$⊢ x = z \to ((m x \in S \to m \in S) \leftrightarrow (m z \in S \to m \in S))$
28	27	ralbidv	$⊢ x = z \to (\forall m \in ℕ (m x \in S \to m \in S) \leftrightarrow \forall m \in ℕ (m z \in S \to m \in S))$
29	24 28	imbi12d	$⊢ x = z \to ((\forall p \in ℙ (p ∥ x \to p \in S) \to \forall m \in ℕ (m x \in S \to m \in S)) \leftrightarrow (\forall p \in ℙ (p ∥ z \to p \in S) \to \forall m \in ℕ (m z \in S \to m \in S)))$
30		breq2	$⊢ x = y z \to (p ∥ x \leftrightarrow p ∥ y z)$
31	30	imbi1d	$⊢ x = y z \to ((p ∥ x \to p \in S) \leftrightarrow (p ∥ y z \to p \in S))$
32	31	ralbidv	$⊢ x = y z \to (\forall p \in ℙ (p ∥ x \to p \in S) \leftrightarrow \forall p \in ℙ (p ∥ y z \to p \in S))$
33		oveq2	$⊢ x = y z \to m x = m y z$
34	33	eleq1d	$⊢ x = y z \to (m x \in S \leftrightarrow m y z \in S)$
35	34	imbi1d	$⊢ x = y z \to ((m x \in S \to m \in S) \leftrightarrow (m y z \in S \to m \in S))$
36	35	ralbidv	$⊢ x = y z \to (\forall m \in ℕ (m x \in S \to m \in S) \leftrightarrow \forall m \in ℕ (m y z \in S \to m \in S))$
37	32 36	imbi12d	$⊢ x = y z \to ((\forall p \in ℙ (p ∥ x \to p \in S) \to \forall m \in ℕ (m x \in S \to m \in S)) \leftrightarrow (\forall p \in ℙ (p ∥ y z \to p \in S) \to \forall m \in ℕ (m y z \in S \to m \in S)))$
38		breq2	$⊢ x = B \to (p ∥ x \leftrightarrow p ∥ B)$
39	38	imbi1d	$⊢ x = B \to ((p ∥ x \to p \in S) \leftrightarrow (p ∥ B \to p \in S))$
40	39	ralbidv	$⊢ x = B \to (\forall p \in ℙ (p ∥ x \to p \in S) \leftrightarrow \forall p \in ℙ (p ∥ B \to p \in S))$
41		oveq2	$⊢ x = B \to m x = m B$
42	41	eleq1d	$⊢ x = B \to (m x \in S \leftrightarrow m B \in S)$
43	42	imbi1d	$⊢ x = B \to ((m x \in S \to m \in S) \leftrightarrow (m B \in S \to m \in S))$
44	43	ralbidv	$⊢ x = B \to (\forall m \in ℕ (m x \in S \to m \in S) \leftrightarrow \forall m \in ℕ (m B \in S \to m \in S))$
45	40 44	imbi12d	$⊢ x = B \to ((\forall p \in ℙ (p ∥ x \to p \in S) \to \forall m \in ℕ (m x \in S \to m \in S)) \leftrightarrow (\forall p \in ℙ (p ∥ B \to p \in S) \to \forall m \in ℕ (m B \in S \to m \in S)))$
46		nncn	$⊢ m \in ℕ \to m \in ℂ$
47	46	mulid1d	$⊢ m \in ℕ \to m \cdot 1 = m$
48	47	eleq1d	$⊢ m \in ℕ \to (m \cdot 1 \in S \leftrightarrow m \in S)$
49	48	biimpd	$⊢ m \in ℕ \to (m \cdot 1 \in S \to m \in S)$
50	49	rgen	$⊢ \forall m \in ℕ (m \cdot 1 \in S \to m \in S)$
51	50	a1i	$⊢ \forall p \in ℙ (p ∥ 1 \to p \in S) \to \forall m \in ℕ (m \cdot 1 \in S \to m \in S)$
52		breq1	$⊢ p = x \to (p ∥ x \leftrightarrow x ∥ x)$
53		eleq1	$⊢ p = x \to (p \in S \leftrightarrow x \in S)$
54	52 53	imbi12d	$⊢ p = x \to ((p ∥ x \to p \in S) \leftrightarrow (x ∥ x \to x \in S))$
55	54	rspcv	$⊢ x \in ℙ \to (\forall p \in ℙ (p ∥ x \to p \in S) \to (x ∥ x \to x \in S))$
56		prmz	$⊢ x \in ℙ \to x \in ℤ$
57		iddvds	$⊢ x \in ℤ \to x ∥ x$
58	56 57	syl	$⊢ x \in ℙ \to x ∥ x$
59		simprl	$⊢ ((x \in ℙ \land x \in S) \land (m \in ℕ \land m x \in S)) \to m \in ℕ$
60		simpll	$⊢ ((x \in ℙ \land x \in S) \land (m \in ℕ \land m x \in S)) \to x \in ℙ$
61		simprr	$⊢ ((x \in ℙ \land x \in S) \land (m \in ℕ \land m x \in S)) \to m x \in S$
62		simplr	$⊢ ((x \in ℙ \land x \in S) \land (m \in ℕ \land m x \in S)) \to x \in S$
63	1 59 60 61 62	2sqlem5	$⊢ ((x \in ℙ \land x \in S) \land (m \in ℕ \land m x \in S)) \to m \in S$
64	63	expr	$⊢ ((x \in ℙ \land x \in S) \land m \in ℕ) \to (m x \in S \to m \in S)$
65	64	ralrimiva	$⊢ (x \in ℙ \land x \in S) \to \forall m \in ℕ (m x \in S \to m \in S)$
66	65	ex	$⊢ x \in ℙ \to (x \in S \to \forall m \in ℕ (m x \in S \to m \in S))$
67	58 66	embantd	$⊢ x \in ℙ \to ((x ∥ x \to x \in S) \to \forall m \in ℕ (m x \in S \to m \in S))$
68	55 67	syld	$⊢ x \in ℙ \to (\forall p \in ℙ (p ∥ x \to p \in S) \to \forall m \in ℕ (m x \in S \to m \in S))$
69		anim12	$⊢ ((\forall p \in ℙ (p ∥ y \to p \in S) \to \forall m \in ℕ (m y \in S \to m \in S)) \land (\forall p \in ℙ (p ∥ z \to p \in S) \to \forall m \in ℕ (m z \in S \to m \in S))) \to ((\forall p \in ℙ (p ∥ y \to p \in S) \land \forall p \in ℙ (p ∥ z \to p \in S)) \to (\forall m \in ℕ (m y \in S \to m \in S) \land \forall m \in ℕ (m z \in S \to m \in S)))$
70		simpr	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to p \in ℙ$
71		eluzelz	$⊢ y \in ℤ_{\geq 2} \to y \in ℤ$
72	71	ad2antrr	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to y \in ℤ$
73		eluzelz	$⊢ z \in ℤ_{\geq 2} \to z \in ℤ$
74	73	ad2antlr	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to z \in ℤ$
75		euclemma	$⊢ (p \in ℙ \land y \in ℤ \land z \in ℤ) \to (p ∥ y z \leftrightarrow (p ∥ y \lor p ∥ z))$
76	70 72 74 75	syl3anc	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to (p ∥ y z \leftrightarrow (p ∥ y \lor p ∥ z))$
77	76	imbi1d	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to ((p ∥ y z \to p \in S) \leftrightarrow ((p ∥ y \lor p ∥ z) \to p \in S))$
78		jaob	$⊢ ((p ∥ y \lor p ∥ z) \to p \in S) \leftrightarrow ((p ∥ y \to p \in S) \land (p ∥ z \to p \in S))$
79	77 78	bitrdi	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land p \in ℙ) \to ((p ∥ y z \to p \in S) \leftrightarrow ((p ∥ y \to p \in S) \land (p ∥ z \to p \in S)))$
80	79	ralbidva	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to (\forall p \in ℙ (p ∥ y z \to p \in S) \leftrightarrow \forall p \in ℙ ((p ∥ y \to p \in S) \land (p ∥ z \to p \in S)))$
81		r19.26	$⊢ \forall p \in ℙ ((p ∥ y \to p \in S) \land (p ∥ z \to p \in S)) \leftrightarrow (\forall p \in ℙ (p ∥ y \to p \in S) \land \forall p \in ℙ (p ∥ z \to p \in S))$
82	80 81	bitrdi	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to (\forall p \in ℙ (p ∥ y z \to p \in S) \leftrightarrow (\forall p \in ℙ (p ∥ y \to p \in S) \land \forall p \in ℙ (p ∥ z \to p \in S)))$
83	82	biimpa	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \to (\forall p \in ℙ (p ∥ y \to p \in S) \land \forall p \in ℙ (p ∥ z \to p \in S))$
84		oveq1	$⊢ m = n \to m y = n y$
85	84	eleq1d	$⊢ m = n \to (m y \in S \leftrightarrow n y \in S)$
86		eleq1	$⊢ m = n \to (m \in S \leftrightarrow n \in S)$
87	85 86	imbi12d	$⊢ m = n \to ((m y \in S \to m \in S) \leftrightarrow (n y \in S \to n \in S))$
88	87	cbvralvw	$⊢ \forall m \in ℕ (m y \in S \to m \in S) \leftrightarrow \forall n \in ℕ (n y \in S \to n \in S)$
89	46	adantl	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to m \in ℂ$
90		uzssz	$⊢ ℤ_{\geq 2} \subseteq ℤ$
91		zsscn	$⊢ ℤ \subseteq ℂ$
92	90 91	sstri	$⊢ ℤ_{\geq 2} \subseteq ℂ$
93		simpll	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \to y \in ℤ_{\geq 2}$
94	93	ad2antrr	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to y \in ℤ_{\geq 2}$
95	92 94	sselid	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to y \in ℂ$
96		simplr	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \to z \in ℤ_{\geq 2}$
97	96	ad2antrr	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to z \in ℤ_{\geq 2}$
98	92 97	sselid	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to z \in ℂ$
99		mul32	$⊢ (m \in ℂ \land y \in ℂ \land z \in ℂ) \to m y z = m z y$
100		mulass	$⊢ (m \in ℂ \land y \in ℂ \land z \in ℂ) \to m y z = m y z$
101	99 100	eqtr3d	$⊢ (m \in ℂ \land y \in ℂ \land z \in ℂ) \to m z y = m y z$
102	89 95 98 101	syl3anc	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to m z y = m y z$
103	102	eleq1d	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to (m z y \in S \leftrightarrow m y z \in S)$
104		simpr	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to m \in ℕ$
105		eluz2nn	$⊢ z \in ℤ_{\geq 2} \to z \in ℕ$
106	97 105	syl	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to z \in ℕ$
107	104 106	nnmulcld	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to m z \in ℕ$
108		simplr	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to \forall n \in ℕ (n y \in S \to n \in S)$
109		oveq1	$⊢ n = m z \to n y = m z y$
110	109	eleq1d	$⊢ n = m z \to (n y \in S \leftrightarrow m z y \in S)$
111		eleq1	$⊢ n = m z \to (n \in S \leftrightarrow m z \in S)$
112	110 111	imbi12d	$⊢ n = m z \to ((n y \in S \to n \in S) \leftrightarrow (m z y \in S \to m z \in S))$
113	112	rspcv	$⊢ m z \in ℕ \to (\forall n \in ℕ (n y \in S \to n \in S) \to (m z y \in S \to m z \in S))$
114	107 108 113	sylc	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to (m z y \in S \to m z \in S)$
115	103 114	sylbird	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to (m y z \in S \to m z \in S)$
116	115	imim1d	$⊢ ((((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \land m \in ℕ) \to ((m z \in S \to m \in S) \to (m y z \in S \to m \in S))$
117	116	ralimdva	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall n \in ℕ (n y \in S \to n \in S)) \to (\forall m \in ℕ (m z \in S \to m \in S) \to \forall m \in ℕ (m y z \in S \to m \in S))$
118	88 117	sylan2b	$⊢ (((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \land \forall m \in ℕ (m y \in S \to m \in S)) \to (\forall m \in ℕ (m z \in S \to m \in S) \to \forall m \in ℕ (m y z \in S \to m \in S))$
119	118	expimpd	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \to ((\forall m \in ℕ (m y \in S \to m \in S) \land \forall m \in ℕ (m z \in S \to m \in S)) \to \forall m \in ℕ (m y z \in S \to m \in S))$
120	83 119	embantd	$⊢ ((y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \land \forall p \in ℙ (p ∥ y z \to p \in S)) \to (((\forall p \in ℙ (p ∥ y \to p \in S) \land \forall p \in ℙ (p ∥ z \to p \in S)) \to (\forall m \in ℕ (m y \in S \to m \in S) \land \forall m \in ℕ (m z \in S \to m \in S))) \to \forall m \in ℕ (m y z \in S \to m \in S))$
121	120	ex	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to (\forall p \in ℙ (p ∥ y z \to p \in S) \to (((\forall p \in ℙ (p ∥ y \to p \in S) \land \forall p \in ℙ (p ∥ z \to p \in S)) \to (\forall m \in ℕ (m y \in S \to m \in S) \land \forall m \in ℕ (m z \in S \to m \in S))) \to \forall m \in ℕ (m y z \in S \to m \in S)))$
122	121	com23	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to (((\forall p \in ℙ (p ∥ y \to p \in S) \land \forall p \in ℙ (p ∥ z \to p \in S)) \to (\forall m \in ℕ (m y \in S \to m \in S) \land \forall m \in ℕ (m z \in S \to m \in S))) \to (\forall p \in ℙ (p ∥ y z \to p \in S) \to \forall m \in ℕ (m y z \in S \to m \in S)))$
123	69 122	syl5	$⊢ (y \in ℤ_{\geq 2} \land z \in ℤ_{\geq 2}) \to (((\forall p \in ℙ (p ∥ y \to p \in S) \to \forall m \in ℕ (m y \in S \to m \in S)) \land (\forall p \in ℙ (p ∥ z \to p \in S) \to \forall m \in ℕ (m z \in S \to m \in S))) \to (\forall p \in ℙ (p ∥ y z \to p \in S) \to \forall m \in ℕ (m y z \in S \to m \in S)))$
124	13 21 29 37 45 51 68 123	prmind	$⊢ B \in ℕ \to (\forall p \in ℙ (p ∥ B \to p \in S) \to \forall m \in ℕ (m B \in S \to m \in S))$
125	3 4 124	sylc	$⊢ φ \to \forall m \in ℕ (m B \in S \to m \in S)$
126		oveq1	$⊢ m = A \to m B = A B$
127	126	eleq1d	$⊢ m = A \to (m B \in S \leftrightarrow A B \in S)$
128		eleq1	$⊢ m = A \to (m \in S \leftrightarrow A \in S)$
129	127 128	imbi12d	$⊢ m = A \to ((m B \in S \to m \in S) \leftrightarrow (A B \in S \to A \in S))$
130	129	rspcv	$⊢ A \in ℕ \to (\forall m \in ℕ (m B \in S \to m \in S) \to (A B \in S \to A \in S))$
131	2 125 5 130	syl3c	$⊢ φ \to A \in S$

Metamath Proof Explorer

Theorem 2sqlem6

Proof