Metamath Proof Explorer


Theorem nnn1suc

Description: A positive integer that is not 1 is a successor of some other positive integer. (Contributed by Steven Nguyen, 19-Aug-2023)

Ref Expression
Assertion nnn1suc A A 1 x x + 1 = A

Proof

Step Hyp Ref Expression
1 neeq1 y = 1 y 1 1 1
2 eqeq2 y = 1 x + 1 = y x + 1 = 1
3 2 rexbidv y = 1 x x + 1 = y x x + 1 = 1
4 1 3 imbi12d y = 1 y 1 x x + 1 = y 1 1 x x + 1 = 1
5 neeq1 y = z y 1 z 1
6 eqeq2 y = z x + 1 = y x + 1 = z
7 6 rexbidv y = z x x + 1 = y x x + 1 = z
8 5 7 imbi12d y = z y 1 x x + 1 = y z 1 x x + 1 = z
9 neeq1 y = z + 1 y 1 z + 1 1
10 eqeq2 y = z + 1 x + 1 = y x + 1 = z + 1
11 10 rexbidv y = z + 1 x x + 1 = y x x + 1 = z + 1
12 9 11 imbi12d y = z + 1 y 1 x x + 1 = y z + 1 1 x x + 1 = z + 1
13 neeq1 y = A y 1 A 1
14 eqeq2 y = A x + 1 = y x + 1 = A
15 14 rexbidv y = A x x + 1 = y x x + 1 = A
16 13 15 imbi12d y = A y 1 x x + 1 = y A 1 x x + 1 = A
17 df-ne 1 1 ¬ 1 = 1
18 eqid 1 = 1
19 18 pm2.24i ¬ 1 = 1 x x + 1 = 1
20 17 19 sylbi 1 1 x x + 1 = 1
21 id z z
22 oveq1 x = z x + 1 = z + 1
23 22 eqeq1d x = z x + 1 = z + 1 z + 1 = z + 1
24 23 adantl z x = z x + 1 = z + 1 z + 1 = z + 1
25 eqidd z z + 1 = z + 1
26 21 24 25 rspcedvd z x x + 1 = z + 1
27 26 2a1d z z 1 x x + 1 = z z + 1 1 x x + 1 = z + 1
28 4 8 12 16 20 27 nnind A A 1 x x + 1 = A
29 28 imp A A 1 x x + 1 = A