Metamath Proof Explorer

Theorem nn0prpw

Description: Two nonnegative integers are the same if and only if they are divisible by the same prime powers. (Contributed by Jeff Hankins, 29-Sep-2013)

Ref Expression
Assertion nn0prpw ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝐴 = 𝐵 → ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) )
2 1 a1d ⊢ ( 𝐴 = 𝐵 → ( ( 𝑝 ∈ ℙ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
3 2 ralrimivv ⊢ ( 𝐴 = 𝐵 → ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) )
4 elnn0 ⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
5 elnn0 ⊢ ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
6 nnre ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
7 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
8 lttri2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
9 6 7 8 syl2an ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
10 9 ancoms ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
11 nn0prpwlem ⊢ ( 𝐵 ∈ ℕ → ∀ 𝑘 ∈ ℕ ( 𝑘 < 𝐵 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
12 breq1 ⊢ ( 𝑘 = 𝐴 → ( 𝑘 < 𝐵 ↔ 𝐴 < 𝐵 ) )
13 breq2 ⊢ ( 𝑘 = 𝐴 → ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) )
14 13 bibi1d ⊢ ( 𝑘 = 𝐴 → ( ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
15 14 notbid ⊢ ( 𝑘 = 𝐴 → ( ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
16 15 2rexbidv ⊢ ( 𝑘 = 𝐴 → ( ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
17 12 16 imbi12d ⊢ ( 𝑘 = 𝐴 → ( ( 𝑘 < 𝐵 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) ↔ ( 𝐴 < 𝐵 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) ) )
18 17 rspcv ⊢ ( 𝐴 ∈ ℕ → ( ∀ 𝑘 ∈ ℕ ( 𝑘 < 𝐵 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) → ( 𝐴 < 𝐵 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) ) )
19 11 18 mpan9 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 𝐴 < 𝐵 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
20 breq1 ⊢ ( 𝑘 = 𝐵 → ( 𝑘 < 𝐴 ↔ 𝐵 < 𝐴 ) )
21 breq2 ⊢ ( 𝑘 = 𝐵 → ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) )
22 21 bibi1d ⊢ ( 𝑘 = 𝐵 → ( ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) ↔ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) ) )
23 bicom ⊢ ( ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) ↔ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) )
24 22 23 bitrdi ⊢ ( 𝑘 = 𝐵 → ( ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) ↔ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
25 24 notbid ⊢ ( 𝑘 = 𝐵 → ( ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) ↔ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
26 25 2rexbidv ⊢ ( 𝑘 = 𝐵 → ( ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
27 20 26 imbi12d ⊢ ( 𝑘 = 𝐵 → ( ( 𝑘 < 𝐴 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) ) ↔ ( 𝐵 < 𝐴 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) ) )
28 27 rspcv ⊢ ( 𝐵 ∈ ℕ → ( ∀ 𝑘 ∈ ℕ ( 𝑘 < 𝐴 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) ) → ( 𝐵 < 𝐴 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) ) )
29 nn0prpwlem ⊢ ( 𝐴 ∈ ℕ → ∀ 𝑘 ∈ ℕ ( 𝑘 < 𝐴 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝑘 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ) ) )
30 28 29 impel ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 𝐵 < 𝐴 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
31 19 30 jaod ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
32 10 31 sylbid ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 𝐴 ≠ 𝐵 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
33 df-ne ⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵 )
34 rexnal2 ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ¬ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) )
35 32 33 34 3imtr3g ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( ¬ 𝐴 = 𝐵 → ¬ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
36 35 con4d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) )
37 36 ex ⊢ ( 𝐵 ∈ ℕ → ( 𝐴 ∈ ℕ → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) ) )
38 prmunb ⊢ ( 𝐴 ∈ ℕ → ∃ 𝑝 ∈ ℙ 𝐴 < 𝑝 )
39 1nn ⊢ 1 ∈ ℕ
40 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
41 1nn0 ⊢ 1 ∈ ℕ0
42 zexpcl ⊢ ( ( 𝑝 ∈ ℤ ∧ 1 ∈ ℕ0 ) → ( 𝑝 ↑ 1 ) ∈ ℤ )
43 40 41 42 sylancl ⊢ ( 𝑝 ∈ ℙ → ( 𝑝 ↑ 1 ) ∈ ℤ )
44 dvds0 ⊢ ( ( 𝑝 ↑ 1 ) ∈ ℤ → ( 𝑝 ↑ 1 ) ∥ 0 )
45 43 44 syl ⊢ ( 𝑝 ∈ ℙ → ( 𝑝 ↑ 1 ) ∥ 0 )
46 45 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ∧ 𝐴 < 𝑝 ) → ( 𝑝 ↑ 1 ) ∥ 0 )
47 dvdsle ⊢ ( ( ( 𝑝 ↑ 1 ) ∈ ℤ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑝 ↑ 1 ) ∥ 𝐴 → ( 𝑝 ↑ 1 ) ≤ 𝐴 ) )
48 43 47 sylan ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑝 ↑ 1 ) ∥ 𝐴 → ( 𝑝 ↑ 1 ) ≤ 𝐴 ) )
49 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
50 nnre ⊢ ( 𝑝 ∈ ℕ → 𝑝 ∈ ℝ )
51 49 50 syl ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ )
52 reexpcl ⊢ ( ( 𝑝 ∈ ℝ ∧ 1 ∈ ℕ0 ) → ( 𝑝 ↑ 1 ) ∈ ℝ )
53 51 41 52 sylancl ⊢ ( 𝑝 ∈ ℙ → ( 𝑝 ↑ 1 ) ∈ ℝ )
54 lenlt ⊢ ( ( ( 𝑝 ↑ 1 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑝 ↑ 1 ) ≤ 𝐴 ↔ ¬ 𝐴 < ( 𝑝 ↑ 1 ) ) )
55 53 6 54 syl2an ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑝 ↑ 1 ) ≤ 𝐴 ↔ ¬ 𝐴 < ( 𝑝 ↑ 1 ) ) )
56 49 nncnd ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℂ )
57 56 exp1d ⊢ ( 𝑝 ∈ ℙ → ( 𝑝 ↑ 1 ) = 𝑝 )
58 57 adantr ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑝 ↑ 1 ) = 𝑝 )
59 58 breq2d ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝐴 < ( 𝑝 ↑ 1 ) ↔ 𝐴 < 𝑝 ) )
60 59 notbid ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ¬ 𝐴 < ( 𝑝 ↑ 1 ) ↔ ¬ 𝐴 < 𝑝 ) )
61 55 60 bitrd ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑝 ↑ 1 ) ≤ 𝐴 ↔ ¬ 𝐴 < 𝑝 ) )
62 48 61 sylibd ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑝 ↑ 1 ) ∥ 𝐴 → ¬ 𝐴 < 𝑝 ) )
63 62 ancoms ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ↑ 1 ) ∥ 𝐴 → ¬ 𝐴 < 𝑝 ) )
64 63 con2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝐴 < 𝑝 → ¬ ( 𝑝 ↑ 1 ) ∥ 𝐴 ) )
65 64 3impia ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ∧ 𝐴 < 𝑝 ) → ¬ ( 𝑝 ↑ 1 ) ∥ 𝐴 )
66 46 65 jcnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ∧ 𝐴 < 𝑝 ) → ¬ ( ( 𝑝 ↑ 1 ) ∥ 0 → ( 𝑝 ↑ 1 ) ∥ 𝐴 ) )
67 biimpr ⊢ ( ( ( 𝑝 ↑ 1 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 1 ) ∥ 0 ) → ( ( 𝑝 ↑ 1 ) ∥ 0 → ( 𝑝 ↑ 1 ) ∥ 𝐴 ) )
68 66 67 nsyl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ∧ 𝐴 < 𝑝 ) → ¬ ( ( 𝑝 ↑ 1 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 1 ) ∥ 0 ) )
69 oveq2 ⊢ ( 𝑛 = 1 → ( 𝑝 ↑ 𝑛 ) = ( 𝑝 ↑ 1 ) )
70 69 breq1d ⊢ ( 𝑛 = 1 → ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 1 ) ∥ 𝐴 ) )
71 69 breq1d ⊢ ( 𝑛 = 1 → ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 1 ) ∥ 0 ) )
72 70 71 bibi12d ⊢ ( 𝑛 = 1 → ( ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) ↔ ( ( 𝑝 ↑ 1 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 1 ) ∥ 0 ) ) )
73 72 notbid ⊢ ( 𝑛 = 1 → ( ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) ↔ ¬ ( ( 𝑝 ↑ 1 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 1 ) ∥ 0 ) ) )
74 73 rspcev ⊢ ( ( 1 ∈ ℕ ∧ ¬ ( ( 𝑝 ↑ 1 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 1 ) ∥ 0 ) ) → ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) )
75 39 68 74 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ∧ 𝐴 < 𝑝 ) → ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) )
76 75 3expia ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝐴 < 𝑝 → ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) ) )
77 76 reximdva ⊢ ( 𝐴 ∈ ℕ → ( ∃ 𝑝 ∈ ℙ 𝐴 < 𝑝 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) ) )
78 38 77 mpd ⊢ ( 𝐴 ∈ ℕ → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) )
79 rexnal2 ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) ↔ ¬ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) )
80 78 79 sylib ⊢ ( 𝐴 ∈ ℕ → ¬ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) )
81 80 pm2.21d ⊢ ( 𝐴 ∈ ℕ → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) → 𝐴 = 0 ) )
82 breq2 ⊢ ( 𝐵 = 0 → ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) )
83 82 bibi2d ⊢ ( 𝐵 = 0 → ( ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) ) )
84 83 2ralbidv ⊢ ( 𝐵 = 0 → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) ) )
85 eqeq2 ⊢ ( 𝐵 = 0 → ( 𝐴 = 𝐵 ↔ 𝐴 = 0 ) )
86 84 85 imbi12d ⊢ ( 𝐵 = 0 → ( ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) ↔ ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) → 𝐴 = 0 ) ) )
87 81 86 syl5ibr ⊢ ( 𝐵 = 0 → ( 𝐴 ∈ ℕ → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) ) )
88 37 87 jaoi ⊢ ( ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) → ( 𝐴 ∈ ℕ → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) ) )
89 5 88 sylbi ⊢ ( 𝐵 ∈ ℕ0 → ( 𝐴 ∈ ℕ → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) ) )
90 89 com12 ⊢ ( 𝐴 ∈ ℕ → ( 𝐵 ∈ ℕ0 → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) ) )
91 orcom ⊢ ( ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) ↔ ( 𝐵 = 0 ∨ 𝐵 ∈ ℕ ) )
92 df-or ⊢ ( ( 𝐵 = 0 ∨ 𝐵 ∈ ℕ ) ↔ ( ¬ 𝐵 = 0 → 𝐵 ∈ ℕ ) )
93 5 91 92 3bitri ⊢ ( 𝐵 ∈ ℕ0 ↔ ( ¬ 𝐵 = 0 → 𝐵 ∈ ℕ ) )
94 prmunb ⊢ ( 𝐵 ∈ ℕ → ∃ 𝑝 ∈ ℙ 𝐵 < 𝑝 )
95 45 3ad2ant2 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑝 ∈ ℙ ∧ 𝐵 < 𝑝 ) → ( 𝑝 ↑ 1 ) ∥ 0 )
96 dvdsle ⊢ ( ( ( 𝑝 ↑ 1 ) ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑝 ↑ 1 ) ∥ 𝐵 → ( 𝑝 ↑ 1 ) ≤ 𝐵 ) )
97 43 96 sylan ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑝 ↑ 1 ) ∥ 𝐵 → ( 𝑝 ↑ 1 ) ≤ 𝐵 ) )
98 lenlt ⊢ ( ( ( 𝑝 ↑ 1 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝑝 ↑ 1 ) ≤ 𝐵 ↔ ¬ 𝐵 < ( 𝑝 ↑ 1 ) ) )
99 53 7 98 syl2an ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑝 ↑ 1 ) ≤ 𝐵 ↔ ¬ 𝐵 < ( 𝑝 ↑ 1 ) ) )
100 57 adantr ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ ) → ( 𝑝 ↑ 1 ) = 𝑝 )
101 100 breq2d ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 < ( 𝑝 ↑ 1 ) ↔ 𝐵 < 𝑝 ) )
102 101 notbid ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ ) → ( ¬ 𝐵 < ( 𝑝 ↑ 1 ) ↔ ¬ 𝐵 < 𝑝 ) )
103 99 102 bitrd ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑝 ↑ 1 ) ≤ 𝐵 ↔ ¬ 𝐵 < 𝑝 ) )
104 97 103 sylibd ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑝 ↑ 1 ) ∥ 𝐵 → ¬ 𝐵 < 𝑝 ) )
105 104 ancoms ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ↑ 1 ) ∥ 𝐵 → ¬ 𝐵 < 𝑝 ) )
106 105 con2d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝐵 < 𝑝 → ¬ ( 𝑝 ↑ 1 ) ∥ 𝐵 ) )
107 106 3impia ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑝 ∈ ℙ ∧ 𝐵 < 𝑝 ) → ¬ ( 𝑝 ↑ 1 ) ∥ 𝐵 )
108 95 107 jcnd ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑝 ∈ ℙ ∧ 𝐵 < 𝑝 ) → ¬ ( ( 𝑝 ↑ 1 ) ∥ 0 → ( 𝑝 ↑ 1 ) ∥ 𝐵 ) )
109 biimp ⊢ ( ( ( 𝑝 ↑ 1 ) ∥ 0 ↔ ( 𝑝 ↑ 1 ) ∥ 𝐵 ) → ( ( 𝑝 ↑ 1 ) ∥ 0 → ( 𝑝 ↑ 1 ) ∥ 𝐵 ) )
110 108 109 nsyl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑝 ∈ ℙ ∧ 𝐵 < 𝑝 ) → ¬ ( ( 𝑝 ↑ 1 ) ∥ 0 ↔ ( 𝑝 ↑ 1 ) ∥ 𝐵 ) )
111 69 breq1d ⊢ ( 𝑛 = 1 → ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ↔ ( 𝑝 ↑ 1 ) ∥ 𝐵 ) )
112 71 111 bibi12d ⊢ ( 𝑛 = 1 → ( ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ( ( 𝑝 ↑ 1 ) ∥ 0 ↔ ( 𝑝 ↑ 1 ) ∥ 𝐵 ) ) )
113 112 notbid ⊢ ( 𝑛 = 1 → ( ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ¬ ( ( 𝑝 ↑ 1 ) ∥ 0 ↔ ( 𝑝 ↑ 1 ) ∥ 𝐵 ) ) )
114 113 rspcev ⊢ ( ( 1 ∈ ℕ ∧ ¬ ( ( 𝑝 ↑ 1 ) ∥ 0 ↔ ( 𝑝 ↑ 1 ) ∥ 𝐵 ) ) → ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) )
115 39 110 114 sylancr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑝 ∈ ℙ ∧ 𝐵 < 𝑝 ) → ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) )
116 115 3expia ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝐵 < 𝑝 → ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
117 116 reximdva ⊢ ( 𝐵 ∈ ℕ → ( ∃ 𝑝 ∈ ℙ 𝐵 < 𝑝 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
118 94 117 mpd ⊢ ( 𝐵 ∈ ℕ → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) )
119 rexnal2 ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ ¬ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ¬ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) )
120 118 119 sylib ⊢ ( 𝐵 ∈ ℕ → ¬ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) )
121 120 imim2i ⊢ ( ( ¬ 𝐵 = 0 → 𝐵 ∈ ℕ ) → ( ¬ 𝐵 = 0 → ¬ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
122 93 121 sylbi ⊢ ( 𝐵 ∈ ℕ0 → ( ¬ 𝐵 = 0 → ¬ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
123 122 con4d ⊢ ( 𝐵 ∈ ℕ0 → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐵 = 0 ) )
124 eqcom ⊢ ( 𝐵 = 0 ↔ 0 = 𝐵 )
125 123 124 syl6ib ⊢ ( 𝐵 ∈ ℕ0 → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 0 = 𝐵 ) )
126 breq2 ⊢ ( 𝐴 = 0 → ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 0 ) )
127 126 bibi1d ⊢ ( 𝐴 = 0 → ( ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
128 127 2ralbidv ⊢ ( 𝐴 = 0 → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ↔ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )
129 eqeq1 ⊢ ( 𝐴 = 0 → ( 𝐴 = 𝐵 ↔ 0 = 𝐵 ) )
130 128 129 imbi12d ⊢ ( 𝐴 = 0 → ( ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) ↔ ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 0 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 0 = 𝐵 ) ) )
131 125 130 syl5ibr ⊢ ( 𝐴 = 0 → ( 𝐵 ∈ ℕ0 → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) ) )
132 90 131 jaoi ⊢ ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) → ( 𝐵 ∈ ℕ0 → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) ) )
133 132 imp ⊢ ( ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ∧ 𝐵 ∈ ℕ0 ) → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) )
134 4 133 sylanb ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) → 𝐴 = 𝐵 ) )
135 3 134 impbid2 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ( ( 𝑝 ↑ 𝑛 ) ∥ 𝐴 ↔ ( 𝑝 ↑ 𝑛 ) ∥ 𝐵 ) ) )