Step |
Hyp |
Ref |
Expression |
1 |
|
gexod.1 |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
gexod.2 |
⊢ 𝐸 = ( gEx ‘ 𝐺 ) |
3 |
|
gexod.3 |
⊢ 𝑂 = ( od ‘ 𝐺 ) |
4 |
|
simpl |
⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝐺 ∈ Grp ) |
5 |
1
|
grpbn0 |
⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ ) |
6 |
|
r19.2z |
⊢ ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) |
7 |
5 6
|
sylan |
⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ∃ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) |
8 |
|
elfzuz2 |
⊢ ( ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) ) |
9 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
10 |
8 9
|
eleqtrrdi |
⊢ ( ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℕ ) |
11 |
10
|
rexlimivw |
⊢ ( ∃ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℕ ) |
12 |
7 11
|
syl |
⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ ) |
13 |
12
|
nnnn0d |
⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 ) |
14 |
13
|
faccld |
⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℕ ) |
15 |
|
elfzuzb |
⊢ ( ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑂 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑂 ‘ 𝑥 ) ) ) ) |
16 |
|
elnnuz |
⊢ ( ( 𝑂 ‘ 𝑥 ) ∈ ℕ ↔ ( 𝑂 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) ) |
17 |
|
dvdsfac |
⊢ ( ( ( 𝑂 ‘ 𝑥 ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑂 ‘ 𝑥 ) ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( ! ‘ 𝑁 ) ) |
18 |
16 17
|
sylanbr |
⊢ ( ( ( 𝑂 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑂 ‘ 𝑥 ) ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( ! ‘ 𝑁 ) ) |
19 |
15 18
|
sylbi |
⊢ ( ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) → ( 𝑂 ‘ 𝑥 ) ∥ ( ! ‘ 𝑁 ) ) |
20 |
19
|
adantl |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( ! ‘ 𝑁 ) ) |
21 |
|
simpll |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝐺 ∈ Grp ) |
22 |
|
simplr |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝑥 ∈ 𝑋 ) |
23 |
10
|
adantl |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ ) |
24 |
23
|
nnnn0d |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 ) |
25 |
24
|
faccld |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℕ ) |
26 |
25
|
nnzd |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℤ ) |
27 |
|
eqid |
⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 ) |
28 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
29 |
1 3 27 28
|
oddvds |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( ( 𝑂 ‘ 𝑥 ) ∥ ( ! ‘ 𝑁 ) ↔ ( ( ! ‘ 𝑁 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) ) |
30 |
21 22 26 29
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑂 ‘ 𝑥 ) ∥ ( ! ‘ 𝑁 ) ↔ ( ( ! ‘ 𝑁 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) ) |
31 |
20 30
|
mpbid |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ( ( ! ‘ 𝑁 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) |
32 |
31
|
ex |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) ) |
33 |
32
|
ralimdva |
⊢ ( 𝐺 ∈ Grp → ( ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) → ∀ 𝑥 ∈ 𝑋 ( ( ! ‘ 𝑁 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) ) |
34 |
33
|
imp |
⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → ∀ 𝑥 ∈ 𝑋 ( ( ! ‘ 𝑁 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) |
35 |
1 2 27 28
|
gexlem2 |
⊢ ( ( 𝐺 ∈ Grp ∧ ( ! ‘ 𝑁 ) ∈ ℕ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ! ‘ 𝑁 ) ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) → 𝐸 ∈ ( 1 ... ( ! ‘ 𝑁 ) ) ) |
36 |
4 14 34 35
|
syl3anc |
⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝐸 ∈ ( 1 ... ( ! ‘ 𝑁 ) ) ) |
37 |
|
elfznn |
⊢ ( 𝐸 ∈ ( 1 ... ( ! ‘ 𝑁 ) ) → 𝐸 ∈ ℕ ) |
38 |
36 37
|
syl |
⊢ ( ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ( 1 ... 𝑁 ) ) → 𝐸 ∈ ℕ ) |