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 ⊢A∈ℕ0∧B∈ℕ0→A=B↔∀p∈ℙ∀n∈ℕpn∥A↔pn∥B

Proof

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