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 e. NN0 /\ B e. NN0 ) -> ( A = B <-> A. p e. Prime A. n e. NN ( ( p ^ n ) || A <-> ( p ^ n ) || B ) ) )

Proof

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