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		gcdcom	$⊢ (p^{n} \in ℤ \land q \in ℤ) \to p^{n} \gcd q = q \gcd p^{n}$
202	196 197 201	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} \gcd q = q \gcd p^{n}$
203		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 ℙ$
204		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 ℙ$
205		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 ℕ$
206		prmdvdsexpb	$⊢ (q \in ℙ \land p \in ℙ \land n \in ℕ) \to (q ∥ p^{n} \leftrightarrow q = p)$
207		equcom	$⊢ q = p \leftrightarrow p = q$
208	206 207	syl6bb	$⊢ (q \in ℙ \land p \in ℙ \land n \in ℕ) \to (q ∥ p^{n} \leftrightarrow p = q)$
209	208	biimpd	$⊢ (q \in ℙ \land p \in ℙ \land n \in ℕ) \to (q ∥ p^{n} \to p = q)$
210	203 204 205 209	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)$
211	210	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})$
212	211	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}$
213		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 ℙ$
214		coprm	$⊢ (q \in ℙ \land p^{n} \in ℤ) \to (\neg q ∥ p^{n} \leftrightarrow q \gcd p^{n} = 1)$
215	213 196 214	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)$
216	212 215	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$
217	202 216	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$
218		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}))$
219	196 197 198 218	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}))$
220	217 219	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}))$
221	200 220	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}))$
222	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 ℂ$
223	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 ℂ$
224	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$
225	222 223 224	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$
226	225	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)$
227	221 226	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)$
228	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 ℤ$
229		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}))$
230	196 197 228 229	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}))$
231		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}))$
232	196 197 228 231	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}))$
233	217 232	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}))$
234	230 233	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}))$
235	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 ℂ$
236	235 223 224	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$
237	236	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)$
238	234 237	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)$
239	227 238	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))$
240	239	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))$
241	240	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)$
242		oveq2	$⊢ m = n \to p^{m} = p^{n}$
243	242	breq1d	$⊢ m = n \to (p^{m} ∥ t \leftrightarrow p^{n} ∥ t)$
244	242	breq1d	$⊢ m = n \to (p^{m} ∥ x \leftrightarrow p^{n} ∥ x)$
245	243 244	bibi12d	$⊢ m = n \to ((p^{m} ∥ t \leftrightarrow p^{m} ∥ x) \leftrightarrow (p^{n} ∥ t \leftrightarrow p^{n} ∥ x))$
246	245	notbid	$⊢ m = n \to (\neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x) \leftrightarrow \neg (p^{n} ∥ t \leftrightarrow p^{n} ∥ x))$
247	246	rspcev	$⊢ (n \in ℕ \land \neg (p^{n} ∥ t \leftrightarrow p^{n} ∥ x)) \to \exists m \in ℕ \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x)$
248	189 241 247	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)$
249	248	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))$
250	249	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)))$
251	250	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)))$
252	251	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))$
253	187 252	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)$
254		oveq1	$⊢ r = p \to r^{m} = p^{m}$
255	254	breq1d	$⊢ r = p \to (r^{m} ∥ t \leftrightarrow p^{m} ∥ t)$
256	254	breq1d	$⊢ r = p \to (r^{m} ∥ x \leftrightarrow p^{m} ∥ x)$
257	255 256	bibi12d	$⊢ r = p \to ((r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow (p^{m} ∥ t \leftrightarrow p^{m} ∥ x))$
258	257	notbid	$⊢ r = p \to (\neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow \neg (p^{m} ∥ t \leftrightarrow p^{m} ∥ x))$
259	258	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))$
260	259	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)$
261	127 253 260	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)$
262	261	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)))$
263	262	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))$
264	126 263	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))$
265	264	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)))$
266	265	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)))$
267	121 266	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)))$
268	112 267	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)))$
269	93 268	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)))$
270	269	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))))))$
271	81 270	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))))))$
272	271	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)))))$
273	272	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)))))$
274	273	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)))$
275	37 53 274	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)))$
276		simpl2	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land (\neg q ∥ t \land t < x))) \to q \in ℙ$
277		1nn	$⊢ 1 \in ℕ$
278	277	a1i	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (t \in ℕ \land (\neg q ∥ t \land t < x))) \to 1 \in ℕ$
279	142	exp1d	$⊢ q \in ℙ \to q^{1} = q$
280	279	breq1d	$⊢ q \in ℙ \to (q^{1} ∥ t \leftrightarrow q ∥ t)$
281	280	notbid	$⊢ q \in ℙ \to (\neg q^{1} ∥ t \leftrightarrow \neg q ∥ t)$
282	281	biimpar	$⊢ (q \in ℙ \land \neg q ∥ t) \to \neg q^{1} ∥ t$
283	282	3ad2antl2	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land \neg q ∥ t) \to \neg q^{1} ∥ t$
284	283	adantrr	$⊢ ((x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \land (\neg q ∥ t \land t < x)) \to \neg q^{1} ∥ t$
285	284	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$
286	279	breq1d	$⊢ q \in ℙ \to (q^{1} ∥ x \leftrightarrow q ∥ x)$
287	286	biimpar	$⊢ (q \in ℙ \land q ∥ x) \to q^{1} ∥ x$
288	287	3adant1	$⊢ (x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \to q^{1} ∥ x$
289		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))$
290	288 289	mpid	$⊢ (x \in ℤ_{\geq 2} \land q \in ℙ \land q ∥ x) \to ((q^{1} ∥ x \to q^{1} ∥ t) \to q^{1} ∥ t)$
291	290	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)$
292	285 291	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)$
293		biimpr	$⊢ (q^{1} ∥ t \leftrightarrow q^{1} ∥ x) \to (q^{1} ∥ x \to q^{1} ∥ t)$
294	292 293	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)$
295		oveq1	$⊢ r = q \to r^{m} = q^{m}$
296	295	breq1d	$⊢ r = q \to (r^{m} ∥ t \leftrightarrow q^{m} ∥ t)$
297	295	breq1d	$⊢ r = q \to (r^{m} ∥ x \leftrightarrow q^{m} ∥ x)$
298	296 297	bibi12d	$⊢ r = q \to ((r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow (q^{m} ∥ t \leftrightarrow q^{m} ∥ x))$
299	298	notbid	$⊢ r = q \to (\neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow \neg (q^{m} ∥ t \leftrightarrow q^{m} ∥ x))$
300		oveq2	$⊢ m = 1 \to q^{m} = q^{1}$
301	300	breq1d	$⊢ m = 1 \to (q^{m} ∥ t \leftrightarrow q^{1} ∥ t)$
302	300	breq1d	$⊢ m = 1 \to (q^{m} ∥ x \leftrightarrow q^{1} ∥ x)$
303	301 302	bibi12d	$⊢ m = 1 \to ((q^{m} ∥ t \leftrightarrow q^{m} ∥ x) \leftrightarrow (q^{1} ∥ t \leftrightarrow q^{1} ∥ x))$
304	303	notbid	$⊢ m = 1 \to (\neg (q^{m} ∥ t \leftrightarrow q^{m} ∥ x) \leftrightarrow \neg (q^{1} ∥ t \leftrightarrow q^{1} ∥ x))$
305	299 304	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)$
306	276 278 294 305	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)$
307	306	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))$
308	307	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)))$
309	308	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)))$
310	275 309	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))$
311	310	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)))$
312	311	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))$
313		breq1	$⊢ t = k \to (t < x \leftrightarrow k < x)$
314		breq2	$⊢ t = k \to (r^{m} ∥ t \leftrightarrow r^{m} ∥ k)$
315	314	bibi1d	$⊢ t = k \to ((r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow (r^{m} ∥ k \leftrightarrow r^{m} ∥ x))$
316	315	notbid	$⊢ t = k \to (\neg (r^{m} ∥ t \leftrightarrow r^{m} ∥ x) \leftrightarrow \neg (r^{m} ∥ k \leftrightarrow r^{m} ∥ x))$
317	316	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))$
318	254	breq1d	$⊢ r = p \to (r^{m} ∥ k \leftrightarrow p^{m} ∥ k)$
319	318 256	bibi12d	$⊢ r = p \to ((r^{m} ∥ k \leftrightarrow r^{m} ∥ x) \leftrightarrow (p^{m} ∥ k \leftrightarrow p^{m} ∥ x))$
320	319	notbid	$⊢ r = p \to (\neg (r^{m} ∥ k \leftrightarrow r^{m} ∥ x) \leftrightarrow \neg (p^{m} ∥ k \leftrightarrow p^{m} ∥ x))$
321	242	breq1d	$⊢ m = n \to (p^{m} ∥ k \leftrightarrow p^{n} ∥ k)$
322	321 244	bibi12d	$⊢ m = n \to ((p^{m} ∥ k \leftrightarrow p^{m} ∥ x) \leftrightarrow (p^{n} ∥ k \leftrightarrow p^{n} ∥ x))$
323	322	notbid	$⊢ m = n \to (\neg (p^{m} ∥ k \leftrightarrow p^{m} ∥ x) \leftrightarrow \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x))$
324	320 323	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)$
325	317 324	syl6bb	$⊢ 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))$
326	313 325	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)))$
327	326	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))$
328	312 327	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))$
329	328	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)))))$
330	329	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))))$
331	25 330	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)))$
332	14 21 24 331	indstr2	$⊢ x \in ℕ \to \forall k \in ℕ (k < x \to \exists p \in ℙ \exists n \in ℕ \neg (p^{n} ∥ k \leftrightarrow p^{n} ∥ x))$
333	7 332	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