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