Metamath Proof Explorer


Theorem goalrlem

Description: Lemma for goalr (induction step). (Contributed by AV, 22-Oct-2023)

Ref Expression
Assertion goalrlem Nω𝑔iaFmlasucNaFmlasucN𝑔iaFmlasucsucNaFmlasucsucN

Proof

Step Hyp Ref Expression
1 peano2 NωsucNω
2 df-goal 𝑔ia=2𝑜ia
3 opex 2𝑜iaV
4 2 3 eqeltri 𝑔iaV
5 isfmlasuc sucNω𝑔iaV𝑔iaFmlasucsucN𝑔iaFmlasucNuFmlasucNvFmlasucN𝑔ia=u𝑔vjω𝑔ia=𝑔ju
6 1 4 5 sylancl Nω𝑔iaFmlasucsucN𝑔iaFmlasucNuFmlasucNvFmlasucN𝑔ia=u𝑔vjω𝑔ia=𝑔ju
7 6 adantr Nω𝑔iaFmlasucNaFmlasucN𝑔iaFmlasucsucN𝑔iaFmlasucNuFmlasucNvFmlasucN𝑔ia=u𝑔vjω𝑔ia=𝑔ju
8 fmlasssuc sucNωFmlasucNFmlasucsucN
9 1 8 syl NωFmlasucNFmlasucsucN
10 9 sseld NωaFmlasucNaFmlasucsucN
11 10 com12 aFmlasucNNωaFmlasucsucN
12 11 imim2i 𝑔iaFmlasucNaFmlasucN𝑔iaFmlasucNNωaFmlasucsucN
13 12 com23 𝑔iaFmlasucNaFmlasucNNω𝑔iaFmlasucNaFmlasucsucN
14 13 impcom Nω𝑔iaFmlasucNaFmlasucN𝑔iaFmlasucNaFmlasucsucN
15 gonanegoal u𝑔v𝑔ia
16 eqneqall u𝑔v=𝑔iau𝑔v𝑔iaaFmlasucsucN
17 15 16 mpi u𝑔v=𝑔iaaFmlasucsucN
18 17 eqcoms 𝑔ia=u𝑔vaFmlasucsucN
19 18 a1i NωuFmlasucNvFmlasucN𝑔ia=u𝑔vaFmlasucsucN
20 19 rexlimdva NωuFmlasucNvFmlasucN𝑔ia=u𝑔vaFmlasucsucN
21 df-goal 𝑔ju=2𝑜ju
22 2 21 eqeq12i 𝑔ia=𝑔ju2𝑜ia=2𝑜ju
23 2oex 2𝑜V
24 opex iaV
25 23 24 opth 2𝑜ia=2𝑜ju2𝑜=2𝑜ia=ju
26 22 25 bitri 𝑔ia=𝑔ju2𝑜=2𝑜ia=ju
27 vex iV
28 vex aV
29 27 28 opth ia=jui=ja=u
30 eleq1w u=auFmlasucNaFmlasucN
31 30 eqcoms a=uuFmlasucNaFmlasucN
32 31 11 syl6bi a=uuFmlasucNNωaFmlasucsucN
33 32 impcomd a=uNωuFmlasucNaFmlasucsucN
34 29 33 simplbiim ia=juNωuFmlasucNaFmlasucsucN
35 26 34 simplbiim 𝑔ia=𝑔juNωuFmlasucNaFmlasucsucN
36 35 com12 NωuFmlasucN𝑔ia=𝑔juaFmlasucsucN
37 36 adantr NωuFmlasucNjω𝑔ia=𝑔juaFmlasucsucN
38 37 rexlimdva NωuFmlasucNjω𝑔ia=𝑔juaFmlasucsucN
39 20 38 jaod NωuFmlasucNvFmlasucN𝑔ia=u𝑔vjω𝑔ia=𝑔juaFmlasucsucN
40 39 rexlimdva NωuFmlasucNvFmlasucN𝑔ia=u𝑔vjω𝑔ia=𝑔juaFmlasucsucN
41 40 adantr Nω𝑔iaFmlasucNaFmlasucNuFmlasucNvFmlasucN𝑔ia=u𝑔vjω𝑔ia=𝑔juaFmlasucsucN
42 14 41 jaod Nω𝑔iaFmlasucNaFmlasucN𝑔iaFmlasucNuFmlasucNvFmlasucN𝑔ia=u𝑔vjω𝑔ia=𝑔juaFmlasucsucN
43 7 42 sylbid Nω𝑔iaFmlasucNaFmlasucN𝑔iaFmlasucsucNaFmlasucsucN
44 43 ex Nω𝑔iaFmlasucNaFmlasucN𝑔iaFmlasucsucNaFmlasucsucN