nn0prpwlem

Description: Lemma for nn0prpw . Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013)

		Ref	Expression
	Assertion	nn0prpwlem	$⊢ A \in ℕ \to \forall k \in ℕ (k < A \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A))$

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ x = A \to (k < x \leftrightarrow k < A)$
2		breq2	$⊢ x = A \to (p^{n} ∥ x \leftrightarrow p^{n} ∥ A)$
3	2	bibi2d	$⊢ x = A \to ((p^{n} ∥ k \leftrightarrow p^{n} ∥ x) \leftrightarrow (p^{n} ∥ k \leftrightarrow p^{n} ∥ A))$
4	3	notbid	$⊢ x = A \to (\neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x) \leftrightarrow \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A))$
5	4	2rexbidv	$⊢ x = A \to (\exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x) \leftrightarrow \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A))$
6	1 5	imbi12d	$⊢ x = A \to ((k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x)) \leftrightarrow (k < A \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A)))$
7	6	ralbidv	$⊢ x = A \to (\forall k \in ℕ (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x)) \leftrightarrow \forall k \in ℕ (k < A \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A)))$
8		breq2	$⊢ x = 1 \to (k < x \leftrightarrow k < 1)$
9		breq2	$⊢ x = 1 \to (p^{n} ∥ x \leftrightarrow p^{n} ∥ 1)$
10	9	bibi2d	$⊢ x = 1 \to ((p^{n} ∥ k \leftrightarrow p^{n} ∥ x) \leftrightarrow (p^{n} ∥ k \leftrightarrow p^{n} ∥ 1))$
11	10	notbid	$⊢ x = 1 \to (\neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x) \leftrightarrow \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ 1))$
12	11	2rexbidv	$⊢ x = 1 \to (\exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x) \leftrightarrow \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ 1))$
13	8 12	imbi12d	$⊢ x = 1 \to ((k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x)) \leftrightarrow (k < 1 \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ 1)))$
14	13	ralbidv	$⊢ x = 1 \to (\forall k \in ℕ (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x)) \leftrightarrow \forall k \in ℕ (k < 1 \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ 1)))$
15		breq2	$⊢ x = y \to (k < x \leftrightarrow k < y)$
16		breq2	$⊢ x = y \to (p^{n} ∥ x \leftrightarrow p^{n} ∥ y)$
17	16	bibi2d	$⊢ x = y \to ((p^{n} ∥ k \leftrightarrow p^{n} ∥ x) \leftrightarrow (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))$
18	17	notbid	$⊢ x = y \to (\neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x) \leftrightarrow \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))$
19	18	2rexbidv	$⊢ x = y \to (\exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x) \leftrightarrow \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))$
20	15 19	imbi12d	$⊢ x = y \to ((k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x)) \leftrightarrow (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y)))$
21	20	ralbidv	$⊢ x = y \to (\forall k \in ℕ (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x)) \leftrightarrow \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y)))$
22		nnnlt1	$⊢ k \in ℕ \to \neg k < 1$
23	22	pm2.21d	$⊢ k \in ℕ \to (k < 1 \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ 1))$
24	23	rgen	$⊢ \forall k \in ℕ (k < 1 \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ 1))$
25		exprmfct	$⊢ x \in ℤ_{\geq 2} \to \exists q \in ℙ q ∥ x$
26		prmz	$⊢ q \in ℙ \to q \in ℤ$
27	26	adantr	$⊢ (q \in ℙ \land t \in ℕ) \to q \in ℤ$
28		prmnn	$⊢ q \in ℙ \to q \in ℕ$
29	28	nnne0d	$⊢ q \in ℙ \to q \neq 0$
30	29	adantr	$⊢ (q \in ℙ \land t \in ℕ) \to q \neq 0$
31		nnz	$⊢ t \in ℕ \to t \in ℤ$
32	31	adantl	$⊢ (q \in ℙ \land t \in ℕ) \to t \in ℤ$
33		dvdsval2	$⊢ (q \in ℤ \land q \neq 0 \land t \in ℤ) \to (q ∥ t \leftrightarrow \frac{t}{q} \in ℤ)$
34	27 30 32 33	syl3anc	$⊢ (q \in ℙ \land t \in ℕ) \to (q ∥ t \leftrightarrow \frac{t}{q} \in ℤ)$
35	34	biimpd	$⊢ (q \in ℙ \land t \in ℕ) \to (q ∥ t \to \frac{t}{q} \in ℤ)$
36	35	3ad2antl2	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land t \in ℕ) \to (q ∥ t \to \frac{t}{q} \in ℤ)$
37	36	adantrl	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \land t \in ℕ)) \to (q ∥ t \to \frac{t}{q} \in ℤ)$
38		simprr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land \frac{t}{q} \in ℤ)) \to \frac{t}{q} \in ℤ$
39		nnre	$⊢ t \in ℕ \to t \in ℝ$
40		nngt0	$⊢ t \in ℕ \to 0 < t$
41	39 40	jca	$⊢ t \in ℕ \to (t \in ℝ \land 0 < t)$
42		nnre	$⊢ q \in ℕ \to q \in ℝ$
43		nngt0	$⊢ q \in ℕ \to 0 < q$
44	42 43	jca	$⊢ q \in ℕ \to (q \in ℝ \land 0 < q)$
45	28 44	syl	$⊢ q \in ℙ \to (q \in ℝ \land 0 < q)$
46		divgt0	$⊢ ((t \in ℝ \land 0 < t) \land (q \in ℝ \land 0 < q)) \to 0 < \frac{t}{q}$
47	41 45 46	syl2anr	$⊢ (q \in ℙ \land t \in ℕ) \to 0 < \frac{t}{q}$
48	47	3ad2antl2	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land t \in ℕ) \to 0 < \frac{t}{q}$
49	48	adantrr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land \frac{t}{q} \in ℤ)) \to 0 < \frac{t}{q}$
50		elnnz	$⊢ \frac{t}{q} \in ℕ \leftrightarrow (\frac{t}{q} \in ℤ \land 0 < \frac{t}{q})$
51	38 49 50	sylanbrc	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land \frac{t}{q} \in ℤ)) \to \frac{t}{q} \in ℕ$
52	51	expr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land t \in ℕ) \to (\frac{t}{q} \in ℤ \to \frac{t}{q} \in ℕ)$
53	52	adantrl	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \land t \in ℕ)) \to (\frac{t}{q} \in ℤ \to \frac{t}{q} \in ℕ)$
54	26	adantr	$⊢ (q \in ℙ \land x \in ℤ_{\geq 2}) \to q \in ℤ$
55	29	adantr	$⊢ (q \in ℙ \land x \in ℤ_{\geq 2}) \to q \neq 0$
56		eluzelz	$⊢ x \in ℤ_{\geq 2} \to x \in ℤ$
57	56	adantl	$⊢ (q \in ℙ \land x \in ℤ_{\geq 2}) \to x \in ℤ$
58		dvdsval2	$⊢ (q \in ℤ \land q \neq 0 \land x \in ℤ) \to (q ∥ x \leftrightarrow \frac{x}{q} \in ℤ)$
59	54 55 57 58	syl3anc	$⊢ (q \in ℙ \land x \in ℤ_{\geq 2}) \to (q ∥ x \leftrightarrow \frac{x}{q} \in ℤ)$
60		eluzelre	$⊢ x \in ℤ_{\geq 2} \to x \in ℝ$
61		2z	$⊢ 2 \in ℤ$
62	61	eluz1i	$⊢ x \in ℤ_{\geq 2} \leftrightarrow (x \in ℤ \land 2 \leq x)$
63		2pos	$⊢ 0 < 2$
64		zre	$⊢ x \in ℤ \to x \in ℝ$
65		0re	$⊢ 0 \in ℝ$
66		2re	$⊢ 2 \in ℝ$
67		ltletr	$⊢ (0 \in ℝ \land 2 \in ℝ \land x \in ℝ) \to ((0 < 2 \land 2 \leq x) \to 0 < x)$
68	65 66 67	mp3an12	$⊢ x \in ℝ \to ((0 < 2 \land 2 \leq x) \to 0 < x)$
69	64 68	syl	$⊢ x \in ℤ \to ((0 < 2 \land 2 \leq x) \to 0 < x)$
70	63 69	mpani	$⊢ x \in ℤ \to (2 \leq x \to 0 < x)$
71	70	imp	$⊢ (x \in ℤ \land 2 \leq x) \to 0 < x$
72	62 71	sylbi	$⊢ x \in ℤ_{\geq 2} \to 0 < x$
73	60 72	jca	$⊢ x \in ℤ_{\geq 2} \to (x \in ℝ \land 0 < x)$
74		divgt0	$⊢ ((x \in ℝ \land 0 < x) \land (q \in ℝ \land 0 < q)) \to 0 < \frac{x}{q}$
75	73 45 74	syl2anr	$⊢ (q \in ℙ \land x \in ℤ_{\geq 2}) \to 0 < \frac{x}{q}$
76	75	a1d	$⊢ (q \in ℙ \land x \in ℤ_{\geq 2}) \to (\frac{x}{q} \in ℤ \to 0 < \frac{x}{q})$
77	76	ancld	$⊢ (q \in ℙ \land x \in ℤ_{\geq 2}) \to (\frac{x}{q} \in ℤ \to (\frac{x}{q} \in ℤ \land 0 < \frac{x}{q}))$
78		elnnz	$⊢ \frac{x}{q} \in ℕ \leftrightarrow (\frac{x}{q} \in ℤ \land 0 < \frac{x}{q})$
79	77 78	syl6ibr	$⊢ (q \in ℙ \land x \in ℤ_{\geq 2}) \to (\frac{x}{q} \in ℤ \to \frac{x}{q} \in ℕ)$
80	59 79	sylbid	$⊢ (q \in ℙ \land x \in ℤ_{\geq 2}) \to (q ∥ x \to \frac{x}{q} \in ℕ)$
81	80	ancoms	$⊢ (x \in ℤ_{\geq 2} \land q \in ℙ) \to (q ∥ x \to \frac{x}{q} \in ℕ)$
82		breq1	$⊢ y = \frac{x}{q} \to (y < x \leftrightarrow \frac{x}{q} < x)$
83		breq2	$⊢ y = \frac{x}{q} \to (k < y \leftrightarrow k < \frac{x}{q})$
84		breq2	$⊢ y = \frac{x}{q} \to (p^{n} ∥ y \leftrightarrow p^{n} ∥ (\frac{x}{q}))$
85	84	bibi2d	$⊢ y = \frac{x}{q} \to ((p^{n} ∥ k \leftrightarrow p^{n} ∥ y) \leftrightarrow (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})))$
86	85	notbid	$⊢ y = \frac{x}{q} \to (\neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y) \leftrightarrow \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})))$
87	86	2rexbidv	$⊢ y = \frac{x}{q} \to (\exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y) \leftrightarrow \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})))$
88	83 87	imbi12d	$⊢ y = \frac{x}{q} \to ((k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y)) \leftrightarrow (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q}))))$
89	88	ralbidv	$⊢ y = \frac{x}{q} \to (\forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y)) \leftrightarrow \forall k \in ℕ (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q}))))$
90	82 89	imbi12d	$⊢ y = \frac{x}{q} \to ((y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \leftrightarrow (\frac{x}{q} < x \to \forall k \in ℕ (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})))))$
91	90	rspcv	$⊢ \frac{x}{q} \in ℕ \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to (\frac{x}{q} < x \to \forall k \in ℕ (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})))))$
92	91	3ad2ant1	$⊢ (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ) \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to (\frac{x}{q} < x \to \forall k \in ℕ (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})))))$
93	92	adantl	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to (\frac{x}{q} < x \to \forall k \in ℕ (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})))))$
94		eluzelcn	$⊢ x \in ℤ_{\geq 2} \to x \in ℂ$
95	94	mulid2d	$⊢ x \in ℤ_{\geq 2} \to 1 x = x$
96	95	ad2antrr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to 1 x = x$
97		prmgt1	$⊢ q \in ℙ \to 1 < q$
98	97	ad2antlr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to 1 < q$
99		1red	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to 1 \in ℝ$
100	28	nnred	$⊢ q \in ℙ \to q \in ℝ$
101	100	ad2antlr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to q \in ℝ$
102	60	ad2antrr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to x \in ℝ$
103	72	ad2antrr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to 0 < x$
104		ltmul1	$⊢ (1 \in ℝ \land q \in ℝ \land (x \in ℝ \land 0 < x)) \to (1 < q \leftrightarrow 1 x < q x)$
105	99 101 102 103 104	syl112anc	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to (1 < q \leftrightarrow 1 x < q x)$
106	98 105	mpbid	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to 1 x < q x$
107	96 106	eqbrtrrd	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to x < q x$
108	28 43	syl	$⊢ q \in ℙ \to 0 < q$
109	108	ad2antlr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to 0 < q$
110		ltdivmul	$⊢ (x \in ℝ \land x \in ℝ \land (q \in ℝ \land 0 < q)) \to (\frac{x}{q} < x \leftrightarrow x < q x)$
111	102 102 101 109 110	syl112anc	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to (\frac{x}{q} < x \leftrightarrow x < q x)$
112	107 111	mpbird	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to \frac{x}{q} < x$
113		breq1	$⊢ k = \frac{t}{q} \to (k < \frac{x}{q} \leftrightarrow \frac{t}{q} < \frac{x}{q})$
114		breq2	$⊢ k = \frac{t}{q} \to (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{t}{q}))$
115	114	bibi1d	$⊢ k = \frac{t}{q} \to ((p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})) \leftrightarrow (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))$
116	115	notbid	$⊢ k = \frac{t}{q} \to (\neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})) \leftrightarrow \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))$
117	116	2rexbidv	$⊢ k = \frac{t}{q} \to (\exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})) \leftrightarrow \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))$
118	113 117	imbi12d	$⊢ k = \frac{t}{q} \to ((k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \leftrightarrow (\frac{t}{q} < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))))$
119	118	rspcv	$⊢ \frac{t}{q} \in ℕ \to (\forall k \in ℕ (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \to (\frac{t}{q} < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))))$
120	119	3ad2ant2	$⊢ (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ) \to (\forall k \in ℕ (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \to (\frac{t}{q} < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))))$
121	120	adantl	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to (\forall k \in ℕ (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \to (\frac{t}{q} < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))))$
122	39	3ad2ant3	$⊢ (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ) \to t \in ℝ$
123	122	adantl	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to t \in ℝ$
124		ltdiv1	$⊢ (t \in ℝ \land x \in ℝ \land (q \in ℝ \land 0 < q)) \to (t < x \leftrightarrow \frac{t}{q} < \frac{x}{q})$
125	123 102 101 109 124	syl112anc	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to (t < x \leftrightarrow \frac{t}{q} < \frac{x}{q})$
126	125	biimpa	$⊢ (((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \to \frac{t}{q} < \frac{x}{q}$
127		simprll	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))) \to p \in ℙ$
128		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
129	128	adantl	$⊢ (p \in ℙ \land n \in ℕ) \to n + 1 \in ℕ$
130	129	ad2antrl	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q})))) \to n + 1 \in ℕ$
131	26	ad4antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to q \in ℤ$
132		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
133	132	ad2antll	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to n \in ℕ_{0}$
134		zexpcl	$⊢ (q \in ℤ \land n \in ℕ_{0}) \to q^{n} \in ℤ$
135	131 133 134	syl2anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to q^{n} \in ℤ$
136		nnz	$⊢ \frac{t}{q} \in ℕ \to \frac{t}{q} \in ℤ$
137	136	3ad2ant2	$⊢ (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ) \to \frac{t}{q} \in ℤ$
138	137	ad3antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to \frac{t}{q} \in ℤ$
139	29	ad4antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to q \neq 0$
140		dvdsmulcr	$⊢ (q^{n} \in ℤ \land \frac{t}{q} \in ℤ \land (q \in ℤ \land q \neq 0)) \to (q^{n} q ∥ (\frac{t}{q}) q \leftrightarrow q^{n} ∥ (\frac{t}{q}))$
141	135 138 131 139 140	syl112anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (q^{n} q ∥ (\frac{t}{q}) q \leftrightarrow q^{n} ∥ (\frac{t}{q}))$
142	28	nncnd	$⊢ q \in ℙ \to q \in ℂ$
143	142	ad4antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to q \in ℂ$
144	143 133	expp1d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to q^{n + 1} = q^{n} q$
145	144	eqcomd	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to q^{n} q = q^{n + 1}$
146		nncn	$⊢ t \in ℕ \to t \in ℂ$
147	146	3ad2ant3	$⊢ (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ) \to t \in ℂ$
148	147	ad3antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to t \in ℂ$
149	148 143 139	divcan1d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (\frac{t}{q}) q = t$
150	145 149	breq12d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (q^{n} q ∥ (\frac{t}{q}) q \leftrightarrow q^{n + 1} ∥ t)$
151	141 150	bitr3d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n + 1} ∥ t)$
152		nnz	$⊢ \frac{x}{q} \in ℕ \to \frac{x}{q} \in ℤ$
153	152	3ad2ant1	$⊢ (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ) \to \frac{x}{q} \in ℤ$
154	153	ad3antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to \frac{x}{q} \in ℤ$
155		dvdsmulcr	$⊢ (q^{n} \in ℤ \land \frac{x}{q} \in ℤ \land (q \in ℤ \land q \neq 0)) \to (q^{n} q ∥ (\frac{x}{q}) q \leftrightarrow q^{n} ∥ (\frac{x}{q}))$
156	135 154 131 139 155	syl112anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (q^{n} q ∥ (\frac{x}{q}) q \leftrightarrow q^{n} ∥ (\frac{x}{q}))$
157	94	ad4antr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to x \in ℂ$
158	157 143 139	divcan1d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (\frac{x}{q}) q = x$
159	145 158	breq12d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (q^{n} q ∥ (\frac{x}{q}) q \leftrightarrow q^{n + 1} ∥ x)$
160	156 159	bitr3d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (q^{n} ∥ (\frac{x}{q}) \leftrightarrow q^{n + 1} ∥ x)$
161	151 160	bibi12d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to ((q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q})) \leftrightarrow (q^{n + 1} ∥ t \leftrightarrow q^{n + 1} ∥ x))$
162	161	notbid	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (\neg (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q})) \leftrightarrow \neg (q^{n + 1} ∥ t \leftrightarrow q^{n + 1} ∥ x))$
163	162	biimpd	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (\neg (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q})) \to \neg (q^{n + 1} ∥ t \leftrightarrow q^{n + 1} ∥ x))$
164	163	impr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q})))) \to \neg (q^{n + 1} ∥ t \leftrightarrow q^{n + 1} ∥ x)$
165		oveq2	$⊢ m = n + 1 \to q^{m} = q^{n + 1}$
166	165	breq1d	$⊢ m = n + 1 \to (q^{m} ∥ t \leftrightarrow q^{n + 1} ∥ t)$
167	165	breq1d	$⊢ m = n + 1 \to (q^{m} ∥ x \leftrightarrow q^{n + 1} ∥ x)$
168	166 167	bibi12d	$⊢ m = n + 1 \to ((q^{m} ∥ t \leftrightarrow q^{m} ∥ x) \leftrightarrow (q^{n + 1} ∥ t \leftrightarrow q^{n + 1} ∥ x))$
169	168	notbid	$⊢ m = n + 1 \to (\neg (q^{m} ∥ t \leftrightarrow q^{m} ∥ x) \leftrightarrow \neg (q^{n + 1} ∥ t \leftrightarrow q^{n + 1} ∥ x))$
170	169	rspcev	$⊢ (n + 1 \in ℕ \land \neg (q^{n + 1} ∥ t \leftrightarrow q^{n + 1} ∥ x)) \to \exists m \in ℕ \neg (q^{m} ∥ t \leftrightarrow q^{m} ∥ x)$
171	130 164 170	syl2anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q})))) \to \exists m \in ℕ \neg (q^{m} ∥ t \leftrightarrow q^{m} ∥ x)$
172		oveq1	$⊢ p = q \to p^{n} = q^{n}$
173	172	breq1d	$⊢ p = q \to (p^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{t}{q}))$
174	172	breq1d	$⊢ p = q \to (p^{n} ∥ (\frac{x}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q}))$
175	173 174	bibi12d	$⊢ p = q \to ((p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})) \leftrightarrow (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q})))$
176	175	notbid	$⊢ p = q \to (\neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})) \leftrightarrow \neg (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q})))$
177	176	anbi2d	$⊢ p = q \to (((p \in ℙ \land n \in ℕ) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \leftrightarrow ((p \in ℙ \land n \in ℕ) \land \neg (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q}))))$
178	177	anbi2d	$⊢ p = q \to (((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))) \leftrightarrow ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q})))))$
179		oveq1	$⊢ p = q \to p^{m} = q^{m}$
180	179	breq1d	$⊢ p = q \to (p^{m} ∥ t \leftrightarrow q^{m} ∥ t)$
181	179	breq1d	$⊢ p = q \to (p^{m} ∥ x \leftrightarrow q^{m} ∥ x)$
182	180 181	bibi12d	$⊢ p = q \to ((p^{m} ∥ t \leftrightarrow p^{m} ∥ x) \leftrightarrow (q^{m} ∥ t \leftrightarrow q^{m} ∥ x))$
183	182	notbid	$⊢ p = q \to (\neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x) \leftrightarrow \neg (q^{m} ∥ t \leftrightarrow q^{m} ∥ x))$
184	183	rexbidv	$⊢ p = q \to (\exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x) \leftrightarrow \exists m \in ℕ \neg (q^{m} ∥ t \leftrightarrow q^{m} ∥ x))$
185	178 184	imbi12d	$⊢ p = q \to ((((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))) \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x)) \leftrightarrow (((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (q^{n} ∥ (\frac{t}{q}) \leftrightarrow q^{n} ∥ (\frac{x}{q})))) \to \exists m \in ℕ \neg (q^{m} ∥ t \leftrightarrow q^{m} ∥ x)))$
186	171 185	mpbiri	$⊢ p = q \to (((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))) \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x))$
187	186	com12	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))) \to (p = q \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x))$
188		simplr	$⊢ ((p \in ℙ \land n \in ℕ) \land \neg p = q) \to n \in ℕ$
189	188	ad2antlr	$⊢ (((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \to n \in ℕ$
190		prmz	$⊢ p \in ℙ \to p \in ℤ$
191	190	adantr	$⊢ (p \in ℙ \land n \in ℕ) \to p \in ℤ$
192	191	ad2antrl	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to p \in ℤ$
193	132	adantl	$⊢ (p \in ℙ \land n \in ℕ) \to n \in ℕ_{0}$
194	193	ad2antrl	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to n \in ℕ_{0}$
195		zexpcl	$⊢ (p \in ℤ \land n \in ℕ_{0}) \to p^{n} \in ℤ$
196	192 194 195	syl2anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to p^{n} \in ℤ$
197	26	ad4antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to q \in ℤ$
198	137	ad3antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to \frac{t}{q} \in ℤ$
199		dvdsmultr2	$⊢ (p^{n} \in ℤ \land q \in ℤ \land \frac{t}{q} \in ℤ) \to (p^{n} ∥ (\frac{t}{q}) \to p^{n} ∥ q (\frac{t}{q}))$
200	196 197 198 199	syl3anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (p^{n} ∥ (\frac{t}{q}) \to p^{n} ∥ q (\frac{t}{q}))$
201	196 197	gcdcomd	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to p^{n} \gcd q = q \gcd p^{n}$
202		simp-4r	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to q \in ℙ$
203		simprl	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to p \in ℙ$
204		simprr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to n \in ℕ$
205		prmdvdsexpb	$⊢ (q \in ℙ \land p \in ℙ \land n \in ℕ) \to (q ∥ p^{n} \leftrightarrow q = p)$
206		equcom	$⊢ q = p \leftrightarrow p = q$
207	205 206	bitrdi	$⊢ (q \in ℙ \land p \in ℙ \land n \in ℕ) \to (q ∥ p^{n} \leftrightarrow p = q)$
208	207	biimpd	$⊢ (q \in ℙ \land p \in ℙ \land n \in ℕ) \to (q ∥ p^{n} \to p = q)$
209	202 203 204 208	syl3anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (q ∥ p^{n} \to p = q)$
210	209	con3d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (\neg p = q \to \neg q ∥ p^{n})$
211	210	impr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to \neg q ∥ p^{n}$
212		simp-4r	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to q \in ℙ$
213		coprm	$⊢ (q \in ℙ \land p^{n} \in ℤ) \to (\neg q ∥ p^{n} \leftrightarrow q \gcd p^{n} = 1)$
214	212 196 213	syl2anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (\neg q ∥ p^{n} \leftrightarrow q \gcd p^{n} = 1)$
215	211 214	mpbid	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to q \gcd p^{n} = 1$
216	201 215	eqtrd	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to p^{n} \gcd q = 1$
217		coprmdvds	$⊢ (p^{n} \in ℤ \land q \in ℤ \land \frac{t}{q} \in ℤ) \to ((p^{n} ∥ q (\frac{t}{q}) \land p^{n} \gcd q = 1) \to p^{n} ∥ (\frac{t}{q}))$
218	196 197 198 217	syl3anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to ((p^{n} ∥ q (\frac{t}{q}) \land p^{n} \gcd q = 1) \to p^{n} ∥ (\frac{t}{q}))$
219	216 218	mpan2d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (p^{n} ∥ q (\frac{t}{q}) \to p^{n} ∥ (\frac{t}{q}))$
220	200 219	impbid	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ q (\frac{t}{q}))$
221	147	ad3antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to t \in ℂ$
222	142	ad4antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to q \in ℂ$
223	29	ad4antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to q \neq 0$
224	221 222 223	divcan2d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to q (\frac{t}{q}) = t$
225	224	breq2d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (p^{n} ∥ q (\frac{t}{q}) \leftrightarrow p^{n} ∥ t)$
226	220 225	bitrd	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ t)$
227	153	ad3antlr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to \frac{x}{q} \in ℤ$
228		dvdsmultr2	$⊢ (p^{n} \in ℤ \land q \in ℤ \land \frac{x}{q} \in ℤ) \to (p^{n} ∥ (\frac{x}{q}) \to p^{n} ∥ q (\frac{x}{q}))$
229	196 197 227 228	syl3anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (p^{n} ∥ (\frac{x}{q}) \to p^{n} ∥ q (\frac{x}{q}))$
230		coprmdvds	$⊢ (p^{n} \in ℤ \land q \in ℤ \land \frac{x}{q} \in ℤ) \to ((p^{n} ∥ q (\frac{x}{q}) \land p^{n} \gcd q = 1) \to p^{n} ∥ (\frac{x}{q}))$
231	196 197 227 230	syl3anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to ((p^{n} ∥ q (\frac{x}{q}) \land p^{n} \gcd q = 1) \to p^{n} ∥ (\frac{x}{q}))$
232	216 231	mpan2d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (p^{n} ∥ q (\frac{x}{q}) \to p^{n} ∥ (\frac{x}{q}))$
233	229 232	impbid	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (p^{n} ∥ (\frac{x}{q}) \leftrightarrow p^{n} ∥ q (\frac{x}{q}))$
234	94	ad4antr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to x \in ℂ$
235	234 222 223	divcan2d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to q (\frac{x}{q}) = x$
236	235	breq2d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (p^{n} ∥ q (\frac{x}{q}) \leftrightarrow p^{n} ∥ x)$
237	233 236	bitrd	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (p^{n} ∥ (\frac{x}{q}) \leftrightarrow p^{n} ∥ x)$
238	226 237	bibi12d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to ((p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})) \leftrightarrow (p^{n} ∥ t \leftrightarrow p^{n} ∥ x))$
239	238	notbid	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (\neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})) \leftrightarrow \neg (p^{n} ∥ t \leftrightarrow p^{n} ∥ x))$
240	239	biimpa	$⊢ (((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \to \neg (p^{n} ∥ t \leftrightarrow p^{n} ∥ x)$
241		oveq2	$⊢ m = n \to p^{m} = p^{n}$
242	241	breq1d	$⊢ m = n \to (p^{m} ∥ t \leftrightarrow p^{n} ∥ t)$
243	241	breq1d	$⊢ m = n \to (p^{m} ∥ x \leftrightarrow p^{n} ∥ x)$
244	242 243	bibi12d	$⊢ m = n \to ((p^{m} ∥ t \leftrightarrow p^{m} ∥ x) \leftrightarrow (p^{n} ∥ t \leftrightarrow p^{n} ∥ x))$
245	244	notbid	$⊢ m = n \to (\neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x) \leftrightarrow \neg (p^{n} ∥ t \leftrightarrow p^{n} ∥ x))$
246	245	rspcev	$⊢ (n \in ℕ \land \neg (p^{n} ∥ t \leftrightarrow p^{n} ∥ x)) \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x)$
247	189 240 246	syl2anc	$⊢ (((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x)$
248	247	ex	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg p = q)) \to (\neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})) \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x))$
249	248	expr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (\neg p = q \to (\neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})) \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x)))$
250	249	com23	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land (p \in ℙ \land n \in ℕ)) \to (\neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})) \to (\neg p = q \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x)))$
251	250	impr	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))) \to (\neg p = q \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x))$
252	187 251	pm2.61d	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))) \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x)$
253		oveq1	$⊢ r = p \to r^{m} = p^{m}$
254	253	breq1d	$⊢ r = p \to (r^{m} ∥ t \leftrightarrow p^{m} ∥ t)$
255	253	breq1d	$⊢ r = p \to (r^{m} ∥ x \leftrightarrow p^{m} ∥ x)$
256	254 255	bibi12d	$⊢ r = p \to ((r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow (p^{m} ∥ t \leftrightarrow p^{m} ∥ x))$
257	256	notbid	$⊢ r = p \to (\neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x))$
258	257	rexbidv	$⊢ r = p \to (\exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x))$
259	258	rspcev	$⊢ (p \in ℙ \land \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x)) \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)$
260	127 252 259	syl2anc	$⊢ ((((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \land ((p \in ℙ \land n \in ℕ) \land \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})))) \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)$
261	260	exp32	$⊢ (((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \to ((p \in ℙ \land n \in ℕ) \to (\neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})) \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
262	261	rexlimdvv	$⊢ (((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \to (\exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q})) \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x))$
263	126 262	embantd	$⊢ (((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \land t < x) \to ((\frac{t}{q} < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x))$
264	263	ex	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to (t < x \to ((\frac{t}{q} < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
265	264	com23	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to ((\frac{t}{q} < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ (\frac{t}{q}) \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
266	121 265	syld	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to (\forall k \in ℕ (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q}))) \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
267	112 266	embantd	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to ((\frac{x}{q} < x \to \forall k \in ℕ (k < \frac{x}{q} \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ (\frac{x}{q})))) \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
268	93 267	syld	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ) \land (\frac{x}{q} \in ℕ \land \frac{t}{q} \in ℕ \land t \in ℕ)) \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
269	268	3exp2	$⊢ (x \in ℤ_{\geq 2} \land q \in ℙ) \to (\frac{x}{q} \in ℕ \to (\frac{t}{q} \in ℕ \to (t \in ℕ \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x))))))$
270	81 269	syld	$⊢ (x \in ℤ_{\geq 2} \land q \in ℙ) \to (q ∥ x \to (\frac{t}{q} \in ℕ \to (t \in ℕ \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x))))))$
271	270	3impia	$⊢ (x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \to (\frac{t}{q} \in ℕ \to (t \in ℕ \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))))$
272	271	com24	$⊢ (x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to (t \in ℕ \to (\frac{t}{q} \in ℕ \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))))$
273	272	imp32	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \land t \in ℕ)) \to (\frac{t}{q} \in ℕ \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
274	37 53 273	3syld	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \land t \in ℕ)) \to (q ∥ t \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
275		simpl2	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land (\neg q ∥ t \land t < x))) \to q \in ℙ$
276		1nn	$⊢ 1 \in ℕ$
277	276	a1i	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land (\neg q ∥ t \land t < x))) \to 1 \in ℕ$
278	142	exp1d	$⊢ q \in ℙ \to q^{1} = q$
279	278	breq1d	$⊢ q \in ℙ \to (q^{1} ∥ t \leftrightarrow q ∥ t)$
280	279	notbid	$⊢ q \in ℙ \to (\neg q^{1} ∥ t \leftrightarrow \neg q ∥ t)$
281	280	biimpar	$⊢ (q \in ℙ \land \neg q ∥ t) \to \neg q^{1} ∥ t$
282	281	3ad2antl2	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land \neg q ∥ t) \to \neg q^{1} ∥ t$
283	282	adantrr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (\neg q ∥ t \land t < x)) \to \neg q^{1} ∥ t$
284	283	adantrl	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land (\neg q ∥ t \land t < x))) \to \neg q^{1} ∥ t$
285	278	breq1d	$⊢ q \in ℙ \to (q^{1} ∥ x \leftrightarrow q ∥ x)$
286	285	biimpar	$⊢ (q \in ℙ \land q ∥ x) \to q^{1} ∥ x$
287	286	3adant1	$⊢ (x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \to q^{1} ∥ x$
288		idd	$⊢ (x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \to ((q^{1} ∥ x \to q^{1} ∥ t) \to (q^{1} ∥ x \to q^{1} ∥ t))$
289	287 288	mpid	$⊢ (x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \to ((q^{1} ∥ x \to q^{1} ∥ t) \to q^{1} ∥ t)$
290	289	adantr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land (\neg q ∥ t \land t < x))) \to ((q^{1} ∥ x \to q^{1} ∥ t) \to q^{1} ∥ t)$
291	284 290	mtod	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land (\neg q ∥ t \land t < x))) \to \neg (q^{1} ∥ x \to q^{1} ∥ t)$
292		biimpr	$⊢ (q^{1} ∥ t \leftrightarrow q^{1} ∥ x) \to (q^{1} ∥ x \to q^{1} ∥ t)$
293	291 292	nsyl	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land (\neg q ∥ t \land t < x))) \to \neg (q^{1} ∥ t \leftrightarrow q^{1} ∥ x)$
294		oveq1	$⊢ r = q \to r^{m} = q^{m}$
295	294	breq1d	$⊢ r = q \to (r^{m} ∥ t \leftrightarrow q^{m} ∥ t)$
296	294	breq1d	$⊢ r = q \to (r^{m} ∥ x \leftrightarrow q^{m} ∥ x)$
297	295 296	bibi12d	$⊢ r = q \to ((r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow (q^{m} ∥ t \leftrightarrow q^{m} ∥ x))$
298	297	notbid	$⊢ r = q \to (\neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow \neg (q^{m} ∥ t \leftrightarrow q^{m} ∥ x))$
299		oveq2	$⊢ m = 1 \to q^{m} = q^{1}$
300	299	breq1d	$⊢ m = 1 \to (q^{m} ∥ t \leftrightarrow q^{1} ∥ t)$
301	299	breq1d	$⊢ m = 1 \to (q^{m} ∥ x \leftrightarrow q^{1} ∥ x)$
302	300 301	bibi12d	$⊢ m = 1 \to ((q^{m} ∥ t \leftrightarrow q^{m} ∥ x) \leftrightarrow (q^{1} ∥ t \leftrightarrow q^{1} ∥ x))$
303	302	notbid	$⊢ m = 1 \to (\neg (q^{m} ∥ t \leftrightarrow q^{m} ∥ x) \leftrightarrow \neg (q^{1} ∥ t \leftrightarrow q^{1} ∥ x))$
304	298 303	rspc2ev	$⊢ (q \in ℙ \land 1 \in ℕ \land \neg (q^{1} ∥ t \leftrightarrow q^{1} ∥ x)) \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)$
305	275 277 293 304	syl3anc	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land (\neg q ∥ t \land t < x))) \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)$
306	305	expr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land t \in ℕ) \to ((\neg q ∥ t \land t < x) \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x))$
307	306	expd	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land t \in ℕ) \to (\neg q ∥ t \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
308	307	adantrl	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \land t \in ℕ)) \to (\neg q ∥ t \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
309	274 308	pm2.61d	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \land t \in ℕ)) \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x))$
310	309	expr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land \forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y)))) \to (t \in ℕ \to (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)))$
311	310	ralrimiv	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land \forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y)))) \to \forall t \in ℕ (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x))$
312		breq1	$⊢ t = k \to (t < x \leftrightarrow k < x)$
313		breq2	$⊢ t = k \to (r^{m} ∥ t \leftrightarrow r^{m} ∥ k)$
314	313	bibi1d	$⊢ t = k \to ((r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow (r^{m} ∥ k \leftrightarrow r^{m} ∥ x))$
315	314	notbid	$⊢ t = k \to (\neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow \neg (r^{m} ∥ k \leftrightarrow r^{m} ∥ x))$
316	315	2rexbidv	$⊢ t = k \to (\exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ k \leftrightarrow r^{m} ∥ x))$
317	253	breq1d	$⊢ r = p \to (r^{m} ∥ k \leftrightarrow p^{m} ∥ k)$
318	317 255	bibi12d	$⊢ r = p \to ((r^{m} ∥ k \leftrightarrow r^{m} ∥ x) \leftrightarrow (p^{m} ∥ k \leftrightarrow p^{m} ∥ x))$
319	318	notbid	$⊢ r = p \to (\neg (r^{m} ∥ k \leftrightarrow r^{m} ∥ x) \leftrightarrow \neg (p^{m} ∥ k \leftrightarrow p^{m} ∥ x))$
320	241	breq1d	$⊢ m = n \to (p^{m} ∥ k \leftrightarrow p^{n} ∥ k)$
321	320 243	bibi12d	$⊢ m = n \to ((p^{m} ∥ k \leftrightarrow p^{m} ∥ x) \leftrightarrow (p^{n} ∥ k \leftrightarrow p^{n} ∥ x))$
322	321	notbid	$⊢ m = n \to (\neg (p^{m} ∥ k \leftrightarrow p^{m} ∥ x) \leftrightarrow \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x))$
323	319 322	cbvrex2vw	$⊢ \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ k \leftrightarrow r^{m} ∥ x) \leftrightarrow \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x)$
324	316 323	bitrdi	$⊢ t = k \to (\exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x))$
325	312 324	imbi12d	$⊢ t = k \to ((t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)) \leftrightarrow (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x)))$
326	325	cbvralvw	$⊢ \forall t \in ℕ (t < x \to \exists r \in ℙ \exists m \in ℕ \neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x)) \leftrightarrow \forall k \in ℕ (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x))$
327	311 326	sylib	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land \forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y)))) \to \forall k \in ℕ (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x))$
328	327	3exp1	$⊢ x \in ℤ_{\geq 2} \to (q \in ℙ \to (q ∥ x \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to \forall k \in ℕ (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x)))))$
329	328	rexlimdv	$⊢ x \in ℤ_{\geq 2} \to (\exists q \in ℙ q ∥ x \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to \forall k \in ℕ (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x))))$
330	25 329	mpd	$⊢ x \in ℤ_{\geq 2} \to (\forall y \in ℕ (y < x \to \forall k \in ℕ (k < y \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ y))) \to \forall k \in ℕ (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x)))$
331	14 21 24 330	indstr2	$⊢ x \in ℕ \to \forall k \in ℕ (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x))$
332	7 331	vtoclga	$⊢ A \in ℕ \to \forall k \in ℕ (k < A \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ A))$

Metamath Proof Explorer

Theorem nn0prpwlem

Proof