Step | Hyp | Ref
| Expression |
1 | | nn0addcl 12453 |
. . . . 5
β’ ((π₯ β β0
β§ π¦ β
β0) β (π₯ + π¦) β
β0) |
2 | | nn0cn 12428 |
. . . . . . . . 9
β’ (π₯ β β0
β π₯ β
β) |
3 | | nn0cn 12428 |
. . . . . . . . 9
β’ (π¦ β β0
β π¦ β
β) |
4 | | nn0cn 12428 |
. . . . . . . . 9
β’ (π§ β β0
β π§ β
β) |
5 | 2, 3, 4 | 3anim123i 1152 |
. . . . . . . 8
β’ ((π₯ β β0
β§ π¦ β
β0 β§ π§
β β0) β (π₯ β β β§ π¦ β β β§ π§ β β)) |
6 | 5 | 3expa 1119 |
. . . . . . 7
β’ (((π₯ β β0
β§ π¦ β
β0) β§ π§ β β0) β (π₯ β β β§ π¦ β β β§ π§ β
β)) |
7 | | addass 11143 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
8 | 6, 7 | syl 17 |
. . . . . 6
β’ (((π₯ β β0
β§ π¦ β
β0) β§ π§ β β0) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
9 | 8 | ralrimiva 3140 |
. . . . 5
β’ ((π₯ β β0
β§ π¦ β
β0) β βπ§ β β0 ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
10 | 1, 9 | jca 513 |
. . . 4
β’ ((π₯ β β0
β§ π¦ β
β0) β ((π₯ + π¦) β β0 β§
βπ§ β
β0 ((π₯ +
π¦) + π§) = (π₯ + (π¦ + π§)))) |
11 | 10 | rgen2 3191 |
. . 3
β’
βπ₯ β
β0 βπ¦ β β0 ((π₯ + π¦) β β0 β§
βπ§ β
β0 ((π₯ +
π¦) + π§) = (π₯ + (π¦ + π§))) |
12 | | c0ex 11154 |
. . . . 5
β’ 0 β
V |
13 | | eleq1 2822 |
. . . . . 6
β’ (π = 0 β (π β β0 β 0 β
β0)) |
14 | | oveq1 7365 |
. . . . . . . . 9
β’ (π = 0 β (π + π₯) = (0 + π₯)) |
15 | 14 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = 0 β ((π + π₯) = π₯ β (0 + π₯) = π₯)) |
16 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = 0 β (π₯ + π) = (π₯ + 0)) |
17 | 16 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = 0 β ((π₯ + π) = π₯ β (π₯ + 0) = π₯)) |
18 | 15, 17 | anbi12d 632 |
. . . . . . 7
β’ (π = 0 β (((π + π₯) = π₯ β§ (π₯ + π) = π₯) β ((0 + π₯) = π₯ β§ (π₯ + 0) = π₯))) |
19 | 18 | ralbidv 3171 |
. . . . . 6
β’ (π = 0 β (βπ₯ β β0
((π + π₯) = π₯ β§ (π₯ + π) = π₯) β βπ₯ β β0 ((0 + π₯) = π₯ β§ (π₯ + 0) = π₯))) |
20 | 13, 19 | anbi12d 632 |
. . . . 5
β’ (π = 0 β ((π β β0 β§
βπ₯ β
β0 ((π +
π₯) = π₯ β§ (π₯ + π) = π₯)) β (0 β β0 β§
βπ₯ β
β0 ((0 + π₯) = π₯ β§ (π₯ + 0) = π₯)))) |
21 | | 0nn0 12433 |
. . . . . 6
β’ 0 β
β0 |
22 | 2 | addid2d 11361 |
. . . . . . . 8
β’ (π₯ β β0
β (0 + π₯) = π₯) |
23 | 2 | addid1d 11360 |
. . . . . . . 8
β’ (π₯ β β0
β (π₯ + 0) = π₯) |
24 | 22, 23 | jca 513 |
. . . . . . 7
β’ (π₯ β β0
β ((0 + π₯) = π₯ β§ (π₯ + 0) = π₯)) |
25 | 24 | rgen 3063 |
. . . . . 6
β’
βπ₯ β
β0 ((0 + π₯) = π₯ β§ (π₯ + 0) = π₯) |
26 | 21, 25 | pm3.2i 472 |
. . . . 5
β’ (0 β
β0 β§ βπ₯ β β0 ((0 + π₯) = π₯ β§ (π₯ + 0) = π₯)) |
27 | 12, 20, 26 | ceqsexv2d 3496 |
. . . 4
β’
βπ(π β β0
β§ βπ₯ β
β0 ((π +
π₯) = π₯ β§ (π₯ + π) = π₯)) |
28 | | df-rex 3071 |
. . . 4
β’
(βπ β
β0 βπ₯ β β0 ((π + π₯) = π₯ β§ (π₯ + π) = π₯) β βπ(π β β0 β§
βπ₯ β
β0 ((π +
π₯) = π₯ β§ (π₯ + π) = π₯))) |
29 | 27, 28 | mpbir 230 |
. . 3
β’
βπ β
β0 βπ₯ β β0 ((π + π₯) = π₯ β§ (π₯ + π) = π₯) |
30 | 11, 29 | pm3.2i 472 |
. 2
β’
(βπ₯ β
β0 βπ¦ β β0 ((π₯ + π¦) β β0 β§
βπ§ β
β0 ((π₯ +
π¦) + π§) = (π₯ + (π¦ + π§))) β§ βπ β β0 βπ₯ β β0
((π + π₯) = π₯ β§ (π₯ + π) = π₯)) |
31 | | nn0ex 12424 |
. . . 4
β’
β0 β V |
32 | | nn0mnd.g |
. . . . 5
β’ π = {β¨(Baseβndx),
β0β©, β¨(+gβndx), +
β©} |
33 | 32 | grpbase 17172 |
. . . 4
β’
(β0 β V β β0 =
(Baseβπ)) |
34 | 31, 33 | ax-mp 5 |
. . 3
β’
β0 = (Baseβπ) |
35 | | addex 12918 |
. . . 4
β’ + β
V |
36 | 32 | grpplusg 17174 |
. . . 4
β’ ( +
β V β + = (+gβπ)) |
37 | 35, 36 | ax-mp 5 |
. . 3
β’ + =
(+gβπ) |
38 | 34, 37 | ismnd 18564 |
. 2
β’ (π β Mnd β
(βπ₯ β
β0 βπ¦ β β0 ((π₯ + π¦) β β0 β§
βπ§ β
β0 ((π₯ +
π¦) + π§) = (π₯ + (π¦ + π§))) β§ βπ β β0 βπ₯ β β0
((π + π₯) = π₯ β§ (π₯ + π) = π₯))) |
39 | 30, 38 | mpbir 230 |
1
β’ π β Mnd |