# Metamath Proof Explorer

## Theorem 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 ℕ\phantom{\rule{.4em}{0ex}}\left({k}<{A}\to \exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}¬\left({{p}}^{{n}}\parallel {k}↔{{p}}^{{n}}\parallel {A}\right)\right)$

### Proof

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