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 ( 𝐴 ∈ ℕ → ∀ 𝑘 ∈ ℕ ( 𝑘 < 𝐴 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) ) )

Proof

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