Step |
Hyp |
Ref |
Expression |
1 |
|
odcl.1 |
|- X = ( Base ` G ) |
2 |
|
odcl.2 |
|- O = ( od ` G ) |
3 |
|
odid.3 |
|- .x. = ( .g ` G ) |
4 |
|
odid.4 |
|- .0. = ( 0g ` G ) |
5 |
|
0nn0 |
|- 0 e. NN0 |
6 |
1 2 3 4
|
mndodcong |
|- ( ( ( G e. Mnd /\ A e. X ) /\ ( N e. NN0 /\ 0 e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) || ( N - 0 ) <-> ( N .x. A ) = ( 0 .x. A ) ) ) |
7 |
6
|
3expia |
|- ( ( ( G e. Mnd /\ A e. X ) /\ ( N e. NN0 /\ 0 e. NN0 ) ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || ( N - 0 ) <-> ( N .x. A ) = ( 0 .x. A ) ) ) ) |
8 |
5 7
|
mpanr2 |
|- ( ( ( G e. Mnd /\ A e. X ) /\ N e. NN0 ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || ( N - 0 ) <-> ( N .x. A ) = ( 0 .x. A ) ) ) ) |
9 |
8
|
3impa |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || ( N - 0 ) <-> ( N .x. A ) = ( 0 .x. A ) ) ) ) |
10 |
|
nn0cn |
|- ( N e. NN0 -> N e. CC ) |
11 |
10
|
3ad2ant3 |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> N e. CC ) |
12 |
11
|
subid1d |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( N - 0 ) = N ) |
13 |
12
|
breq2d |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) || ( N - 0 ) <-> ( O ` A ) || N ) ) |
14 |
1 4 3
|
mulg0 |
|- ( A e. X -> ( 0 .x. A ) = .0. ) |
15 |
14
|
3ad2ant2 |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( 0 .x. A ) = .0. ) |
16 |
15
|
eqeq2d |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( N .x. A ) = ( 0 .x. A ) <-> ( N .x. A ) = .0. ) ) |
17 |
13 16
|
bibi12d |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( ( O ` A ) || ( N - 0 ) <-> ( N .x. A ) = ( 0 .x. A ) ) <-> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) ) ) |
18 |
9 17
|
sylibd |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) ) ) |
19 |
|
simpr |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( O ` A ) = 0 ) |
20 |
19
|
breq1d |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( ( O ` A ) || N <-> 0 || N ) ) |
21 |
|
simpl3 |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> N e. NN0 ) |
22 |
|
nn0z |
|- ( N e. NN0 -> N e. ZZ ) |
23 |
|
0dvds |
|- ( N e. ZZ -> ( 0 || N <-> N = 0 ) ) |
24 |
21 22 23
|
3syl |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( 0 || N <-> N = 0 ) ) |
25 |
15
|
adantr |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( 0 .x. A ) = .0. ) |
26 |
|
oveq1 |
|- ( N = 0 -> ( N .x. A ) = ( 0 .x. A ) ) |
27 |
26
|
eqeq1d |
|- ( N = 0 -> ( ( N .x. A ) = .0. <-> ( 0 .x. A ) = .0. ) ) |
28 |
25 27
|
syl5ibrcom |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( N = 0 -> ( N .x. A ) = .0. ) ) |
29 |
1 2 3 4
|
odlem2 |
|- ( ( A e. X /\ N e. NN /\ ( N .x. A ) = .0. ) -> ( O ` A ) e. ( 1 ... N ) ) |
30 |
29
|
3com23 |
|- ( ( A e. X /\ ( N .x. A ) = .0. /\ N e. NN ) -> ( O ` A ) e. ( 1 ... N ) ) |
31 |
|
elfznn |
|- ( ( O ` A ) e. ( 1 ... N ) -> ( O ` A ) e. NN ) |
32 |
|
nnne0 |
|- ( ( O ` A ) e. NN -> ( O ` A ) =/= 0 ) |
33 |
30 31 32
|
3syl |
|- ( ( A e. X /\ ( N .x. A ) = .0. /\ N e. NN ) -> ( O ` A ) =/= 0 ) |
34 |
33
|
3expia |
|- ( ( A e. X /\ ( N .x. A ) = .0. ) -> ( N e. NN -> ( O ` A ) =/= 0 ) ) |
35 |
34
|
3ad2antl2 |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> ( N e. NN -> ( O ` A ) =/= 0 ) ) |
36 |
35
|
necon2bd |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> ( ( O ` A ) = 0 -> -. N e. NN ) ) |
37 |
|
simpl3 |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> N e. NN0 ) |
38 |
|
elnn0 |
|- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) ) |
39 |
37 38
|
sylib |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> ( N e. NN \/ N = 0 ) ) |
40 |
39
|
ord |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> ( -. N e. NN -> N = 0 ) ) |
41 |
36 40
|
syld |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> ( ( O ` A ) = 0 -> N = 0 ) ) |
42 |
41
|
impancom |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( ( N .x. A ) = .0. -> N = 0 ) ) |
43 |
28 42
|
impbid |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( N = 0 <-> ( N .x. A ) = .0. ) ) |
44 |
20 24 43
|
3bitrd |
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) ) |
45 |
44
|
ex |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) = 0 -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) ) ) |
46 |
1 2
|
odcl |
|- ( A e. X -> ( O ` A ) e. NN0 ) |
47 |
46
|
3ad2ant2 |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( O ` A ) e. NN0 ) |
48 |
|
elnn0 |
|- ( ( O ` A ) e. NN0 <-> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) ) |
49 |
47 48
|
sylib |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) ) |
50 |
18 45 49
|
mpjaod |
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) ) |